PA00BU · theorem

arbitrary_euler_criterion_complete

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

Complete Euler criterion for every representative coprime to the prime.

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. ∀ n. ∀ h. ∀ A. p = S n → Prime(p) → ¬Dvd(p,a) → n = h + h → Pow(a,h,A) → (QRes(p,a) → ModEq(p,A,1)) ∧ (ModEq(p,A,1) → QRes(p,a)) ∧ ((¬QRes(p,a) → ModEq(p,A,n)) ∧ (ModEq(p,A,n) → ¬QRes(p,a)))

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

PD0003 Dvd PD0004 Prime PD0008 ModEq PD0020 Pow PD0021 QRes

11 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall p a n h A. p = S n -> ((~(p = 1) /\ forall frm_prime_left_eca_prime frm_prime_right_eca_prime. p = frm_prime_left_eca_prime * frm_prime_right_eca_prime -> frm_prime_left_eca_prime = 1 \/ frm_prime_right_eca_prime = 1)) -> (~(exists frm_factor_eca_not_divisor. a = p * frm_factor_eca_not_divisor)) -> n = h + h -> (exists ff_b_eca_power_endpoint ff_c_eca_power_endpoint. ((forall ff_i_eca_power_endpoint_repeat. (exists ff_lt_eca_power_endpoint_repeat_bound. ff_lt_eca_power_endpoint_repeat_bound + S ff_i_eca_power_endpoint_repeat = h) -> (((exists ff_h_eca_power_endpoint_repeat_decoded. ff_h_eca_power_endpoint_repeat_decoded + S (a) = S ((S (ff_i_eca_power_endpoint_repeat)) * ff_c_eca_power_endpoint)) /\ exists ff_q_eca_power_endpoint_repeat_decoded. ff_b_eca_power_endpoint = ff_q_eca_power_endpoint_repeat_decoded * S ((S (ff_i_eca_power_endpoint_repeat)) * ff_c_eca_power_endpoint) + (a)))) /\ (exists ff_u_eca_power_endpoint_product ff_v_eca_power_endpoint_product. ((((exists ff_h_eca_power_endpoint_product_start. ff_h_eca_power_endpoint_product_start + S (1) = S ((S (0)) * ff_v_eca_power_endpoint_product)) /\ exists ff_q_eca_power_endpoint_product_start. ff_u_eca_power_endpoint_product = ff_q_eca_power_endpoint_product_start * S ((S (0)) * ff_v_eca_power_endpoint_product) + (1))) /\ ((((exists ff_h_eca_power_endpoint_product_terminal. ff_h_eca_power_endpoint_product_terminal + S (A) = S ((S (h)) * ff_v_eca_power_endpoint_product)) /\ exists ff_q_eca_power_endpoint_product_terminal. ff_u_eca_power_endpoint_product = ff_q_eca_power_endpoint_product_terminal * S ((S (h)) * ff_v_eca_power_endpoint_product) + (A))) /\ forall ff_i_eca_power_endpoint_product. (exists ff_lt_eca_power_endpoint_product_bound. ff_lt_eca_power_endpoint_product_bound + S ff_i_eca_power_endpoint_product = h) -> exists ff_p_eca_power_endpoint_product ff_r_eca_power_endpoint_product ff_s_eca_power_endpoint_product. ((((exists ff_h_eca_power_endpoint_product_factor. ff_h_eca_power_endpoint_product_factor + S (ff_p_eca_power_endpoint_product) = S ((S (ff_i_eca_power_endpoint_product)) * ff_c_eca_power_endpoint)) /\ exists ff_q_eca_power_endpoint_product_factor. ff_b_eca_power_endpoint = ff_q_eca_power_endpoint_product_factor * S ((S (ff_i_eca_power_endpoint_product)) * ff_c_eca_power_endpoint) + (ff_p_eca_power_endpoint_product))) /\ ((((exists ff_h_eca_power_endpoint_product_partial. ff_h_eca_power_endpoint_product_partial + S (ff_r_eca_power_endpoint_product) = S ((S (ff_i_eca_power_endpoint_product)) * ff_v_eca_power_endpoint_product)) /\ exists ff_q_eca_power_endpoint_product_partial. ff_u_eca_power_endpoint_product = ff_q_eca_power_endpoint_product_partial * S ((S (ff_i_eca_power_endpoint_product)) * ff_v_eca_power_endpoint_product) + (ff_r_eca_power_endpoint_product))) /\ ((((exists ff_h_eca_power_endpoint_product_successor. ff_h_eca_power_endpoint_product_successor + S (ff_s_eca_power_endpoint_product) = S ((S (S ff_i_eca_power_endpoint_product)) * ff_v_eca_power_endpoint_product)) /\ exists ff_q_eca_power_endpoint_product_successor. ff_u_eca_power_endpoint_product = ff_q_eca_power_endpoint_product_successor * S ((S (S ff_i_eca_power_endpoint_product)) * ff_v_eca_power_endpoint_product) + (ff_s_eca_power_endpoint_product))) /\ ff_s_eca_power_endpoint_product = ff_r_eca_power_endpoint_product * ff_p_eca_power_endpoint_product)))))))) -> (((((exists qr_x_eca_qres_a. exists qr_u_eca_qres_a qr_v_eca_qres_a. qr_x_eca_qres_a * qr_x_eca_qres_a + p * qr_u_eca_qres_a = a + p * qr_v_eca_qres_a) -> (exists wpp_mod_left_eca_mod_one wpp_mod_right_eca_mod_one. (A) + p * wpp_mod_left_eca_mod_one = (1) + p * wpp_mod_right_eca_mod_one)) /\ ((exists wpp_mod_left_eca_mod_one wpp_mod_right_eca_mod_one. (A) + p * wpp_mod_left_eca_mod_one = (1) + p * wpp_mod_right_eca_mod_one) -> (exists qr_x_eca_qres_a. exists qr_u_eca_qres_a qr_v_eca_qres_a. qr_x_eca_qres_a * qr_x_eca_qres_a + p * qr_u_eca_qres_a = a + p * qr_v_eca_qres_a)))) /\ (((~(exists qr_x_eca_qres_a. exists qr_u_eca_qres_a qr_v_eca_qres_a. qr_x_eca_qres_a * qr_x_eca_qres_a + p * qr_u_eca_qres_a = a + p * qr_v_eca_qres_a) -> (exists wpp_mod_left_eca_mod_predecessor wpp_mod_right_eca_mod_predecessor. (A) + p * wpp_mod_left_eca_mod_predecessor = (n) + p * wpp_mod_right_eca_mod_predecessor)) /\ ((exists wpp_mod_left_eca_mod_predecessor wpp_mod_right_eca_mod_predecessor. (A) + p * wpp_mod_left_eca_mod_predecessor = (n) + p * wpp_mod_right_eca_mod_predecessor) -> ~(exists qr_x_eca_qres_a. exists qr_u_eca_qres_a qr_v_eca_qres_a. qr_x_eca_qres_a * qr_x_eca_qres_a + p * qr_u_eca_qres_a = a + p * qr_v_eca_qres_a)))))

