CG000C

fermat_little_all_inputs

Fermat's little theorem for every natural base in relational-power form.

Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not Stable

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

Each statement retains its explicit modulus, coprimality and divisibility assumptions. These twelve arithmetic laws do not assert all order, primitive-root, Carmichael, exponential or simultaneous-polynomial congruence goals are finished.

Exact theorem in conservative defined notation

∀ p. ∀ a. ∀ A. Prime(p) → Pow(a,p,A) → ModEq(p,A,a)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Dvd(d,n) · 4Prime(p) · 1Coprime(a,b) · 1ModEq(m,a,b) · 3Pow(a,e,z) · 2

Actual proof prerequisites

prime_nonzero · checked external prerequisitenonzero_is_succ · checked external prerequisitepow_successor_decompose · checked external prerequisiteprime_coprime_or_divides · checked external prerequisitemultiple_refl · checked external prerequisitefermat_predecessor_exponent_mod_one · checked external prerequisitemod_eq_mul_right · checked external prerequisiteone_mul · checked external prerequisitemultiple_mul_left · checked external prerequisiteadd_comm · checked external prerequisite
Original expanded first-order statement 
forall p a A. ((~(p = 1) /\ forall frm_prime_left_all_prime frm_prime_right_all_prime. p = frm_prime_left_all_prime * frm_prime_right_all_prime -> frm_prime_left_all_prime = 1 \/ frm_prime_right_all_prime = 1)) -> (exists ff_b_all_power ff_c_all_power. ((forall ff_i_all_power_repeat. (exists ff_lt_all_power_repeat_bound. ff_lt_all_power_repeat_bound + S ff_i_all_power_repeat = p) -> (((exists ff_h_all_power_repeat_decoded. ff_h_all_power_repeat_decoded + S (a) = S ((S (ff_i_all_power_repeat)) * ff_c_all_power)) /\ exists ff_q_all_power_repeat_decoded. ff_b_all_power = ff_q_all_power_repeat_decoded * S ((S (ff_i_all_power_repeat)) * ff_c_all_power) + (a)))) /\ (exists ff_u_all_power_product ff_v_all_power_product. ((((exists ff_h_all_power_product_start. ff_h_all_power_product_start + S (1) = S ((S (0)) * ff_v_all_power_product)) /\ exists ff_q_all_power_product_start. ff_u_all_power_product = ff_q_all_power_product_start * S ((S (0)) * ff_v_all_power_product) + (1))) /\ ((((exists ff_h_all_power_product_terminal. ff_h_all_power_product_terminal + S (A) = S ((S (p)) * ff_v_all_power_product)) /\ exists ff_q_all_power_product_terminal. ff_u_all_power_product = ff_q_all_power_product_terminal * S ((S (p)) * ff_v_all_power_product) + (A))) /\ forall ff_i_all_power_product. (exists ff_lt_all_power_product_bound. ff_lt_all_power_product_bound + S ff_i_all_power_product = p) -> exists ff_p_all_power_product ff_r_all_power_product ff_s_all_power_product. ((((exists ff_h_all_power_product_factor. ff_h_all_power_product_factor + S (ff_p_all_power_product) = S ((S (ff_i_all_power_product)) * ff_c_all_power)) /\ exists ff_q_all_power_product_factor. ff_b_all_power = ff_q_all_power_product_factor * S ((S (ff_i_all_power_product)) * ff_c_all_power) + (ff_p_all_power_product))) /\ ((((exists ff_h_all_power_product_partial. ff_h_all_power_product_partial + S (ff_r_all_power_product) = S ((S (ff_i_all_power_product)) * ff_v_all_power_product)) /\ exists ff_q_all_power_product_partial. ff_u_all_power_product = ff_q_all_power_product_partial * S ((S (ff_i_all_power_product)) * ff_v_all_power_product) + (ff_r_all_power_product))) /\ ((((exists ff_h_all_power_product_successor. ff_h_all_power_product_successor + S (ff_s_all_power_product) = S ((S (S ff_i_all_power_product)) * ff_v_all_power_product)) /\ exists ff_q_all_power_product_successor. ff_u_all_power_product = ff_q_all_power_product_successor * S ((S (S ff_i_all_power_product)) * ff_v_all_power_product) + (ff_s_all_power_product))) /\ ff_s_all_power_product = ff_r_all_power_product * ff_p_all_power_product)))))))) -> (exists fep_mod_left_all_result fep_mod_right_all_result. A + p * fep_mod_left_all_result = a + p * fep_mod_right_all_result)

