PA00BT · theorem

arbitrary_euler_criterion_nonresidue_iff

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

Euler's nonresidue equivalence for an arbitrary nonmultiple representative.

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,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

7 occurrences

In local proof propositions

PD0002 Lt PD0008 ModEq PD0020 Pow PD0021 QRes

17 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_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

PA0031 prime_nonzero PA0086 nondivisor_canonical_remainder_exists PA0087 quadratic_residue_mod_equiv PA0088 pow_congruent_base_witness PA00BS bounded_euler_criterion_nonresidue_iff PA003L mod_eq_symm PA0024 mod_eq_trans

Direct theorem dependents

PA00BU arbitrary_euler_criterion_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

98 script commands · 17 reading checkpoints · 10 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 (7)
prime nonzeronondivisor canonical remainder existsquadratic residue mod equivpow congruent base witnessbounded euler criterion nonresidue iffmod 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 hnotdiv
  9. L9
    intro heven
  10. L10
    intro hpower
02Establish hp0L11–16

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

  1. L11
    have hp0 : ~(p = 0)
  2. L12
    intro hpzero
  3. L13
    specialize prime_nonzero p
  4. L14
    apply prime_nonzero
  5. L15
    exact hp
  6. L16
    exact hpzero
03Establish hcanonicalL17–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply nondivisor canonical remainder exists.

  1. L17
    have hcanonical : ∃ r. ¬r = 0 ∧ (Lt(r,p) ∧ ModEq(p,a,r))Definitions: Lt(r,p)ModEq(p,a,r)Original native command in the exact edition
  2. L18
    specialize nondivisor_canonical_remainder_exists p
  3. L19
    specialize nondivisor_canonical_remainder_exists a
  4. L20
    apply nondivisor_canonical_remainder_exists
  5. L21
    exact hp0
  6. L22
    exact hnotdiv
04Separate the logical casesL23–25

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

  1. L23
    cases hcanonical
  2. L24
    cases hcanonical_witness
  3. L25
    cases hcanonical_witness_right
05Establish hpower_transportL26–34

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

  1. L26
    have hpower_transport : ∃ R. Pow(x,h,R) ∧ ModEq(p,A,R)Definitions: Pow(x,h,R)ModEq(p,A,R)Original native command in the exact edition
  2. L27
    specialize pow_congruent_base_witness p
  3. L28
    specialize pow_congruent_base_witness a
  4. L29
    specialize pow_congruent_base_witness x
  5. L30
    specialize pow_congruent_base_witness h
  6. L31
    specialize pow_congruent_base_witness A
  7. L32
    apply pow_congruent_base_witness
  8. L33
    exact hcanonical_witness_right_right
  9. L34
    exact hpower
06Separate the logical casesL35–36

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

  1. L35
    cases hpower_transport
  2. L36
    cases hpower_transport_witness
07Establish hqres_equivL37–42

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

  1. L37
    have hqres_equiv : (QRes(p,a) → QRes(p,x)) ∧ (QRes(p,x) → QRes(p,a))Definitions: QRes(p,a)QRes(p,x)Original native command in the exact edition
  2. L38
    specialize quadratic_residue_mod_equiv p
  3. L39
    specialize quadratic_residue_mod_equiv a
  4. L40
    specialize quadratic_residue_mod_equiv x
  5. L41
    apply quadratic_residue_mod_equiv
  6. L42
    exact hcanonical_witness_right_right
08Establish hboundedL43–52

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

  1. L43
    have hbounded : (¬QRes(p,x) → ModEq(p,x1,n)) ∧ (ModEq(p,x1,n) → ¬QRes(p,x))Definitions: QRes(p,x)ModEq(p,x1,n)Original native command in the exact edition
  2. L44
    specialize bounded_euler_criterion_nonresidue_iff p
  3. L45
    specialize bounded_euler_criterion_nonresidue_iff x
  4. L46
    specialize bounded_euler_criterion_nonresidue_iff n
  5. L47
    specialize bounded_euler_criterion_nonresidue_iff h
  6. L48
    specialize bounded_euler_criterion_nonresidue_iff x1
  7. L49
    apply bounded_euler_criterion_nonresidue_iff
  8. L50
    exact hpn
  9. L51
    exact hp
  10. L52
    exact hcanonical_witness_left
