AF0009

factor_permutation_cancel_last

Cancel an actual final prime factor, retaining the nonzero predecessor product and all actual prime prefix entries.

Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable

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.

The original division, gcd, cancellation, and factor-existence foundations are exposed through checked wrappers. Unordered uniqueness adds an actual bounded, injective, surjective index map matching repeated prime occurrences. The empty factor list represents one, not zero.

Exact theorem in conservative defined notation

∀ n. ∀ p. ∀ r. ∀ b. ∀ c. ∀ l. PrimeFactorList(n,b,c,S l) → BetaAt(b,c,l,p) → n = r · p → PrimeFactorList(r,b,c,l)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

PrimeFactorList(n,b,c,l) · 2BetaAt(b,c,i,x) · 2Product(b,c,l,z) · 1

Actual proof prerequisites

beta_product_succ_decompose · checked external prerequisitebeta_at_unique · checked external prerequisitefactor_permutation_all_prime_entryprime_nonzero · checked external prerequisitemul_right_cancel_nonzero · checked external prerequisiteall_prime_succ_elim_prefix · checked external prerequisitele_refl · checked external prerequisitemul_zero_left · checked external prerequisite
Original expanded first-order statement 
forall n p r b c l. ((~(n = 0) /\ ((exists ff_u_fsat_cancel_full_product ff_v_fsat_cancel_full_product. ((((exists ff_h_fsat_cancel_full_product_start. ff_h_fsat_cancel_full_product_start + S (1) = S ((S (0)) * ff_v_fsat_cancel_full_product)) /\ exists ff_q_fsat_cancel_full_product_start. ff_u_fsat_cancel_full_product = ff_q_fsat_cancel_full_product_start * S ((S (0)) * ff_v_fsat_cancel_full_product) + (1))) /\ ((((exists ff_h_fsat_cancel_full_product_terminal. ff_h_fsat_cancel_full_product_terminal + S (n) = S ((S (S l)) * ff_v_fsat_cancel_full_product)) /\ exists ff_q_fsat_cancel_full_product_terminal. ff_u_fsat_cancel_full_product = ff_q_fsat_cancel_full_product_terminal * S ((S (S l)) * ff_v_fsat_cancel_full_product) + (n))) /\ forall ff_i_fsat_cancel_full_product. (exists ff_lt_fsat_cancel_full_product_bound. ff_lt_fsat_cancel_full_product_bound + S ff_i_fsat_cancel_full_product = S l) -> exists ff_p_fsat_cancel_full_product ff_r_fsat_cancel_full_product ff_s_fsat_cancel_full_product. ((((exists ff_h_fsat_cancel_full_product_factor. ff_h_fsat_cancel_full_product_factor + S (ff_p_fsat_cancel_full_product) = S ((S (ff_i_fsat_cancel_full_product)) * c)) /\ exists ff_q_fsat_cancel_full_product_factor. b = ff_q_fsat_cancel_full_product_factor * S ((S (ff_i_fsat_cancel_full_product)) * c) + (ff_p_fsat_cancel_full_product))) /\ ((((exists ff_h_fsat_cancel_full_product_partial. ff_h_fsat_cancel_full_product_partial + S (ff_r_fsat_cancel_full_product) = S ((S (ff_i_fsat_cancel_full_product)) * ff_v_fsat_cancel_full_product)) /\ exists ff_q_fsat_cancel_full_product_partial. ff_u_fsat_cancel_full_product = ff_q_fsat_cancel_full_product_partial * S ((S (ff_i_fsat_cancel_full_product)) * ff_v_fsat_cancel_full_product) + (ff_r_fsat_cancel_full_product))) /\ ((((exists ff_h_fsat_cancel_full_product_successor. ff_h_fsat_cancel_full_product_successor + S (ff_s_fsat_cancel_full_product) = S ((S (S ff_i_fsat_cancel_full_product)) * ff_v_fsat_cancel_full_product)) /\ exists ff_q_fsat_cancel_full_product_successor. ff_u_fsat_cancel_full_product = ff_q_fsat_cancel_full_product_successor * S ((S (S ff_i_fsat_cancel_full_product)) * ff_v_fsat_cancel_full_product) + (ff_s_fsat_cancel_full_product))) /\ ff_s_fsat_cancel_full_product = ff_r_fsat_cancel_full_product * ff_p_fsat_cancel_full_product)))))) /\ (forall ftsf_index_fsat_cancel_full_primes. (exists ftsf_gap_fsat_cancel_full_primes_bound. ftsf_gap_fsat_cancel_full_primes_bound + S ftsf_index_fsat_cancel_full_primes = (S l)) -> exists ftsf_factor_fsat_cancel_full_primes. ((((exists ff_h_ftsf_fsat_cancel_full_primes_entry. ff_h_ftsf_fsat_cancel_full_primes_entry + S (ftsf_factor_fsat_cancel_full_primes) = S ((S (ftsf_index_fsat_cancel_full_primes)) * c)) /\ exists ff_q_ftsf_fsat_cancel_full_primes_entry. b = ff_q_ftsf_fsat_cancel_full_primes_entry * S ((S (ftsf_index_fsat_cancel_full_primes)) * c) + (ftsf_factor_fsat_cancel_full_primes))) /\ ((~(ftsf_factor_fsat_cancel_full_primes = 1) /\ forall frm_prime_left_ftsf_fsat_cancel_full_primes_prime frm_prime_right_ftsf_fsat_cancel_full_primes_prime. ftsf_factor_fsat_cancel_full_primes = frm_prime_left_ftsf_fsat_cancel_full_primes_prime * frm_prime_right_ftsf_fsat_cancel_full_primes_prime -> frm_prime_left_ftsf_fsat_cancel_full_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_cancel_full_primes_prime = 1))))))) -> (((exists ff_h_pfp_cancel_last. ff_h_pfp_cancel_last + S (p) = S ((S (l)) * c)) /\ exists ff_q_pfp_cancel_last. b = ff_q_pfp_cancel_last * S ((S (l)) * c) + (p))) -> n = r * p -> ((~(r = 0) /\ ((exists ff_u_fsat_cancel_prefix_product ff_v_fsat_cancel_prefix_product. ((((exists ff_h_fsat_cancel_prefix_product_start. ff_h_fsat_cancel_prefix_product_start + S (1) = S ((S (0)) * ff_v_fsat_cancel_prefix_product)) /\ exists ff_q_fsat_cancel_prefix_product_start. ff_u_fsat_cancel_prefix_product = ff_q_fsat_cancel_prefix_product_start * S ((S (0)) * ff_v_fsat_cancel_prefix_product) + (1))) /\ ((((exists ff_h_fsat_cancel_prefix_product_terminal. ff_h_fsat_cancel_prefix_product_terminal + S (r) = S ((S (l)) * ff_v_fsat_cancel_prefix_product)) /\ exists ff_q_fsat_cancel_prefix_product_terminal. ff_u_fsat_cancel_prefix_product = ff_q_fsat_cancel_prefix_product_terminal * S ((S (l)) * ff_v_fsat_cancel_prefix_product) + (r))) /\ forall ff_i_fsat_cancel_prefix_product. (exists ff_lt_fsat_cancel_prefix_product_bound. ff_lt_fsat_cancel_prefix_product_bound + S ff_i_fsat_cancel_prefix_product = l) -> exists ff_p_fsat_cancel_prefix_product ff_r_fsat_cancel_prefix_product ff_s_fsat_cancel_prefix_product. ((((exists ff_h_fsat_cancel_prefix_product_factor. ff_h_fsat_cancel_prefix_product_factor + S (ff_p_fsat_cancel_prefix_product) = S ((S (ff_i_fsat_cancel_prefix_product)) * c)) /\ exists ff_q_fsat_cancel_prefix_product_factor. b = ff_q_fsat_cancel_prefix_product_factor * S ((S (ff_i_fsat_cancel_prefix_product)) * c) + (ff_p_fsat_cancel_prefix_product))) /\ ((((exists ff_h_fsat_cancel_prefix_product_partial. ff_h_fsat_cancel_prefix_product_partial + S (ff_r_fsat_cancel_prefix_product) = S ((S (ff_i_fsat_cancel_prefix_product)) * ff_v_fsat_cancel_prefix_product)) /\ exists ff_q_fsat_cancel_prefix_product_partial. ff_u_fsat_cancel_prefix_product = ff_q_fsat_cancel_prefix_product_partial * S ((S (ff_i_fsat_cancel_prefix_product)) * ff_v_fsat_cancel_prefix_product) + (ff_r_fsat_cancel_prefix_product))) /\ ((((exists ff_h_fsat_cancel_prefix_product_successor. ff_h_fsat_cancel_prefix_product_successor + S (ff_s_fsat_cancel_prefix_product) = S ((S (S ff_i_fsat_cancel_prefix_product)) * ff_v_fsat_cancel_prefix_product)) /\ exists ff_q_fsat_cancel_prefix_product_successor. ff_u_fsat_cancel_prefix_product = ff_q_fsat_cancel_prefix_product_successor * S ((S (S ff_i_fsat_cancel_prefix_product)) * ff_v_fsat_cancel_prefix_product) + (ff_s_fsat_cancel_prefix_product))) /\ ff_s_fsat_cancel_prefix_product = ff_r_fsat_cancel_prefix_product * ff_p_fsat_cancel_prefix_product)))))) /\ (forall ftsf_index_fsat_cancel_prefix_primes. (exists ftsf_gap_fsat_cancel_prefix_primes_bound. ftsf_gap_fsat_cancel_prefix_primes_bound + S ftsf_index_fsat_cancel_prefix_primes = (l)) -> exists ftsf_factor_fsat_cancel_prefix_primes. ((((exists ff_h_ftsf_fsat_cancel_prefix_primes_entry. ff_h_ftsf_fsat_cancel_prefix_primes_entry + S (ftsf_factor_fsat_cancel_prefix_primes) = S ((S (ftsf_index_fsat_cancel_prefix_primes)) * c)) /\ exists ff_q_ftsf_fsat_cancel_prefix_primes_entry. b = ff_q_ftsf_fsat_cancel_prefix_primes_entry * S ((S (ftsf_index_fsat_cancel_prefix_primes)) * c) + (ftsf_factor_fsat_cancel_prefix_primes))) /\ ((~(ftsf_factor_fsat_cancel_prefix_primes = 1) /\ forall frm_prime_left_ftsf_fsat_cancel_prefix_primes_prime frm_prime_right_ftsf_fsat_cancel_prefix_primes_prime. ftsf_factor_fsat_cancel_prefix_primes = frm_prime_left_ftsf_fsat_cancel_prefix_primes_prime * frm_prime_right_ftsf_fsat_cancel_prefix_primes_prime -> frm_prime_left_ftsf_fsat_cancel_prefix_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_cancel_prefix_primes_prime = 1)))))))

