BT00VB · Bertrand theorem

factorial_prime_le_of_divides

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Every prime divisor of n! is at most n.

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. Prime(p) → Factorial(n,F) → Dvd(p,F) → Le(p,n)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0003 Dvd PD0004 Prime PD0023 Factorial

4 occurrences

In local proof propositions

PD0001 Le PD0003 Dvd PD0023 Factorial

4 occurrences

Exact expanded native-PA statement
forall p n F. ((~(p = 1) /\ forall bpr_left_bfplod_prime bpr_right_bfplod_prime. p = bpr_left_bfplod_prime * bpr_right_bfplod_prime -> bpr_left_bfplod_prime = 1 \/ bpr_right_bfplod_prime = 1)) -> (exists ff_b_bfplod_source ff_c_bfplod_source. ((forall ff_i_bfplod_source_range. (exists ff_lt_bfplod_source_range_bound. ff_lt_bfplod_source_range_bound + S ff_i_bfplod_source_range = n) -> (((exists ff_h_bfplod_source_range_decoded. ff_h_bfplod_source_range_decoded + S (1 + ff_i_bfplod_source_range) = S ((S (ff_i_bfplod_source_range)) * ff_c_bfplod_source)) /\ exists ff_q_bfplod_source_range_decoded. ff_b_bfplod_source = ff_q_bfplod_source_range_decoded * S ((S (ff_i_bfplod_source_range)) * ff_c_bfplod_source) + (1 + ff_i_bfplod_source_range)))) /\ (exists ff_u_bfplod_source_product ff_v_bfplod_source_product. ((((exists ff_h_bfplod_source_product_start. ff_h_bfplod_source_product_start + S (1) = S ((S (0)) * ff_v_bfplod_source_product)) /\ exists ff_q_bfplod_source_product_start. ff_u_bfplod_source_product = ff_q_bfplod_source_product_start * S ((S (0)) * ff_v_bfplod_source_product) + (1))) /\ ((((exists ff_h_bfplod_source_product_terminal. ff_h_bfplod_source_product_terminal + S (F) = S ((S (n)) * ff_v_bfplod_source_product)) /\ exists ff_q_bfplod_source_product_terminal. ff_u_bfplod_source_product = ff_q_bfplod_source_product_terminal * S ((S (n)) * ff_v_bfplod_source_product) + (F))) /\ forall ff_i_bfplod_source_product. (exists ff_lt_bfplod_source_product_bound. ff_lt_bfplod_source_product_bound + S ff_i_bfplod_source_product = n) -> exists ff_p_bfplod_source_product ff_r_bfplod_source_product ff_s_bfplod_source_product. ((((exists ff_h_bfplod_source_product_factor. ff_h_bfplod_source_product_factor + S (ff_p_bfplod_source_product) = S ((S (ff_i_bfplod_source_product)) * ff_c_bfplod_source)) /\ exists ff_q_bfplod_source_product_factor. ff_b_bfplod_source = ff_q_bfplod_source_product_factor * S ((S (ff_i_bfplod_source_product)) * ff_c_bfplod_source) + (ff_p_bfplod_source_product))) /\ ((((exists ff_h_bfplod_source_product_partial. ff_h_bfplod_source_product_partial + S (ff_r_bfplod_source_product) = S ((S (ff_i_bfplod_source_product)) * ff_v_bfplod_source_product)) /\ exists ff_q_bfplod_source_product_partial. ff_u_bfplod_source_product = ff_q_bfplod_source_product_partial * S ((S (ff_i_bfplod_source_product)) * ff_v_bfplod_source_product) + (ff_r_bfplod_source_product))) /\ ((((exists ff_h_bfplod_source_product_successor. ff_h_bfplod_source_product_successor + S (ff_s_bfplod_source_product) = S ((S (S ff_i_bfplod_source_product)) * ff_v_bfplod_source_product)) /\ exists ff_q_bfplod_source_product_successor. ff_u_bfplod_source_product = ff_q_bfplod_source_product_successor * S ((S (S ff_i_bfplod_source_product)) * ff_v_bfplod_source_product) + (ff_s_bfplod_source_product))) /\ ff_s_bfplod_source_product = ff_r_bfplod_source_product * ff_p_bfplod_source_product)))))))) -> (exists bpr_quotient_bfplod_divides. F = (p) * bpr_quotient_bfplod_divides) -> (exists bpr_le_gap_bfplod_result. bpr_le_gap_bfplod_result + (p) = (n))