Proof neighborhood

Direct theorem prerequisites

PA00BR arbitrary_euler_criterion_residue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff

Direct theorem dependents

PA00BV arbitrary_gauss_lemma_complete

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

33 script commands · 5 reading checkpoints · 0 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)
arbitrary euler criterion residue iffarbitrary euler criterion nonresidue iff
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro n
  4. L4
    intro h
  5. L5
    intro A
  6. L6
    intro hpn
  7. L7
    intro hp
  8. L8
    intro hnotdiv
  9. L9
    intro heven
  10. L10
    intro hpower
02Separate the logical casesL11–11

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

  1. L11
    split
03Use earlier factsL12–21

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

  1. L12
    specialize arbitrary_euler_criterion_residue_iff p
  2. L13
    specialize arbitrary_euler_criterion_residue_iff a
  3. L14
    specialize arbitrary_euler_criterion_residue_iff n
  4. L15
    specialize arbitrary_euler_criterion_residue_iff h
  5. L16
    specialize arbitrary_euler_criterion_residue_iff A
  6. L17
    apply arbitrary_euler_criterion_residue_iff
  7. L18
    exact hpn
  8. L19
    exact hp
  9. L20
    exact hnotdiv
  10. L21
    exact heven
04Use earlier factsL22–31

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

  1. L22
    exact hpower
  2. L23
    specialize arbitrary_euler_criterion_nonresidue_iff p
  3. L24
    specialize arbitrary_euler_criterion_nonresidue_iff a
  4. L25
    specialize arbitrary_euler_criterion_nonresidue_iff n
  5. L26
    specialize arbitrary_euler_criterion_nonresidue_iff h
  6. L27
    specialize arbitrary_euler_criterion_nonresidue_iff A
  7. L28
    apply arbitrary_euler_criterion_nonresidue_iff
  8. L29
    exact hpn
  9. L30
    exact hp
  10. L31
    exact hnotdiv
05Use earlier factsL32–33

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

  1. L32
    exact heven
  2. L33
    exact hpower

Library-wide reading audit

Original defined command ledger · 33 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro h
  5. 0005intro A
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro hnotdiv
  9. 0009intro heven
  10. 0010intro hpower
  11. 0011split
  12. 0012specialize arbitrary_euler_criterion_residue_iff p
  13. 0013specialize arbitrary_euler_criterion_residue_iff a
  14. 0014specialize arbitrary_euler_criterion_residue_iff n
  15. 0015specialize arbitrary_euler_criterion_residue_iff h
  16. 0016specialize arbitrary_euler_criterion_residue_iff A
  17. 0017apply arbitrary_euler_criterion_residue_iff
  18. 0018exact hpn
  19. 0019exact hp
  20. 0020exact hnotdiv
  21. 0021exact heven
  22. 0022exact hpower
  23. 0023specialize arbitrary_euler_criterion_nonresidue_iff p
  24. 0024specialize arbitrary_euler_criterion_nonresidue_iff a
  25. 0025specialize arbitrary_euler_criterion_nonresidue_iff n
  26. 0026specialize arbitrary_euler_criterion_nonresidue_iff h
  27. 0027specialize arbitrary_euler_criterion_nonresidue_iff A
  28. 0028apply arbitrary_euler_criterion_nonresidue_iff
  29. 0029exact hpn
  30. 0030exact hp
  31. 0031exact hnotdiv
  32. 0032exact heven
  33. 0033exact hpower