BT0092

factorial_succ_decompose

Stable checked-use theorem · independently kernel verified

A successor factorial is its predecessor factorial times the successor.

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.

Exact expanded PA statement

forall n sn z. sn = S n -> (exists ff_b_successor ff_c_successor. ((forall ff_i_successor_range. (exists ff_lt_successor_range_bound. ff_lt_successor_range_bound + S ff_i_successor_range = sn) -> (((exists ff_h_successor_range_decoded. ff_h_successor_range_decoded + S (1 + ff_i_successor_range) = S ((S (ff_i_successor_range)) * ff_c_successor)) /\ exists ff_q_successor_range_decoded. ff_b_successor = ff_q_successor_range_decoded * S ((S (ff_i_successor_range)) * ff_c_successor) + (1 + ff_i_successor_range)))) /\ (exists ff_u_successor_product ff_v_successor_product. ((((exists ff_h_successor_product_start. ff_h_successor_product_start + S (1) = S ((S (0)) * ff_v_successor_product)) /\ exists ff_q_successor_product_start. ff_u_successor_product = ff_q_successor_product_start * S ((S (0)) * ff_v_successor_product) + (1))) /\ ((((exists ff_h_successor_product_terminal. ff_h_successor_product_terminal + S (z) = S ((S (sn)) * ff_v_successor_product)) /\ exists ff_q_successor_product_terminal. ff_u_successor_product = ff_q_successor_product_terminal * S ((S (sn)) * ff_v_successor_product) + (z))) /\ forall ff_i_successor_product. (exists ff_lt_successor_product_bound. ff_lt_successor_product_bound + S ff_i_successor_product = sn) -> exists ff_p_successor_product ff_r_successor_product ff_s_successor_product. ((((exists ff_h_successor_product_factor. ff_h_successor_product_factor + S (ff_p_successor_product) = S ((S (ff_i_successor_product)) * ff_c_successor)) /\ exists ff_q_successor_product_factor. ff_b_successor = ff_q_successor_product_factor * S ((S (ff_i_successor_product)) * ff_c_successor) + (ff_p_successor_product))) /\ ((((exists ff_h_successor_product_partial. ff_h_successor_product_partial + S (ff_r_successor_product) = S ((S (ff_i_successor_product)) * ff_v_successor_product)) /\ exists ff_q_successor_product_partial. ff_u_successor_product = ff_q_successor_product_partial * S ((S (ff_i_successor_product)) * ff_v_successor_product) + (ff_r_successor_product))) /\ ((((exists ff_h_successor_product_successor. ff_h_successor_product_successor + S (ff_s_successor_product) = S ((S (S ff_i_successor_product)) * ff_v_successor_product)) /\ exists ff_q_successor_product_successor. ff_u_successor_product = ff_q_successor_product_successor * S ((S (S ff_i_successor_product)) * ff_v_successor_product) + (ff_s_successor_product))) /\ ff_s_successor_product = ff_r_successor_product * ff_p_successor_product)))))))) -> exists r. (exists ff_b_predecessor ff_c_predecessor. ((forall ff_i_predecessor_range. (exists ff_lt_predecessor_range_bound. ff_lt_predecessor_range_bound + S ff_i_predecessor_range = n) -> (((exists ff_h_predecessor_range_decoded. ff_h_predecessor_range_decoded + S (1 + ff_i_predecessor_range) = S ((S (ff_i_predecessor_range)) * ff_c_predecessor)) /\ exists ff_q_predecessor_range_decoded. ff_b_predecessor = ff_q_predecessor_range_decoded * S ((S (ff_i_predecessor_range)) * ff_c_predecessor) + (1 + ff_i_predecessor_range)))) /\ (exists ff_u_predecessor_product ff_v_predecessor_product. ((((exists ff_h_predecessor_product_start. ff_h_predecessor_product_start + S (1) = S ((S (0)) * ff_v_predecessor_product)) /\ exists ff_q_predecessor_product_start. ff_u_predecessor_product = ff_q_predecessor_product_start * S ((S (0)) * ff_v_predecessor_product) + (1))) /\ ((((exists ff_h_predecessor_product_terminal. ff_h_predecessor_product_terminal + S (r) = S ((S (n)) * ff_v_predecessor_product)) /\ exists ff_q_predecessor_product_terminal. ff_u_predecessor_product = ff_q_predecessor_product_terminal * S ((S (n)) * ff_v_predecessor_product) + (r))) /\ forall ff_i_predecessor_product. (exists ff_lt_predecessor_product_bound. ff_lt_predecessor_product_bound + S ff_i_predecessor_product = n) -> exists ff_p_predecessor_product ff_r_predecessor_product ff_s_predecessor_product. ((((exists ff_h_predecessor_product_factor. ff_h_predecessor_product_factor + S (ff_p_predecessor_product) = S ((S (ff_i_predecessor_product)) * ff_c_predecessor)) /\ exists ff_q_predecessor_product_factor. ff_b_predecessor = ff_q_predecessor_product_factor * S ((S (ff_i_predecessor_product)) * ff_c_predecessor) + (ff_p_predecessor_product))) /\ ((((exists ff_h_predecessor_product_partial. ff_h_predecessor_product_partial + S (ff_r_predecessor_product) = S ((S (ff_i_predecessor_product)) * ff_v_predecessor_product)) /\ exists ff_q_predecessor_product_partial. ff_u_predecessor_product = ff_q_predecessor_product_partial * S ((S (ff_i_predecessor_product)) * ff_v_predecessor_product) + (ff_r_predecessor_product))) /\ ((((exists ff_h_predecessor_product_successor. ff_h_predecessor_product_successor + S (ff_s_predecessor_product) = S ((S (S ff_i_predecessor_product)) * ff_v_predecessor_product)) /\ exists ff_q_predecessor_product_successor. ff_u_predecessor_product = ff_q_predecessor_product_successor * S ((S (S ff_i_predecessor_product)) * ff_v_predecessor_product) + (ff_s_predecessor_product))) /\ ff_s_predecessor_product = ff_r_predecessor_product * ff_p_predecessor_product)))))))) /\ z = r * S n

