PA005E

pow_predecessor_parity_mod

Stable checked-use theorem · independently closed

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

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

Structural proof guide

Generated structural guide

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

Use the direct prerequisites pow_zero, pow_successor_decompose, odd_not_even, even_successor_to_odd, odd_successor_to_even, predecessor_square_mod_one, mod_eq_refl, mod_eq_mul, mod_eq_trans, one_mul as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (3), intermediate claims (13), equality transport (4), closed numeral normalization (1).

Referenced ingredients

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

Proof neighborhood

Direct dependencies

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 dependents

PA00BV arbitrary_gauss_lemma_complete

Formal native tactic body

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

  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 : 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 : (((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 : 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 : exists u v. x + p * u = r + p * v
  53. 0053apply hinv_right
  54. 0054exact heo
  55. 0055have 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 : 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 : 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 : 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 : exists a. e = 2 * a
  85. 0085specialize odd_successor_to_even e
  86. 0086apply odd_successor_to_even
  87. 0087exact hso
  88. 0088have hw1 : exists u v. x + p * u = 1 + p * v
  89. 0089apply hinv_left
  90. 0090exact hee
  91. 0091have 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 : 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