PA00BK

scaled_pair_order_terminal_power_mod_predecessor

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

A completed terminal scaled pairing sends a^h to the predecessor p-1 modulo p.

Exact expanded PA statement

forall p a n u v b c 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)) -> (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 -> (((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)))))))) -> (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 completed terminal scaled pairing sends a^h to the predecessor p-1 modulo p.

Use the direct prerequisites beta_successor_lift_exists, scaled_pair_order_successor_lift_adjacent_targets, beta_product_exists, beta_adjacent_target_pairs_product_power, factorial_exists, scaled_pair_order_successor_lift_product_is_factorial, prime_factorial_wilson_congruence, mod_eq_symm, mod_eq_trans as previously established PA formulas.

The proof proceeds by case analysis (6), intermediate claims (12), equality transport (7).

Referenced ingredients

PA008C beta_successor_lift_exists PA009X scaled_pair_order_successor_lift_adjacent_targets PA003X beta_product_exists PA00A0 beta_adjacent_target_pairs_product_power PA0060 factorial_exists PA00A1 scaled_pair_order_successor_lift_product_is_factorial PA00BJ prime_factorial_wilson_congruence PA003L mod_eq_symm PA0024 mod_eq_trans

Proof neighborhood

Direct dependencies

PA008C beta_successor_lift_exists PA009X scaled_pair_order_successor_lift_adjacent_targets PA003X beta_product_exists PA00A0 beta_adjacent_target_pairs_product_power PA0060 factorial_exists PA00A1 scaled_pair_order_successor_lift_product_is_factorial PA00BJ prime_factorial_wilson_congruence PA003L mod_eq_symm PA0024 mod_eq_trans

Direct dependents

PA00BL scaled_inverse_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 b
  7. 0007intro c
  8. 0008intro h
  9. 0009intro A
  10. 0010intro hpn
  11. 0011intro hp
  12. 0012intro hprefix
  13. 0013intro heven
  14. 0014intro hstate
  15. 0015intro hhistory
  16. 0016intro hpower
  17. 0017cases hstate
  18. 0018cases hstate_right
  19. 0019have hlift_exists : exists f g. (forall wsl_index_enr_lift_n wsl_value_enr_lift_n. (exists wpo_gap_enr_lift_n_bound. wpo_gap_enr_lift_n_bound + S (wsl_index_enr_lift_n) = n) -> (((exists wpo_beta_height_enr_lift_n_source. wpo_beta_height_enr_lift_n_source + S (wsl_value_enr_lift_n) = S ((S (wsl_index_enr_lift_n)) * c)) /\ exists wpo_beta_quotient_enr_lift_n_source. b = wpo_beta_quotient_enr_lift_n_source * S ((S (wsl_index_enr_lift_n)) * c) + (wsl_value_enr_lift_n))) -> (((exists wpo_beta_height_enr_lift_n_target. wpo_beta_height_enr_lift_n_target + S (S wsl_value_enr_lift_n) = S ((S (wsl_index_enr_lift_n)) * g)) /\ exists wpo_beta_quotient_enr_lift_n_target. f = wpo_beta_quotient_enr_lift_n_target * S ((S (wsl_index_enr_lift_n)) * g) + (S wsl_value_enr_lift_n))))
  20. 0020specialize beta_successor_lift_exists b
  21. 0021specialize beta_successor_lift_exists c
  22. 0022specialize beta_successor_lift_exists n
  23. 0023exact beta_successor_lift_exists
  24. 0024cases hlift_exists
  25. 0025cases hlift_exists_witness
  26. 0026have hpairs : forall wpp_pair_enr_target_pairs_x wpp_left_enr_target_pairs_x wpp_right_enr_target_pairs_x. (exists wpp_gap_enr_target_pairs_x_pair_bound. wpp_gap_enr_target_pairs_x_pair_bound + S (wpp_pair_enr_target_pairs_x) = h) -> (((exists wpp_beta_height_enr_target_pairs_x_left_entry. wpp_beta_height_enr_target_pairs_x_left_entry + S (wpp_left_enr_target_pairs_x) = S ((S ((wpp_pair_enr_target_pairs_x + wpp_pair_enr_target_pairs_x))) * x1)) /\ exists wpp_beta_quotient_enr_target_pairs_x_left_entry. x = wpp_beta_quotient_enr_target_pairs_x_left_entry * S ((S ((wpp_pair_enr_target_pairs_x + wpp_pair_enr_target_pairs_x))) * x1) + (wpp_left_enr_target_pairs_x))) -> (((exists wpp_beta_height_enr_target_pairs_x_right_entry. wpp_beta_height_enr_target_pairs_x_right_entry + S (wpp_right_enr_target_pairs_x) = S ((S (S (wpp_pair_enr_target_pairs_x + wpp_pair_enr_target_pairs_x))) * x1)) /\ exists wpp_beta_quotient_enr_target_pairs_x_right_entry. x = wpp_beta_quotient_enr_target_pairs_x_right_entry * S ((S (S (wpp_pair_enr_target_pairs_x + wpp_pair_enr_target_pairs_x))) * x1) + (wpp_right_enr_target_pairs_x))) -> (exists wpp_mod_left_enr_target_pairs_x_pair_mod wpp_mod_right_enr_target_pairs_x_pair_mod. (wpp_left_enr_target_pairs_x * wpp_right_enr_target_pairs_x) + p * wpp_mod_left_enr_target_pairs_x_pair_mod = (a) + p * wpp_mod_right_enr_target_pairs_x_pair_mod)
  27. 0027specialize scaled_pair_order_successor_lift_adjacent_targets p
  28. 0028specialize scaled_pair_order_successor_lift_adjacent_targets a
  29. 0029specialize scaled_pair_order_successor_lift_adjacent_targets n
  30. 0030specialize scaled_pair_order_successor_lift_adjacent_targets u
  31. 0031specialize scaled_pair_order_successor_lift_adjacent_targets v
  32. 0032specialize scaled_pair_order_successor_lift_adjacent_targets b
  33. 0033specialize scaled_pair_order_successor_lift_adjacent_targets c
  34. 0034specialize scaled_pair_order_successor_lift_adjacent_targets x
  35. 0035specialize scaled_pair_order_successor_lift_adjacent_targets x1
  36. 0036specialize scaled_pair_order_successor_lift_adjacent_targets h
  37. 0037apply scaled_pair_order_successor_lift_adjacent_targets
  38. 0038exact heven
  39. 0039exact hprefix
  40. 0040exact hstate_right_left
  41. 0041exact hhistory
  42. 0042exact hlift_exists_witness_witness
  43. 0043have hproduct_exists : exists Q. exists ff_u_enr_terminal_product_x ff_v_enr_terminal_product_x. ((((exists ff_h_enr_terminal_product_x_start. ff_h_enr_terminal_product_x_start + S (1) = S ((S (0)) * ff_v_enr_terminal_product_x)) /\ exists ff_q_enr_terminal_product_x_start. ff_u_enr_terminal_product_x = ff_q_enr_terminal_product_x_start * S ((S (0)) * ff_v_enr_terminal_product_x) + (1))) /\ ((((exists ff_h_enr_terminal_product_x_terminal. ff_h_enr_terminal_product_x_terminal + S (Q) = S ((S (n)) * ff_v_enr_terminal_product_x)) /\ exists ff_q_enr_terminal_product_x_terminal. ff_u_enr_terminal_product_x = ff_q_enr_terminal_product_x_terminal * S ((S (n)) * ff_v_enr_terminal_product_x) + (Q))) /\ forall ff_i_enr_terminal_product_x. (exists ff_lt_enr_terminal_product_x_bound. ff_lt_enr_terminal_product_x_bound + S ff_i_enr_terminal_product_x = n) -> exists ff_p_enr_terminal_product_x ff_r_enr_terminal_product_x ff_s_enr_terminal_product_x. ((((exists ff_h_enr_terminal_product_x_factor. ff_h_enr_terminal_product_x_factor + S (ff_p_enr_terminal_product_x) = S ((S (ff_i_enr_terminal_product_x)) * x1)) /\ exists ff_q_enr_terminal_product_x_factor. x = ff_q_enr_terminal_product_x_factor * S ((S (ff_i_enr_terminal_product_x)) * x1) + (ff_p_enr_terminal_product_x))) /\ ((((exists ff_h_enr_terminal_product_x_partial. ff_h_enr_terminal_product_x_partial + S (ff_r_enr_terminal_product_x) = S ((S (ff_i_enr_terminal_product_x)) * ff_v_enr_terminal_product_x)) /\ exists ff_q_enr_terminal_product_x_partial. ff_u_enr_terminal_product_x = ff_q_enr_terminal_product_x_partial * S ((S (ff_i_enr_terminal_product_x)) * ff_v_enr_terminal_product_x) + (ff_r_enr_terminal_product_x))) /\ ((((exists ff_h_enr_terminal_product_x_successor. ff_h_enr_terminal_product_x_successor + S (ff_s_enr_terminal_product_x) = S ((S (S ff_i_enr_terminal_product_x)) * ff_v_enr_terminal_product_x)) /\ exists ff_q_enr_terminal_product_x_successor. ff_u_enr_terminal_product_x = ff_q_enr_terminal_product_x_successor * S ((S (S ff_i_enr_terminal_product_x)) * ff_v_enr_terminal_product_x) + (ff_s_enr_terminal_product_x))) /\ ff_s_enr_terminal_product_x = ff_r_enr_terminal_product_x * ff_p_enr_terminal_product_x)))))
  44. 0044specialize beta_product_exists x
  45. 0045specialize beta_product_exists x1
  46. 0046specialize beta_product_exists n
  47. 0047exact beta_product_exists
  48. 0048cases hproduct_exists
  49. 0049have hproduct_even : exists ff_u_enr_terminal_product_even ff_v_enr_terminal_product_even. ((((exists ff_h_enr_terminal_product_even_start. ff_h_enr_terminal_product_even_start + S (1) = S ((S (0)) * ff_v_enr_terminal_product_even)) /\ exists ff_q_enr_terminal_product_even_start. ff_u_enr_terminal_product_even = ff_q_enr_terminal_product_even_start * S ((S (0)) * ff_v_enr_terminal_product_even) + (1))) /\ ((((exists ff_h_enr_terminal_product_even_terminal. ff_h_enr_terminal_product_even_terminal + S (x2) = S ((S (h + h)) * ff_v_enr_terminal_product_even)) /\ exists ff_q_enr_terminal_product_even_terminal. ff_u_enr_terminal_product_even = ff_q_enr_terminal_product_even_terminal * S ((S (h + h)) * ff_v_enr_terminal_product_even) + (x2))) /\ forall ff_i_enr_terminal_product_even. (exists ff_lt_enr_terminal_product_even_bound. ff_lt_enr_terminal_product_even_bound + S ff_i_enr_terminal_product_even = h + h) -> exists ff_p_enr_terminal_product_even ff_r_enr_terminal_product_even ff_s_enr_terminal_product_even. ((((exists ff_h_enr_terminal_product_even_factor. ff_h_enr_terminal_product_even_factor + S (ff_p_enr_terminal_product_even) = S ((S (ff_i_enr_terminal_product_even)) * x1)) /\ exists ff_q_enr_terminal_product_even_factor. x = ff_q_enr_terminal_product_even_factor * S ((S (ff_i_enr_terminal_product_even)) * x1) + (ff_p_enr_terminal_product_even))) /\ ((((exists ff_h_enr_terminal_product_even_partial. ff_h_enr_terminal_product_even_partial + S (ff_r_enr_terminal_product_even) = S ((S (ff_i_enr_terminal_product_even)) * ff_v_enr_terminal_product_even)) /\ exists ff_q_enr_terminal_product_even_partial. ff_u_enr_terminal_product_even = ff_q_enr_terminal_product_even_partial * S ((S (ff_i_enr_terminal_product_even)) * ff_v_enr_terminal_product_even) + (ff_r_enr_terminal_product_even))) /\ ((((exists ff_h_enr_terminal_product_even_successor. ff_h_enr_terminal_product_even_successor + S (ff_s_enr_terminal_product_even) = S ((S (S ff_i_enr_terminal_product_even)) * ff_v_enr_terminal_product_even)) /\ exists ff_q_enr_terminal_product_even_successor. ff_u_enr_terminal_product_even = ff_q_enr_terminal_product_even_successor * S ((S (S ff_i_enr_terminal_product_even)) * ff_v_enr_terminal_product_even) + (ff_s_enr_terminal_product_even))) /\ ff_s_enr_terminal_product_even = ff_r_enr_terminal_product_even * ff_p_enr_terminal_product_even)))))
  50. 0050rewrite <- heven
  51. 0051rewrite <- heven
  52. 0052rewrite <- heven
  53. 0053exact hproduct_exists_witness
  54. 0054have hproduct_power : exists wpp_mod_left_enr_product_mod_power wpp_mod_right_enr_product_mod_power. (x2) + p * wpp_mod_left_enr_product_mod_power = (A) + p * wpp_mod_right_enr_product_mod_power
  55. 0055specialize beta_adjacent_target_pairs_product_power p
  56. 0056specialize beta_adjacent_target_pairs_product_power a
  57. 0057specialize beta_adjacent_target_pairs_product_power x
  58. 0058specialize beta_adjacent_target_pairs_product_power x1
  59. 0059specialize beta_adjacent_target_pairs_product_power h
  60. 0060specialize beta_adjacent_target_pairs_product_power x2
  61. 0061specialize beta_adjacent_target_pairs_product_power A
  62. 0062apply beta_adjacent_target_pairs_product_power
  63. 0063exact hpairs
  64. 0064exact hproduct_even
  65. 0065exact hpower
  66. 0066have hfactorial_exists : exists F. (exists ff_b_enr_terminal_factorial ff_c_enr_terminal_factorial. ((forall ff_i_enr_terminal_factorial_range. (exists ff_lt_enr_terminal_factorial_range_bound. ff_lt_enr_terminal_factorial_range_bound + S ff_i_enr_terminal_factorial_range = n) -> (((exists ff_h_enr_terminal_factorial_range_decoded. ff_h_enr_terminal_factorial_range_decoded + S (1 + ff_i_enr_terminal_factorial_range) = S ((S (ff_i_enr_terminal_factorial_range)) * ff_c_enr_terminal_factorial)) /\ exists ff_q_enr_terminal_factorial_range_decoded. ff_b_enr_terminal_factorial = ff_q_enr_terminal_factorial_range_decoded * S ((S (ff_i_enr_terminal_factorial_range)) * ff_c_enr_terminal_factorial) + (1 + ff_i_enr_terminal_factorial_range)))) /\ (exists ff_u_enr_terminal_factorial_product ff_v_enr_terminal_factorial_product. ((((exists ff_h_enr_terminal_factorial_product_start. ff_h_enr_terminal_factorial_product_start + S (1) = S ((S (0)) * ff_v_enr_terminal_factorial_product)) /\ exists ff_q_enr_terminal_factorial_product_start. ff_u_enr_terminal_factorial_product = ff_q_enr_terminal_factorial_product_start * S ((S (0)) * ff_v_enr_terminal_factorial_product) + (1))) /\ ((((exists ff_h_enr_terminal_factorial_product_terminal. ff_h_enr_terminal_factorial_product_terminal + S (F) = S ((S (n)) * ff_v_enr_terminal_factorial_product)) /\ exists ff_q_enr_terminal_factorial_product_terminal. ff_u_enr_terminal_factorial_product = ff_q_enr_terminal_factorial_product_terminal * S ((S (n)) * ff_v_enr_terminal_factorial_product) + (F))) /\ forall ff_i_enr_terminal_factorial_product. (exists ff_lt_enr_terminal_factorial_product_bound. ff_lt_enr_terminal_factorial_product_bound + S ff_i_enr_terminal_factorial_product = n) -> exists ff_p_enr_terminal_factorial_product ff_r_enr_terminal_factorial_product ff_s_enr_terminal_factorial_product. ((((exists ff_h_enr_terminal_factorial_product_factor. ff_h_enr_terminal_factorial_product_factor + S (ff_p_enr_terminal_factorial_product) = S ((S (ff_i_enr_terminal_factorial_product)) * ff_c_enr_terminal_factorial)) /\ exists ff_q_enr_terminal_factorial_product_factor. ff_b_enr_terminal_factorial = ff_q_enr_terminal_factorial_product_factor * S ((S (ff_i_enr_terminal_factorial_product)) * ff_c_enr_terminal_factorial) + (ff_p_enr_terminal_factorial_product))) /\ ((((exists ff_h_enr_terminal_factorial_product_partial. ff_h_enr_terminal_factorial_product_partial + S (ff_r_enr_terminal_factorial_product) = S ((S (ff_i_enr_terminal_factorial_product)) * ff_v_enr_terminal_factorial_product)) /\ exists ff_q_enr_terminal_factorial_product_partial. ff_u_enr_terminal_factorial_product = ff_q_enr_terminal_factorial_product_partial * S ((S (ff_i_enr_terminal_factorial_product)) * ff_v_enr_terminal_factorial_product) + (ff_r_enr_terminal_factorial_product))) /\ ((((exists ff_h_enr_terminal_factorial_product_successor. ff_h_enr_terminal_factorial_product_successor + S (ff_s_enr_terminal_factorial_product) = S ((S (S ff_i_enr_terminal_factorial_product)) * ff_v_enr_terminal_factorial_product)) /\ exists ff_q_enr_terminal_factorial_product_successor. ff_u_enr_terminal_factorial_product = ff_q_enr_terminal_factorial_product_successor * S ((S (S ff_i_enr_terminal_factorial_product)) * ff_v_enr_terminal_factorial_product) + (ff_s_enr_terminal_factorial_product))) /\ ff_s_enr_terminal_factorial_product = ff_r_enr_terminal_factorial_product * ff_p_enr_terminal_factorial_product))))))))
  67. 0067specialize factorial_exists n
  68. 0068exact factorial_exists
  69. 0069cases hfactorial_exists
  70. 0070have hbounded_n : forall fom_index_enr_generic_bounded. (exists fom_gap_enr_generic_bounded_index_bound. fom_gap_enr_generic_bounded_index_bound + S (fom_index_enr_generic_bounded) = n) -> exists fom_value_enr_generic_bounded. ((((exists fom_beta_height_enr_generic_bounded_entry. fom_beta_height_enr_generic_bounded_entry + S (fom_value_enr_generic_bounded) = S ((S (fom_index_enr_generic_bounded)) * c)) /\ exists fom_beta_quotient_enr_generic_bounded_entry. b = fom_beta_quotient_enr_generic_bounded_entry * S ((S (fom_index_enr_generic_bounded)) * c) + (fom_value_enr_generic_bounded))) /\ (exists fom_gap_enr_generic_bounded_value_bound. fom_gap_enr_generic_bounded_value_bound + S (fom_value_enr_generic_bounded) = n))
  71. 0071rewrite heven
  72. 0072exact hstate_right_left
  73. 0073have hinjective_n : forall wpo_injective_left_enr_generic_injective wpo_injective_right_enr_generic_injective wpo_injective_value_enr_generic_injective. (exists wpo_gap_enr_generic_injective_left_bound. wpo_gap_enr_generic_injective_left_bound + S (wpo_injective_left_enr_generic_injective) = n) -> (exists wpo_gap_enr_generic_injective_right_bound. wpo_gap_enr_generic_injective_right_bound + S (wpo_injective_right_enr_generic_injective) = n) -> (((exists wpo_beta_height_enr_generic_injective_left_entry. wpo_beta_height_enr_generic_injective_left_entry + S (wpo_injective_value_enr_generic_injective) = S ((S (wpo_injective_left_enr_generic_injective)) * c)) /\ exists wpo_beta_quotient_enr_generic_injective_left_entry. b = wpo_beta_quotient_enr_generic_injective_left_entry * S ((S (wpo_injective_left_enr_generic_injective)) * c) + (wpo_injective_value_enr_generic_injective))) -> (((exists wpo_beta_height_enr_generic_injective_right_entry. wpo_beta_height_enr_generic_injective_right_entry + S (wpo_injective_value_enr_generic_injective) = S ((S (wpo_injective_right_enr_generic_injective)) * c)) /\ exists wpo_beta_quotient_enr_generic_injective_right_entry. b = wpo_beta_quotient_enr_generic_injective_right_entry * S ((S (wpo_injective_right_enr_generic_injective)) * c) + (wpo_injective_value_enr_generic_injective))) -> wpo_injective_left_enr_generic_injective = wpo_injective_right_enr_generic_injective
  74. 0074rewrite heven
  75. 0075rewrite heven
  76. 0076exact hstate_right_right
  77. 0077have hQF : x2 = x3
  78. 0078specialize scaled_pair_order_successor_lift_product_is_factorial b
  79. 0079specialize scaled_pair_order_successor_lift_product_is_factorial c
  80. 0080specialize scaled_pair_order_successor_lift_product_is_factorial x
  81. 0081specialize scaled_pair_order_successor_lift_product_is_factorial x1
  82. 0082specialize scaled_pair_order_successor_lift_product_is_factorial n
  83. 0083specialize scaled_pair_order_successor_lift_product_is_factorial x2
  84. 0084specialize scaled_pair_order_successor_lift_product_is_factorial x3
  85. 0085apply scaled_pair_order_successor_lift_product_is_factorial
  86. 0086exact hbounded_n
  87. 0087exact hinjective_n
  88. 0088exact hlift_exists_witness_witness
  89. 0089exact hproduct_exists_witness
  90. 0090exact hfactorial_exists_witness
  91. 0091have hpower_product : exists wpp_mod_left_enr_power_mod_product wpp_mod_right_enr_power_mod_product. (A) + p * wpp_mod_left_enr_power_mod_product = (x2) + p * wpp_mod_right_enr_power_mod_product
  92. 0092specialize mod_eq_symm p
  93. 0093specialize mod_eq_symm x2
  94. 0094specialize mod_eq_symm A
  95. 0095apply mod_eq_symm
  96. 0096exact hproduct_power
  97. 0097have hpower_factorial : exists wpp_mod_left_enr_power_mod_factorial wpp_mod_right_enr_power_mod_factorial. (A) + p * wpp_mod_left_enr_power_mod_factorial = (x3) + p * wpp_mod_right_enr_power_mod_factorial
  98. 0098rewrite <- hQF
  99. 0099exact hpower_product
  100. 0100have hfactorial_mod : exists wpp_mod_left_enr_factorial_mod_predecessor wpp_mod_right_enr_factorial_mod_predecessor. (x3) + p * wpp_mod_left_enr_factorial_mod_predecessor = (n) + p * wpp_mod_right_enr_factorial_mod_predecessor
  101. 0101specialize prime_factorial_wilson_congruence p
  102. 0102specialize prime_factorial_wilson_congruence n
  103. 0103specialize prime_factorial_wilson_congruence x3
  104. 0104apply prime_factorial_wilson_congruence
  105. 0105exact hpn
  106. 0106exact hp
  107. 0107exact hfactorial_exists_witness
  108. 0108specialize mod_eq_trans p
  109. 0109specialize mod_eq_trans A
  110. 0110specialize mod_eq_trans x3
  111. 0111specialize mod_eq_trans n
  112. 0112apply mod_eq_trans
  113. 0113exact hpower_factorial
  114. 0114exact hfactorial_mod