PA0088 · theorem

pow_congruent_base_witness

Alpha v34 checked-use theorem · independently closed; not Stable

A congruent base has a relational power congruent to the supplied power.

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. ∀ a. ∀ r. ∀ h. ∀ A. ModEq(p,a,r) → Pow(a,h,A) → ∃ x. Pow(r,h,x) ∧ ModEq(p,A,x)

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

PD0020 Pow

1 occurrences

Exact expanded native-PA statement
forall p a r h A. (exists wpp_mod_left_eca_power_base_mod wpp_mod_right_eca_power_base_mod. (a) + p * wpp_mod_left_eca_power_base_mod = (r) + p * wpp_mod_right_eca_power_base_mod) -> (exists ff_b_eca_power_a ff_c_eca_power_a. ((forall ff_i_eca_power_a_repeat. (exists ff_lt_eca_power_a_repeat_bound. ff_lt_eca_power_a_repeat_bound + S ff_i_eca_power_a_repeat = h) -> (((exists ff_h_eca_power_a_repeat_decoded. ff_h_eca_power_a_repeat_decoded + S (a) = S ((S (ff_i_eca_power_a_repeat)) * ff_c_eca_power_a)) /\ exists ff_q_eca_power_a_repeat_decoded. ff_b_eca_power_a = ff_q_eca_power_a_repeat_decoded * S ((S (ff_i_eca_power_a_repeat)) * ff_c_eca_power_a) + (a)))) /\ (exists ff_u_eca_power_a_product ff_v_eca_power_a_product. ((((exists ff_h_eca_power_a_product_start. ff_h_eca_power_a_product_start + S (1) = S ((S (0)) * ff_v_eca_power_a_product)) /\ exists ff_q_eca_power_a_product_start. ff_u_eca_power_a_product = ff_q_eca_power_a_product_start * S ((S (0)) * ff_v_eca_power_a_product) + (1))) /\ ((((exists ff_h_eca_power_a_product_terminal. ff_h_eca_power_a_product_terminal + S (A) = S ((S (h)) * ff_v_eca_power_a_product)) /\ exists ff_q_eca_power_a_product_terminal. ff_u_eca_power_a_product = ff_q_eca_power_a_product_terminal * S ((S (h)) * ff_v_eca_power_a_product) + (A))) /\ forall ff_i_eca_power_a_product. (exists ff_lt_eca_power_a_product_bound. ff_lt_eca_power_a_product_bound + S ff_i_eca_power_a_product = h) -> exists ff_p_eca_power_a_product ff_r_eca_power_a_product ff_s_eca_power_a_product. ((((exists ff_h_eca_power_a_product_factor. ff_h_eca_power_a_product_factor + S (ff_p_eca_power_a_product) = S ((S (ff_i_eca_power_a_product)) * ff_c_eca_power_a)) /\ exists ff_q_eca_power_a_product_factor. ff_b_eca_power_a = ff_q_eca_power_a_product_factor * S ((S (ff_i_eca_power_a_product)) * ff_c_eca_power_a) + (ff_p_eca_power_a_product))) /\ ((((exists ff_h_eca_power_a_product_partial. ff_h_eca_power_a_product_partial + S (ff_r_eca_power_a_product) = S ((S (ff_i_eca_power_a_product)) * ff_v_eca_power_a_product)) /\ exists ff_q_eca_power_a_product_partial. ff_u_eca_power_a_product = ff_q_eca_power_a_product_partial * S ((S (ff_i_eca_power_a_product)) * ff_v_eca_power_a_product) + (ff_r_eca_power_a_product))) /\ ((((exists ff_h_eca_power_a_product_successor. ff_h_eca_power_a_product_successor + S (ff_s_eca_power_a_product) = S ((S (S ff_i_eca_power_a_product)) * ff_v_eca_power_a_product)) /\ exists ff_q_eca_power_a_product_successor. ff_u_eca_power_a_product = ff_q_eca_power_a_product_successor * S ((S (S ff_i_eca_power_a_product)) * ff_v_eca_power_a_product) + (ff_s_eca_power_a_product))) /\ ff_s_eca_power_a_product = ff_r_eca_power_a_product * ff_p_eca_power_a_product)))))))) -> (exists R. (exists ff_b_eca_power_r ff_c_eca_power_r. ((forall ff_i_eca_power_r_repeat. (exists ff_lt_eca_power_r_repeat_bound. ff_lt_eca_power_r_repeat_bound + S ff_i_eca_power_r_repeat = h) -> (((exists ff_h_eca_power_r_repeat_decoded. ff_h_eca_power_r_repeat_decoded + S (r) = S ((S (ff_i_eca_power_r_repeat)) * ff_c_eca_power_r)) /\ exists ff_q_eca_power_r_repeat_decoded. ff_b_eca_power_r = ff_q_eca_power_r_repeat_decoded * S ((S (ff_i_eca_power_r_repeat)) * ff_c_eca_power_r) + (r)))) /\ (exists ff_u_eca_power_r_product ff_v_eca_power_r_product. ((((exists ff_h_eca_power_r_product_start. ff_h_eca_power_r_product_start + S (1) = S ((S (0)) * ff_v_eca_power_r_product)) /\ exists ff_q_eca_power_r_product_start. ff_u_eca_power_r_product = ff_q_eca_power_r_product_start * S ((S (0)) * ff_v_eca_power_r_product) + (1))) /\ ((((exists ff_h_eca_power_r_product_terminal. ff_h_eca_power_r_product_terminal + S (R) = S ((S (h)) * ff_v_eca_power_r_product)) /\ exists ff_q_eca_power_r_product_terminal. ff_u_eca_power_r_product = ff_q_eca_power_r_product_terminal * S ((S (h)) * ff_v_eca_power_r_product) + (R))) /\ forall ff_i_eca_power_r_product. (exists ff_lt_eca_power_r_product_bound. ff_lt_eca_power_r_product_bound + S ff_i_eca_power_r_product = h) -> exists ff_p_eca_power_r_product ff_r_eca_power_r_product ff_s_eca_power_r_product. ((((exists ff_h_eca_power_r_product_factor. ff_h_eca_power_r_product_factor + S (ff_p_eca_power_r_product) = S ((S (ff_i_eca_power_r_product)) * ff_c_eca_power_r)) /\ exists ff_q_eca_power_r_product_factor. ff_b_eca_power_r = ff_q_eca_power_r_product_factor * S ((S (ff_i_eca_power_r_product)) * ff_c_eca_power_r) + (ff_p_eca_power_r_product))) /\ ((((exists ff_h_eca_power_r_product_partial. ff_h_eca_power_r_product_partial + S (ff_r_eca_power_r_product) = S ((S (ff_i_eca_power_r_product)) * ff_v_eca_power_r_product)) /\ exists ff_q_eca_power_r_product_partial. ff_u_eca_power_r_product = ff_q_eca_power_r_product_partial * S ((S (ff_i_eca_power_r_product)) * ff_v_eca_power_r_product) + (ff_r_eca_power_r_product))) /\ ((((exists ff_h_eca_power_r_product_successor. ff_h_eca_power_r_product_successor + S (ff_s_eca_power_r_product) = S ((S (S ff_i_eca_power_r_product)) * ff_v_eca_power_r_product)) /\ exists ff_q_eca_power_r_product_successor. ff_u_eca_power_r_product = ff_q_eca_power_r_product_successor * S ((S (S ff_i_eca_power_r_product)) * ff_v_eca_power_r_product) + (ff_s_eca_power_r_product))) /\ ff_s_eca_power_r_product = ff_r_eca_power_r_product * ff_p_eca_power_r_product)))))))) /\ (exists wpp_mod_left_eca_power_result_mod wpp_mod_right_eca_power_result_mod. (A) + p * wpp_mod_left_eca_power_result_mod = (R) + p * wpp_mod_right_eca_power_result_mod))

