MC0007

prime_factor_toggle_preserves_divisor

Every actual prime toggle of a divisor of n is again a divisor, provided p itself is a prime divisor of n.

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. ∀ e. Prime(p) → Dvd(p,n) → Dvd(d,n) → PrimeFactorToggle(p,d,e) → Dvd(e,n)

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

Definition DAG

PrimeFactorToggle(p,d,e) · 1Dvd(d,n) · 3Prime(p) · 1

Actual proof prerequisites

prime_toggle_fresh_divisor_productmultiple_trans · checked external prerequisitemul_comm · checked external prerequisite
Original expanded first-order statement 
forall p n d e. (~((p) = 1) /\ forall pvs_left_preserve_prime pvs_right_preserve_prime. (p) = pvs_left_preserve_prime * pvs_right_preserve_prime -> pvs_left_preserve_prime = 1 \/ pvs_right_preserve_prime = 1) -> (exists pvs_factor_preserve_p. (n) = (p) * pvs_factor_preserve_p) -> (exists pvs_factor_preserve_d. (n) = (d) * pvs_factor_preserve_d) -> ((((~(exists pvs_factor_preserve_graphfresh_input. (d) = (p) * pvs_factor_preserve_graphfresh_input)) /\ ((e)=(p)*(d)))) \/ (((((d)=(p)*(e)) /\ (~(exists pvs_factor_preserve_graphfresh_output. (e) = (p) * pvs_factor_preserve_graphfresh_output)))) \/ (((exists pvs_factor_preserve_graphsquare. (d) = ((p)*(p)) * pvs_factor_preserve_graphsquare) /\ ((e)=(d)))))) -> (exists pvs_factor_preserve_e. (n) = (e) * pvs_factor_preserve_e)

Complete tactic proof in conservative notation

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

33 script commands · 12 reading checkpoints · 0 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)
prime toggle fresh divisor product
01Fix variables and assumptionsL1–8

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 e
  5. L5
    intro hp
  6. L6
    intro hpn
  7. L7
    intro hdn
  8. L8
    intro he
02Separate the logical casesL9–10

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

  1. L9
    cases he
  2. L10
    cases he_left
03Calculate and transport equalitiesL11–11

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

  1. L11
    rewrite he_left_right
04Use earlier factsL12–19

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

  1. L12
    specialize prime_toggle_fresh_divisor_product (p)
  2. L13
    specialize prime_toggle_fresh_divisor_product (n)
  3. L14
    specialize prime_toggle_fresh_divisor_product (d)
  4. L15
    apply prime_toggle_fresh_divisor_product
  5. L16
    exact hp
  6. L17
    exact hpn
  7. L18
    exact hdn
  8. L19
    exact he_left_left
05Separate the logical casesL20–21

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

  1. L20
    cases he_right
  2. L21
    cases he_right_left
06Use earlier factsL22–26

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

  1. L22
    specialize multiple_trans (d)
  2. L23
    specialize multiple_trans (e)
  3. L24
    specialize multiple_trans (n)
  4. L25
    apply multiple_trans
  5. L26
    exact hdn
07Construct an explicit witnessL27–27

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

  1. L27
    exists p
08Calculate and transport equalitiesL28–28

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

  1. L28
    trans p*e
09Use earlier factsL29–30

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

  1. L29
    exact he_right_left_left
  2. L30
    apply mul_comm
10Separate the logical casesL31–31

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

  1. L31
    cases he_right_right
11Calculate and transport equalitiesL32–32

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

  1. L32
    rewrite he_right_right_right
12Use earlier factsL33–33

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

  1. L33
    exact hdn

Library-wide reading audit

Original defined command ledger · 33 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro d
  4. 0004intro e
  5. 0005intro hp
  6. 0006intro hpn
  7. 0007intro hdn
  8. 0008intro he
  9. 0009cases he
  10. 0010cases he_left
  11. 0011rewrite he_left_right
  12. 0012specialize prime_toggle_fresh_divisor_product (p)
  13. 0013specialize prime_toggle_fresh_divisor_product (n)
  14. 0014specialize prime_toggle_fresh_divisor_product (d)
  15. 0015apply prime_toggle_fresh_divisor_product
  16. 0016exact hp
  17. 0017exact hpn
  18. 0018exact hdn
  19. 0019exact he_left_left
  20. 0020cases he_right
  21. 0021cases he_right_left
  22. 0022specialize multiple_trans (d)
  23. 0023specialize multiple_trans (e)
  24. 0024specialize multiple_trans (n)
  25. 0025apply multiple_trans
  26. 0026exact hdn
  27. 0027exists p
  28. 0028trans p*e
  29. 0029exact he_right_left_left
  30. 0030apply mul_comm
  31. 0031cases he_right_right
  32. 0032rewrite he_right_right_right
  33. 0033exact hdn