PA00BM

quadratic_nonresidue_half_power_mod_predecessor

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

For a reduced nonzero nonresidue, a^((p-1)/2) is p-1 modulo p.

Exact expanded PA statement

forall p a n h A. p = S n -> ((~(p = 1) /\ forall esi_prime_left_enr_prime esi_prime_right_enr_prime. p = esi_prime_left_enr_prime * esi_prime_right_enr_prime -> esi_prime_left_enr_prime = 1 \/ esi_prime_right_enr_prime = 1)) -> ~(a = 0) -> (exists wpo_gap_enr_target_bound. wpo_gap_enr_target_bound + S (a) = p) -> ~(exists qr_x_enr_nonresidue. exists qr_u_enr_nonresidue qr_v_enr_nonresidue. qr_x_enr_nonresidue * qr_x_enr_nonresidue + p * qr_u_enr_nonresidue = a + p * qr_v_enr_nonresidue) -> n = h + h -> (exists ff_b_enr_terminal_power ff_c_enr_terminal_power. ((forall ff_i_enr_terminal_power_repeat. (exists ff_lt_enr_terminal_power_repeat_bound. ff_lt_enr_terminal_power_repeat_bound + S ff_i_enr_terminal_power_repeat = h) -> (((exists ff_h_enr_terminal_power_repeat_decoded. ff_h_enr_terminal_power_repeat_decoded + S (a) = S ((S (ff_i_enr_terminal_power_repeat)) * ff_c_enr_terminal_power)) /\ exists ff_q_enr_terminal_power_repeat_decoded. ff_b_enr_terminal_power = ff_q_enr_terminal_power_repeat_decoded * S ((S (ff_i_enr_terminal_power_repeat)) * ff_c_enr_terminal_power) + (a)))) /\ (exists ff_u_enr_terminal_power_product ff_v_enr_terminal_power_product. ((((exists ff_h_enr_terminal_power_product_start. ff_h_enr_terminal_power_product_start + S (1) = S ((S (0)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_start. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_start * S ((S (0)) * ff_v_enr_terminal_power_product) + (1))) /\ ((((exists ff_h_enr_terminal_power_product_terminal. ff_h_enr_terminal_power_product_terminal + S (A) = S ((S (h)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_terminal. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_terminal * S ((S (h)) * ff_v_enr_terminal_power_product) + (A))) /\ forall ff_i_enr_terminal_power_product. (exists ff_lt_enr_terminal_power_product_bound. ff_lt_enr_terminal_power_product_bound + S ff_i_enr_terminal_power_product = h) -> exists ff_p_enr_terminal_power_product ff_r_enr_terminal_power_product ff_s_enr_terminal_power_product. ((((exists ff_h_enr_terminal_power_product_factor. ff_h_enr_terminal_power_product_factor + S (ff_p_enr_terminal_power_product) = S ((S (ff_i_enr_terminal_power_product)) * ff_c_enr_terminal_power)) /\ exists ff_q_enr_terminal_power_product_factor. ff_b_enr_terminal_power = ff_q_enr_terminal_power_product_factor * S ((S (ff_i_enr_terminal_power_product)) * ff_c_enr_terminal_power) + (ff_p_enr_terminal_power_product))) /\ ((((exists ff_h_enr_terminal_power_product_partial. ff_h_enr_terminal_power_product_partial + S (ff_r_enr_terminal_power_product) = S ((S (ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_partial. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_partial * S ((S (ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product) + (ff_r_enr_terminal_power_product))) /\ ((((exists ff_h_enr_terminal_power_product_successor. ff_h_enr_terminal_power_product_successor + S (ff_s_enr_terminal_power_product) = S ((S (S ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_successor. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_successor * S ((S (S ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product) + (ff_s_enr_terminal_power_product))) /\ ff_s_enr_terminal_power_product = ff_r_enr_terminal_power_product * ff_p_enr_terminal_power_product)))))))) -> (exists wpp_mod_left_enr_terminal_result wpp_mod_right_enr_terminal_result. (A) + p * wpp_mod_left_enr_terminal_result = (n) + p * wpp_mod_right_enr_terminal_result)

Structural proof guide

Generated structural guide

For a reduced nonzero nonresidue, a^((p-1)/2) is p-1 modulo p.

Use the direct prerequisites prime_scaled_inverse_prefix_exists, scaled_inverse_nonresidue_half_power_mod_predecessor as previously established PA formulas.

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

Referenced ingredients

PA008T prime_scaled_inverse_prefix_exists PA00BL scaled_inverse_nonresidue_half_power_mod_predecessor

Proof neighborhood

Direct dependencies

PA008T prime_scaled_inverse_prefix_exists PA00BL scaled_inverse_nonresidue_half_power_mod_predecessor

Direct dependents

PA00BN bounded_euler_criterion_dichotomy

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 ha0
  9. 0009intro hap
  10. 0010intro hnonresidue
  11. 0011intro heven
  12. 0012intro hpower
  13. 0013have hprefix_exists : exists u v. (forall esip_index_enr_prefix. (exists esip_gap_enr_prefix_prefix_bound. esip_gap_enr_prefix_prefix_bound + S (esip_index_enr_prefix) = n) -> exists esip_mate_enr_prefix. ((((exists ff_h_esip_enr_prefix_entry. ff_h_esip_enr_prefix_entry + S (esip_mate_enr_prefix) = S ((S (esip_index_enr_prefix)) * v)) /\ exists ff_q_esip_enr_prefix_entry. u = ff_q_esip_enr_prefix_entry * S ((S (esip_index_enr_prefix)) * v) + (esip_mate_enr_prefix))) /\ ((exists esip_gap_enr_prefix_relation_index_bound. esip_gap_enr_prefix_relation_index_bound + S (esip_index_enr_prefix) = n) /\ ((((~((S esip_index_enr_prefix) = 0) /\ (exists esip_gap_enr_prefix_relation_scaled_left_bound. esip_gap_enr_prefix_relation_scaled_left_bound + S (S esip_index_enr_prefix) = p))) /\ (((~(esip_mate_enr_prefix = 0) /\ (exists esip_gap_enr_prefix_relation_scaled_right_bound. esip_gap_enr_prefix_relation_scaled_right_bound + S (esip_mate_enr_prefix) = p))) /\ (exists esi_mod_left_enr_prefix_relation_scaled_mod esi_mod_right_enr_prefix_relation_scaled_mod. ((S esip_index_enr_prefix) * esip_mate_enr_prefix) + p * esi_mod_left_enr_prefix_relation_scaled_mod = (a) + p * esi_mod_right_enr_prefix_relation_scaled_mod)))))))
  14. 0014specialize prime_scaled_inverse_prefix_exists p
  15. 0015specialize prime_scaled_inverse_prefix_exists a
  16. 0016specialize prime_scaled_inverse_prefix_exists n
  17. 0017apply prime_scaled_inverse_prefix_exists
  18. 0018exact hpn
  19. 0019exact hp
  20. 0020exact ha0
  21. 0021exact hap
  22. 0022cases hprefix_exists
  23. 0023cases hprefix_exists_witness
  24. 0024specialize scaled_inverse_nonresidue_half_power_mod_predecessor p
  25. 0025specialize scaled_inverse_nonresidue_half_power_mod_predecessor a
  26. 0026specialize scaled_inverse_nonresidue_half_power_mod_predecessor n
  27. 0027specialize scaled_inverse_nonresidue_half_power_mod_predecessor x
  28. 0028specialize scaled_inverse_nonresidue_half_power_mod_predecessor x1
  29. 0029specialize scaled_inverse_nonresidue_half_power_mod_predecessor h
  30. 0030specialize scaled_inverse_nonresidue_half_power_mod_predecessor A
  31. 0031apply scaled_inverse_nonresidue_half_power_mod_predecessor
  32. 0032exact hpn
  33. 0033exact hp
  34. 0034exact hnonresidue
  35. 0035exact hprefix_exists_witness_witness
  36. 0036exact heven
  37. 0037exact hpower