PA00BJ

prime_factorial_wilson_congruence

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

Wilson's factorial congruence for every prime, with p=2 handled before terminal pairing.

Exact expanded PA statement

forall p n F. p = S n -> ((~(p = 1) /\ forall wip_prime_left_wer_shape_prime wip_prime_right_wer_shape_prime. p = wip_prime_left_wer_shape_prime * wip_prime_right_wer_shape_prime -> wip_prime_left_wer_shape_prime = 1 \/ wip_prime_right_wer_shape_prime = 1)) -> (exists ff_b_wer_final_factorial ff_c_wer_final_factorial. ((forall ff_i_wer_final_factorial_range. (exists ff_lt_wer_final_factorial_range_bound. ff_lt_wer_final_factorial_range_bound + S ff_i_wer_final_factorial_range = n) -> (((exists ff_h_wer_final_factorial_range_decoded. ff_h_wer_final_factorial_range_decoded + S (1 + ff_i_wer_final_factorial_range) = S ((S (ff_i_wer_final_factorial_range)) * ff_c_wer_final_factorial)) /\ exists ff_q_wer_final_factorial_range_decoded. ff_b_wer_final_factorial = ff_q_wer_final_factorial_range_decoded * S ((S (ff_i_wer_final_factorial_range)) * ff_c_wer_final_factorial) + (1 + ff_i_wer_final_factorial_range)))) /\ (exists ff_u_wer_final_factorial_product ff_v_wer_final_factorial_product. ((((exists ff_h_wer_final_factorial_product_start. ff_h_wer_final_factorial_product_start + S (1) = S ((S (0)) * ff_v_wer_final_factorial_product)) /\ exists ff_q_wer_final_factorial_product_start. ff_u_wer_final_factorial_product = ff_q_wer_final_factorial_product_start * S ((S (0)) * ff_v_wer_final_factorial_product) + (1))) /\ ((((exists ff_h_wer_final_factorial_product_terminal. ff_h_wer_final_factorial_product_terminal + S (F) = S ((S (n)) * ff_v_wer_final_factorial_product)) /\ exists ff_q_wer_final_factorial_product_terminal. ff_u_wer_final_factorial_product = ff_q_wer_final_factorial_product_terminal * S ((S (n)) * ff_v_wer_final_factorial_product) + (F))) /\ forall ff_i_wer_final_factorial_product. (exists ff_lt_wer_final_factorial_product_bound. ff_lt_wer_final_factorial_product_bound + S ff_i_wer_final_factorial_product = n) -> exists ff_p_wer_final_factorial_product ff_r_wer_final_factorial_product ff_s_wer_final_factorial_product. ((((exists ff_h_wer_final_factorial_product_factor. ff_h_wer_final_factorial_product_factor + S (ff_p_wer_final_factorial_product) = S ((S (ff_i_wer_final_factorial_product)) * ff_c_wer_final_factorial)) /\ exists ff_q_wer_final_factorial_product_factor. ff_b_wer_final_factorial = ff_q_wer_final_factorial_product_factor * S ((S (ff_i_wer_final_factorial_product)) * ff_c_wer_final_factorial) + (ff_p_wer_final_factorial_product))) /\ ((((exists ff_h_wer_final_factorial_product_partial. ff_h_wer_final_factorial_product_partial + S (ff_r_wer_final_factorial_product) = S ((S (ff_i_wer_final_factorial_product)) * ff_v_wer_final_factorial_product)) /\ exists ff_q_wer_final_factorial_product_partial. ff_u_wer_final_factorial_product = ff_q_wer_final_factorial_product_partial * S ((S (ff_i_wer_final_factorial_product)) * ff_v_wer_final_factorial_product) + (ff_r_wer_final_factorial_product))) /\ ((((exists ff_h_wer_final_factorial_product_successor. ff_h_wer_final_factorial_product_successor + S (ff_s_wer_final_factorial_product) = S ((S (S ff_i_wer_final_factorial_product)) * ff_v_wer_final_factorial_product)) /\ exists ff_q_wer_final_factorial_product_successor. ff_u_wer_final_factorial_product = ff_q_wer_final_factorial_product_successor * S ((S (S ff_i_wer_final_factorial_product)) * ff_v_wer_final_factorial_product) + (ff_s_wer_final_factorial_product))) /\ ff_s_wer_final_factorial_product = ff_r_wer_final_factorial_product * ff_p_wer_final_factorial_product)))))))) -> (exists wpp_mod_left_wer_final_mod wpp_mod_right_wer_final_mod. (F) + p * wpp_mod_left_wer_final_mod = (n) + p * wpp_mod_right_wer_final_mod)

