PA004A · theorem

beta_product_succ_decompose

Stable checked-use theorem · independently closed

A successor product decomposes into its prefix product and final decoded factor.

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

∀ b. ∀ c. ∀ l. ∀ n. Product(b,c,S l,n) → ∃ x. ∃ y. BetaAt(b,c,l,x) ∧ (Product(b,c,l,y) ∧ n = y · x)

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

PD0013 BetaAt PD0014 Product

3 occurrences

In local proof propositions

PD0013 BetaAt

3 occurrences

Exact expanded native-PA statement
forall b c l n. (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S S l) * v)) /\ exists q. u = q * S ((S S l) * v) + n) /\ forall i. (exists h. h + S i = S l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) -> exists p r. (((exists h. h + S p = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + p) /\ ((exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S r = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + r) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) /\ n = r * p))

Proof neighborhood

Direct theorem prerequisites

PA001A le_refl PA002O le_succ PA002F beta_at_unique

Direct theorem dependents

PA004D pow_successor_decompose PA0052 beta_product_replace_balance PA0053 beta_product_swap_last_invariant PA0065 factorial_succ_decompose PA007I beta_sign_factor_product_power PA007N beta_product_pointwise_mul_exact PA007Q beta_product_pointwise_scale_mod PA007W beta_product_reindex_fixed_last PA0081 beta_product_pointwise_coprime PA009Y beta_product_double_succ_decompose PA00BG beta_range_two_product_is_factorial_succ

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

51 script commands · 18 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.

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 (3)
le reflle succbeta at unique
01Fix variables and assumptionsL1–5

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro n
  5. L5
    intro hproduct
02Separate the logical casesL6–9

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

  1. L6
    cases hproduct
  2. L7
    cases hproduct_witness
  3. L8
    cases hproduct_witness_witness
  4. L9
    cases hproduct_witness_witness_right
03Establish hstepL10–14

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

  1. L10
    have hstep : ∃ p. ∃ r. ∃ s. BetaAt(b,c,l,p) ∧ (BetaAt(x,x1,l,r) ∧ (BetaAt(x,x1,S l,s) ∧ s = r · p))Definitions: BetaAt(b,c,l,p)BetaAt(x,x1,l,r)BetaAt(x,x1,S l,s)Original native command in the exact edition
  2. L11
    specialize hproduct_witness_witness_right_right l
  3. L12
    apply hproduct_witness_witness_right_right
  4. L13
    specialize le_refl (S l)
  5. L14
    exact le_refl
04Separate the logical casesL15–20

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

  1. L15
    cases hstep
  2. L16
    cases hstep_witness
  3. L17
    cases hstep_witness_witness
  4. L18
    cases hstep_witness_witness_witness
  5. L19
    cases hstep_witness_witness_witness_right
  6. L20
    cases hstep_witness_witness_witness_right_right
05Establish hnL21–29

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

  1. L21
    have hn : n = x4
  2. L22
    specialize beta_at_unique x
  3. L23
    specialize beta_at_unique x1
  4. L24
    specialize beta_at_unique (S l)
  5. L25
    specialize beta_at_unique n
  6. L26
    specialize beta_at_unique x4
  7. L27
    apply beta_at_unique
  8. L28
    exact hproduct_witness_witness_right_left
  9. L29
    exact hstep_witness_witness_witness_right_right_left
06Construct an explicit witnessL30–31

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

  1. L30
    exists x2
  2. L31
    exists x3
07Separate the logical casesL32–32

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

  1. L32
    split
08Use earlier factsL33–33

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

  1. L33
    exact hstep_witness_witness_witness_left
09Separate the logical casesL34–34

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

  1. L34
    split
10Construct an explicit witnessL35–36

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

  1. L35
    exists x
  2. L36
    exists x1
11Separate the logical casesL37–37

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

  1. L37
    split
12Use earlier factsL38–38

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

  1. L38
    exact hproduct_witness_witness_left
13Separate the logical casesL39–39

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

  1. L39
    split
14Use earlier factsL40–40

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

  1. L40
    exact hstep_witness_witness_witness_right_left
15Fix variables and assumptionsL41–42

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

  1. L41
    intro i
  2. L42
    intro hi
16Use earlier factsL43–48

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

  1. L43
    specialize hproduct_witness_witness_right_right i
  2. L44
    apply hproduct_witness_witness_right_right
  3. L45
    specialize le_succ (S i)
  4. L46
    specialize le_succ l
  5. L47
    apply le_succ
  6. L48
    exact hi
17Calculate and transport equalitiesL49–49

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

  1. L49
    trans x4
18Use earlier factsL50–51

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

  1. L50
    exact hn
  2. L51
    exact hstep_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro n
  5. 0005intro hproduct
  6. 0006cases hproduct
  7. 0007cases hproduct_witness
  8. 0008cases hproduct_witness_witness
  9. 0009cases hproduct_witness_witness_right
  10. 0010have hstep : ∃ p. ∃ r. ∃ s. BetaAt(b,c,l,p) ∧ (BetaAt(x,x1,l,r) ∧ (BetaAt(x,x1,S l,s) ∧ s = r · p))
    Exact native replay linehave hstep : exists p r s. (((exists h. h + S p = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + p) /\ (((exists h. h + S r = S ((S l) * x1)) /\ exists q. x = q * S ((S l) * x1) + r) /\ (((exists h. h + S s = S ((S S l) * x1)) /\ exists q. x = q * S ((S S l) * x1) + s) /\ s = r * p)))
  11. 0011specialize hproduct_witness_witness_right_right l
  12. 0012apply hproduct_witness_witness_right_right
  13. 0013specialize le_refl (S l)
  14. 0014exact le_refl
  15. 0015cases hstep
  16. 0016cases hstep_witness
  17. 0017cases hstep_witness_witness
  18. 0018cases hstep_witness_witness_witness
  19. 0019cases hstep_witness_witness_witness_right
  20. 0020cases hstep_witness_witness_witness_right_right
  21. 0021have hn : n = x4
  22. 0022specialize beta_at_unique x
  23. 0023specialize beta_at_unique x1
  24. 0024specialize beta_at_unique (S l)
  25. 0025specialize beta_at_unique n
  26. 0026specialize beta_at_unique x4
  27. 0027apply beta_at_unique
  28. 0028exact hproduct_witness_witness_right_left
  29. 0029exact hstep_witness_witness_witness_right_right_left
  30. 0030exists x2
  31. 0031exists x3
  32. 0032split
  33. 0033exact hstep_witness_witness_witness_left
  34. 0034split
  35. 0035exists x
  36. 0036exists x1
  37. 0037split
  38. 0038exact hproduct_witness_witness_left
  39. 0039split
  40. 0040exact hstep_witness_witness_witness_right_left
  41. 0041intro i
  42. 0042intro hi
  43. 0043specialize hproduct_witness_witness_right_right i
  44. 0044apply hproduct_witness_witness_right_right
  45. 0045specialize le_succ (S i)
  46. 0046specialize le_succ l
  47. 0047apply le_succ
  48. 0048exact hi
  49. 0049trans x4
  50. 0050exact hn
  51. 0051exact hstep_witness_witness_witness_right_right_right