MC0002

prime_toggle_fresh_divisor_product

A prime divisor of n not dividing d can be adjoined to an actual divisor d: Euclid cancellation constructs the required quotient.

Alpha v34 checked-use · first admitted v31 · 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.

The input n is positive. Signed code 2 denotes +1, so the actual sum is +1 at n=1 and zero for n>1. The positive-values result permits arbitrary F(0), which the divisor mask excludes. Prime-square multiples contribute zero. Full G007 inversion is established in its separate family.

Exact theorem in conservative defined notation

∀ p. ∀ n. ∀ d. Prime(p) → Dvd(p,n) → Dvd(d,n) → ¬Dvd(p,d) → Dvd(p · d,n)

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

Definition DAG

Dvd(d,n) · 6Prime(p) · 1Coprime(a,b) · 2

Actual proof prerequisites

prime_coprime_or_divides · checked external prerequisitegauss_coprime_cancel · checked external prerequisitenatural_mul_swap_right_tail · checked external prerequisitemul_assoc · checked external prerequisite
Original expanded first-order statement 
forall p n d. (~((p) = 1) /\ forall pvs_left_fresh_prime pvs_right_fresh_prime. (p) = pvs_left_fresh_prime * pvs_right_fresh_prime -> pvs_left_fresh_prime = 1 \/ pvs_right_fresh_prime = 1) -> (exists pvs_factor_fresh_p_divisor. (n) = (p) * pvs_factor_fresh_p_divisor) -> (exists pvs_factor_fresh_d_divisor. (n) = (d) * pvs_factor_fresh_d_divisor) -> ~(exists pvs_factor_fresh_guard. (d) = (p) * pvs_factor_fresh_guard) -> (exists pvs_factor_fresh_product_divisor. (n) = (p*d) * pvs_factor_fresh_product_divisor)

Complete tactic proof in conservative notation

All 38 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

38 script commands · 17 reading checkpoints · 3 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.

01Fix variables and assumptionsL1–7

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro d
  4. L4
    intro hp
  5. L5
    intro hpn
  6. L6
    intro hdn
  7. L7
    intro hfresh
02Establish hcL8–8

Establish this local claim before using it. It is not an additional assumption.

  1. L8
03Establish hcasesL9–13

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

  1. L9
    have hcases : Coprime(p,d) ∨ Dvd(p,d)Definitions: Coprime(p,d)Dvd(p,d)Original native command in the exact edition
  2. L10
    specialize prime_coprime_or_divides (p)
  3. L11
    specialize prime_coprime_or_divides (d)
  4. L12
    apply prime_coprime_or_divides
  5. L13
    exact hp
04Separate the logical casesL14–14

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

  1. L14
    cases hcases
05Use earlier factsL15–15

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

  1. L15
    exact hcases_left
06Separate the logical casesL16–16

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

  1. L16
    exfalso
07Use earlier factsL17–18

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

  1. L17
    apply hfresh
  2. L18
    exact hcases_right
08Separate the logical casesL19–19

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

  1. L19
    cases hdn
09Establish hqL20–27

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

  1. L20
  2. L21
    specialize gauss_coprime_cancel (p)
  3. L22
    specialize gauss_coprime_cancel (d)
  4. L23
    specialize gauss_coprime_cancel (x)
  5. L24
    apply gauss_coprime_cancel
  6. L25
    exact hc
  7. L26
    rewrite hdn_witness at hpn
  8. L27
    exact hpn
10Separate the logical casesL28–28

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

  1. L28
    cases hq
11Construct an explicit witnessL29–29

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

  1. L29
    exists x1
12Calculate and transport equalitiesL30–30

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

  1. L30
    trans d*x
13Use earlier factsL31–31

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

  1. L31
    exact hdn_witness
14Calculate and transport equalitiesL32–35

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

  1. L32
    trans d*(p*x1)
  2. L33
    rewrite hq_witness
  3. L34
    refl
  4. L35
    trans p*(d*x1)
15Use earlier factsL36–36

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

  1. L36
    apply natural_mul_swap_right_tail
16Calculate and transport equalitiesL37–37

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

  1. L37
    symm
17Use earlier factsL38–38

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

  1. L38
    apply mul_assoc

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro d
  4. 0004intro hp
  5. 0005intro hpn
  6. 0006intro hdn
  7. 0007intro hfresh
  8. 0008have hc : Coprime(p,d)
  9. 0009have hcases : Coprime(p,d) ∨ Dvd(p,d)
  10. 0010specialize prime_coprime_or_divides (p)
  11. 0011specialize prime_coprime_or_divides (d)
  12. 0012apply prime_coprime_or_divides
  13. 0013exact hp
  14. 0014cases hcases
  15. 0015exact hcases_left
  16. 0016exfalso
  17. 0017apply hfresh
  18. 0018exact hcases_right
  19. 0019cases hdn
  20. 0020have hq : Dvd(p,x)
  21. 0021specialize gauss_coprime_cancel (p)
  22. 0022specialize gauss_coprime_cancel (d)
  23. 0023specialize gauss_coprime_cancel (x)
  24. 0024apply gauss_coprime_cancel
  25. 0025exact hc
  26. 0026rewrite hdn_witness at hpn
  27. 0027exact hpn
  28. 0028cases hq
  29. 0029exists x1
  30. 0030trans d*x
  31. 0031exact hdn_witness
  32. 0032trans d*(p*x1)
  33. 0033rewrite hq_witness
  34. 0034refl
  35. 0035trans p*(d*x1)
  36. 0036apply natural_mul_swap_right_tail
  37. 0037symm
  38. 0038apply mul_assoc