AF0009

factor_permutation_cancel_last

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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 first-order arithmetic 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)))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 8 declared prerequisites and contains 73 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_product_succ_decompose Stable theorem; checked-use authorized beta_at_unique Stable theorem; checked-use authorized AF0007 factor_permutation_all_prime_entry prime_nonzero Stable theorem; checked-use authorized mul_right_cancel_nonzero Stable theorem; checked-use authorized all_prime_succ_elim_prefix Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized mul_zero_left Stable theorem; checked-use authorized

Direct dependents

AF000A factor_permutation_successor_decompose AF0019 prime_factor_lists_matching_by_length

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (1)
factor permutation all prime entry

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–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: BetaAtProduct
  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 exact 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 : exists q R. ((((exists ff_h_pfp_cancel_decoded. ff_h_pfp_cancel_decoded + S (q) = S ((S (l)) * c)) /\ exists ff_q_pfp_cancel_decoded. b = ff_q_pfp_cancel_decoded * S ((S (l)) * c) + (q))) /\ (((exists ff_u_fsat_cancel_product ff_v_fsat_cancel_product. ((((exists ff_h_fsat_cancel_product_start. ff_h_fsat_cancel_product_start + S (1) = S ((S (0)) * ff_v_fsat_cancel_product)) /\ exists ff_q_fsat_cancel_product_start. ff_u_fsat_cancel_product = ff_q_fsat_cancel_product_start * S ((S (0)) * ff_v_fsat_cancel_product) + (1))) /\ ((((exists ff_h_fsat_cancel_product_terminal. ff_h_fsat_cancel_product_terminal + S (R) = S ((S (l)) * ff_v_fsat_cancel_product)) /\ exists ff_q_fsat_cancel_product_terminal. ff_u_fsat_cancel_product = ff_q_fsat_cancel_product_terminal * S ((S (l)) * ff_v_fsat_cancel_product) + (R))) /\ forall ff_i_fsat_cancel_product. (exists ff_lt_fsat_cancel_product_bound. ff_lt_fsat_cancel_product_bound + S ff_i_fsat_cancel_product = l) -> exists ff_p_fsat_cancel_product ff_r_fsat_cancel_product ff_s_fsat_cancel_product. ((((exists ff_h_fsat_cancel_product_factor. ff_h_fsat_cancel_product_factor + S (ff_p_fsat_cancel_product) = S ((S (ff_i_fsat_cancel_product)) * c)) /\ exists ff_q_fsat_cancel_product_factor. b = ff_q_fsat_cancel_product_factor * S ((S (ff_i_fsat_cancel_product)) * c) + (ff_p_fsat_cancel_product))) /\ ((((exists ff_h_fsat_cancel_product_partial. ff_h_fsat_cancel_product_partial + S (ff_r_fsat_cancel_product) = S ((S (ff_i_fsat_cancel_product)) * ff_v_fsat_cancel_product)) /\ exists ff_q_fsat_cancel_product_partial. ff_u_fsat_cancel_product = ff_q_fsat_cancel_product_partial * S ((S (ff_i_fsat_cancel_product)) * ff_v_fsat_cancel_product) + (ff_r_fsat_cancel_product))) /\ ((((exists ff_h_fsat_cancel_product_successor. ff_h_fsat_cancel_product_successor + S (ff_s_fsat_cancel_product) = S ((S (S ff_i_fsat_cancel_product)) * ff_v_fsat_cancel_product)) /\ exists ff_q_fsat_cancel_product_successor. ff_u_fsat_cancel_product = ff_q_fsat_cancel_product_successor * S ((S (S ff_i_fsat_cancel_product)) * ff_v_fsat_cancel_product) + (ff_s_fsat_cancel_product))) /\ ff_s_fsat_cancel_product = ff_r_fsat_cancel_product * ff_p_fsat_cancel_product)))))) /\ (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