BT00RK · Bertrand theorem

factorial_nonzero

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

A relational factorial value is never zero.

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

∀ n. ∀ F. Factorial(n,F) → ¬F = 0

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

PD0023 Factorial

1 occurrences

In local proof propositions

PD0023 Factorial

1 occurrences

Exact expanded native-PA statement
forall n F. (exists ff_b_bfv_nonzero ff_c_bfv_nonzero. ((forall ff_i_bfv_nonzero_range. (exists ff_lt_bfv_nonzero_range_bound. ff_lt_bfv_nonzero_range_bound + S ff_i_bfv_nonzero_range = n) -> (((exists ff_h_bfv_nonzero_range_decoded. ff_h_bfv_nonzero_range_decoded + S (1 + ff_i_bfv_nonzero_range) = S ((S (ff_i_bfv_nonzero_range)) * ff_c_bfv_nonzero)) /\ exists ff_q_bfv_nonzero_range_decoded. ff_b_bfv_nonzero = ff_q_bfv_nonzero_range_decoded * S ((S (ff_i_bfv_nonzero_range)) * ff_c_bfv_nonzero) + (1 + ff_i_bfv_nonzero_range)))) /\ (exists ff_u_bfv_nonzero_product ff_v_bfv_nonzero_product. ((((exists ff_h_bfv_nonzero_product_start. ff_h_bfv_nonzero_product_start + S (1) = S ((S (0)) * ff_v_bfv_nonzero_product)) /\ exists ff_q_bfv_nonzero_product_start. ff_u_bfv_nonzero_product = ff_q_bfv_nonzero_product_start * S ((S (0)) * ff_v_bfv_nonzero_product) + (1))) /\ ((((exists ff_h_bfv_nonzero_product_terminal. ff_h_bfv_nonzero_product_terminal + S (F) = S ((S (n)) * ff_v_bfv_nonzero_product)) /\ exists ff_q_bfv_nonzero_product_terminal. ff_u_bfv_nonzero_product = ff_q_bfv_nonzero_product_terminal * S ((S (n)) * ff_v_bfv_nonzero_product) + (F))) /\ forall ff_i_bfv_nonzero_product. (exists ff_lt_bfv_nonzero_product_bound. ff_lt_bfv_nonzero_product_bound + S ff_i_bfv_nonzero_product = n) -> exists ff_p_bfv_nonzero_product ff_r_bfv_nonzero_product ff_s_bfv_nonzero_product. ((((exists ff_h_bfv_nonzero_product_factor. ff_h_bfv_nonzero_product_factor + S (ff_p_bfv_nonzero_product) = S ((S (ff_i_bfv_nonzero_product)) * ff_c_bfv_nonzero)) /\ exists ff_q_bfv_nonzero_product_factor. ff_b_bfv_nonzero = ff_q_bfv_nonzero_product_factor * S ((S (ff_i_bfv_nonzero_product)) * ff_c_bfv_nonzero) + (ff_p_bfv_nonzero_product))) /\ ((((exists ff_h_bfv_nonzero_product_partial. ff_h_bfv_nonzero_product_partial + S (ff_r_bfv_nonzero_product) = S ((S (ff_i_bfv_nonzero_product)) * ff_v_bfv_nonzero_product)) /\ exists ff_q_bfv_nonzero_product_partial. ff_u_bfv_nonzero_product = ff_q_bfv_nonzero_product_partial * S ((S (ff_i_bfv_nonzero_product)) * ff_v_bfv_nonzero_product) + (ff_r_bfv_nonzero_product))) /\ ((((exists ff_h_bfv_nonzero_product_successor. ff_h_bfv_nonzero_product_successor + S (ff_s_bfv_nonzero_product) = S ((S (S ff_i_bfv_nonzero_product)) * ff_v_bfv_nonzero_product)) /\ exists ff_q_bfv_nonzero_product_successor. ff_u_bfv_nonzero_product = ff_q_bfv_nonzero_product_successor * S ((S (S ff_i_bfv_nonzero_product)) * ff_v_bfv_nonzero_product) + (ff_s_bfv_nonzero_product))) /\ ff_s_bfv_nonzero_product = ff_r_bfv_nonzero_product * ff_p_bfv_nonzero_product)))))))) -> ~(F = 0)

Proof neighborhood

Direct theorem prerequisites

BT0091 factorial_zero BT0092 factorial_succ_decompose BT000C succ_ne_zero BT0021 mul_ne_zero

Direct theorem dependents

BT00RP prime_factorial_valuation_succ BT00XM central_binom_factorial_valuation_balance

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