Proof neighborhood

Direct theorem prerequisites

BT002E divisor_one BT0018 le_succ BT003N euclid_prime_dvd_product BT002D divisor_le_nonzero BT000C succ_ne_zero BT0091 factorial_zero BT0092 factorial_succ_decompose

Direct theorem dependents

BT00VC choose_prime_divides_between BT00VX central_binom_prime_divisor_le_double

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

64 script commands · 22 reading checkpoints · 5 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)
divisor onele succeuclid prime dvd productdivisor le nonzerosucc ne zerofactorial zerofactorial succ decompose
01Fix variables and assumptionsL1–1

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

  1. L1
    intro p
02Induction on nL2–4

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction n
  2. L3
    intro F
  3. L4
    intro hp
03Separate the logical casesL5–5

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

  1. L5
    cases hp
04Fix variables and assumptionsL6–7

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

  1. L6
    intro hfactorial
  2. L7
    intro hdivides
05Establish hF_oneL8–14

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

  1. L8
    have hF_one : F = 1
  2. L9
    specialize factorial_zero 0
  3. L10
    specialize factorial_zero F
  4. L11
    apply factorial_zero
  5. L12
    refl
  6. L13
    exact hfactorial
  7. L14
    rewrite hF_one at hdivides
06Establish hp_oneL15–18

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

  1. L15
    have hp_one : p = 1
  2. L16
    specialize divisor_one p
  3. L17
    apply divisor_one
  4. L18
    exact hdivides
07Separate the logical casesL19–19

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

  1. L19
    exfalso
08Use earlier factsL20–21

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

  1. L20
    apply hp_left
  2. L21
    exact hp_one
09Fix variables and assumptionsL22–23

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

  1. L22
    intro F
  2. L23
    intro hp
10Separate the logical casesL24–24

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

  1. L24
    cases hp
11Fix variables and assumptionsL25–26

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

  1. L25
    intro hfactorial
  2. L26
    intro hdivides
12Establish hdecompositionL27–33

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

  1. L27
    have hdecomposition : ∃ r. Factorial(n,r) ∧ F = r · S nDefinitions: Factorial(n,r)Original native command in the exact edition
  2. L28
    specialize factorial_succ_decompose n
  3. L29
    specialize factorial_succ_decompose (S n)
  4. L30
    specialize factorial_succ_decompose F
  5. L31
    apply factorial_succ_decompose
  6. L32
    refl
  7. L33
    exact hfactorial
13Separate the logical casesL34–35

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

  1. L34
    cases hdecomposition
  2. L35
    cases hdecomposition_witness
14Calculate and transport equalitiesL36–36

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L36
    rewrite hdecomposition_witness_right at hdivides
15Establish hsplitL37–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclid prime dvd product.

  1. L37
    have hsplit : Dvd(p,x) ∨ Dvd(p,S n)Definitions: Dvd(p,x)Dvd(p,S n)Original native command in the exact edition
  2. L38
    specialize euclid_prime_dvd_product p
  3. L39
    specialize euclid_prime_dvd_product x
  4. L40
    specialize euclid_prime_dvd_product (S n)
  5. L41
    apply euclid_prime_dvd_product
16Separate the logical casesL42–42

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

  1. L42
    split
17Use earlier factsL43–45

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

  1. L43
    exact hp_left
  2. L44
    exact hp_right
  3. L45
    exact hdivides