Structural proof guide

A successor factorial is its predecessor factorial times the successor.

Direct prerequisites: beta_product_succ_decompose, beta_range_entry_eq, le_refl, le_succ, add_succ_left, zero_add. The authored body proceeds by case analysis (7), intermediate claims (2), equality transport (5).

Proof neighborhood

Direct dependencies

BT005J beta_product_succ_decompose BT0087 beta_range_entry_eq BT000E le_refl BT0018 le_succ BT0001 add_succ_left BT0000 zero_add

Direct dependents

BT00RK factorial_nonzero BT00RP prime_factorial_valuation_succ BT00TX choose_factorial_bridge BT00VB factorial_prime_le_of_divides

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

60 script commands · 21 reading checkpoints · 2 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.

Named ingredients (6)
beta product succ decomposebeta range entry eqle reflle succadd succ leftzero add

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–5

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

  1. L1
    intro n
  2. L2
    intro sn
  3. L3
    intro z
  4. L4
    intro hsn
  5. L5
    intro hfactorial
02Calculate and transport equalitiesL6–9

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

  1. L6
    rewrite hsn at hfactorial
  2. L7
    rewrite hsn at hfactorial
  3. L8
    rewrite hsn at hfactorial
  4. L9
    rewrite hsn at hfactorial
03Separate the logical casesL10–12

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

  1. L10
    cases hfactorial
  2. L11
    cases hfactorial_witness
  3. L12
    cases hfactorial_witness_witness
04Establish hdecompL13–19

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

  1. L13
    have hdecomp : ∃ p. ∃ r. BetaAt(x,x1,n,p) ∧ (Product(x,x1,n,r) ∧ z = r · p)Definitions: BetaAtProduct
  2. L14
    specialize beta_product_succ_decompose x
  3. L15
    specialize beta_product_succ_decompose x1
  4. L16
    specialize beta_product_succ_decompose n
  5. L17
    specialize beta_product_succ_decompose z
  6. L18
    apply beta_product_succ_decompose
  7. L19
    exact hfactorial_witness_witness_right