Complete tactic proof in conservative notation

All 83 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

83 script commands · 24 reading checkpoints · 10 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.

01Fix variables and assumptionsL1–5

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro A
  4. L4
    intro hp
  5. L5
    intro hpow
02Establish hp0L6–11

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

  1. L6
    have hp0 : ~(p = 0)
  2. L7
    intro hpzero
  3. L8
    specialize prime_nonzero p
  4. L9
    apply prime_nonzero
  5. L10
    exact hp
  6. L11
    exact hpzero
03Establish hpsL12–15

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

  1. L12
    have hps : exists n. p = S n
  2. L13
    specialize nonzero_is_succ p
  3. L14
    apply nonzero_is_succ
  4. L15
    exact hp0
04Separate the logical casesL16–16

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

  1. L16
    cases hps
05Establish hdecompL17–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor decompose.

  1. L17
    have hdecomp : ∃ r. Pow(a,x,r) ∧ A = r · aDefinitions: Pow(a,x,r)Original native command in the exact edition
  2. L18
    specialize pow_successor_decompose a
  3. L19
    specialize pow_successor_decompose x
  4. L20
    specialize pow_successor_decompose p
  5. L21
    specialize pow_successor_decompose A
  6. L22
    apply pow_successor_decompose
  7. L23
    exact hps_witness
  8. L24
    exact hpow
06Separate the logical casesL25–26

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

  1. L25
    cases hdecomp
  2. L26
    cases hdecomp_witness
07Establish hsplitL27–31

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

  1. L27
    have hsplit : Coprime(p,a) ∨ Dvd(p,a)Definitions: Coprime(p,a)Dvd(p,a)Original native command in the exact edition
  2. L28
    specialize prime_coprime_or_divides p
  3. L29
    specialize prime_coprime_or_divides a
  4. L30
    apply prime_coprime_or_divides
  5. L31
    exact hp
08Separate the logical casesL32–32

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

  1. L32
    cases hsplit
09Establish hnotdivL33–34

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

  1. L33
    have hnotdiv : ¬Dvd(p,a)Definitions: Dvd(p,a)Original native command in the exact edition
  2. L34
    intro hdiv
10Establish hpdivL35–37

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

  1. L35
  2. L36
    specialize multiple_refl p
  3. L37
    exact multiple_refl
11Establish hponeL38–42

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

  1. L38
    have hpone : p = 1
  2. L39
    specialize hsplit_left p
  3. L40
    apply hsplit_left
  4. L41
    exact hpdiv
  5. L42
    exact hdiv
12Separate the logical casesL43–43

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

  1. L43
    cases hp
13Use earlier factsL44–45

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

  1. L44
    apply hp_left
  2. L45
    exact hpone
14Establish hprevL46–55

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply fermat predecessor exponent mod one.

  1. L46
    have hprev : ModEq(p,x1,1)Definitions: ModEq(p,x1,1)Original native command in the exact edition
  2. L47
    specialize fermat_predecessor_exponent_mod_one p
  3. L48
    specialize fermat_predecessor_exponent_mod_one x
  4. L49
    specialize fermat_predecessor_exponent_mod_one a
  5. L50
    specialize fermat_predecessor_exponent_mod_one x1
  6. L51
    apply fermat_predecessor_exponent_mod_one
  7. L52
    exact hps_witness
  8. L53
    exact hp
  9. L54
    exact hnotdiv
  10. L55
    exact hdecomp_witness_left
15Establish hscaledL56–65

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq mul right.

  1. L56
    have hscaled : ModEq(p,x1 · a,1 · a)Definitions: ModEq(p,x1 · a,1 · a)Original native command in the exact edition
  2. L57
    specialize mod_eq_mul_right p
  3. L58
    specialize mod_eq_mul_right x1
  4. L59
    specialize mod_eq_mul_right 1
  5. L60
    specialize mod_eq_mul_right a
  6. L61
    apply mod_eq_mul_right
  7. L62
    exact hprev
  8. L63
    rewrite hdecomp_witness_right
  9. L64
    specialize one_mul a
  10. L65
    rewrite one_mul at hscaled
16Use earlier factsL66–66

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

  1. L66
    exact hscaled
17Separate the logical casesL67–67

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

  1. L67
    cases hsplit_right
18Establish hAdivL68–73

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply multiple mul left.

  1. L68
  2. L69
    rewrite hdecomp_witness_right
  3. L70
    specialize multiple_mul_left p
  4. L71
    specialize multiple_mul_left a
  5. L72
    specialize multiple_mul_left x1
  6. L73
    apply multiple_mul_left