47 script commands · 12 reading checkpoints · 4 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)
factorial zerofactorial succ decomposesucc ne zeromul ne zero
01Fix variables and assumptionsL1–1

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

  1. L1
    intro n
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 hfactorial
03Establish hvalueL5–14

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

  1. L5
    have hvalue : F = 1
  2. L6
    specialize factorial_zero 0
  3. L7
    specialize factorial_zero F
  4. L8
    apply factorial_zero
  5. L9
    refl
  6. L10
    exact hfactorial
  7. L11
    intro hzero
  8. L12
    specialize succ_ne_zero 0
  9. L13
    apply succ_ne_zero
  10. L14
    trans F
04Calculate and transport equalitiesL15–15

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

  1. L15
    symm
05Use earlier factsL16–17

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

  1. L16
    exact hvalue
  2. L17
    exact hzero
06Fix variables and assumptionsL18–19

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

  1. L18
    intro F
  2. L19
    intro hfactorial
07Establish hdecompositionL20–26

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

  1. L20
    have hdecomposition : ∃ R. Factorial(n,R) ∧ F = R · S nDefinitions: Factorial(n,R)Original native command in the exact edition
  2. L21
    specialize factorial_succ_decompose n
  3. L22
    specialize factorial_succ_decompose (S n)
  4. L23
    specialize factorial_succ_decompose F
  5. L24
    apply factorial_succ_decompose
  6. L25
    refl
  7. L26
    exact hfactorial
08Separate the logical casesL27–28

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

  1. L27
    cases hdecomposition
  2. L28
    cases hdecomposition_witness
09Establish hpredecessorL29–34

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

  1. L29
    have hpredecessor : ~(x = 0)
  2. L30
    intro hpredecessor_zero
  3. L31
    specialize IH x
  4. L32
    apply IH
  5. L33
    exact hdecomposition_witness_left
  6. L34
    exact hpredecessor_zero
10Establish hsuccessorL35–44

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

  1. L35
    have hsuccessor : ~(S n = 0)
  2. L36
    specialize succ_ne_zero n
  3. L37
    exact succ_ne_zero
  4. L38
    intro hzero
  5. L39
    specialize mul_ne_zero x
  6. L40
    specialize mul_ne_zero (S n)
  7. L41
    apply mul_ne_zero
  8. L42
    exact hpredecessor
  9. L43
    exact hsuccessor
  10. L44
    trans F
11Calculate and transport equalitiesL45–45

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

  1. L45
    symm