09Use earlier factsL53–55

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

  1. L53
    exact hcanonical_witness_right_left
  2. L54
    exact heven
  3. L55
    exact hpower_transport_witness_left
10Separate the logical casesL56–58

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

  1. L56
    cases hqres_equiv
  2. L57
    cases hbounded
  3. L58
    split
11Fix variables and assumptionsL59–59

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

  1. L59
    intro hnqa
12Establish hnqrL60–64

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

  1. L60
    have hnqr : ¬QRes(p,x)Definitions: QRes(p,x)Original native command in the exact edition
  2. L61
    intro hqr
  3. L62
    apply hnqa
  4. L63
    apply hqres_equiv_right
  5. L64
    exact hqr
13Establish hRminusL65–74

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

  1. L65
    have hRminus : ModEq(p,x1,n)Definitions: ModEq(p,x1,n)Original native command in the exact edition
  2. L66
    apply hbounded_left
  3. L67
    exact hnqr
  4. L68
    specialize mod_eq_trans p
  5. L69
    specialize mod_eq_trans A
  6. L70
    specialize mod_eq_trans x1
  7. L71
    specialize mod_eq_trans n
  8. L72
    apply mod_eq_trans
  9. L73
    exact hpower_transport_witness_right
  10. L74
    exact hRminus
14Fix variables and assumptionsL75–75

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

  1. L75
    intro hAminus
15Establish hRAL76–81

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

  1. L76
  2. L77
    specialize mod_eq_symm p
  3. L78
    specialize mod_eq_symm A
  4. L79
    specialize mod_eq_symm x1
  5. L80
    apply mod_eq_symm
  6. L81
    exact hpower_transport_witness_right
16Establish hRminusL82–89

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

  1. L82
    have hRminus : ModEq(p,x1,n)Definitions: ModEq(p,x1,n)Original native command in the exact edition
  2. L83
    specialize mod_eq_trans p
  3. L84
    specialize mod_eq_trans x1
  4. L85
    specialize mod_eq_trans A
  5. L86
    specialize mod_eq_trans n
  6. L87
    apply mod_eq_trans
  7. L88
    exact hRA
  8. L89
    exact hAminus
17Establish hnqrL90–98

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

  1. L90
    have hnqr : ¬QRes(p,x)Definitions: QRes(p,x)Original native command in the exact edition
  2. L91
    intro hqr
  3. L92
    apply hbounded_right
  4. L93
    exact hRminus
  5. L94
    exact hqr
  6. L95
    intro hqa
  7. L96
    apply hnqr
  8. L97
    apply hqres_equiv_left
  9. L98
    exact hqa

Library-wide reading audit

