PA008L · theorem

fermat_predecessor_exponent_mod_one

Alpha v34 checked-use theorem · independently closed; not Stable

Fermat's theorem for the native predecessor exponent p-1.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ p. ∀ n. ∀ a. ∀ A. p = S n → Prime(p) → ¬Dvd(p,a) → Pow(a,n,A) → ModEq(p,A,1)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0003 Dvd PD0004 Prime PD0008 ModEq PD0020 Pow

4 occurrences

In local proof propositions

PD0005 Coprime PD0008 ModEq

3 occurrences

Exact expanded native-PA statement
forall p n a A. p = S n -> ((~(p = 1) /\ forall frm_prime_left_predecessor_prime frm_prime_right_predecessor_prime. p = frm_prime_left_predecessor_prime * frm_prime_right_predecessor_prime -> frm_prime_left_predecessor_prime = 1 \/ frm_prime_right_predecessor_prime = 1)) -> (~(exists frm_factor_predecessor_multiplier. a = p * frm_factor_predecessor_multiplier)) -> (exists ff_b_predecessor_power ff_c_predecessor_power. ((forall ff_i_predecessor_power_repeat. (exists ff_lt_predecessor_power_repeat_bound. ff_lt_predecessor_power_repeat_bound + S ff_i_predecessor_power_repeat = n) -> (((exists ff_h_predecessor_power_repeat_decoded. ff_h_predecessor_power_repeat_decoded + S (a) = S ((S (ff_i_predecessor_power_repeat)) * ff_c_predecessor_power)) /\ exists ff_q_predecessor_power_repeat_decoded. ff_b_predecessor_power = ff_q_predecessor_power_repeat_decoded * S ((S (ff_i_predecessor_power_repeat)) * ff_c_predecessor_power) + (a)))) /\ (exists ff_u_predecessor_power_product ff_v_predecessor_power_product. ((((exists ff_h_predecessor_power_product_start. ff_h_predecessor_power_product_start + S (1) = S ((S (0)) * ff_v_predecessor_power_product)) /\ exists ff_q_predecessor_power_product_start. ff_u_predecessor_power_product = ff_q_predecessor_power_product_start * S ((S (0)) * ff_v_predecessor_power_product) + (1))) /\ ((((exists ff_h_predecessor_power_product_terminal. ff_h_predecessor_power_product_terminal + S (A) = S ((S (n)) * ff_v_predecessor_power_product)) /\ exists ff_q_predecessor_power_product_terminal. ff_u_predecessor_power_product = ff_q_predecessor_power_product_terminal * S ((S (n)) * ff_v_predecessor_power_product) + (A))) /\ forall ff_i_predecessor_power_product. (exists ff_lt_predecessor_power_product_bound. ff_lt_predecessor_power_product_bound + S ff_i_predecessor_power_product = n) -> exists ff_p_predecessor_power_product ff_r_predecessor_power_product ff_s_predecessor_power_product. ((((exists ff_h_predecessor_power_product_factor. ff_h_predecessor_power_product_factor + S (ff_p_predecessor_power_product) = S ((S (ff_i_predecessor_power_product)) * ff_c_predecessor_power)) /\ exists ff_q_predecessor_power_product_factor. ff_b_predecessor_power = ff_q_predecessor_power_product_factor * S ((S (ff_i_predecessor_power_product)) * ff_c_predecessor_power) + (ff_p_predecessor_power_product))) /\ ((((exists ff_h_predecessor_power_product_partial. ff_h_predecessor_power_product_partial + S (ff_r_predecessor_power_product) = S ((S (ff_i_predecessor_power_product)) * ff_v_predecessor_power_product)) /\ exists ff_q_predecessor_power_product_partial. ff_u_predecessor_power_product = ff_q_predecessor_power_product_partial * S ((S (ff_i_predecessor_power_product)) * ff_v_predecessor_power_product) + (ff_r_predecessor_power_product))) /\ ((((exists ff_h_predecessor_power_product_successor. ff_h_predecessor_power_product_successor + S (ff_s_predecessor_power_product) = S ((S (S ff_i_predecessor_power_product)) * ff_v_predecessor_power_product)) /\ exists ff_q_predecessor_power_product_successor. ff_u_predecessor_power_product = ff_q_predecessor_power_product_successor * S ((S (S ff_i_predecessor_power_product)) * ff_v_predecessor_power_product) + (ff_s_predecessor_power_product))) /\ ff_s_predecessor_power_product = ff_r_predecessor_power_product * ff_p_predecessor_power_product)))))))) -> (exists fep_mod_left_predecessor_result fep_mod_right_predecessor_result. A + p * fep_mod_left_predecessor_result = 1 + p * fep_mod_right_predecessor_result)

