PA008L

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.

Exact expanded 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)

Structural proof guide

Generated structural guide

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

Use the direct prerequisites factorial_exists, prime_mul_residue_product_balance, prime_range_product_coprime, prime_nonzero, mod_eq_cancel_coprime, mul_comm, mul_one as previously established PA formulas.

The proof proceeds by case analysis (6), intermediate claims (4).

Referenced ingredients

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

Proof neighborhood

Direct dependencies

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 dependents

PA008M quadratic_residue_half_power_mod_one

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

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.

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 : 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
  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
    have 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
  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 : 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
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 exact 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 : 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 : 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 : 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