PA0088

pow_congruent_base_witness

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

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

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

Structural proof guide

Generated structural guide

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

Use the direct prerequisites pow_exists, pow_mod_congruent as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (1).

Referenced ingredients

PA0046 pow_exists PA005I pow_mod_congruent

Proof neighborhood

Direct dependencies

PA0046 pow_exists PA005I pow_mod_congruent

Direct dependents

PA00BR arbitrary_euler_criterion_residue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff

Formal native tactic body

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

  1. 0001intro p
  2. 0002intro a
  3. 0003intro r
  4. 0004intro h
  5. 0005intro A
  6. 0006intro har
  7. 0007intro hpower
  8. 0008have 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