Original defined command ledger · 98 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. 0011have hp0 : ~(p = 0)
  12. 0012intro hpzero
  13. 0013specialize prime_nonzero p
  14. 0014apply prime_nonzero
  15. 0015exact hp
  16. 0016exact hpzero
  17. 0017have hcanonical : ∃ r. ¬r = 0 ∧ (Lt(r,p) ∧ ModEq(p,a,r))
    Exact native replay linehave hcanonical : exists r. ~(r = 0) /\ ((exists wpo_gap_eca_local_r_bound. wpo_gap_eca_local_r_bound + S (r) = p) /\ (exists wpp_mod_left_eca_local_a_r wpp_mod_right_eca_local_a_r. (a) + p * wpp_mod_left_eca_local_a_r = (r) + p * wpp_mod_right_eca_local_a_r))
  18. 0018specialize nondivisor_canonical_remainder_exists p
  19. 0019specialize nondivisor_canonical_remainder_exists a
  20. 0020apply nondivisor_canonical_remainder_exists
  21. 0021exact hp0
  22. 0022exact hnotdiv
  23. 0023cases hcanonical
  24. 0024cases hcanonical_witness
  25. 0025cases hcanonical_witness_right
  26. 0026have hpower_transport : ∃ R. Pow(x,h,R) ∧ ModEq(p,A,R)
    Exact native replay linehave hpower_transport : exists R. (exists ff_b_eca_proof_power_x_R ff_c_eca_proof_power_x_R. ((forall ff_i_eca_proof_power_x_R_repeat. (exists ff_lt_eca_proof_power_x_R_repeat_bound. ff_lt_eca_proof_power_x_R_repeat_bound + S ff_i_eca_proof_power_x_R_repeat = h) -> (((exists ff_h_eca_proof_power_x_R_repeat_decoded. ff_h_eca_proof_power_x_R_repeat_decoded + S (x) = S ((S (ff_i_eca_proof_power_x_R_repeat)) * ff_c_eca_proof_power_x_R)) /\ exists ff_q_eca_proof_power_x_R_repeat_decoded. ff_b_eca_proof_power_x_R = ff_q_eca_proof_power_x_R_repeat_decoded * S ((S (ff_i_eca_proof_power_x_R_repeat)) * ff_c_eca_proof_power_x_R) + (x)))) /\ (exists ff_u_eca_proof_power_x_R_product ff_v_eca_proof_power_x_R_product. ((((exists ff_h_eca_proof_power_x_R_product_start. ff_h_eca_proof_power_x_R_product_start + S (1) = S ((S (0)) * ff_v_eca_proof_power_x_R_product)) /\ exists ff_q_eca_proof_power_x_R_product_start. ff_u_eca_proof_power_x_R_product = ff_q_eca_proof_power_x_R_product_start * S ((S (0)) * ff_v_eca_proof_power_x_R_product) + (1))) /\ ((((exists ff_h_eca_proof_power_x_R_product_terminal. ff_h_eca_proof_power_x_R_product_terminal + S (R) = S ((S (h)) * ff_v_eca_proof_power_x_R_product)) /\ exists ff_q_eca_proof_power_x_R_product_terminal. ff_u_eca_proof_power_x_R_product = ff_q_eca_proof_power_x_R_product_terminal * S ((S (h)) * ff_v_eca_proof_power_x_R_product) + (R))) /\ forall ff_i_eca_proof_power_x_R_product. (exists ff_lt_eca_proof_power_x_R_product_bound. ff_lt_eca_proof_power_x_R_product_bound + S ff_i_eca_proof_power_x_R_product = h) -> exists ff_p_eca_proof_power_x_R_product ff_r_eca_proof_power_x_R_product ff_s_eca_proof_power_x_R_product. ((((exists ff_h_eca_proof_power_x_R_product_factor. ff_h_eca_proof_power_x_R_product_factor + S (ff_p_eca_proof_power_x_R_product) = S ((S (ff_i_eca_proof_power_x_R_product)) * ff_c_eca_proof_power_x_R)) /\ exists ff_q_eca_proof_power_x_R_product_factor. ff_b_eca_proof_power_x_R = ff_q_eca_proof_power_x_R_product_factor * S ((S (ff_i_eca_proof_power_x_R_product)) * ff_c_eca_proof_power_x_R) + (ff_p_eca_proof_power_x_R_product))) /\ ((((exists ff_h_eca_proof_power_x_R_product_partial. ff_h_eca_proof_power_x_R_product_partial + S (ff_r_eca_proof_power_x_R_product) = S ((S (ff_i_eca_proof_power_x_R_product)) * ff_v_eca_proof_power_x_R_product)) /\ exists ff_q_eca_proof_power_x_R_product_partial. ff_u_eca_proof_power_x_R_product = ff_q_eca_proof_power_x_R_product_partial * S ((S (ff_i_eca_proof_power_x_R_product)) * ff_v_eca_proof_power_x_R_product) + (ff_r_eca_proof_power_x_R_product))) /\ ((((exists ff_h_eca_proof_power_x_R_product_successor. ff_h_eca_proof_power_x_R_product_successor + S (ff_s_eca_proof_power_x_R_product) = S ((S (S ff_i_eca_proof_power_x_R_product)) * ff_v_eca_proof_power_x_R_product)) /\ exists ff_q_eca_proof_power_x_R_product_successor. ff_u_eca_proof_power_x_R_product = ff_q_eca_proof_power_x_R_product_successor * S ((S (S ff_i_eca_proof_power_x_R_product)) * ff_v_eca_proof_power_x_R_product) + (ff_s_eca_proof_power_x_R_product))) /\ ff_s_eca_proof_power_x_R_product = ff_r_eca_proof_power_x_R_product * ff_p_eca_proof_power_x_R_product)))))))) /\ (exists wpp_mod_left_eca_proof_A_R wpp_mod_right_eca_proof_A_R. (A) + p * wpp_mod_left_eca_proof_A_R = (R) + p * wpp_mod_right_eca_proof_A_R)
  27. 0027specialize pow_congruent_base_witness p
  28. 0028specialize pow_congruent_base_witness a
  29. 0029specialize pow_congruent_base_witness x
  30. 0030specialize pow_congruent_base_witness h
  31. 0031specialize pow_congruent_base_witness A
  32. 0032apply pow_congruent_base_witness
  33. 0033exact hcanonical_witness_right_right
  34. 0034exact hpower
  35. 0035cases hpower_transport
  36. 0036cases hpower_transport_witness
  37. 0037have hqres_equiv : (QRes(p,a) → QRes(p,x)) ∧ (QRes(p,x) → QRes(p,a))
    Exact native replay linehave hqres_equiv : (((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_proof_qres_x. exists qr_u_eca_proof_qres_x qr_v_eca_proof_qres_x. qr_x_eca_proof_qres_x * qr_x_eca_proof_qres_x + p * qr_u_eca_proof_qres_x = x + p * qr_v_eca_proof_qres_x)) /\ ((exists qr_x_eca_proof_qres_x. exists qr_u_eca_proof_qres_x qr_v_eca_proof_qres_x. qr_x_eca_proof_qres_x * qr_x_eca_proof_qres_x + p * qr_u_eca_proof_qres_x = x + p * qr_v_eca_proof_qres_x) -> (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)))
  38. 0038specialize quadratic_residue_mod_equiv p
  39. 0039specialize quadratic_residue_mod_equiv a
  40. 0040specialize quadratic_residue_mod_equiv x
  41. 0041apply quadratic_residue_mod_equiv
  42. 0042exact hcanonical_witness_right_right
  43. 0043have hbounded : (¬QRes(p,x) → ModEq(p,x1,n)) ∧ (ModEq(p,x1,n) → ¬QRes(p,x))
    Exact native replay linehave hbounded : ((~(exists qr_x_eca_proof_qres_x. exists qr_u_eca_proof_qres_x qr_v_eca_proof_qres_x. qr_x_eca_proof_qres_x * qr_x_eca_proof_qres_x + p * qr_u_eca_proof_qres_x = x + p * qr_v_eca_proof_qres_x) -> (exists wpp_mod_left_eca_proof_x1_predecessor wpp_mod_right_eca_proof_x1_predecessor. (x1) + p * wpp_mod_left_eca_proof_x1_predecessor = (n) + p * wpp_mod_right_eca_proof_x1_predecessor)) /\ ((exists wpp_mod_left_eca_proof_x1_predecessor wpp_mod_right_eca_proof_x1_predecessor. (x1) + p * wpp_mod_left_eca_proof_x1_predecessor = (n) + p * wpp_mod_right_eca_proof_x1_predecessor) -> ~(exists qr_x_eca_proof_qres_x. exists qr_u_eca_proof_qres_x qr_v_eca_proof_qres_x. qr_x_eca_proof_qres_x * qr_x_eca_proof_qres_x + p * qr_u_eca_proof_qres_x = x + p * qr_v_eca_proof_qres_x)))
  44. 0044specialize bounded_euler_criterion_nonresidue_iff p
  45. 0045specialize bounded_euler_criterion_nonresidue_iff x
  46. 0046specialize bounded_euler_criterion_nonresidue_iff n
  47. 0047specialize bounded_euler_criterion_nonresidue_iff h
  48. 0048specialize bounded_euler_criterion_nonresidue_iff x1
  49. 0049apply bounded_euler_criterion_nonresidue_iff
  50. 0050exact hpn
  51. 0051exact hp
  52. 0052exact hcanonical_witness_left
  53. 0053exact hcanonical_witness_right_left
  54. 0054exact heven
  55. 0055exact hpower_transport_witness_left
  56. 0056cases hqres_equiv
  57. 0057cases hbounded
  58. 0058split
  59. 0059intro hnqa
  60. 0060have hnqr : ¬QRes(p,x)
    Exact native replay linehave hnqr : ~(exists qr_x_eca_proof_qres_x. exists qr_u_eca_proof_qres_x qr_v_eca_proof_qres_x. qr_x_eca_proof_qres_x * qr_x_eca_proof_qres_x + p * qr_u_eca_proof_qres_x = x + p * qr_v_eca_proof_qres_x)
  61. 0061intro hqr
  62. 0062apply hnqa
  63. 0063apply hqres_equiv_right
  64. 0064exact hqr
  65. 0065have hRminus : ModEq(p,x1,n)
    Exact native replay linehave hRminus : exists wpp_mod_left_eca_proof_x1_predecessor wpp_mod_right_eca_proof_x1_predecessor. (x1) + p * wpp_mod_left_eca_proof_x1_predecessor = (n) + p * wpp_mod_right_eca_proof_x1_predecessor
  66. 0066apply hbounded_left
  67. 0067exact hnqr
  68. 0068specialize mod_eq_trans p
  69. 0069specialize mod_eq_trans A
  70. 0070specialize mod_eq_trans x1
  71. 0071specialize mod_eq_trans n
  72. 0072apply mod_eq_trans
  73. 0073exact hpower_transport_witness_right
  74. 0074exact hRminus
  75. 0075intro hAminus
  76. 0076have hRA : ModEq(p,x1,A)
    Exact native replay linehave hRA : exists wpp_mod_left_eca_proof_x1_A wpp_mod_right_eca_proof_x1_A. (x1) + p * wpp_mod_left_eca_proof_x1_A = (A) + p * wpp_mod_right_eca_proof_x1_A
  77. 0077specialize mod_eq_symm p
  78. 0078specialize mod_eq_symm A
  79. 0079specialize mod_eq_symm x1
  80. 0080apply mod_eq_symm
  81. 0081exact hpower_transport_witness_right
  82. 0082have hRminus : ModEq(p,x1,n)
    Exact native replay linehave hRminus : exists wpp_mod_left_eca_proof_x1_predecessor wpp_mod_right_eca_proof_x1_predecessor. (x1) + p * wpp_mod_left_eca_proof_x1_predecessor = (n) + p * wpp_mod_right_eca_proof_x1_predecessor
  83. 0083specialize mod_eq_trans p
  84. 0084specialize mod_eq_trans x1
  85. 0085specialize mod_eq_trans A
  86. 0086specialize mod_eq_trans n
  87. 0087apply mod_eq_trans
  88. 0088exact hRA
  89. 0089exact hAminus
  90. 0090have hnqr : ¬QRes(p,x)
    Exact native replay linehave hnqr : ~(exists qr_x_eca_proof_qres_x. exists qr_u_eca_proof_qres_x qr_v_eca_proof_qres_x. qr_x_eca_proof_qres_x * qr_x_eca_proof_qres_x + p * qr_u_eca_proof_qres_x = x + p * qr_v_eca_proof_qres_x)
  91. 0091intro hqr
  92. 0092apply hbounded_right
  93. 0093exact hRminus
  94. 0094exact hqr
  95. 0095intro hqa
  96. 0096apply hnqr
  97. 0097apply hqres_equiv_left
  98. 0098exact hqa