Complete tactic proof in conservative notation

All 73 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

73 script commands · 18 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 (1)
factor permutation all prime entry
01Fix variables and assumptionsL1–9

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

  1. L1
    intro n
  2. L2
    intro p
  3. L3
    intro r
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro l
  7. L7
    intro hf
  8. L8
    intro hlast
  9. L9
    intro heq
02Separate the logical casesL10–11

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

  1. L10
    cases hf
  2. L11
    cases hf_right
03Establish hdL12–18

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

  1. L12
    have hd : ∃ q. ∃ R. BetaAt(b,c,l,q) ∧ (Product(b,c,l,R) ∧ n = R · q)Definitions: BetaAt(b,c,l,q)Product(b,c,l,R)Original native command in the exact edition
  2. L13
    specialize beta_product_succ_decompose (b)
  3. L14
    specialize beta_product_succ_decompose (c)
  4. L15
    specialize beta_product_succ_decompose (l)
  5. L16
    specialize beta_product_succ_decompose (n)
  6. L17
    apply beta_product_succ_decompose
  7. L18
    exact hf_right_left
04Separate the logical casesL19–22

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

  1. L19
    cases hd
  2. L20
    cases hd_witness
  3. L21
    cases hd_witness_witness
  4. L22
    cases hd_witness_witness_right
