PA005E · theorem

pow_predecessor_parity_mod

Stable checked-use theorem · independently closed

Powers of the predecessor of p alternate between one and the predecessor modulo p.

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. ∀ r. ∀ e. ∀ z. p = S r → Pow(r,e,z) → (Even(e) → ModEq(p,z,1)) ∧ (Odd(e) → ModEq(p,z,r))

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

PD0008 ModEq PD0009 Even PD0010 Odd PD0020 Pow

5 occurrences

In local proof propositions

PD0008 ModEq PD0009 Even PD0010 Odd PD0020 Pow PD0031 BalancedInverse

15 occurrences

Exact expanded native-PA statement
forall p r e z. p = S r -> (exists ff_b_main ff_c_main. ((forall ff_i_main_repeat. (exists ff_lt_main_repeat_bound. ff_lt_main_repeat_bound + S ff_i_main_repeat = e) -> (((exists ff_h_main_repeat_decoded. ff_h_main_repeat_decoded + S (r) = S ((S (ff_i_main_repeat)) * ff_c_main)) /\ exists ff_q_main_repeat_decoded. ff_b_main = ff_q_main_repeat_decoded * S ((S (ff_i_main_repeat)) * ff_c_main) + (r)))) /\ (exists ff_u_main_product ff_v_main_product. ((((exists ff_h_main_product_start. ff_h_main_product_start + S (1) = S ((S (0)) * ff_v_main_product)) /\ exists ff_q_main_product_start. ff_u_main_product = ff_q_main_product_start * S ((S (0)) * ff_v_main_product) + (1))) /\ ((((exists ff_h_main_product_terminal. ff_h_main_product_terminal + S (z) = S ((S (e)) * ff_v_main_product)) /\ exists ff_q_main_product_terminal. ff_u_main_product = ff_q_main_product_terminal * S ((S (e)) * ff_v_main_product) + (z))) /\ forall ff_i_main_product. (exists ff_lt_main_product_bound. ff_lt_main_product_bound + S ff_i_main_product = e) -> exists ff_p_main_product ff_r_main_product ff_s_main_product. ((((exists ff_h_main_product_factor. ff_h_main_product_factor + S (ff_p_main_product) = S ((S (ff_i_main_product)) * ff_c_main)) /\ exists ff_q_main_product_factor. ff_b_main = ff_q_main_product_factor * S ((S (ff_i_main_product)) * ff_c_main) + (ff_p_main_product))) /\ ((((exists ff_h_main_product_partial. ff_h_main_product_partial + S (ff_r_main_product) = S ((S (ff_i_main_product)) * ff_v_main_product)) /\ exists ff_q_main_product_partial. ff_u_main_product = ff_q_main_product_partial * S ((S (ff_i_main_product)) * ff_v_main_product) + (ff_r_main_product))) /\ ((((exists ff_h_main_product_successor. ff_h_main_product_successor + S (ff_s_main_product) = S ((S (S ff_i_main_product)) * ff_v_main_product)) /\ exists ff_q_main_product_successor. ff_u_main_product = ff_q_main_product_successor * S ((S (S ff_i_main_product)) * ff_v_main_product) + (ff_s_main_product))) /\ ff_s_main_product = ff_r_main_product * ff_p_main_product)))))))) -> (((exists gs_even_main. e = 2 * gs_even_main) -> (exists gs_u_result_even gs_v_result_even. (z) + p * gs_u_result_even = (1) + p * gs_v_result_even)) /\ ((exists gs_odd_main. e = 2 * gs_odd_main + 1) -> (exists gs_u_result_odd gs_v_result_odd. (z) + p * gs_u_result_odd = (r) + p * gs_v_result_odd)))

Proof neighborhood

Direct theorem prerequisites

PA004B pow_zero PA004D pow_successor_decompose PA0056 odd_not_even PA005A even_successor_to_odd PA005C odd_successor_to_even PA005D predecessor_square_mod_one PA0023 mod_eq_refl PA004E mod_eq_mul PA0024 mod_eq_trans PA000M one_mul

