PA005I · theorem

pow_mod_congruent

Stable checked-use theorem · independently closed

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

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

∀ m. ∀ a. ∀ b. ∀ e. ∀ x. ∀ y. ModEq(m,a,b) → Pow(a,e,x) → Pow(b,e,y) → ModEq(m,x,y)

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 PD0020 Pow

4 occurrences

In local proof propositions

PD0008 ModEq PD0020 Pow

4 occurrences

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

Proof neighborhood

Direct theorem prerequisites

PA004B pow_zero PA004D pow_successor_decompose PA005H pow_successor_pair_mul PA0023 mod_eq_refl PA004E mod_eq_mul

Direct theorem dependents

PA0088 pow_congruent_base_witness PA008M quadratic_residue_half_power_mod_one

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

92 script commands · 16 reading checkpoints · 8 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 (5)
pow zeropow successor decomposepow successor pair mulmod eq reflmod eq mul
01Fix variables and assumptionsL1–3

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

  1. L1
    intro m
  2. L2
    intro a
  3. L3
    intro b
02Induction on eL4–9

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

  1. L4
    induction e
  2. L5
    intro x
  3. L6
    intro y
  4. L7
    intro hab
  5. L8
    intro hx
  6. L9
    intro hy
03Establish hx1L10–16

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

  1. L10
    have hx1 : x = 1
  2. L11
    specialize pow_zero a
  3. L12
    specialize pow_zero 0
  4. L13
    specialize pow_zero x
  5. L14
    apply pow_zero
  6. L15
    refl
  7. L16
    exact hx
04Establish hy1L17–26

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

  1. L17
    have hy1 : y = 1
  2. L18
    specialize pow_zero b
  3. L19
    specialize pow_zero 0
  4. L20
    specialize pow_zero y
  5. L21
    apply pow_zero
  6. L22
    refl
  7. L23
    exact hy
  8. L24
    rewrite hx1
  9. L25
    rewrite hy1
  10. L26
    specialize mod_eq_refl m
05Use earlier factsL27–28

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

  1. L27
    specialize mod_eq_refl 1
  2. L28
    exact mod_eq_refl
06Fix variables and assumptionsL29–33

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

  1. L29
    intro x
  2. L30
    intro y
  3. L31
    intro hab
  4. L32
    intro hx
  5. L33
    intro hy
07Establish hleftL34–41

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

  1. L34
    have hleft : ∃ r. Pow(a,e,r) ∧ x = r · aDefinitions: Pow(a,e,r)Original native command in the exact edition
  2. L35
    specialize pow_successor_decompose a
  3. L36
    specialize pow_successor_decompose e
  4. L37
    specialize pow_successor_decompose (S e)
  5. L38
    specialize pow_successor_decompose x
  6. L39
    apply pow_successor_decompose
  7. L40
    refl
  8. L41
    exact hx
08Separate the logical casesL42–43

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

  1. L42
    cases hleft
  2. L43
    cases hleft_witness
09Establish hrightL44–51

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

  1. L44
    have hright : ∃ r. Pow(b,e,r) ∧ y = r · bDefinitions: Pow(b,e,r)Original native command in the exact edition
  2. L45
    specialize pow_successor_decompose b
  3. L46
    specialize pow_successor_decompose e
  4. L47
    specialize pow_successor_decompose (S e)
  5. L48
    specialize pow_successor_decompose y
  6. L49
    apply pow_successor_decompose
  7. L50
    refl
  8. L51
    exact hy
10Separate the logical casesL52–53

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

  1. L52
    cases hright
  2. L53
    cases hright_witness
11Establish hxmulL54–63

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

  1. L54
    have hxmul : x = x1 * a
  2. L55
    specialize pow_successor_pair_mul a
  3. L56
    specialize pow_successor_pair_mul e
  4. L57
    specialize pow_successor_pair_mul (S e)
  5. L58
    specialize pow_successor_pair_mul x1
  6. L59
    specialize pow_successor_pair_mul x
  7. L60
    apply pow_successor_pair_mul
  8. L61
    refl
  9. L62
    exact hleft_witness_left
  10. L63
    exact hx
12Establish hymulL64–73

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

  1. L64
    have hymul : y = x2 * b
  2. L65
    specialize pow_successor_pair_mul b
  3. L66
    specialize pow_successor_pair_mul e
  4. L67
    specialize pow_successor_pair_mul (S e)
  5. L68
    specialize pow_successor_pair_mul x2
  6. L69
    specialize pow_successor_pair_mul y
  7. L70
    apply pow_successor_pair_mul
  8. L71
    refl
  9. L72
    exact hright_witness_left
  10. L73
    exact hy
13Establish hpreL74–80

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

  1. L74
    have hpre : ModEq(m,x1,x2)Definitions: ModEq(m,x1,x2)Original native command in the exact edition
  2. L75
    specialize IH x1
  3. L76
    specialize IH x2
  4. L77
    apply IH
  5. L78
    exact hab
  6. L79
    exact hleft_witness_left
  7. L80
    exact hright_witness_left
14Establish hmulL81–90

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

  1. L81
    have hmul : ModEq(m,x1 · a,x2 · b)Definitions: ModEq(m,x1 · a,x2 · b)Original native command in the exact edition
  2. L82
    specialize mod_eq_mul m
  3. L83
    specialize mod_eq_mul x1
  4. L84
    specialize mod_eq_mul x2
  5. L85
    specialize mod_eq_mul a
  6. L86
    specialize mod_eq_mul b
  7. L87
    apply mod_eq_mul
  8. L88
    exact hpre
  9. L89
    exact hab
  10. L90
    rewrite hxmul
15Calculate and transport equalitiesL91–91

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

  1. L91
    rewrite hymul
16Use earlier factsL92–92

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

  1. L92
    exact hmul

Library-wide reading audit

Original defined command ledger · 92 lines
  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 : ∃ r. Pow(a,e,r) ∧ x = r · a
    Exact native replay linehave 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 : ∃ r. Pow(b,e,r) ∧ y = r · b
    Exact native replay linehave 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 : ModEq(m,x1,x2)
    Exact native replay linehave 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 : ModEq(m,x1 · a,x2 · b)
    Exact native replay linehave 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