PA005I

pow_mod_congruent

Stable checked-use theorem · independently closed

Balanced-congruent bases have congruent relational powers at every exponent.

Exact expanded PA statement

forall m a b e x y. (exists qr_u_base qr_v_base. a + m * qr_u_base = b + m * qr_v_base) -> (exists ff_b_left ff_c_left. ((forall ff_i_left_repeat. (exists ff_lt_left_repeat_bound. ff_lt_left_repeat_bound + S ff_i_left_repeat = e) -> (((exists ff_h_left_repeat_decoded. ff_h_left_repeat_decoded + S (a) = S ((S (ff_i_left_repeat)) * ff_c_left)) /\ exists ff_q_left_repeat_decoded. ff_b_left = ff_q_left_repeat_decoded * S ((S (ff_i_left_repeat)) * ff_c_left) + (a)))) /\ (exists ff_u_left_product ff_v_left_product. ((((exists ff_h_left_product_start. ff_h_left_product_start + S (1) = S ((S (0)) * ff_v_left_product)) /\ exists ff_q_left_product_start. ff_u_left_product = ff_q_left_product_start * S ((S (0)) * ff_v_left_product) + (1))) /\ ((((exists ff_h_left_product_terminal. ff_h_left_product_terminal + S (x) = S ((S (e)) * ff_v_left_product)) /\ exists ff_q_left_product_terminal. ff_u_left_product = ff_q_left_product_terminal * S ((S (e)) * ff_v_left_product) + (x))) /\ forall ff_i_left_product. (exists ff_lt_left_product_bound. ff_lt_left_product_bound + S ff_i_left_product = e) -> exists ff_p_left_product ff_r_left_product ff_s_left_product. ((((exists ff_h_left_product_factor. ff_h_left_product_factor + S (ff_p_left_product) = S ((S (ff_i_left_product)) * ff_c_left)) /\ exists ff_q_left_product_factor. ff_b_left = ff_q_left_product_factor * S ((S (ff_i_left_product)) * ff_c_left) + (ff_p_left_product))) /\ ((((exists ff_h_left_product_partial. ff_h_left_product_partial + S (ff_r_left_product) = S ((S (ff_i_left_product)) * ff_v_left_product)) /\ exists ff_q_left_product_partial. ff_u_left_product = ff_q_left_product_partial * S ((S (ff_i_left_product)) * ff_v_left_product) + (ff_r_left_product))) /\ ((((exists ff_h_left_product_successor. ff_h_left_product_successor + S (ff_s_left_product) = S ((S (S ff_i_left_product)) * ff_v_left_product)) /\ exists ff_q_left_product_successor. ff_u_left_product = ff_q_left_product_successor * S ((S (S ff_i_left_product)) * ff_v_left_product) + (ff_s_left_product))) /\ ff_s_left_product = ff_r_left_product * ff_p_left_product)))))))) -> (exists ff_b_right ff_c_right. ((forall ff_i_right_repeat. (exists ff_lt_right_repeat_bound. ff_lt_right_repeat_bound + S ff_i_right_repeat = e) -> (((exists ff_h_right_repeat_decoded. ff_h_right_repeat_decoded + S (b) = S ((S (ff_i_right_repeat)) * ff_c_right)) /\ exists ff_q_right_repeat_decoded. ff_b_right = ff_q_right_repeat_decoded * S ((S (ff_i_right_repeat)) * ff_c_right) + (b)))) /\ (exists ff_u_right_product ff_v_right_product. ((((exists ff_h_right_product_start. ff_h_right_product_start + S (1) = S ((S (0)) * ff_v_right_product)) /\ exists ff_q_right_product_start. ff_u_right_product = ff_q_right_product_start * S ((S (0)) * ff_v_right_product) + (1))) /\ ((((exists ff_h_right_product_terminal. ff_h_right_product_terminal + S (y) = S ((S (e)) * ff_v_right_product)) /\ exists ff_q_right_product_terminal. ff_u_right_product = ff_q_right_product_terminal * S ((S (e)) * ff_v_right_product) + (y))) /\ forall ff_i_right_product. (exists ff_lt_right_product_bound. ff_lt_right_product_bound + S ff_i_right_product = e) -> exists ff_p_right_product ff_r_right_product ff_s_right_product. ((((exists ff_h_right_product_factor. ff_h_right_product_factor + S (ff_p_right_product) = S ((S (ff_i_right_product)) * ff_c_right)) /\ exists ff_q_right_product_factor. ff_b_right = ff_q_right_product_factor * S ((S (ff_i_right_product)) * ff_c_right) + (ff_p_right_product))) /\ ((((exists ff_h_right_product_partial. ff_h_right_product_partial + S (ff_r_right_product) = S ((S (ff_i_right_product)) * ff_v_right_product)) /\ exists ff_q_right_product_partial. ff_u_right_product = ff_q_right_product_partial * S ((S (ff_i_right_product)) * ff_v_right_product) + (ff_r_right_product))) /\ ((((exists ff_h_right_product_successor. ff_h_right_product_successor + S (ff_s_right_product) = S ((S (S ff_i_right_product)) * ff_v_right_product)) /\ exists ff_q_right_product_successor. ff_u_right_product = ff_q_right_product_successor * S ((S (S ff_i_right_product)) * ff_v_right_product) + (ff_s_right_product))) /\ ff_s_right_product = ff_r_right_product * ff_p_right_product)))))))) -> (exists qr_u_result qr_v_result. x + m * qr_u_result = y + m * qr_v_result)