05Establish hfactorL23–32

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

  1. L23
    have hfactor : x = p
  2. L24
    specialize beta_at_unique (b)
  3. L25
    specialize beta_at_unique (c)
  4. L26
    specialize beta_at_unique (l)
  5. L27
    specialize beta_at_unique (x)
  6. L28
    specialize beta_at_unique (p)
  7. L29
    apply beta_at_unique
  8. L30
    exact hd_witness_witness_left
  9. L31
    exact hlast
  10. L32
    rewrite hfactor at hd_witness_witness_right_right
06Establish hpzeroL33–42

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

  1. L33
    have hpzero : ~(p = 0)
  2. L34
    intro hzero
  3. L35
    specialize prime_nonzero (p)
  4. L36
    apply prime_nonzero
  5. L37
    specialize factor_permutation_all_prime_entry (b)
  6. L38
    specialize factor_permutation_all_prime_entry (c)
  7. L39
    specialize factor_permutation_all_prime_entry (S l)
  8. L40
    specialize factor_permutation_all_prime_entry (l)
  9. L41
    specialize factor_permutation_all_prime_entry (p)
  10. L42
    apply factor_permutation_all_prime_entry
07Use earlier factsL43–47

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

  1. L43
    exact hf_right_right
  2. L44
    specialize le_refl (S l)
  3. L45
    apply le_refl
  4. L46
    exact hlast
  5. L47
    exact hzero
08Establish hquotientL48–57

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

  1. L48
    have hquotient : x1 = r
  2. L49
    specialize mul_right_cancel_nonzero (x1)
  3. L50
    specialize mul_right_cancel_nonzero (r)
  4. L51
    specialize mul_right_cancel_nonzero (p)
  5. L52
    apply mul_right_cancel_nonzero
  6. L53
    exact hpzero
  7. L54
    trans n
  8. L55
    symm
  9. L56
    exact hd_witness_witness_right_right
  10. L57
    exact heq