Proof neighborhood

Direct theorem prerequisites

PA0046 pow_exists PA005I pow_mod_congruent

Direct theorem dependents

PA00BR arbitrary_euler_criterion_residue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff

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

25 script commands · 7 reading checkpoints · 1 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 (2)
pow existspow mod congruent
01Fix variables and assumptionsL1–7

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro r
  4. L4
    intro h
  5. L5
    intro A
  6. L6
    intro har
  7. L7
    intro hpower
02Establish hrpowerL8–11

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

  1. L8
    have hrpower : ∃ R. Pow(r,h,R)Definitions: Pow(r,h,R)Original native command in the exact edition
  2. L9
    specialize pow_exists r
  3. L10
    specialize pow_exists h
  4. L11
    exact pow_exists
03Separate the logical casesL12–12

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

  1. L12
    cases hrpower
04Construct an explicit witnessL13–13

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

  1. L13
    exists x
05Separate the logical casesL14–14

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

  1. L14
    split
06Use earlier factsL15–24

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

  1. L15
    exact hrpower_witness
  2. L16
    specialize pow_mod_congruent p
  3. L17
    specialize pow_mod_congruent a
  4. L18
    specialize pow_mod_congruent r
  5. L19
    specialize pow_mod_congruent h
  6. L20
    specialize pow_mod_congruent A
  7. L21
    specialize pow_mod_congruent x
  8. L22
    apply pow_mod_congruent
  9. L23
    exact har
  10. L24
    exact hpower
07Use earlier factsL25–25

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

  1. L25
    exact hrpower_witness

Library-wide reading audit

