PA00BT

arbitrary_euler_criterion_nonresidue_iff

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

Euler's nonresidue equivalence for an arbitrary nonmultiple representative.

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

Structural proof guide

Generated structural guide

Euler's nonresidue equivalence for an arbitrary nonmultiple representative.

Use the direct prerequisites prime_nonzero, nondivisor_canonical_remainder_exists, quadratic_residue_mod_equiv, pow_congruent_base_witness, bounded_euler_criterion_nonresidue_iff, mod_eq_symm, mod_eq_trans as previously established PA formulas.

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

Referenced ingredients

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

Proof neighborhood

Direct dependencies

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 dependents

PA00BU arbitrary_euler_criterion_complete

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 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 : 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 : 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 : (((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 : ((~(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 : ~(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 : 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 : 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 : 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 : ~(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