PA00BJ · theorem

prime_factorial_wilson_congruence

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ p. ∀ n. ∀ F. p = S n → Prime(p) → Factorial(n,F) → ModEq(p,F,n)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0004 Prime PD0008 ModEq PD0023 Factorial

3 occurrences

In local proof propositions

PD0008 ModEq PD0014 Product PD0018 Range

3 occurrences

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

Proof neighborhood

Direct theorem prerequisites

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 theorem dependents

PA00BK scaled_pair_order_terminal_power_mod_predecessor

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

77 script commands · 12 reading checkpoints · 7 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (7)
prime two or terminal odd shapesucc injectivefactorial one valuemod eq reflprime terminal range two product mod one existsbeta range two product restore lastmod one product restore predecessor
01Fix variables and assumptionsL1–6

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro F
  4. L4
    intro hpn
  5. L5
    intro hp
  6. L6
    intro hfactorial
02Establish hshapeL7–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime two or terminal odd shape.

  1. L7
    have hshape : p = 2 \/ exists m. p = S (S (S (m + m)))
  2. L8
    specialize prime_two_or_terminal_odd_shape p
  3. L9
    apply prime_two_or_terminal_odd_shape
  4. L10
    exact hp
03Separate the logical casesL11–11

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L11
    cases hshape
04Establish hnL12–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply succ injective.

  1. L12
    have hn : n = 1
  2. L13
    specialize succ_injective n
  3. L14
    specialize succ_injective 1
  4. L15
    apply succ_injective
  5. L16
    trans p
  6. L17
    symm
  7. L18
    exact hpn
  8. L19
    trans 2
  9. L20
    exact hshape_left
  10. L21
    refl
05Establish hfoneL22–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factorial one value.

  1. L22
    have hfone : F = 1
  2. L23
    specialize factorial_one_value n
  3. L24
    specialize factorial_one_value F
  4. L25
    apply factorial_one_value
  5. L26
    exact hn
  6. L27
    exact hfactorial
06Establish hfnL28–36

Establish this local claim before using it. It is not an additional assumption.

  1. L28
    have hfn : F = n
  2. L29
    trans 1
  3. L30
    exact hfone
  4. L31
    symm
  5. L32
    exact hn
  6. L33
    rewrite hfn
  7. L34
    specialize mod_eq_refl p
  8. L35
    specialize mod_eq_refl n
  9. L36
    exact mod_eq_refl
07Separate the logical casesL37–37

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L37
    cases hshape_right
08Establish hnterminalL38–45

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply succ injective.

  1. L38
    have hnterminal : n = S (S (x + x))
  2. L39
    specialize succ_injective n
  3. L40
    specialize succ_injective (S (S (x + x)))
  4. L41
    apply succ_injective
  5. L42
    trans p
  6. L43
    symm
  7. L44
    exact hpn
  8. L45
    exact hshape_right_witness
09Establish hterminal_productL46–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime terminal range two product mod one exists.

  1. L46
    have hterminal_product : ∃ z. ∃ d. ∃ P. Range(z,d,2,x + x) ∧ (Product(z,d,x + x,P) ∧ ModEq(p,P,1))Definitions: Range(z,d,2,x + x)Product(z,d,x + x,P)ModEq(p,P,1)Original native command in the exact edition
  2. L47
    specialize prime_terminal_range_two_product_mod_one_exists p
  3. L48
    specialize prime_terminal_range_two_product_mod_one_exists n
  4. L49
    specialize prime_terminal_range_two_product_mod_one_exists x
  5. L50
    apply prime_terminal_range_two_product_mod_one_exists
  6. L51
    exact hpn
  7. L52
    exact hp
  8. L53
    exact hnterminal
10Separate the logical casesL54–58

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L54
    cases hterminal_product
  2. L55
    cases hterminal_product_witness
  3. L56
    cases hterminal_product_witness_witness
  4. L57
    cases hterminal_product_witness_witness_witness
  5. L58
    cases hterminal_product_witness_witness_witness_right
11Establish hrestoredL59–68

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta range two product restore last.

  1. L59
    have hrestored : F = x3 * n
  2. L60
    specialize beta_range_two_product_restore_last x1
  3. L61
    specialize beta_range_two_product_restore_last x2
  4. L62
    specialize beta_range_two_product_restore_last (x + x)
  5. L63
    specialize beta_range_two_product_restore_last x3
  6. L64
    specialize beta_range_two_product_restore_last n
  7. L65
    specialize beta_range_two_product_restore_last F
  8. L66
    apply beta_range_two_product_restore_last
  9. L67
    exact hnterminal
  10. L68
    exact hterminal_product_witness_witness_witness_left
12Use earlier factsL69–77

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L69
    exact hterminal_product_witness_witness_witness_right_left
  2. L70
    exact hfactorial
  3. L71
    specialize mod_one_product_restore_predecessor p
  4. L72
    specialize mod_one_product_restore_predecessor x3
  5. L73
    specialize mod_one_product_restore_predecessor n
  6. L74
    specialize mod_one_product_restore_predecessor F
  7. L75
    apply mod_one_product_restore_predecessor
  8. L76
    exact hrestored
  9. L77
    exact hterminal_product_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 77 lines
  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 : ∃ z. ∃ d. ∃ P. Range(z,d,2,x + x) ∧ (Product(z,d,x + x,P) ∧ ModEq(p,P,1))
    Exact native replay linehave 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