Original defined command ledger · 25 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro r
  4. 0004intro h
  5. 0005intro A
  6. 0006intro har
  7. 0007intro hpower
  8. 0008have hrpower : ∃ R. Pow(r,h,R)
    Exact native replay linehave hrpower : exists R. (exists ff_b_eca_power_proof_exists ff_c_eca_power_proof_exists. ((forall ff_i_eca_power_proof_exists_repeat. (exists ff_lt_eca_power_proof_exists_repeat_bound. ff_lt_eca_power_proof_exists_repeat_bound + S ff_i_eca_power_proof_exists_repeat = h) -> (((exists ff_h_eca_power_proof_exists_repeat_decoded. ff_h_eca_power_proof_exists_repeat_decoded + S (r) = S ((S (ff_i_eca_power_proof_exists_repeat)) * ff_c_eca_power_proof_exists)) /\ exists ff_q_eca_power_proof_exists_repeat_decoded. ff_b_eca_power_proof_exists = ff_q_eca_power_proof_exists_repeat_decoded * S ((S (ff_i_eca_power_proof_exists_repeat)) * ff_c_eca_power_proof_exists) + (r)))) /\ (exists ff_u_eca_power_proof_exists_product ff_v_eca_power_proof_exists_product. ((((exists ff_h_eca_power_proof_exists_product_start. ff_h_eca_power_proof_exists_product_start + S (1) = S ((S (0)) * ff_v_eca_power_proof_exists_product)) /\ exists ff_q_eca_power_proof_exists_product_start. ff_u_eca_power_proof_exists_product = ff_q_eca_power_proof_exists_product_start * S ((S (0)) * ff_v_eca_power_proof_exists_product) + (1))) /\ ((((exists ff_h_eca_power_proof_exists_product_terminal. ff_h_eca_power_proof_exists_product_terminal + S (R) = S ((S (h)) * ff_v_eca_power_proof_exists_product)) /\ exists ff_q_eca_power_proof_exists_product_terminal. ff_u_eca_power_proof_exists_product = ff_q_eca_power_proof_exists_product_terminal * S ((S (h)) * ff_v_eca_power_proof_exists_product) + (R))) /\ forall ff_i_eca_power_proof_exists_product. (exists ff_lt_eca_power_proof_exists_product_bound. ff_lt_eca_power_proof_exists_product_bound + S ff_i_eca_power_proof_exists_product = h) -> exists ff_p_eca_power_proof_exists_product ff_r_eca_power_proof_exists_product ff_s_eca_power_proof_exists_product. ((((exists ff_h_eca_power_proof_exists_product_factor. ff_h_eca_power_proof_exists_product_factor + S (ff_p_eca_power_proof_exists_product) = S ((S (ff_i_eca_power_proof_exists_product)) * ff_c_eca_power_proof_exists)) /\ exists ff_q_eca_power_proof_exists_product_factor. ff_b_eca_power_proof_exists = ff_q_eca_power_proof_exists_product_factor * S ((S (ff_i_eca_power_proof_exists_product)) * ff_c_eca_power_proof_exists) + (ff_p_eca_power_proof_exists_product))) /\ ((((exists ff_h_eca_power_proof_exists_product_partial. ff_h_eca_power_proof_exists_product_partial + S (ff_r_eca_power_proof_exists_product) = S ((S (ff_i_eca_power_proof_exists_product)) * ff_v_eca_power_proof_exists_product)) /\ exists ff_q_eca_power_proof_exists_product_partial. ff_u_eca_power_proof_exists_product = ff_q_eca_power_proof_exists_product_partial * S ((S (ff_i_eca_power_proof_exists_product)) * ff_v_eca_power_proof_exists_product) + (ff_r_eca_power_proof_exists_product))) /\ ((((exists ff_h_eca_power_proof_exists_product_successor. ff_h_eca_power_proof_exists_product_successor + S (ff_s_eca_power_proof_exists_product) = S ((S (S ff_i_eca_power_proof_exists_product)) * ff_v_eca_power_proof_exists_product)) /\ exists ff_q_eca_power_proof_exists_product_successor. ff_u_eca_power_proof_exists_product = ff_q_eca_power_proof_exists_product_successor * S ((S (S ff_i_eca_power_proof_exists_product)) * ff_v_eca_power_proof_exists_product) + (ff_s_eca_power_proof_exists_product))) /\ ff_s_eca_power_proof_exists_product = ff_r_eca_power_proof_exists_product * ff_p_eca_power_proof_exists_product))))))))
  9. 0009specialize pow_exists r
  10. 0010specialize pow_exists h
  11. 0011exact pow_exists
  12. 0012cases hrpower
  13. 0013exists x
  14. 0014split
  15. 0015exact hrpower_witness
  16. 0016specialize pow_mod_congruent p
  17. 0017specialize pow_mod_congruent a
  18. 0018specialize pow_mod_congruent r
  19. 0019specialize pow_mod_congruent h
  20. 0020specialize pow_mod_congruent A
  21. 0021specialize pow_mod_congruent x
  22. 0022apply pow_mod_congruent
  23. 0023exact har
  24. 0024exact hpower
  25. 0025exact hrpower_witness