PA00BL

scaled_inverse_nonresidue_half_power_mod_predecessor

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

A full nonresidue scaled-inverse prefix satisfies Euler's minus-one branch.

Exact expanded PA statement

forall p a n u v 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)) -> ~(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) -> (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))))))) -> 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

A full nonresidue scaled-inverse prefix satisfies Euler's minus-one branch.

Use the direct prerequisites scaled_inverse_pair_order_terminal_package, scaled_pair_order_terminal_power_mod_predecessor as previously established PA formulas.

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

Referenced ingredients

PA009W scaled_inverse_pair_order_terminal_package PA00BK scaled_pair_order_terminal_power_mod_predecessor

Proof neighborhood

Direct dependencies

PA009W scaled_inverse_pair_order_terminal_package PA00BK scaled_pair_order_terminal_power_mod_predecessor

Direct dependents

PA00BM quadratic_nonresidue_half_power_mod_predecessor

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 u
  5. 0005intro v
  6. 0006intro h
  7. 0007intro A
  8. 0008intro hpn
  9. 0009intro hp
  10. 0010intro hnonresidue
  11. 0011intro hprefix
  12. 0012intro heven
  13. 0013intro hpower
  14. 0014have hterminal : exists b c. (((forall espo_position_enr_terminal_state_closed espo_source_enr_terminal_state_closed espo_mate_enr_terminal_state_closed. (exists wpo_gap_enr_terminal_state_closed_position_bound. wpo_gap_enr_terminal_state_closed_position_bound + S (espo_position_enr_terminal_state_closed) = h + h) -> (((exists wpo_beta_height_enr_terminal_state_closed_source_entry. wpo_beta_height_enr_terminal_state_closed_source_entry + S (espo_source_enr_terminal_state_closed) = S ((S (espo_position_enr_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_closed_source_entry. b = wpo_beta_quotient_enr_terminal_state_closed_source_entry * S ((S (espo_position_enr_terminal_state_closed)) * c) + (espo_source_enr_terminal_state_closed))) -> (((exists wpo_beta_height_enr_terminal_state_closed_scaled_entry. wpo_beta_height_enr_terminal_state_closed_scaled_entry + S (S espo_mate_enr_terminal_state_closed) = S ((S (espo_source_enr_terminal_state_closed)) * v)) /\ exists wpo_beta_quotient_enr_terminal_state_closed_scaled_entry. u = wpo_beta_quotient_enr_terminal_state_closed_scaled_entry * S ((S (espo_source_enr_terminal_state_closed)) * v) + (S espo_mate_enr_terminal_state_closed))) -> exists espo_mate_position_enr_terminal_state_closed. ((exists wpo_gap_enr_terminal_state_closed_mate_bound. wpo_gap_enr_terminal_state_closed_mate_bound + S (espo_mate_position_enr_terminal_state_closed) = h + h) /\ (((exists wpo_beta_height_enr_terminal_state_closed_mate_entry. wpo_beta_height_enr_terminal_state_closed_mate_entry + S (espo_mate_enr_terminal_state_closed) = S ((S (espo_mate_position_enr_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_closed_mate_entry. b = wpo_beta_quotient_enr_terminal_state_closed_mate_entry * S ((S (espo_mate_position_enr_terminal_state_closed)) * c) + (espo_mate_enr_terminal_state_closed))))) /\ (((forall fom_index_enr_terminal_state_bounded. (exists fom_gap_enr_terminal_state_bounded_index_bound. fom_gap_enr_terminal_state_bounded_index_bound + S (fom_index_enr_terminal_state_bounded) = h + h) -> exists fom_value_enr_terminal_state_bounded. ((((exists fom_beta_height_enr_terminal_state_bounded_entry. fom_beta_height_enr_terminal_state_bounded_entry + S (fom_value_enr_terminal_state_bounded) = S ((S (fom_index_enr_terminal_state_bounded)) * c)) /\ exists fom_beta_quotient_enr_terminal_state_bounded_entry. b = fom_beta_quotient_enr_terminal_state_bounded_entry * S ((S (fom_index_enr_terminal_state_bounded)) * c) + (fom_value_enr_terminal_state_bounded))) /\ (exists fom_gap_enr_terminal_state_bounded_value_bound. fom_gap_enr_terminal_state_bounded_value_bound + S (fom_value_enr_terminal_state_bounded) = n))) /\ (forall wpo_injective_left_enr_terminal_state_injective wpo_injective_right_enr_terminal_state_injective wpo_injective_value_enr_terminal_state_injective. (exists wpo_gap_enr_terminal_state_injective_left_bound. wpo_gap_enr_terminal_state_injective_left_bound + S (wpo_injective_left_enr_terminal_state_injective) = h + h) -> (exists wpo_gap_enr_terminal_state_injective_right_bound. wpo_gap_enr_terminal_state_injective_right_bound + S (wpo_injective_right_enr_terminal_state_injective) = h + h) -> (((exists wpo_beta_height_enr_terminal_state_injective_left_entry. wpo_beta_height_enr_terminal_state_injective_left_entry + S (wpo_injective_value_enr_terminal_state_injective) = S ((S (wpo_injective_left_enr_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_injective_left_entry. b = wpo_beta_quotient_enr_terminal_state_injective_left_entry * S ((S (wpo_injective_left_enr_terminal_state_injective)) * c) + (wpo_injective_value_enr_terminal_state_injective))) -> (((exists wpo_beta_height_enr_terminal_state_injective_right_entry. wpo_beta_height_enr_terminal_state_injective_right_entry + S (wpo_injective_value_enr_terminal_state_injective) = S ((S (wpo_injective_right_enr_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_injective_right_entry. b = wpo_beta_quotient_enr_terminal_state_injective_right_entry * S ((S (wpo_injective_right_enr_terminal_state_injective)) * c) + (wpo_injective_value_enr_terminal_state_injective))) -> wpo_injective_left_enr_terminal_state_injective = wpo_injective_right_enr_terminal_state_injective))))) /\ (forall espi_pair_enr_history. (exists wpo_gap_enr_history_pair_bound. wpo_gap_enr_history_pair_bound + S (espi_pair_enr_history) = h) -> exists espi_left_enr_history espi_right_enr_history. (((((exists wpo_beta_height_enr_history_left_entry. wpo_beta_height_enr_history_left_entry + S (espi_left_enr_history) = S ((S (espi_pair_enr_history + espi_pair_enr_history)) * c)) /\ exists wpo_beta_quotient_enr_history_left_entry. b = wpo_beta_quotient_enr_history_left_entry * S ((S (espi_pair_enr_history + espi_pair_enr_history)) * c) + (espi_left_enr_history))) /\ (((((exists wpo_beta_height_enr_history_right_entry. wpo_beta_height_enr_history_right_entry + S (espi_right_enr_history) = S ((S (S (espi_pair_enr_history + espi_pair_enr_history))) * c)) /\ exists wpo_beta_quotient_enr_history_right_entry. b = wpo_beta_quotient_enr_history_right_entry * S ((S (S (espi_pair_enr_history + espi_pair_enr_history))) * c) + (espi_right_enr_history))) /\ (((exists wpo_beta_height_enr_history_scaled_edge. wpo_beta_height_enr_history_scaled_edge + S (S espi_right_enr_history) = S ((S (espi_left_enr_history)) * v)) /\ exists wpo_beta_quotient_enr_history_scaled_edge. u = wpo_beta_quotient_enr_history_scaled_edge * S ((S (espi_left_enr_history)) * v) + (S espi_right_enr_history))))))))
  15. 0015specialize scaled_inverse_pair_order_terminal_package p
  16. 0016specialize scaled_inverse_pair_order_terminal_package a
  17. 0017specialize scaled_inverse_pair_order_terminal_package n
  18. 0018specialize scaled_inverse_pair_order_terminal_package u
  19. 0019specialize scaled_inverse_pair_order_terminal_package v
  20. 0020specialize scaled_inverse_pair_order_terminal_package h
  21. 0021apply scaled_inverse_pair_order_terminal_package
  22. 0022exact hpn
  23. 0023exact hp
  24. 0024exact hnonresidue
  25. 0025exact hprefix
  26. 0026exact heven
  27. 0027cases hterminal
  28. 0028cases hterminal_witness
  29. 0029cases hterminal_witness_witness
  30. 0030specialize scaled_pair_order_terminal_power_mod_predecessor p
  31. 0031specialize scaled_pair_order_terminal_power_mod_predecessor a
  32. 0032specialize scaled_pair_order_terminal_power_mod_predecessor n
  33. 0033specialize scaled_pair_order_terminal_power_mod_predecessor u
  34. 0034specialize scaled_pair_order_terminal_power_mod_predecessor v
  35. 0035specialize scaled_pair_order_terminal_power_mod_predecessor x
  36. 0036specialize scaled_pair_order_terminal_power_mod_predecessor x1
  37. 0037specialize scaled_pair_order_terminal_power_mod_predecessor h
  38. 0038specialize scaled_pair_order_terminal_power_mod_predecessor A
  39. 0039apply scaled_pair_order_terminal_power_mod_predecessor
  40. 0040exact hpn
  41. 0041exact hp
  42. 0042exact hprefix
  43. 0043exact heven
  44. 0044exact hterminal_witness_witness_left
  45. 0045exact hterminal_witness_witness_right
  46. 0046exact hpower