12Use earlier factsL46–47

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

  1. L46
    exact hdecomposition_witness_right
  2. L47
    exact hzero

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro n
  2. 0002induction n
  3. 0003intro F
  4. 0004intro hfactorial
  5. 0005have hvalue : F = 1
  6. 0006specialize factorial_zero 0
  7. 0007specialize factorial_zero F
  8. 0008apply factorial_zero
  9. 0009refl
  10. 0010exact hfactorial
  11. 0011intro hzero
  12. 0012specialize succ_ne_zero 0
  13. 0013apply succ_ne_zero
  14. 0014trans F
  15. 0015symm
  16. 0016exact hvalue
  17. 0017exact hzero
  18. 0018intro F
  19. 0019intro hfactorial
  20. 0020have hdecomposition : ∃ R. Factorial(n,R) ∧ F = R · S n
    Exact native replay linehave hdecomposition : exists R. (exists ff_b_bfv_nonzero_predecessor ff_c_bfv_nonzero_predecessor. ((forall ff_i_bfv_nonzero_predecessor_range. (exists ff_lt_bfv_nonzero_predecessor_range_bound. ff_lt_bfv_nonzero_predecessor_range_bound + S ff_i_bfv_nonzero_predecessor_range = n) -> (((exists ff_h_bfv_nonzero_predecessor_range_decoded. ff_h_bfv_nonzero_predecessor_range_decoded + S (1 + ff_i_bfv_nonzero_predecessor_range) = S ((S (ff_i_bfv_nonzero_predecessor_range)) * ff_c_bfv_nonzero_predecessor)) /\ exists ff_q_bfv_nonzero_predecessor_range_decoded. ff_b_bfv_nonzero_predecessor = ff_q_bfv_nonzero_predecessor_range_decoded * S ((S (ff_i_bfv_nonzero_predecessor_range)) * ff_c_bfv_nonzero_predecessor) + (1 + ff_i_bfv_nonzero_predecessor_range)))) /\ (exists ff_u_bfv_nonzero_predecessor_product ff_v_bfv_nonzero_predecessor_product. ((((exists ff_h_bfv_nonzero_predecessor_product_start. ff_h_bfv_nonzero_predecessor_product_start + S (1) = S ((S (0)) * ff_v_bfv_nonzero_predecessor_product)) /\ exists ff_q_bfv_nonzero_predecessor_product_start. ff_u_bfv_nonzero_predecessor_product = ff_q_bfv_nonzero_predecessor_product_start * S ((S (0)) * ff_v_bfv_nonzero_predecessor_product) + (1))) /\ ((((exists ff_h_bfv_nonzero_predecessor_product_terminal. ff_h_bfv_nonzero_predecessor_product_terminal + S (R) = S ((S (n)) * ff_v_bfv_nonzero_predecessor_product)) /\ exists ff_q_bfv_nonzero_predecessor_product_terminal. ff_u_bfv_nonzero_predecessor_product = ff_q_bfv_nonzero_predecessor_product_terminal * S ((S (n)) * ff_v_bfv_nonzero_predecessor_product) + (R))) /\ forall ff_i_bfv_nonzero_predecessor_product. (exists ff_lt_bfv_nonzero_predecessor_product_bound. ff_lt_bfv_nonzero_predecessor_product_bound + S ff_i_bfv_nonzero_predecessor_product = n) -> exists ff_p_bfv_nonzero_predecessor_product ff_r_bfv_nonzero_predecessor_product ff_s_bfv_nonzero_predecessor_product. ((((exists ff_h_bfv_nonzero_predecessor_product_factor. ff_h_bfv_nonzero_predecessor_product_factor + S (ff_p_bfv_nonzero_predecessor_product) = S ((S (ff_i_bfv_nonzero_predecessor_product)) * ff_c_bfv_nonzero_predecessor)) /\ exists ff_q_bfv_nonzero_predecessor_product_factor. ff_b_bfv_nonzero_predecessor = ff_q_bfv_nonzero_predecessor_product_factor * S ((S (ff_i_bfv_nonzero_predecessor_product)) * ff_c_bfv_nonzero_predecessor) + (ff_p_bfv_nonzero_predecessor_product))) /\ ((((exists ff_h_bfv_nonzero_predecessor_product_partial. ff_h_bfv_nonzero_predecessor_product_partial + S (ff_r_bfv_nonzero_predecessor_product) = S ((S (ff_i_bfv_nonzero_predecessor_product)) * ff_v_bfv_nonzero_predecessor_product)) /\ exists ff_q_bfv_nonzero_predecessor_product_partial. ff_u_bfv_nonzero_predecessor_product = ff_q_bfv_nonzero_predecessor_product_partial * S ((S (ff_i_bfv_nonzero_predecessor_product)) * ff_v_bfv_nonzero_predecessor_product) + (ff_r_bfv_nonzero_predecessor_product))) /\ ((((exists ff_h_bfv_nonzero_predecessor_product_successor. ff_h_bfv_nonzero_predecessor_product_successor + S (ff_s_bfv_nonzero_predecessor_product) = S ((S (S ff_i_bfv_nonzero_predecessor_product)) * ff_v_bfv_nonzero_predecessor_product)) /\ exists ff_q_bfv_nonzero_predecessor_product_successor. ff_u_bfv_nonzero_predecessor_product = ff_q_bfv_nonzero_predecessor_product_successor * S ((S (S ff_i_bfv_nonzero_predecessor_product)) * ff_v_bfv_nonzero_predecessor_product) + (ff_s_bfv_nonzero_predecessor_product))) /\ ff_s_bfv_nonzero_predecessor_product = ff_r_bfv_nonzero_predecessor_product * ff_p_bfv_nonzero_predecessor_product)))))))) /\ F = R * S n
  21. 0021specialize factorial_succ_decompose n
  22. 0022specialize factorial_succ_decompose (S n)
  23. 0023specialize factorial_succ_decompose F
  24. 0024apply factorial_succ_decompose
  25. 0025refl
  26. 0026exact hfactorial
  27. 0027cases hdecomposition
  28. 0028cases hdecomposition_witness
  29. 0029have hpredecessor : ~(x = 0)
  30. 0030intro hpredecessor_zero
  31. 0031specialize IH x
  32. 0032apply IH
  33. 0033exact hdecomposition_witness_left
  34. 0034exact hpredecessor_zero
  35. 0035have hsuccessor : ~(S n = 0)
  36. 0036specialize succ_ne_zero n
  37. 0037exact succ_ne_zero
  38. 0038intro hzero
  39. 0039specialize mul_ne_zero x
  40. 0040specialize mul_ne_zero (S n)
  41. 0041apply mul_ne_zero
  42. 0042exact hpredecessor
  43. 0043exact hsuccessor
  44. 0044trans F
  45. 0045symm
  46. 0046exact hdecomposition_witness_right
  47. 0047exact hzero