BT00VA · Bertrand theorem

factorial_prime_divides_of_le

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

Every prime at most n divides the relational factorial 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) → Le(p,n) → Factorial(n,F) → Dvd(p,F)

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

PD0003 Dvd PD0013 BetaAt

2 occurrences

Exact expanded native-PA statement
forall p n F. ((~(p = 1) /\ forall bpr_left_bfpdol_prime bpr_right_bfpdol_prime. p = bpr_left_bfpdol_prime * bpr_right_bfpdol_prime -> bpr_left_bfpdol_prime = 1 \/ bpr_right_bfpdol_prime = 1)) -> (exists bpr_le_gap_bfpdol_bound. bpr_le_gap_bfpdol_bound + (p) = (n)) -> (exists ff_b_bfpdol_source ff_c_bfpdol_source. ((forall ff_i_bfpdol_source_range. (exists ff_lt_bfpdol_source_range_bound. ff_lt_bfpdol_source_range_bound + S ff_i_bfpdol_source_range = n) -> (((exists ff_h_bfpdol_source_range_decoded. ff_h_bfpdol_source_range_decoded + S (1 + ff_i_bfpdol_source_range) = S ((S (ff_i_bfpdol_source_range)) * ff_c_bfpdol_source)) /\ exists ff_q_bfpdol_source_range_decoded. ff_b_bfpdol_source = ff_q_bfpdol_source_range_decoded * S ((S (ff_i_bfpdol_source_range)) * ff_c_bfpdol_source) + (1 + ff_i_bfpdol_source_range)))) /\ (exists ff_u_bfpdol_source_product ff_v_bfpdol_source_product. ((((exists ff_h_bfpdol_source_product_start. ff_h_bfpdol_source_product_start + S (1) = S ((S (0)) * ff_v_bfpdol_source_product)) /\ exists ff_q_bfpdol_source_product_start. ff_u_bfpdol_source_product = ff_q_bfpdol_source_product_start * S ((S (0)) * ff_v_bfpdol_source_product) + (1))) /\ ((((exists ff_h_bfpdol_source_product_terminal. ff_h_bfpdol_source_product_terminal + S (F) = S ((S (n)) * ff_v_bfpdol_source_product)) /\ exists ff_q_bfpdol_source_product_terminal. ff_u_bfpdol_source_product = ff_q_bfpdol_source_product_terminal * S ((S (n)) * ff_v_bfpdol_source_product) + (F))) /\ forall ff_i_bfpdol_source_product. (exists ff_lt_bfpdol_source_product_bound. ff_lt_bfpdol_source_product_bound + S ff_i_bfpdol_source_product = n) -> exists ff_p_bfpdol_source_product ff_r_bfpdol_source_product ff_s_bfpdol_source_product. ((((exists ff_h_bfpdol_source_product_factor. ff_h_bfpdol_source_product_factor + S (ff_p_bfpdol_source_product) = S ((S (ff_i_bfpdol_source_product)) * ff_c_bfpdol_source)) /\ exists ff_q_bfpdol_source_product_factor. ff_b_bfpdol_source = ff_q_bfpdol_source_product_factor * S ((S (ff_i_bfpdol_source_product)) * ff_c_bfpdol_source) + (ff_p_bfpdol_source_product))) /\ ((((exists ff_h_bfpdol_source_product_partial. ff_h_bfpdol_source_product_partial + S (ff_r_bfpdol_source_product) = S ((S (ff_i_bfpdol_source_product)) * ff_v_bfpdol_source_product)) /\ exists ff_q_bfpdol_source_product_partial. ff_u_bfpdol_source_product = ff_q_bfpdol_source_product_partial * S ((S (ff_i_bfpdol_source_product)) * ff_v_bfpdol_source_product) + (ff_r_bfpdol_source_product))) /\ ((((exists ff_h_bfpdol_source_product_successor. ff_h_bfpdol_source_product_successor + S (ff_s_bfpdol_source_product) = S ((S (S ff_i_bfpdol_source_product)) * ff_v_bfpdol_source_product)) /\ exists ff_q_bfpdol_source_product_successor. ff_u_bfpdol_source_product = ff_q_bfpdol_source_product_successor * S ((S (S ff_i_bfpdol_source_product)) * ff_v_bfpdol_source_product) + (ff_s_bfpdol_source_product))) /\ ff_s_bfpdol_source_product = ff_r_bfpdol_source_product * ff_p_bfpdol_source_product)))))))) -> (exists bpr_quotient_bfpdol_result. F = (p) * bpr_quotient_bfpdol_result)

Proof neighborhood

Direct theorem prerequisites

BT00AW prime_is_succ_succ BT0069 beta_factor_divides_product BT0001 add_succ_left BT0000 zero_add

Direct theorem dependents

BT00VC choose_prime_divides_between

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

44 script commands · 19 reading checkpoints · 3 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 (4)
prime is succ succbeta factor divides productadd succ leftzero add
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 hp
  5. L5
    intro hle
  6. L6
    intro hfactorial