Direct theorem dependents

PA00BV arbitrary_gauss_lemma_complete

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

107 script commands · 30 reading checkpoints · 13 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 (10)
pow zeropow successor decomposeodd not eveneven successor to oddodd successor to evenpredecessor square mod onemod eq reflmod eq mulmod eq transone mul
01Fix variables and assumptionsL1–2

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

  1. L1
    intro p
  2. L2
    intro r
02Induction on eL3–6

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L3
    induction e
  2. L4
    intro z
  3. L5
    intro hp
  4. L6
    intro hpow
03Separate the logical casesL7–7

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

  1. L7
    split
04Fix variables and assumptionsL8–8

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

  1. L8
    intro he
05Establish hzL9–18

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

  1. L9
    have hz : z = 1
  2. L10
    specialize pow_zero r
  3. L11
    specialize pow_zero 0
  4. L12
    specialize pow_zero z
  5. L13
    apply pow_zero
  6. L14
    refl
  7. L15
    exact hpow
  8. L16
    rewrite hz
  9. L17
    specialize mod_eq_refl p
  10. L18
    specialize mod_eq_refl 1
06Use earlier factsL19–19

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

  1. L19
    exact mod_eq_refl
07Fix variables and assumptionsL20–20

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

  1. L20
    intro ho
08Separate the logical casesL21–21

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

  1. L21
    exfalso
09Use earlier factsL22–24

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

  1. L22
    specialize odd_not_even 0
  2. L23
    apply odd_not_even
  3. L24
    exact ho
10Construct an explicit witnessL25–25

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

  1. L25
    exists 0
11Calculate and transport equalitiesL26–26

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

  1. L26
    norm_num
12Fix variables and assumptionsL27–29

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

  1. L27
    intro z
  2. L28
    intro hp
  3. L29
    intro hpow
13Establish hstepL30–37

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

  1. L30
    have hstep : ∃ w. Pow(r,e,w) ∧ z = w · rDefinitions: Pow(r,e,w)Original native command in the exact edition
  2. L31
    specialize pow_successor_decompose r
  3. L32
    specialize pow_successor_decompose e
  4. L33
    specialize pow_successor_decompose (S e)
  5. L34
    specialize pow_successor_decompose z
  6. L35
    apply pow_successor_decompose
  7. L36
    refl
  8. L37
    exact hpow
14Separate the logical casesL38–39

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

  1. L38
    cases hstep
  2. L39
    cases hstep_witness
15Establish hinvL40–44

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

  1. L40
    have hinv : (Even(e) → ModEq(p,x,1)) ∧ (Odd(e) → ModEq(p,x,r))Definitions: Even(e)ModEq(p,x,1)Odd(e)ModEq(p,x,r)Original native command in the exact edition
  2. L41
    specialize IH x
  3. L42
    apply IH
  4. L43
    exact hp
  5. L44
    exact hstep_witness_left
16Separate the logical casesL45–46

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

  1. L45
    cases hinv
  2. L46
    split
17Fix variables and assumptionsL47–47

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

  1. L47
    intro hse
18Establish heoL48–51

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

  1. L48
  2. L49
    specialize even_successor_to_odd e
  3. L50
    apply even_successor_to_odd
  4. L51
    exact hse
19Establish hwrL52–54

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

  1. L52
  2. L53
    apply hinv_right
  3. L54
    exact heo
20Establish hrrL55–58

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

  1. L55
  2. L56
    specialize mod_eq_refl p
  3. L57
    specialize mod_eq_refl r
  4. L58
    exact mod_eq_refl