Proof neighborhood

Direct theorem prerequisites

PA0060 factorial_exists PA008J prime_mul_residue_product_balance PA008K prime_range_product_coprime PA0031 prime_nonzero PA003R mod_eq_cancel_coprime PA000H mul_comm PA0002 mul_one

Direct theorem dependents

PA008M quadratic_residue_half_power_mod_one

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

68 script commands · 19 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (7)
factorial existsprime mul residue product balanceprime range product coprimeprime nonzeromod eq cancel coprimemul commmul one
01Fix variables and assumptionsL1–8

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro a
  4. L4
    intro A
  5. L5
    intro hpn
  6. L6
    intro hp
  7. L7
    intro hnotdiv
  8. L8
    intro hA
02Use earlier factsL9–9

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L9
    specialize factorial_exists n
03Separate the logical casesL10–13

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L10
    cases factorial_exists
  2. L11
    cases factorial_exists_witness
  3. L12
    cases factorial_exists_witness_witness
  4. L13
    cases factorial_exists_witness_witness_witness
04Establish hbalanceL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime mul residue product balance.

  1. L14
    have hbalance : ModEq(p,A · x,x)Definitions: ModEq(p,A · x,x)Original native command in the exact edition
  2. L15
    specialize prime_mul_residue_product_balance p
  3. L16
    specialize prime_mul_residue_product_balance n
  4. L17
    specialize prime_mul_residue_product_balance a
  5. L18
    specialize prime_mul_residue_product_balance x1
  6. L19
    specialize prime_mul_residue_product_balance x2
  7. L20
    specialize prime_mul_residue_product_balance x
  8. L21
    specialize prime_mul_residue_product_balance A
  9. L22
    apply prime_mul_residue_product_balance
  10. L23
    exact hpn
05Use earlier factsL24–28

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L24
    exact hp
  2. L25
    exact hnotdiv
  3. L26
    exact factorial_exists_witness_witness_witness_left
  4. L27
    exact factorial_exists_witness_witness_witness_right
  5. L28
    exact hA
06Establish hcopL29–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime range product coprime.

  1. L29
  2. L30
    specialize prime_range_product_coprime p
  3. L31
    specialize prime_range_product_coprime n
  4. L32
    specialize prime_range_product_coprime x1
  5. L33
    specialize prime_range_product_coprime x2
  6. L34
    specialize prime_range_product_coprime x
  7. L35
    apply prime_range_product_coprime
  8. L36
    exact hpn
  9. L37
    exact hp
  10. L38
    exact factorial_exists_witness_witness_witness_left
07Use earlier factsL39–39

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L39
    exact factorial_exists_witness_witness_witness_right
08Establish hp0L40–45

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime nonzero.

  1. L40
    have hp0 : ~(p = 0)
  2. L41
    intro hpzero
  3. L42
    specialize prime_nonzero p
  4. L43
    apply prime_nonzero
  5. L44
    exact hp
  6. L45
    exact hpzero
09Establish hscaledL46–46

Establish this local claim before using it. It is not an additional assumption.

  1. L46
    have hscaled : ModEq(p,x · A,x · 1)Definitions: ModEq(p,x · A,x · 1)Original native command in the exact edition
10Separate the logical casesL47–48

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L47
    cases hbalance
  2. L48
    cases hbalance_witness
11Construct an explicit witnessL49–50

Supply the displayed value, then prove that it has the required property.

  1. L49
    exists x3
  2. L50
    exists x4
12Calculate and transport equalitiesL51–52

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L51
    trans (A * x) + p * x3
  2. L52
    congr
13Use earlier factsL53–53

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L53
    apply mul_comm
14Calculate and transport equalitiesL54–55

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L54
    refl
  2. L55
    trans x + p * x4
15Use earlier factsL56–56

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L56
    exact hbalance_witness_witness
16Calculate and transport equalitiesL57–58

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L57
    congr
  2. L58
    symm
17Use earlier factsL59–59

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L59
    apply mul_one
18Calculate and transport equalitiesL60–60

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L60
    refl