Structural proof guide

Generated structural guide

Wilson's factorial congruence for every prime, with p=2 handled before terminal pairing.

Use the direct prerequisites prime_two_or_terminal_odd_shape, succ_injective, factorial_one_value, mod_eq_refl, prime_terminal_range_two_product_mod_one_exists, beta_range_two_product_restore_last, mod_one_product_restore_predecessor as previously established PA formulas.

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

Referenced ingredients

PA00A2 prime_two_or_terminal_odd_shape PA003V succ_injective PA00A3 factorial_one_value PA0023 mod_eq_refl PA00BF prime_terminal_range_two_product_mod_one_exists PA00BH beta_range_two_product_restore_last PA00BI mod_one_product_restore_predecessor

Proof neighborhood

Direct dependencies

PA00A2 prime_two_or_terminal_odd_shape PA003V succ_injective PA00A3 factorial_one_value PA0023 mod_eq_refl PA00BF prime_terminal_range_two_product_mod_one_exists PA00BH beta_range_two_product_restore_last PA00BI mod_one_product_restore_predecessor

Direct dependents

PA00BK scaled_pair_order_terminal_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 n
  3. 0003intro F
  4. 0004intro hpn
  5. 0005intro hp
  6. 0006intro hfactorial
  7. 0007have hshape : p = 2 \/ exists m. p = S (S (S (m + m)))
  8. 0008specialize prime_two_or_terminal_odd_shape p
  9. 0009apply prime_two_or_terminal_odd_shape
  10. 0010exact hp
  11. 0011cases hshape
  12. 0012have hn : n = 1
  13. 0013specialize succ_injective n
  14. 0014specialize succ_injective 1
  15. 0015apply succ_injective
  16. 0016trans p
  17. 0017symm
  18. 0018exact hpn
  19. 0019trans 2
  20. 0020exact hshape_left
  21. 0021refl
  22. 0022have hfone : F = 1
  23. 0023specialize factorial_one_value n
  24. 0024specialize factorial_one_value F
  25. 0025apply factorial_one_value
  26. 0026exact hn
  27. 0027exact hfactorial
  28. 0028have hfn : F = n
  29. 0029trans 1
  30. 0030exact hfone
  31. 0031symm
  32. 0032exact hn
  33. 0033rewrite hfn
  34. 0034specialize mod_eq_refl p
  35. 0035specialize mod_eq_refl n
  36. 0036exact mod_eq_refl
  37. 0037cases hshape_right
  38. 0038have hnterminal : n = S (S (x + x))
  39. 0039specialize succ_injective n
  40. 0040specialize succ_injective (S (S (x + x)))
  41. 0041apply succ_injective
  42. 0042trans p
  43. 0043symm
  44. 0044exact hpn
  45. 0045exact hshape_right_witness
  46. 0046have hterminal_product : exists z d P. ((forall wtp_range_index_wer_final_terminal_range. (exists wtp_range_gap_wer_final_terminal_range. wtp_range_gap_wer_final_terminal_range + S wtp_range_index_wer_final_terminal_range = x + x) -> (((exists ff_h_wer_final_terminal_range_decoded. ff_h_wer_final_terminal_range_decoded + S (2 + wtp_range_index_wer_final_terminal_range) = S ((S (wtp_range_index_wer_final_terminal_range)) * d)) /\ exists ff_q_wer_final_terminal_range_decoded. z = ff_q_wer_final_terminal_range_decoded * S ((S (wtp_range_index_wer_final_terminal_range)) * d) + (2 + wtp_range_index_wer_final_terminal_range)))) /\ (((exists ff_u_wer_final_terminal_product ff_v_wer_final_terminal_product. ((((exists ff_h_wer_final_terminal_product_start. ff_h_wer_final_terminal_product_start + S (1) = S ((S (0)) * ff_v_wer_final_terminal_product)) /\ exists ff_q_wer_final_terminal_product_start. ff_u_wer_final_terminal_product = ff_q_wer_final_terminal_product_start * S ((S (0)) * ff_v_wer_final_terminal_product) + (1))) /\ ((((exists ff_h_wer_final_terminal_product_terminal. ff_h_wer_final_terminal_product_terminal + S (P) = S ((S (x + x)) * ff_v_wer_final_terminal_product)) /\ exists ff_q_wer_final_terminal_product_terminal. ff_u_wer_final_terminal_product = ff_q_wer_final_terminal_product_terminal * S ((S (x + x)) * ff_v_wer_final_terminal_product) + (P))) /\ forall ff_i_wer_final_terminal_product. (exists ff_lt_wer_final_terminal_product_bound. ff_lt_wer_final_terminal_product_bound + S ff_i_wer_final_terminal_product = x + x) -> exists ff_p_wer_final_terminal_product ff_r_wer_final_terminal_product ff_s_wer_final_terminal_product. ((((exists ff_h_wer_final_terminal_product_factor. ff_h_wer_final_terminal_product_factor + S (ff_p_wer_final_terminal_product) = S ((S (ff_i_wer_final_terminal_product)) * d)) /\ exists ff_q_wer_final_terminal_product_factor. z = ff_q_wer_final_terminal_product_factor * S ((S (ff_i_wer_final_terminal_product)) * d) + (ff_p_wer_final_terminal_product))) /\ ((((exists ff_h_wer_final_terminal_product_partial. ff_h_wer_final_terminal_product_partial + S (ff_r_wer_final_terminal_product) = S ((S (ff_i_wer_final_terminal_product)) * ff_v_wer_final_terminal_product)) /\ exists ff_q_wer_final_terminal_product_partial. ff_u_wer_final_terminal_product = ff_q_wer_final_terminal_product_partial * S ((S (ff_i_wer_final_terminal_product)) * ff_v_wer_final_terminal_product) + (ff_r_wer_final_terminal_product))) /\ ((((exists ff_h_wer_final_terminal_product_successor. ff_h_wer_final_terminal_product_successor + S (ff_s_wer_final_terminal_product) = S ((S (S ff_i_wer_final_terminal_product)) * ff_v_wer_final_terminal_product)) /\ exists ff_q_wer_final_terminal_product_successor. ff_u_wer_final_terminal_product = ff_q_wer_final_terminal_product_successor * S ((S (S ff_i_wer_final_terminal_product)) * ff_v_wer_final_terminal_product) + (ff_s_wer_final_terminal_product))) /\ ff_s_wer_final_terminal_product = ff_r_wer_final_terminal_product * ff_p_wer_final_terminal_product)))))) /\ (exists wpp_mod_left_wer_final_terminal_mod wpp_mod_right_wer_final_terminal_mod. (P) + p * wpp_mod_left_wer_final_terminal_mod = (1) + p * wpp_mod_right_wer_final_terminal_mod))))
  47. 0047specialize prime_terminal_range_two_product_mod_one_exists p
  48. 0048specialize prime_terminal_range_two_product_mod_one_exists n
  49. 0049specialize prime_terminal_range_two_product_mod_one_exists x
  50. 0050apply prime_terminal_range_two_product_mod_one_exists
  51. 0051exact hpn
  52. 0052exact hp
  53. 0053exact hnterminal
  54. 0054cases hterminal_product
  55. 0055cases hterminal_product_witness
  56. 0056cases hterminal_product_witness_witness
  57. 0057cases hterminal_product_witness_witness_witness
  58. 0058cases hterminal_product_witness_witness_witness_right
  59. 0059have hrestored : F = x3 * n
  60. 0060specialize beta_range_two_product_restore_last x1
  61. 0061specialize beta_range_two_product_restore_last x2
  62. 0062specialize beta_range_two_product_restore_last (x + x)
  63. 0063specialize beta_range_two_product_restore_last x3
  64. 0064specialize beta_range_two_product_restore_last n
  65. 0065specialize beta_range_two_product_restore_last F
  66. 0066apply beta_range_two_product_restore_last
  67. 0067exact hnterminal
  68. 0068exact hterminal_product_witness_witness_witness_left
  69. 0069exact hterminal_product_witness_witness_witness_right_left
  70. 0070exact hfactorial
  71. 0071specialize mod_one_product_restore_predecessor p
  72. 0072specialize mod_one_product_restore_predecessor x3
  73. 0073specialize mod_one_product_restore_predecessor n
  74. 0074specialize mod_one_product_restore_predecessor F
  75. 0075apply mod_one_product_restore_predecessor
  76. 0076exact hrestored
  77. 0077exact hterminal_product_witness_witness_witness_right_right