19Construct an explicit witnessL74–74

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

  1. L74
    exists x2
20Use earlier factsL75–75

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

  1. L75
    exact hsplit_right_witness
21Separate the logical casesL76–76

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

  1. L76
    cases hAdiv
22Construct an explicit witnessL77–78

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

  1. L77
    exists x2
  2. L78
    exists x3
23Calculate and transport equalitiesL79–80

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

  1. L79
    rewrite hAdiv_witness
  2. L80
    rewrite hsplit_right_witness
24Use earlier factsL81–83

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

  1. L81
    specialize add_comm (p * x3)
  2. L82
    specialize add_comm (p * x2)
  3. L83
    exact add_comm

Library-wide reading audit

Original defined command ledger · 83 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro A
  4. 0004intro hp
  5. 0005intro hpow
  6. 0006have hp0 : ~(p = 0)
  7. 0007intro hpzero
  8. 0008specialize prime_nonzero p
  9. 0009apply prime_nonzero
  10. 0010exact hp
  11. 0011exact hpzero
  12. 0012have hps : exists n. p = S n
  13. 0013specialize nonzero_is_succ p
  14. 0014apply nonzero_is_succ
  15. 0015exact hp0
  16. 0016cases hps
  17. 0017have hdecomp : ∃ r. Pow(a,x,r) ∧ A = r · a
  18. 0018specialize pow_successor_decompose a
  19. 0019specialize pow_successor_decompose x
  20. 0020specialize pow_successor_decompose p
  21. 0021specialize pow_successor_decompose A
  22. 0022apply pow_successor_decompose
  23. 0023exact hps_witness
  24. 0024exact hpow
  25. 0025cases hdecomp
  26. 0026cases hdecomp_witness
  27. 0027have hsplit : Coprime(p,a) ∨ Dvd(p,a)
  28. 0028specialize prime_coprime_or_divides p
  29. 0029specialize prime_coprime_or_divides a
  30. 0030apply prime_coprime_or_divides
  31. 0031exact hp
  32. 0032cases hsplit
  33. 0033have hnotdiv : ¬Dvd(p,a)
  34. 0034intro hdiv
  35. 0035have hpdiv : Dvd(p,p)
  36. 0036specialize multiple_refl p
  37. 0037exact multiple_refl
  38. 0038have hpone : p = 1
  39. 0039specialize hsplit_left p
  40. 0040apply hsplit_left
  41. 0041exact hpdiv
  42. 0042exact hdiv
  43. 0043cases hp
  44. 0044apply hp_left
  45. 0045exact hpone
  46. 0046have hprev : ModEq(p,x1,1)
  47. 0047specialize fermat_predecessor_exponent_mod_one p
  48. 0048specialize fermat_predecessor_exponent_mod_one x
  49. 0049specialize fermat_predecessor_exponent_mod_one a
  50. 0050specialize fermat_predecessor_exponent_mod_one x1
  51. 0051apply fermat_predecessor_exponent_mod_one
  52. 0052exact hps_witness
  53. 0053exact hp
  54. 0054exact hnotdiv
  55. 0055exact hdecomp_witness_left
  56. 0056have hscaled : ModEq(p,x1 · a,1 · a)
  57. 0057specialize mod_eq_mul_right p
  58. 0058specialize mod_eq_mul_right x1
  59. 0059specialize mod_eq_mul_right 1
  60. 0060specialize mod_eq_mul_right a
  61. 0061apply mod_eq_mul_right
  62. 0062exact hprev
  63. 0063rewrite hdecomp_witness_right
  64. 0064specialize one_mul a
  65. 0065rewrite one_mul at hscaled
  66. 0066exact hscaled
  67. 0067cases hsplit_right
  68. 0068have hAdiv : Dvd(p,A)
  69. 0069rewrite hdecomp_witness_right
  70. 0070specialize multiple_mul_left p
  71. 0071specialize multiple_mul_left a
  72. 0072specialize multiple_mul_left x1
  73. 0073apply multiple_mul_left
  74. 0074exists x2
  75. 0075exact hsplit_right_witness
  76. 0076cases hAdiv
  77. 0077exists x2
  78. 0078exists x3
  79. 0079rewrite hAdiv_witness
  80. 0080rewrite hsplit_right_witness
  81. 0081specialize add_comm (p * x3)
  82. 0082specialize add_comm (p * x2)
  83. 0083exact add_comm