PA00BS · theorem

bounded_euler_criterion_nonresidue_iff

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

For bounded nonzero inputs, nonresiduosity is equivalent to the half-power residue p-1.

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) → ¬a = 0 → Lt(a,p) → n = h + h → Pow(a,h,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

PD0002 Lt PD0004 Prime PD0008 ModEq PD0020 Pow PD0021 QRes

7 occurrences

In local proof propositions

PD0008 ModEq PD0021 QRes

11 occurrences

Exact expanded native-PA statement
forall p a n h A. p = S n -> ((~(p = 1) /\ forall esi_prime_left_ecb_prime esi_prime_right_ecb_prime. p = esi_prime_left_ecb_prime * esi_prime_right_ecb_prime -> esi_prime_left_ecb_prime = 1 \/ esi_prime_right_ecb_prime = 1)) -> ~(a = 0) -> (exists wpo_gap_ecb_a_lt_p. wpo_gap_ecb_a_lt_p + S (a) = p) -> n = h + h -> (exists ff_b_ecb_power ff_c_ecb_power. ((forall ff_i_ecb_power_repeat. (exists ff_lt_ecb_power_repeat_bound. ff_lt_ecb_power_repeat_bound + S ff_i_ecb_power_repeat = h) -> (((exists ff_h_ecb_power_repeat_decoded. ff_h_ecb_power_repeat_decoded + S (a) = S ((S (ff_i_ecb_power_repeat)) * ff_c_ecb_power)) /\ exists ff_q_ecb_power_repeat_decoded. ff_b_ecb_power = ff_q_ecb_power_repeat_decoded * S ((S (ff_i_ecb_power_repeat)) * ff_c_ecb_power) + (a)))) /\ (exists ff_u_ecb_power_product ff_v_ecb_power_product. ((((exists ff_h_ecb_power_product_start. ff_h_ecb_power_product_start + S (1) = S ((S (0)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_start. ff_u_ecb_power_product = ff_q_ecb_power_product_start * S ((S (0)) * ff_v_ecb_power_product) + (1))) /\ ((((exists ff_h_ecb_power_product_terminal. ff_h_ecb_power_product_terminal + S (A) = S ((S (h)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_terminal. ff_u_ecb_power_product = ff_q_ecb_power_product_terminal * S ((S (h)) * ff_v_ecb_power_product) + (A))) /\ forall ff_i_ecb_power_product. (exists ff_lt_ecb_power_product_bound. ff_lt_ecb_power_product_bound + S ff_i_ecb_power_product = h) -> exists ff_p_ecb_power_product ff_r_ecb_power_product ff_s_ecb_power_product. ((((exists ff_h_ecb_power_product_factor. ff_h_ecb_power_product_factor + S (ff_p_ecb_power_product) = S ((S (ff_i_ecb_power_product)) * ff_c_ecb_power)) /\ exists ff_q_ecb_power_product_factor. ff_b_ecb_power = ff_q_ecb_power_product_factor * S ((S (ff_i_ecb_power_product)) * ff_c_ecb_power) + (ff_p_ecb_power_product))) /\ ((((exists ff_h_ecb_power_product_partial. ff_h_ecb_power_product_partial + S (ff_r_ecb_power_product) = S ((S (ff_i_ecb_power_product)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_partial. ff_u_ecb_power_product = ff_q_ecb_power_product_partial * S ((S (ff_i_ecb_power_product)) * ff_v_ecb_power_product) + (ff_r_ecb_power_product))) /\ ((((exists ff_h_ecb_power_product_successor. ff_h_ecb_power_product_successor + S (ff_s_ecb_power_product) = S ((S (S ff_i_ecb_power_product)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_successor. ff_u_ecb_power_product = ff_q_ecb_power_product_successor * S ((S (S ff_i_ecb_power_product)) * ff_v_ecb_power_product) + (ff_s_ecb_power_product))) /\ ff_s_ecb_power_product = ff_r_ecb_power_product * ff_p_ecb_power_product)))))))) -> (((~(exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres) -> (exists wpp_mod_left_ecb_mod_predecessor wpp_mod_right_ecb_mod_predecessor. (A) + p * wpp_mod_left_ecb_mod_predecessor = (n) + p * wpp_mod_right_ecb_mod_predecessor)) /\ ((exists wpp_mod_left_ecb_mod_predecessor wpp_mod_right_ecb_mod_predecessor. (A) + p * wpp_mod_left_ecb_mod_predecessor = (n) + p * wpp_mod_right_ecb_mod_predecessor) -> ~(exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres))))

Proof neighborhood

Direct theorem prerequisites

PA00BN bounded_euler_criterion_dichotomy PA00BQ bounded_euler_criterion_residue_iff PA00BP odd_prime_one_not_mod_predecessor PA003L mod_eq_symm PA0024 mod_eq_trans

Direct theorem dependents

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

76 script commands · 18 reading checkpoints · 5 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)
bounded euler criterion dichotomybounded euler criterion residue iffodd prime one not mod predecessormod eq symmmod eq trans
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 ha0
  9. L9
    intro hap
  10. L10
    intro heven
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hpower
03Establish hdichotomyL12–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bounded euler criterion dichotomy.

  1. L12
    have hdichotomy : QRes(p,a) ∧ ModEq(p,A,1) ∨ ¬QRes(p,a) ∧ ModEq(p,A,n)Definitions: QRes(p,a)ModEq(p,A,1)ModEq(p,A,n)Original native command in the exact edition
  2. L13
    specialize bounded_euler_criterion_dichotomy p
  3. L14
    specialize bounded_euler_criterion_dichotomy a
  4. L15
    specialize bounded_euler_criterion_dichotomy n
  5. L16
    specialize bounded_euler_criterion_dichotomy h
  6. L17
    specialize bounded_euler_criterion_dichotomy A
  7. L18
    apply bounded_euler_criterion_dichotomy
  8. L19
    exact hpn
  9. L20
    exact hp
  10. L21
    exact ha0
04Use earlier factsL22–24

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

  1. L22
    exact hap
  2. L23
    exact heven
  3. L24
    exact hpower
05Establish hresidue_iffL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bounded euler criterion residue iff.

  1. L25
    have hresidue_iff : (QRes(p,a) → ModEq(p,A,1)) ∧ (ModEq(p,A,1) → QRes(p,a))Definitions: QRes(p,a)ModEq(p,A,1)Original native command in the exact edition
  2. L26
    specialize bounded_euler_criterion_residue_iff p
  3. L27
    specialize bounded_euler_criterion_residue_iff a
  4. L28
    specialize bounded_euler_criterion_residue_iff n
  5. L29
    specialize bounded_euler_criterion_residue_iff h
  6. L30
    specialize bounded_euler_criterion_residue_iff A
  7. L31
    apply bounded_euler_criterion_residue_iff
  8. L32
    exact hpn
  9. L33
    exact hp
  10. L34
    exact ha0
06Use earlier factsL35–37

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

  1. L35
    exact hap
  2. L36
    exact heven
  3. L37
    exact hpower
07Establish hdistinctL38–47

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd prime one not mod predecessor.

  1. L38
    have hdistinct : ¬ModEq(p,1,n)Definitions: ModEq(p,1,n)Original native command in the exact edition
  2. L39
    intro hcollision
  3. L40
    specialize odd_prime_one_not_mod_predecessor p
  4. L41
    specialize odd_prime_one_not_mod_predecessor n
  5. L42
    specialize odd_prime_one_not_mod_predecessor h
  6. L43
    apply odd_prime_one_not_mod_predecessor
  7. L44
    exact hpn
  8. L45
    exact hp
  9. L46
    exact heven
  10. L47
    exact hcollision
08Separate the logical casesL48–48

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

  1. L48
    split
09Fix variables and assumptionsL49–49

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

  1. L49
    intro hnonresidue
10Separate the logical casesL50–52

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

  1. L50
    cases hdichotomy
  2. L51
    cases hdichotomy_left
  3. L52
    exfalso
11Use earlier factsL53–54

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

  1. L53
    apply hnonresidue
  2. L54
    exact hdichotomy_left_left
12Separate the logical casesL55–55

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

  1. L55
    cases hdichotomy_right
13Use earlier factsL56–56

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

  1. L56
    exact hdichotomy_right_right
14Fix variables and assumptionsL57–58

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

  1. L57
    intro hminus
  2. L58
    intro hqres
15Separate the logical casesL59–59

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

  1. L59
    cases hresidue_iff
16Establish honeL60–63

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

  1. L60
  2. L61
    apply hresidue_iff_left
  3. L62
    exact hqres
  4. L63
    apply hdistinct
17Establish hone_backL64–73

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

  1. L64
    have hone_back : ModEq(p,1,A)Definitions: ModEq(p,1,A)Original native command in the exact edition
  2. L65
    specialize mod_eq_symm p
  3. L66
    specialize mod_eq_symm A
  4. L67
    specialize mod_eq_symm 1
  5. L68
    apply mod_eq_symm
  6. L69
    exact hone
  7. L70
    specialize mod_eq_trans p
  8. L71
    specialize mod_eq_trans 1
  9. L72
    specialize mod_eq_trans A
  10. L73
    specialize mod_eq_trans n
18Use earlier factsL74–76

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

  1. L74
    apply mod_eq_trans
  2. L75
    exact hone_back
  3. L76
    exact hminus

Library-wide reading audit

Original defined command ledger · 76 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro h
  5. 0005intro A
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro ha0
  9. 0009intro hap
  10. 0010intro heven
  11. 0011intro hpower
  12. 0012have hdichotomy : QRes(p,a) ∧ ModEq(p,A,1) ∨ ¬QRes(p,a) ∧ ModEq(p,A,n)
    Exact native replay linehave hdichotomy : (((exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres) /\ (exists wpp_mod_left_ecb_mod_one wpp_mod_right_ecb_mod_one. (A) + p * wpp_mod_left_ecb_mod_one = (1) + p * wpp_mod_right_ecb_mod_one)) \/ ((~(exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres)) /\ (exists wpp_mod_left_ecb_mod_predecessor wpp_mod_right_ecb_mod_predecessor. (A) + p * wpp_mod_left_ecb_mod_predecessor = (n) + p * wpp_mod_right_ecb_mod_predecessor)))
  13. 0013specialize bounded_euler_criterion_dichotomy p
  14. 0014specialize bounded_euler_criterion_dichotomy a
  15. 0015specialize bounded_euler_criterion_dichotomy n
  16. 0016specialize bounded_euler_criterion_dichotomy h
  17. 0017specialize bounded_euler_criterion_dichotomy A
  18. 0018apply bounded_euler_criterion_dichotomy
  19. 0019exact hpn
  20. 0020exact hp
  21. 0021exact ha0
  22. 0022exact hap
  23. 0023exact heven
  24. 0024exact hpower
  25. 0025have hresidue_iff : (QRes(p,a) → ModEq(p,A,1)) ∧ (ModEq(p,A,1) → QRes(p,a))
    Exact native replay linehave hresidue_iff : (((exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres) -> (exists wpp_mod_left_ecb_mod_one wpp_mod_right_ecb_mod_one. (A) + p * wpp_mod_left_ecb_mod_one = (1) + p * wpp_mod_right_ecb_mod_one)) /\ ((exists wpp_mod_left_ecb_mod_one wpp_mod_right_ecb_mod_one. (A) + p * wpp_mod_left_ecb_mod_one = (1) + p * wpp_mod_right_ecb_mod_one) -> (exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres)))
  26. 0026specialize bounded_euler_criterion_residue_iff p
  27. 0027specialize bounded_euler_criterion_residue_iff a
  28. 0028specialize bounded_euler_criterion_residue_iff n
  29. 0029specialize bounded_euler_criterion_residue_iff h
  30. 0030specialize bounded_euler_criterion_residue_iff A
  31. 0031apply bounded_euler_criterion_residue_iff
  32. 0032exact hpn
  33. 0033exact hp
  34. 0034exact ha0
  35. 0035exact hap
  36. 0036exact heven
  37. 0037exact hpower
  38. 0038have hdistinct : ¬ModEq(p,1,n)
    Exact native replay linehave hdistinct : ~(exists wpp_mod_left_ecb_one_mod_predecessor wpp_mod_right_ecb_one_mod_predecessor. (1) + p * wpp_mod_left_ecb_one_mod_predecessor = (n) + p * wpp_mod_right_ecb_one_mod_predecessor)
  39. 0039intro hcollision
  40. 0040specialize odd_prime_one_not_mod_predecessor p
  41. 0041specialize odd_prime_one_not_mod_predecessor n
  42. 0042specialize odd_prime_one_not_mod_predecessor h
  43. 0043apply odd_prime_one_not_mod_predecessor
  44. 0044exact hpn
  45. 0045exact hp
  46. 0046exact heven
  47. 0047exact hcollision
  48. 0048split
  49. 0049intro hnonresidue
  50. 0050cases hdichotomy
  51. 0051cases hdichotomy_left
  52. 0052exfalso
  53. 0053apply hnonresidue
  54. 0054exact hdichotomy_left_left
  55. 0055cases hdichotomy_right
  56. 0056exact hdichotomy_right_right
  57. 0057intro hminus
  58. 0058intro hqres
  59. 0059cases hresidue_iff
  60. 0060have hone : ModEq(p,A,1)
    Exact native replay linehave hone : exists wpp_mod_left_ecb_mod_one wpp_mod_right_ecb_mod_one. (A) + p * wpp_mod_left_ecb_mod_one = (1) + p * wpp_mod_right_ecb_mod_one
  61. 0061apply hresidue_iff_left
  62. 0062exact hqres
  63. 0063apply hdistinct
  64. 0064have hone_back : ModEq(p,1,A)
    Exact native replay linehave hone_back : exists wpp_mod_left_ecb_nonresidue_one_back wpp_mod_right_ecb_nonresidue_one_back. (1) + p * wpp_mod_left_ecb_nonresidue_one_back = (A) + p * wpp_mod_right_ecb_nonresidue_one_back
  65. 0065specialize mod_eq_symm p
  66. 0066specialize mod_eq_symm A
  67. 0067specialize mod_eq_symm 1
  68. 0068apply mod_eq_symm
  69. 0069exact hone
  70. 0070specialize mod_eq_trans p
  71. 0071specialize mod_eq_trans 1
  72. 0072specialize mod_eq_trans A
  73. 0073specialize mod_eq_trans n
  74. 0074apply mod_eq_trans
  75. 0075exact hone_back
  76. 0076exact hminus