21Establish hmulL59–67

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

  1. L59
    have hmul : ModEq(p,x · r,r · r)Definitions: ModEq(p,x · r,r · r)Original native command in the exact edition
  2. L60
    specialize mod_eq_mul p
  3. L61
    specialize mod_eq_mul x
  4. L62
    specialize mod_eq_mul r
  5. L63
    specialize mod_eq_mul r
  6. L64
    specialize mod_eq_mul r
  7. L65
    apply mod_eq_mul
  8. L66
    exact hwr
  9. L67
    exact hrr
22Establish hsqL68–72

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

  1. L68
    have hsq : BalancedInverse(p,r,r)Definitions: BalancedInverse(p,r,r)Original native command in the exact edition
  2. L69
    specialize predecessor_square_mod_one p
  3. L70
    specialize predecessor_square_mod_one r
  4. L71
    apply predecessor_square_mod_one
  5. L72
    exact hp
23Establish hfinalL73–82

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

  1. L73
    have hfinal : BalancedInverse(p,x,r)Definitions: BalancedInverse(p,x,r)Original native command in the exact edition
  2. L74
    specialize mod_eq_trans p
  3. L75
    specialize mod_eq_trans (x * r)
  4. L76
    specialize mod_eq_trans (r * r)
  5. L77
    specialize mod_eq_trans 1
  6. L78
    apply mod_eq_trans
  7. L79
    exact hmul
  8. L80
    exact hsq
  9. L81
    rewrite hstep_witness_right
  10. L82
    exact hfinal
24Fix variables and assumptionsL83–83

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

  1. L83
    intro hso
25Establish heeL84–87

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

  1. L84
  2. L85
    specialize odd_successor_to_even e
  3. L86
    apply odd_successor_to_even
  4. L87
    exact hso
26Establish hw1L88–90

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

  1. L88
  2. L89
    apply hinv_left
  3. L90
    exact hee
27Establish hrrL91–94

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

  1. L91
  2. L92
    specialize mod_eq_refl p
  3. L93
    specialize mod_eq_refl r
  4. L94
    exact mod_eq_refl
28Establish hmulL95–104

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

  1. L95
    have hmul : ModEq(p,x · r,1 · r)Definitions: ModEq(p,x · r,1 · r)Original native command in the exact edition
  2. L96
    specialize mod_eq_mul p
  3. L97
    specialize mod_eq_mul x
  4. L98
    specialize mod_eq_mul 1
  5. L99
    specialize mod_eq_mul r
  6. L100
    specialize mod_eq_mul r
  7. L101
    apply mod_eq_mul
  8. L102
    exact hw1
  9. L103
    exact hrr
  10. L104
    specialize one_mul r
29Calculate and transport equalitiesL105–106

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

  1. L105
    rewrite one_mul at hmul
  2. L106
    rewrite hstep_witness_right
30Use earlier factsL107–107

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

  1. L107
    exact hmul

Library-wide reading audit