05Separate the logical casesL20–23

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

  1. L20
    cases hdecomp
  2. L21
    cases hdecomp_witness
  3. L22
    cases hdecomp_witness_witness
  4. L23
    cases hdecomp_witness_witness_right
06Establish hpL24–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta range entry eq.

  1. L24
    have hp : x2 = 1 + n
  2. L25
    specialize beta_range_entry_eq x
  3. L26
    specialize beta_range_entry_eq x1
  4. L27
    specialize beta_range_entry_eq 1
  5. L28
    specialize beta_range_entry_eq (S n)
  6. L29
    specialize beta_range_entry_eq n
  7. L30
    specialize beta_range_entry_eq x2
  8. L31
    apply beta_range_entry_eq
  9. L32
    exact hfactorial_witness_witness_left
  10. L33
    specialize le_refl (S n)
07Use earlier factsL34–35

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

  1. L34
    exact le_refl
  2. L35
    exact hdecomp_witness_witness_left
08Construct an explicit witnessL36–36

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

  1. L36
    exists x3
09Separate the logical casesL37–37

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

  1. L37
    split
10Construct an explicit witnessL38–39

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

  1. L38
    exists x
  2. L39
    exists x1
11Separate the logical casesL40–40

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

  1. L40
    split
12Fix variables and assumptionsL41–42

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

  1. L41
    intro i
  2. L42
    intro hi
13Use earlier factsL43–49

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

  1. L43
    specialize hfactorial_witness_witness_left i
  2. L44
    apply hfactorial_witness_witness_left
  3. L45
    specialize le_succ (S i)
  4. L46
    specialize le_succ n
  5. L47
    apply le_succ
  6. L48
    exact hi
  7. L49
    exact hdecomp_witness_witness_right_left
14Calculate and transport equalitiesL50–50

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

  1. L50
    trans x3 * x2
15Use earlier factsL51–51

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

  1. L51
    exact hdecomp_witness_witness_right_right
16Calculate and transport equalitiesL52–54

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

  1. L52
    rewrite hp
  2. L53
    congr
  3. L54
    refl
17Use earlier factsL55–56

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

  1. L55
    specialize add_succ_left 0
  2. L56
    specialize add_succ_left n
18Calculate and transport equalitiesL57–57

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

  1. L57
    trans S (0 + n)
19Use earlier factsL58–58

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

  1. L58
    exact add_succ_left
20Calculate and transport equalitiesL59–59

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

  1. L59
    congr
21Use earlier factsL60–60

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

  1. L60
    apply zero_add

Library-wide reading audit