19Use earlier factsL61–68

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L61
    specialize mod_eq_cancel_coprime p
  2. L62
    specialize mod_eq_cancel_coprime x
  3. L63
    specialize mod_eq_cancel_coprime A
  4. L64
    specialize mod_eq_cancel_coprime 1
  5. L65
    apply mod_eq_cancel_coprime
  6. L66
    exact hp0
  7. L67
    exact hcop
  8. L68
    exact hscaled

Library-wide reading audit

Original defined command ledger · 68 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro a
  4. 0004intro A
  5. 0005intro hpn
  6. 0006intro hp
  7. 0007intro hnotdiv
  8. 0008intro hA
  9. 0009specialize factorial_exists n
  10. 0010cases factorial_exists
  11. 0011cases factorial_exists_witness
  12. 0012cases factorial_exists_witness_witness
  13. 0013cases factorial_exists_witness_witness_witness
  14. 0014have hbalance : ModEq(p,A · x,x)
    Exact native replay linehave hbalance : exists fsp_product_mod_left_predecessor_balance fsp_product_mod_right_predecessor_balance. (A * x) + p * fsp_product_mod_left_predecessor_balance = x + p * fsp_product_mod_right_predecessor_balance
  15. 0015specialize prime_mul_residue_product_balance p
  16. 0016specialize prime_mul_residue_product_balance n
  17. 0017specialize prime_mul_residue_product_balance a
  18. 0018specialize prime_mul_residue_product_balance x1
  19. 0019specialize prime_mul_residue_product_balance x2
  20. 0020specialize prime_mul_residue_product_balance x
  21. 0021specialize prime_mul_residue_product_balance A
  22. 0022apply prime_mul_residue_product_balance
  23. 0023exact hpn
  24. 0024exact hp
  25. 0025exact hnotdiv
  26. 0026exact factorial_exists_witness_witness_witness_left
  27. 0027exact factorial_exists_witness_witness_witness_right
  28. 0028exact hA
  29. 0029have hcop : Coprime(x,p)
    Exact native replay linehave hcop : forall frp_divisor_predecessor_coprime. (exists frp_left_factor_predecessor_coprime. x = frp_divisor_predecessor_coprime * frp_left_factor_predecessor_coprime) -> (exists frp_right_factor_predecessor_coprime. p = frp_divisor_predecessor_coprime * frp_right_factor_predecessor_coprime) -> frp_divisor_predecessor_coprime = 1
  30. 0030specialize prime_range_product_coprime p
  31. 0031specialize prime_range_product_coprime n
  32. 0032specialize prime_range_product_coprime x1
  33. 0033specialize prime_range_product_coprime x2
  34. 0034specialize prime_range_product_coprime x
  35. 0035apply prime_range_product_coprime
  36. 0036exact hpn
  37. 0037exact hp
  38. 0038exact factorial_exists_witness_witness_witness_left
  39. 0039exact factorial_exists_witness_witness_witness_right
  40. 0040have hp0 : ~(p = 0)
  41. 0041intro hpzero
  42. 0042specialize prime_nonzero p
  43. 0043apply prime_nonzero
  44. 0044exact hp
  45. 0045exact hpzero
  46. 0046have hscaled : ModEq(p,x · A,x · 1)
    Exact native replay linehave hscaled : exists fep_product_mod_left_predecessor_normalized fep_product_mod_right_predecessor_normalized. (x * A) + p * fep_product_mod_left_predecessor_normalized = (x * 1) + p * fep_product_mod_right_predecessor_normalized
  47. 0047cases hbalance
  48. 0048cases hbalance_witness
  49. 0049exists x3
  50. 0050exists x4
  51. 0051trans (A * x) + p * x3
  52. 0052congr
  53. 0053apply mul_comm
  54. 0054refl
  55. 0055trans x + p * x4
  56. 0056exact hbalance_witness_witness
  57. 0057congr
  58. 0058symm
  59. 0059apply mul_one
  60. 0060refl
  61. 0061specialize mod_eq_cancel_coprime p
  62. 0062specialize mod_eq_cancel_coprime x
  63. 0063specialize mod_eq_cancel_coprime A
  64. 0064specialize mod_eq_cancel_coprime 1
  65. 0065apply mod_eq_cancel_coprime
  66. 0066exact hp0
  67. 0067exact hcop
  68. 0068exact hscaled