Original defined command ledger · 107 lines
  1. 0001intro p
  2. 0002intro r
  3. 0003induction e
  4. 0004intro z
  5. 0005intro hp
  6. 0006intro hpow
  7. 0007split
  8. 0008intro he
  9. 0009have hz : z = 1
  10. 0010specialize pow_zero r
  11. 0011specialize pow_zero 0
  12. 0012specialize pow_zero z
  13. 0013apply pow_zero
  14. 0014refl
  15. 0015exact hpow
  16. 0016rewrite hz
  17. 0017specialize mod_eq_refl p
  18. 0018specialize mod_eq_refl 1
  19. 0019exact mod_eq_refl
  20. 0020intro ho
  21. 0021exfalso
  22. 0022specialize odd_not_even 0
  23. 0023apply odd_not_even
  24. 0024exact ho
  25. 0025exists 0
  26. 0026norm_num
  27. 0027intro z
  28. 0028intro hp
  29. 0029intro hpow
  30. 0030have hstep : ∃ w. Pow(r,e,w) ∧ z = w · r
    Exact native replay linehave hstep : exists w. (exists ff_b_predecessor ff_c_predecessor. ((forall ff_i_predecessor_repeat. (exists ff_lt_predecessor_repeat_bound. ff_lt_predecessor_repeat_bound + S ff_i_predecessor_repeat = e) -> (((exists ff_h_predecessor_repeat_decoded. ff_h_predecessor_repeat_decoded + S (r) = S ((S (ff_i_predecessor_repeat)) * ff_c_predecessor)) /\ exists ff_q_predecessor_repeat_decoded. ff_b_predecessor = ff_q_predecessor_repeat_decoded * S ((S (ff_i_predecessor_repeat)) * ff_c_predecessor) + (r)))) /\ (exists ff_u_predecessor_product ff_v_predecessor_product. ((((exists ff_h_predecessor_product_start. ff_h_predecessor_product_start + S (1) = S ((S (0)) * ff_v_predecessor_product)) /\ exists ff_q_predecessor_product_start. ff_u_predecessor_product = ff_q_predecessor_product_start * S ((S (0)) * ff_v_predecessor_product) + (1))) /\ ((((exists ff_h_predecessor_product_terminal. ff_h_predecessor_product_terminal + S (w) = S ((S (e)) * ff_v_predecessor_product)) /\ exists ff_q_predecessor_product_terminal. ff_u_predecessor_product = ff_q_predecessor_product_terminal * S ((S (e)) * ff_v_predecessor_product) + (w))) /\ forall ff_i_predecessor_product. (exists ff_lt_predecessor_product_bound. ff_lt_predecessor_product_bound + S ff_i_predecessor_product = e) -> exists ff_p_predecessor_product ff_r_predecessor_product ff_s_predecessor_product. ((((exists ff_h_predecessor_product_factor. ff_h_predecessor_product_factor + S (ff_p_predecessor_product) = S ((S (ff_i_predecessor_product)) * ff_c_predecessor)) /\ exists ff_q_predecessor_product_factor. ff_b_predecessor = ff_q_predecessor_product_factor * S ((S (ff_i_predecessor_product)) * ff_c_predecessor) + (ff_p_predecessor_product))) /\ ((((exists ff_h_predecessor_product_partial. ff_h_predecessor_product_partial + S (ff_r_predecessor_product) = S ((S (ff_i_predecessor_product)) * ff_v_predecessor_product)) /\ exists ff_q_predecessor_product_partial. ff_u_predecessor_product = ff_q_predecessor_product_partial * S ((S (ff_i_predecessor_product)) * ff_v_predecessor_product) + (ff_r_predecessor_product))) /\ ((((exists ff_h_predecessor_product_successor. ff_h_predecessor_product_successor + S (ff_s_predecessor_product) = S ((S (S ff_i_predecessor_product)) * ff_v_predecessor_product)) /\ exists ff_q_predecessor_product_successor. ff_u_predecessor_product = ff_q_predecessor_product_successor * S ((S (S ff_i_predecessor_product)) * ff_v_predecessor_product) + (ff_s_predecessor_product))) /\ ff_s_predecessor_product = ff_r_predecessor_product * ff_p_predecessor_product)))))))) /\ z = w * r
  31. 0031specialize pow_successor_decompose r
  32. 0032specialize pow_successor_decompose e
  33. 0033specialize pow_successor_decompose (S e)
  34. 0034specialize pow_successor_decompose z
  35. 0035apply pow_successor_decompose
  36. 0036refl
  37. 0037exact hpow
  38. 0038cases hstep
  39. 0039cases hstep_witness
  40. 0040have hinv : (Even(e) → ModEq(p,x,1)) ∧ (Odd(e) → ModEq(p,x,r))
    Exact native replay linehave hinv : (((exists gs_even_ih. e = 2 * gs_even_ih) -> (exists gs_u_ih_even gs_v_ih_even. (x) + p * gs_u_ih_even = (1) + p * gs_v_ih_even)) /\ ((exists gs_odd_ih. e = 2 * gs_odd_ih + 1) -> (exists gs_u_ih_odd gs_v_ih_odd. (x) + p * gs_u_ih_odd = (r) + p * gs_v_ih_odd)))
  41. 0041specialize IH x
  42. 0042apply IH
  43. 0043exact hp
  44. 0044exact hstep_witness_left
  45. 0045cases hinv
  46. 0046split
  47. 0047intro hse
  48. 0048have heo : Odd(e)
    Exact native replay linehave heo : exists a. e = 2 * a + 1
  49. 0049specialize even_successor_to_odd e
  50. 0050apply even_successor_to_odd
  51. 0051exact hse
  52. 0052have hwr : ModEq(p,x,r)
    Exact native replay linehave hwr : exists u v. x + p * u = r + p * v
  53. 0053apply hinv_right
  54. 0054exact heo
  55. 0055have hrr : ModEq(p,r,r)
    Exact native replay linehave hrr : exists u v. r + p * u = r + p * v
  56. 0056specialize mod_eq_refl p
  57. 0057specialize mod_eq_refl r
  58. 0058exact mod_eq_refl
  59. 0059have hmul : ModEq(p,x · r,r · r)
    Exact native replay linehave hmul : exists u v. (x * r) + p * u = (r * r) + p * v
  60. 0060specialize mod_eq_mul p
  61. 0061specialize mod_eq_mul x
  62. 0062specialize mod_eq_mul r
  63. 0063specialize mod_eq_mul r
  64. 0064specialize mod_eq_mul r
  65. 0065apply mod_eq_mul
  66. 0066exact hwr
  67. 0067exact hrr
  68. 0068have hsq : BalancedInverse(p,r,r)
    Exact native replay linehave hsq : exists u v. (r * r) + p * u = 1 + p * v
  69. 0069specialize predecessor_square_mod_one p
  70. 0070specialize predecessor_square_mod_one r
  71. 0071apply predecessor_square_mod_one
  72. 0072exact hp
  73. 0073have hfinal : BalancedInverse(p,x,r)
    Exact native replay linehave hfinal : exists u v. (x * r) + p * u = 1 + p * v
  74. 0074specialize mod_eq_trans p
  75. 0075specialize mod_eq_trans (x * r)
  76. 0076specialize mod_eq_trans (r * r)
  77. 0077specialize mod_eq_trans 1
  78. 0078apply mod_eq_trans
  79. 0079exact hmul
  80. 0080exact hsq
  81. 0081rewrite hstep_witness_right
  82. 0082exact hfinal
  83. 0083intro hso
  84. 0084have hee : Even(e)
    Exact native replay linehave hee : exists a. e = 2 * a
  85. 0085specialize odd_successor_to_even e
  86. 0086apply odd_successor_to_even
  87. 0087exact hso
  88. 0088have hw1 : ModEq(p,x,1)
    Exact native replay linehave hw1 : exists u v. x + p * u = 1 + p * v
  89. 0089apply hinv_left
  90. 0090exact hee
  91. 0091have hrr : ModEq(p,r,r)
    Exact native replay linehave hrr : exists u v. r + p * u = r + p * v
  92. 0092specialize mod_eq_refl p
  93. 0093specialize mod_eq_refl r
  94. 0094exact mod_eq_refl
  95. 0095have hmul : ModEq(p,x · r,1 · r)
    Exact native replay linehave hmul : exists u v. (x * r) + p * u = (1 * r) + p * v
  96. 0096specialize mod_eq_mul p
  97. 0097specialize mod_eq_mul x
  98. 0098specialize mod_eq_mul 1
  99. 0099specialize mod_eq_mul r
  100. 0100specialize mod_eq_mul r
  101. 0101apply mod_eq_mul
  102. 0102exact hw1
  103. 0103exact hrr
  104. 0104specialize one_mul r
  105. 0105rewrite one_mul at hmul
  106. 0106rewrite hstep_witness_right
  107. 0107exact hmul