09Separate the logical casesL58–58

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

  1. L58
    split
10Fix variables and assumptionsL59–59

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

  1. L59
    intro hrzero
11Use earlier factsL60–60

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

  1. L60
    apply hf_left
12Calculate and transport equalitiesL61–61

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

  1. L61
    trans r * p
13Use earlier factsL62–62

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

  1. L62
    exact heq
14Calculate and transport equalitiesL63–63

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

  1. L63
    rewrite hrzero
15Use earlier factsL64–64

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

  1. L64
    apply mul_zero_left
16Separate the logical casesL65–65

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

  1. L65
    split
17Calculate and transport equalitiesL66–67

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

  1. L66
    rewrite hquotient at hd_witness_witness_right_left
  2. L67
    rewrite hquotient at hd_witness_witness_right_left
18Use earlier factsL68–73

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

  1. L68
    exact hd_witness_witness_right_left
  2. L69
    specialize all_prime_succ_elim_prefix (b)
  3. L70
    specialize all_prime_succ_elim_prefix (c)
  4. L71
    specialize all_prime_succ_elim_prefix (l)
  5. L72
    apply all_prime_succ_elim_prefix
  6. L73
    exact hf_right_right

Library-wide reading audit

Original defined command ledger · 73 lines
  1. 0001intro n
  2. 0002intro p
  3. 0003intro r
  4. 0004intro b
  5. 0005intro c
  6. 0006intro l
  7. 0007intro hf
  8. 0008intro hlast
  9. 0009intro heq
  10. 0010cases hf
  11. 0011cases hf_right
  12. 0012have hd : ∃ q. ∃ R. BetaAt(b,c,l,q) ∧ (Product(b,c,l,R) ∧ n = R · q)
  13. 0013specialize beta_product_succ_decompose (b)
  14. 0014specialize beta_product_succ_decompose (c)
  15. 0015specialize beta_product_succ_decompose (l)
  16. 0016specialize beta_product_succ_decompose (n)
  17. 0017apply beta_product_succ_decompose
  18. 0018exact hf_right_left
  19. 0019cases hd
  20. 0020cases hd_witness
  21. 0021cases hd_witness_witness
  22. 0022cases hd_witness_witness_right
  23. 0023have hfactor : x = p
  24. 0024specialize beta_at_unique (b)
  25. 0025specialize beta_at_unique (c)
  26. 0026specialize beta_at_unique (l)
  27. 0027specialize beta_at_unique (x)
  28. 0028specialize beta_at_unique (p)
  29. 0029apply beta_at_unique
  30. 0030exact hd_witness_witness_left
  31. 0031exact hlast
  32. 0032rewrite hfactor at hd_witness_witness_right_right
  33. 0033have hpzero : ~(p = 0)
  34. 0034intro hzero
  35. 0035specialize prime_nonzero (p)
  36. 0036apply prime_nonzero
  37. 0037specialize factor_permutation_all_prime_entry (b)
  38. 0038specialize factor_permutation_all_prime_entry (c)
  39. 0039specialize factor_permutation_all_prime_entry (S l)
  40. 0040specialize factor_permutation_all_prime_entry (l)
  41. 0041specialize factor_permutation_all_prime_entry (p)
  42. 0042apply factor_permutation_all_prime_entry
  43. 0043exact hf_right_right
  44. 0044specialize le_refl (S l)
  45. 0045apply le_refl
  46. 0046exact hlast
  47. 0047exact hzero
  48. 0048have hquotient : x1 = r
  49. 0049specialize mul_right_cancel_nonzero (x1)
  50. 0050specialize mul_right_cancel_nonzero (r)
  51. 0051specialize mul_right_cancel_nonzero (p)
  52. 0052apply mul_right_cancel_nonzero
  53. 0053exact hpzero
  54. 0054trans n
  55. 0055symm
  56. 0056exact hd_witness_witness_right_right
  57. 0057exact heq
  58. 0058split
  59. 0059intro hrzero
  60. 0060apply hf_left
  61. 0061trans r * p
  62. 0062exact heq
  63. 0063rewrite hrzero
  64. 0064apply mul_zero_left
  65. 0065split
  66. 0066rewrite hquotient at hd_witness_witness_right_left
  67. 0067rewrite hquotient at hd_witness_witness_right_left
  68. 0068exact hd_witness_witness_right_left
  69. 0069specialize all_prime_succ_elim_prefix (b)
  70. 0070specialize all_prime_succ_elim_prefix (c)
  71. 0071specialize all_prime_succ_elim_prefix (l)
  72. 0072apply all_prime_succ_elim_prefix
  73. 0073exact hf_right_right