Structural proof guide

Generated structural guide

Balanced-congruent bases have congruent relational powers at every exponent.

Use the direct prerequisites pow_zero, pow_successor_decompose, pow_successor_pair_mul, mod_eq_refl, mod_eq_mul as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (4), intermediate claims (8), equality transport (4).

Referenced ingredients

PA004B pow_zero PA004D pow_successor_decompose PA005H pow_successor_pair_mul PA0023 mod_eq_refl PA004E mod_eq_mul

Proof neighborhood

Direct dependencies

PA004B pow_zero PA004D pow_successor_decompose PA005H pow_successor_pair_mul PA0023 mod_eq_refl PA004E mod_eq_mul

Direct dependents

PA0088 pow_congruent_base_witness 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 Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro m
  2. 0002intro a
  3. 0003intro b
  4. 0004induction e
  5. 0005intro x
  6. 0006intro y
  7. 0007intro hab
  8. 0008intro hx
  9. 0009intro hy
  10. 0010have hx1 : x = 1
  11. 0011specialize pow_zero a
  12. 0012specialize pow_zero 0
  13. 0013specialize pow_zero x
  14. 0014apply pow_zero
  15. 0015refl
  16. 0016exact hx
  17. 0017have hy1 : y = 1
  18. 0018specialize pow_zero b
  19. 0019specialize pow_zero 0
  20. 0020specialize pow_zero y
  21. 0021apply pow_zero
  22. 0022refl
  23. 0023exact hy
  24. 0024rewrite hx1
  25. 0025rewrite hy1
  26. 0026specialize mod_eq_refl m
  27. 0027specialize mod_eq_refl 1
  28. 0028exact mod_eq_refl
  29. 0029intro x
  30. 0030intro y
  31. 0031intro hab
  32. 0032intro hx
  33. 0033intro hy
  34. 0034have hleft : exists r. (exists ff_b_left_step ff_c_left_step. ((forall ff_i_left_step_repeat. (exists ff_lt_left_step_repeat_bound. ff_lt_left_step_repeat_bound + S ff_i_left_step_repeat = e) -> (((exists ff_h_left_step_repeat_decoded. ff_h_left_step_repeat_decoded + S (a) = S ((S (ff_i_left_step_repeat)) * ff_c_left_step)) /\ exists ff_q_left_step_repeat_decoded. ff_b_left_step = ff_q_left_step_repeat_decoded * S ((S (ff_i_left_step_repeat)) * ff_c_left_step) + (a)))) /\ (exists ff_u_left_step_product ff_v_left_step_product. ((((exists ff_h_left_step_product_start. ff_h_left_step_product_start + S (1) = S ((S (0)) * ff_v_left_step_product)) /\ exists ff_q_left_step_product_start. ff_u_left_step_product = ff_q_left_step_product_start * S ((S (0)) * ff_v_left_step_product) + (1))) /\ ((((exists ff_h_left_step_product_terminal. ff_h_left_step_product_terminal + S (r) = S ((S (e)) * ff_v_left_step_product)) /\ exists ff_q_left_step_product_terminal. ff_u_left_step_product = ff_q_left_step_product_terminal * S ((S (e)) * ff_v_left_step_product) + (r))) /\ forall ff_i_left_step_product. (exists ff_lt_left_step_product_bound. ff_lt_left_step_product_bound + S ff_i_left_step_product = e) -> exists ff_p_left_step_product ff_r_left_step_product ff_s_left_step_product. ((((exists ff_h_left_step_product_factor. ff_h_left_step_product_factor + S (ff_p_left_step_product) = S ((S (ff_i_left_step_product)) * ff_c_left_step)) /\ exists ff_q_left_step_product_factor. ff_b_left_step = ff_q_left_step_product_factor * S ((S (ff_i_left_step_product)) * ff_c_left_step) + (ff_p_left_step_product))) /\ ((((exists ff_h_left_step_product_partial. ff_h_left_step_product_partial + S (ff_r_left_step_product) = S ((S (ff_i_left_step_product)) * ff_v_left_step_product)) /\ exists ff_q_left_step_product_partial. ff_u_left_step_product = ff_q_left_step_product_partial * S ((S (ff_i_left_step_product)) * ff_v_left_step_product) + (ff_r_left_step_product))) /\ ((((exists ff_h_left_step_product_successor. ff_h_left_step_product_successor + S (ff_s_left_step_product) = S ((S (S ff_i_left_step_product)) * ff_v_left_step_product)) /\ exists ff_q_left_step_product_successor. ff_u_left_step_product = ff_q_left_step_product_successor * S ((S (S ff_i_left_step_product)) * ff_v_left_step_product) + (ff_s_left_step_product))) /\ ff_s_left_step_product = ff_r_left_step_product * ff_p_left_step_product)))))))) /\ x = r * a
  35. 0035specialize pow_successor_decompose a
  36. 0036specialize pow_successor_decompose e
  37. 0037specialize pow_successor_decompose (S e)
  38. 0038specialize pow_successor_decompose x
  39. 0039apply pow_successor_decompose
  40. 0040refl
  41. 0041exact hx
  42. 0042cases hleft
  43. 0043cases hleft_witness
  44. 0044have hright : exists r. (exists ff_b_right_step ff_c_right_step. ((forall ff_i_right_step_repeat. (exists ff_lt_right_step_repeat_bound. ff_lt_right_step_repeat_bound + S ff_i_right_step_repeat = e) -> (((exists ff_h_right_step_repeat_decoded. ff_h_right_step_repeat_decoded + S (b) = S ((S (ff_i_right_step_repeat)) * ff_c_right_step)) /\ exists ff_q_right_step_repeat_decoded. ff_b_right_step = ff_q_right_step_repeat_decoded * S ((S (ff_i_right_step_repeat)) * ff_c_right_step) + (b)))) /\ (exists ff_u_right_step_product ff_v_right_step_product. ((((exists ff_h_right_step_product_start. ff_h_right_step_product_start + S (1) = S ((S (0)) * ff_v_right_step_product)) /\ exists ff_q_right_step_product_start. ff_u_right_step_product = ff_q_right_step_product_start * S ((S (0)) * ff_v_right_step_product) + (1))) /\ ((((exists ff_h_right_step_product_terminal. ff_h_right_step_product_terminal + S (r) = S ((S (e)) * ff_v_right_step_product)) /\ exists ff_q_right_step_product_terminal. ff_u_right_step_product = ff_q_right_step_product_terminal * S ((S (e)) * ff_v_right_step_product) + (r))) /\ forall ff_i_right_step_product. (exists ff_lt_right_step_product_bound. ff_lt_right_step_product_bound + S ff_i_right_step_product = e) -> exists ff_p_right_step_product ff_r_right_step_product ff_s_right_step_product. ((((exists ff_h_right_step_product_factor. ff_h_right_step_product_factor + S (ff_p_right_step_product) = S ((S (ff_i_right_step_product)) * ff_c_right_step)) /\ exists ff_q_right_step_product_factor. ff_b_right_step = ff_q_right_step_product_factor * S ((S (ff_i_right_step_product)) * ff_c_right_step) + (ff_p_right_step_product))) /\ ((((exists ff_h_right_step_product_partial. ff_h_right_step_product_partial + S (ff_r_right_step_product) = S ((S (ff_i_right_step_product)) * ff_v_right_step_product)) /\ exists ff_q_right_step_product_partial. ff_u_right_step_product = ff_q_right_step_product_partial * S ((S (ff_i_right_step_product)) * ff_v_right_step_product) + (ff_r_right_step_product))) /\ ((((exists ff_h_right_step_product_successor. ff_h_right_step_product_successor + S (ff_s_right_step_product) = S ((S (S ff_i_right_step_product)) * ff_v_right_step_product)) /\ exists ff_q_right_step_product_successor. ff_u_right_step_product = ff_q_right_step_product_successor * S ((S (S ff_i_right_step_product)) * ff_v_right_step_product) + (ff_s_right_step_product))) /\ ff_s_right_step_product = ff_r_right_step_product * ff_p_right_step_product)))))))) /\ y = r * b
  45. 0045specialize pow_successor_decompose b
  46. 0046specialize pow_successor_decompose e
  47. 0047specialize pow_successor_decompose (S e)
  48. 0048specialize pow_successor_decompose y
  49. 0049apply pow_successor_decompose
  50. 0050refl
  51. 0051exact hy
  52. 0052cases hright
  53. 0053cases hright_witness
  54. 0054have hxmul : x = x1 * a
  55. 0055specialize pow_successor_pair_mul a
  56. 0056specialize pow_successor_pair_mul e
  57. 0057specialize pow_successor_pair_mul (S e)
  58. 0058specialize pow_successor_pair_mul x1
  59. 0059specialize pow_successor_pair_mul x
  60. 0060apply pow_successor_pair_mul
  61. 0061refl
  62. 0062exact hleft_witness_left
  63. 0063exact hx
  64. 0064have hymul : y = x2 * b
  65. 0065specialize pow_successor_pair_mul b
  66. 0066specialize pow_successor_pair_mul e
  67. 0067specialize pow_successor_pair_mul (S e)
  68. 0068specialize pow_successor_pair_mul x2
  69. 0069specialize pow_successor_pair_mul y
  70. 0070apply pow_successor_pair_mul
  71. 0071refl
  72. 0072exact hright_witness_left
  73. 0073exact hy
  74. 0074have hpre : exists qr_u_predecessors qr_v_predecessors. x1 + m * qr_u_predecessors = x2 + m * qr_v_predecessors
  75. 0075specialize IH x1
  76. 0076specialize IH x2
  77. 0077apply IH
  78. 0078exact hab
  79. 0079exact hleft_witness_left
  80. 0080exact hright_witness_left
  81. 0081have hmul : exists pc_u_products pc_v_products. (x1 * a) + m * pc_u_products = (x2 * b) + m * pc_v_products
  82. 0082specialize mod_eq_mul m
  83. 0083specialize mod_eq_mul x1
  84. 0084specialize mod_eq_mul x2
  85. 0085specialize mod_eq_mul a
  86. 0086specialize mod_eq_mul b
  87. 0087apply mod_eq_mul
  88. 0088exact hpre
  89. 0089exact hab
  90. 0090rewrite hxmul
  91. 0091rewrite hymul
  92. 0092exact hmul