Original exact command ledger · 60 lines
  1. 0001intro n
  2. 0002intro sn
  3. 0003intro z
  4. 0004intro hsn
  5. 0005intro hfactorial
  6. 0006rewrite hsn at hfactorial
  7. 0007rewrite hsn at hfactorial
  8. 0008rewrite hsn at hfactorial
  9. 0009rewrite hsn at hfactorial
  10. 0010cases hfactorial
  11. 0011cases hfactorial_witness
  12. 0012cases hfactorial_witness_witness
  13. 0013have hdecomp : exists p r. (((exists ff_h_factorial_succ_factor. ff_h_factorial_succ_factor + S (p) = S ((S (n)) * x1)) /\ exists ff_q_factorial_succ_factor. x = ff_q_factorial_succ_factor * S ((S (n)) * x1) + (p))) /\ ((exists ff_u_factorial_succ_prefix ff_v_factorial_succ_prefix. ((((exists ff_h_factorial_succ_prefix_start. ff_h_factorial_succ_prefix_start + S (1) = S ((S (0)) * ff_v_factorial_succ_prefix)) /\ exists ff_q_factorial_succ_prefix_start. ff_u_factorial_succ_prefix = ff_q_factorial_succ_prefix_start * S ((S (0)) * ff_v_factorial_succ_prefix) + (1))) /\ ((((exists ff_h_factorial_succ_prefix_terminal. ff_h_factorial_succ_prefix_terminal + S (r) = S ((S (n)) * ff_v_factorial_succ_prefix)) /\ exists ff_q_factorial_succ_prefix_terminal. ff_u_factorial_succ_prefix = ff_q_factorial_succ_prefix_terminal * S ((S (n)) * ff_v_factorial_succ_prefix) + (r))) /\ forall ff_i_factorial_succ_prefix. (exists ff_lt_factorial_succ_prefix_bound. ff_lt_factorial_succ_prefix_bound + S ff_i_factorial_succ_prefix = n) -> exists ff_p_factorial_succ_prefix ff_r_factorial_succ_prefix ff_s_factorial_succ_prefix. ((((exists ff_h_factorial_succ_prefix_factor. ff_h_factorial_succ_prefix_factor + S (ff_p_factorial_succ_prefix) = S ((S (ff_i_factorial_succ_prefix)) * x1)) /\ exists ff_q_factorial_succ_prefix_factor. x = ff_q_factorial_succ_prefix_factor * S ((S (ff_i_factorial_succ_prefix)) * x1) + (ff_p_factorial_succ_prefix))) /\ ((((exists ff_h_factorial_succ_prefix_partial. ff_h_factorial_succ_prefix_partial + S (ff_r_factorial_succ_prefix) = S ((S (ff_i_factorial_succ_prefix)) * ff_v_factorial_succ_prefix)) /\ exists ff_q_factorial_succ_prefix_partial. ff_u_factorial_succ_prefix = ff_q_factorial_succ_prefix_partial * S ((S (ff_i_factorial_succ_prefix)) * ff_v_factorial_succ_prefix) + (ff_r_factorial_succ_prefix))) /\ ((((exists ff_h_factorial_succ_prefix_successor. ff_h_factorial_succ_prefix_successor + S (ff_s_factorial_succ_prefix) = S ((S (S ff_i_factorial_succ_prefix)) * ff_v_factorial_succ_prefix)) /\ exists ff_q_factorial_succ_prefix_successor. ff_u_factorial_succ_prefix = ff_q_factorial_succ_prefix_successor * S ((S (S ff_i_factorial_succ_prefix)) * ff_v_factorial_succ_prefix) + (ff_s_factorial_succ_prefix))) /\ ff_s_factorial_succ_prefix = ff_r_factorial_succ_prefix * ff_p_factorial_succ_prefix)))))) /\ z = r * p)
  14. 0014specialize beta_product_succ_decompose x
  15. 0015specialize beta_product_succ_decompose x1
  16. 0016specialize beta_product_succ_decompose n
  17. 0017specialize beta_product_succ_decompose z
  18. 0018apply beta_product_succ_decompose
  19. 0019exact hfactorial_witness_witness_right
  20. 0020cases hdecomp
  21. 0021cases hdecomp_witness
  22. 0022cases hdecomp_witness_witness
  23. 0023cases hdecomp_witness_witness_right
  24. 0024have hp : x2 = 1 + n
  25. 0025specialize beta_range_entry_eq x
  26. 0026specialize beta_range_entry_eq x1
  27. 0027specialize beta_range_entry_eq 1
  28. 0028specialize beta_range_entry_eq (S n)
  29. 0029specialize beta_range_entry_eq n
  30. 0030specialize beta_range_entry_eq x2
  31. 0031apply beta_range_entry_eq
  32. 0032exact hfactorial_witness_witness_left
  33. 0033specialize le_refl (S n)
  34. 0034exact le_refl
  35. 0035exact hdecomp_witness_witness_left
  36. 0036exists x3
  37. 0037split
  38. 0038exists x
  39. 0039exists x1
  40. 0040split
  41. 0041intro i
  42. 0042intro hi
  43. 0043specialize hfactorial_witness_witness_left i
  44. 0044apply hfactorial_witness_witness_left
  45. 0045specialize le_succ (S i)
  46. 0046specialize le_succ n
  47. 0047apply le_succ
  48. 0048exact hi
  49. 0049exact hdecomp_witness_witness_right_left
  50. 0050trans x3 * x2
  51. 0051exact hdecomp_witness_witness_right_right
  52. 0052rewrite hp
  53. 0053congr
  54. 0054refl
  55. 0055specialize add_succ_left 0
  56. 0056specialize add_succ_left n
  57. 0057trans S (0 + n)
  58. 0058exact add_succ_left
  59. 0059congr
  60. 0060apply zero_add