18Separate the logical casesL46–46

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

  1. L46
    cases hsplit
19Establish hpreviousL47–49

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

  1. L47
    have hprevious : Le(p,n)Definitions: Le(p,n)Original native command in the exact edition
  2. L48
    specialize IH x
  3. L49
    apply IH
20Separate the logical casesL50–50

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

  1. L50
    split
21Use earlier factsL51–60

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

  1. L51
    exact hp_left
  2. L52
    exact hp_right
  3. L53
    exact hdecomposition_witness_left
  4. L54
    exact hsplit_left
  5. L55
    specialize le_succ p
  6. L56
    specialize le_succ n
  7. L57
    apply le_succ
  8. L58
    exact hprevious
  9. L59
    specialize divisor_le_nonzero p
  10. L60
    specialize divisor_le_nonzero (S n)
22Use earlier factsL61–64

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

  1. L61
    apply divisor_le_nonzero
  2. L62
    specialize succ_ne_zero n
  3. L63
    exact succ_ne_zero
  4. L64
    exact hsplit_right

Library-wide reading audit

Original defined command ledger · 64 lines
  1. 0001intro p
  2. 0002induction n
  3. 0003intro F
  4. 0004intro hp
  5. 0005cases hp
  6. 0006intro hfactorial
  7. 0007intro hdivides
  8. 0008have hF_one : F = 1
  9. 0009specialize factorial_zero 0
  10. 0010specialize factorial_zero F
  11. 0011apply factorial_zero
  12. 0012refl
  13. 0013exact hfactorial
  14. 0014rewrite hF_one at hdivides
  15. 0015have hp_one : p = 1
  16. 0016specialize divisor_one p
  17. 0017apply divisor_one
  18. 0018exact hdivides
  19. 0019exfalso
  20. 0020apply hp_left
  21. 0021exact hp_one
  22. 0022intro F
  23. 0023intro hp
  24. 0024cases hp
  25. 0025intro hfactorial
  26. 0026intro hdivides
  27. 0027have hdecomposition : ∃ r. Factorial(n,r) ∧ F = r · S n
    Exact native replay linehave hdecomposition : exists r. (exists ff_b_bfplod_previous ff_c_bfplod_previous. ((forall ff_i_bfplod_previous_range. (exists ff_lt_bfplod_previous_range_bound. ff_lt_bfplod_previous_range_bound + S ff_i_bfplod_previous_range = n) -> (((exists ff_h_bfplod_previous_range_decoded. ff_h_bfplod_previous_range_decoded + S (1 + ff_i_bfplod_previous_range) = S ((S (ff_i_bfplod_previous_range)) * ff_c_bfplod_previous)) /\ exists ff_q_bfplod_previous_range_decoded. ff_b_bfplod_previous = ff_q_bfplod_previous_range_decoded * S ((S (ff_i_bfplod_previous_range)) * ff_c_bfplod_previous) + (1 + ff_i_bfplod_previous_range)))) /\ (exists ff_u_bfplod_previous_product ff_v_bfplod_previous_product. ((((exists ff_h_bfplod_previous_product_start. ff_h_bfplod_previous_product_start + S (1) = S ((S (0)) * ff_v_bfplod_previous_product)) /\ exists ff_q_bfplod_previous_product_start. ff_u_bfplod_previous_product = ff_q_bfplod_previous_product_start * S ((S (0)) * ff_v_bfplod_previous_product) + (1))) /\ ((((exists ff_h_bfplod_previous_product_terminal. ff_h_bfplod_previous_product_terminal + S (r) = S ((S (n)) * ff_v_bfplod_previous_product)) /\ exists ff_q_bfplod_previous_product_terminal. ff_u_bfplod_previous_product = ff_q_bfplod_previous_product_terminal * S ((S (n)) * ff_v_bfplod_previous_product) + (r))) /\ forall ff_i_bfplod_previous_product. (exists ff_lt_bfplod_previous_product_bound. ff_lt_bfplod_previous_product_bound + S ff_i_bfplod_previous_product = n) -> exists ff_p_bfplod_previous_product ff_r_bfplod_previous_product ff_s_bfplod_previous_product. ((((exists ff_h_bfplod_previous_product_factor. ff_h_bfplod_previous_product_factor + S (ff_p_bfplod_previous_product) = S ((S (ff_i_bfplod_previous_product)) * ff_c_bfplod_previous)) /\ exists ff_q_bfplod_previous_product_factor. ff_b_bfplod_previous = ff_q_bfplod_previous_product_factor * S ((S (ff_i_bfplod_previous_product)) * ff_c_bfplod_previous) + (ff_p_bfplod_previous_product))) /\ ((((exists ff_h_bfplod_previous_product_partial. ff_h_bfplod_previous_product_partial + S (ff_r_bfplod_previous_product) = S ((S (ff_i_bfplod_previous_product)) * ff_v_bfplod_previous_product)) /\ exists ff_q_bfplod_previous_product_partial. ff_u_bfplod_previous_product = ff_q_bfplod_previous_product_partial * S ((S (ff_i_bfplod_previous_product)) * ff_v_bfplod_previous_product) + (ff_r_bfplod_previous_product))) /\ ((((exists ff_h_bfplod_previous_product_successor. ff_h_bfplod_previous_product_successor + S (ff_s_bfplod_previous_product) = S ((S (S ff_i_bfplod_previous_product)) * ff_v_bfplod_previous_product)) /\ exists ff_q_bfplod_previous_product_successor. ff_u_bfplod_previous_product = ff_q_bfplod_previous_product_successor * S ((S (S ff_i_bfplod_previous_product)) * ff_v_bfplod_previous_product) + (ff_s_bfplod_previous_product))) /\ ff_s_bfplod_previous_product = ff_r_bfplod_previous_product * ff_p_bfplod_previous_product)))))))) /\ F = r * S n
  28. 0028specialize factorial_succ_decompose n
  29. 0029specialize factorial_succ_decompose (S n)
  30. 0030specialize factorial_succ_decompose F
  31. 0031apply factorial_succ_decompose
  32. 0032refl
  33. 0033exact hfactorial
  34. 0034cases hdecomposition
  35. 0035cases hdecomposition_witness
  36. 0036rewrite hdecomposition_witness_right at hdivides
  37. 0037have hsplit : Dvd(p,x) ∨ Dvd(p,S n)
    Exact native replay linehave hsplit : (exists bpr_quotient_bfplod_split_left. x = (p) * bpr_quotient_bfplod_split_left) \/ (exists bpr_quotient_bfplod_split_right. S n = (p) * bpr_quotient_bfplod_split_right)
  38. 0038specialize euclid_prime_dvd_product p
  39. 0039specialize euclid_prime_dvd_product x
  40. 0040specialize euclid_prime_dvd_product (S n)
  41. 0041apply euclid_prime_dvd_product
  42. 0042split
  43. 0043exact hp_left
  44. 0044exact hp_right
  45. 0045exact hdivides
  46. 0046cases hsplit
  47. 0047have hprevious : Le(p,n)
    Exact native replay linehave hprevious : exists g. g + p = n
  48. 0048specialize IH x
  49. 0049apply IH
  50. 0050split
  51. 0051exact hp_left
  52. 0052exact hp_right
  53. 0053exact hdecomposition_witness_left
  54. 0054exact hsplit_left
  55. 0055specialize le_succ p
  56. 0056specialize le_succ n
  57. 0057apply le_succ
  58. 0058exact hprevious
  59. 0059specialize divisor_le_nonzero p
  60. 0060specialize divisor_le_nonzero (S n)
  61. 0061apply divisor_le_nonzero
  62. 0062specialize succ_ne_zero n
  63. 0063exact succ_ne_zero
  64. 0064exact hsplit_right