02Establish hshapeL7–9

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

  1. L7
    have hshape : exists k. p = S (S k)
  2. L8
    apply prime_is_succ_succ
  3. L9
    exact hp
03Separate the logical casesL10–10

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

  1. L10
    cases hshape
04Calculate and transport equalitiesL11–11

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

  1. L11
    rewrite hshape_witness at hle
05Separate the logical casesL12–14

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

  1. L12
    cases hfactorial
  2. L13
    cases hfactorial_witness
  3. L14
    cases hfactorial_witness_witness
06Establish hentryL15–17

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

  1. L15
    have hentry : BetaAt(x1,x2,S x,1 + S x)Definitions: BetaAt(x1,x2,S x,1 + S x)Original native command in the exact edition
  2. L16
    apply hfactorial_witness_witness_left
  3. L17
    exact hle
07Establish hrawL18–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta factor divides product.

  1. L18
    have hraw : Dvd(1 + S x,F)Definitions: Dvd(1 + S x,F)Original native command in the exact edition
  2. L19
    specialize beta_factor_divides_product x1
  3. L20
    specialize beta_factor_divides_product x2
  4. L21
    specialize beta_factor_divides_product n
  5. L22
    specialize beta_factor_divides_product F
  6. L23
    specialize beta_factor_divides_product (S x)
  7. L24
    specialize beta_factor_divides_product (1 + S x)
  8. L25
    apply beta_factor_divides_product
  9. L26
    exact hle
  10. L27
    exact hentry
08Use earlier factsL28–28

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

  1. L28
    exact hfactorial_witness_witness_right
09Separate the logical casesL29–29

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

  1. L29
    cases hraw
10Construct an explicit witnessL30–30

Supply the displayed value, then prove that it has the required property.

  1. L30
    exists x3
11Calculate and transport equalitiesL31–32

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

  1. L31
    rewrite hshape_witness
  2. L32
    trans (1 + S x) * x3
12Use earlier factsL33–33

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

  1. L33
    exact hraw_witness
13Calculate and transport equalitiesL34–35

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

  1. L34
    congr
  2. L35
    trans S (1 + x)
14Use earlier factsL36–36

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

  1. L36
    apply PA4
15Calculate and transport equalitiesL37–38

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

  1. L37
    congr
  2. L38
    trans S (0 + x)
16Use earlier factsL39–41

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

  1. L39
    specialize add_succ_left 0
  2. L40
    specialize add_succ_left x
  3. L41
    apply add_succ_left
17Calculate and transport equalitiesL42–42

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

  1. L42
    congr
18Use earlier factsL43–43

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

  1. L43
    apply zero_add
19Calculate and transport equalitiesL44–44

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

  1. L44
    refl

Library-wide reading audit

Original defined command ledger · 44 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro F
  4. 0004intro hp
  5. 0005intro hle
  6. 0006intro hfactorial
  7. 0007have hshape : exists k. p = S (S k)
  8. 0008apply prime_is_succ_succ
  9. 0009exact hp
  10. 0010cases hshape
  11. 0011rewrite hshape_witness at hle
  12. 0012cases hfactorial
  13. 0013cases hfactorial_witness
  14. 0014cases hfactorial_witness_witness
  15. 0015have hentry : BetaAt(x1,x2,S x,1 + S x)
    Exact native replay linehave hentry : ((exists bpr_height_bfpdol_entry. bpr_height_bfpdol_entry + S (1 + S x) = S ((S (S x)) * x2)) /\ exists bpr_quotient_bfpdol_entry. x1 = bpr_quotient_bfpdol_entry * S ((S (S x)) * x2) + (1 + S x))
  16. 0016apply hfactorial_witness_witness_left
  17. 0017exact hle
  18. 0018have hraw : Dvd(1 + S x,F)
    Exact native replay linehave hraw : exists q. F = (1 + S x) * q
  19. 0019specialize beta_factor_divides_product x1
  20. 0020specialize beta_factor_divides_product x2
  21. 0021specialize beta_factor_divides_product n
  22. 0022specialize beta_factor_divides_product F
  23. 0023specialize beta_factor_divides_product (S x)
  24. 0024specialize beta_factor_divides_product (1 + S x)
  25. 0025apply beta_factor_divides_product
  26. 0026exact hle
  27. 0027exact hentry
  28. 0028exact hfactorial_witness_witness_right
  29. 0029cases hraw
  30. 0030exists x3
  31. 0031rewrite hshape_witness
  32. 0032trans (1 + S x) * x3
  33. 0033exact hraw_witness
  34. 0034congr
  35. 0035trans S (1 + x)
  36. 0036apply PA4
  37. 0037congr
  38. 0038trans S (0 + x)
  39. 0039specialize add_succ_left 0
  40. 0040specialize add_succ_left x
  41. 0041apply add_succ_left
  42. 0042congr
  43. 0043apply zero_add
  44. 0044refl