MC0002

prime_toggle_fresh_divisor_product

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 38 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_coprime_or_divides Stable theorem; checked-use authorized gauss_coprime_cancel Stable theorem; checked-use authorized natural_mul_swap_right_tail Alpha theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized

Direct dependents

MC0007 prime_factor_toggle_preserves_divisor

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

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.

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
    have hc : forall sfd_common_divisor_fresh_coprime. (exists pvs_factor_fresh_coprimeleft. (p) = (sfd_common_divisor_fresh_coprime) * pvs_factor_fresh_coprimeleft) -> (exists pvs_factor_fresh_coprimeright. (d) = (sfd_common_divisor_fresh_coprime) * pvs_factor_fresh_coprimeright) -> sfd_common_divisor_fresh_coprime = 1
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 : (forall sfd_common_divisor_fresh_coprime_cases. (exists pvs_factor_fresh_coprime_casesleft. (p) = (sfd_common_divisor_fresh_coprime_cases) * pvs_factor_fresh_coprime_casesleft) -> (exists pvs_factor_fresh_coprime_casesright. (d) = (sfd_common_divisor_fresh_coprime_cases) * pvs_factor_fresh_coprime_casesright) -> sfd_common_divisor_fresh_coprime_cases = 1) \/ (exists pvs_factor_fresh_divisor_cases. (d) = (p) * pvs_factor_fresh_divisor_cases)
  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
    have hq : exists pvs_factor_fresh_quotient. (x) = (p) * pvs_factor_fresh_quotient
  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 exact 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 : forall sfd_common_divisor_fresh_coprime. (exists pvs_factor_fresh_coprimeleft. (p) = (sfd_common_divisor_fresh_coprime) * pvs_factor_fresh_coprimeleft) -> (exists pvs_factor_fresh_coprimeright. (d) = (sfd_common_divisor_fresh_coprime) * pvs_factor_fresh_coprimeright) -> sfd_common_divisor_fresh_coprime = 1
  9. 0009have hcases : (forall sfd_common_divisor_fresh_coprime_cases. (exists pvs_factor_fresh_coprime_casesleft. (p) = (sfd_common_divisor_fresh_coprime_cases) * pvs_factor_fresh_coprime_casesleft) -> (exists pvs_factor_fresh_coprime_casesright. (d) = (sfd_common_divisor_fresh_coprime_cases) * pvs_factor_fresh_coprime_casesright) -> sfd_common_divisor_fresh_coprime_cases = 1) \/ (exists pvs_factor_fresh_divisor_cases. (d) = (p) * pvs_factor_fresh_divisor_cases)
  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 : exists pvs_factor_fresh_quotient. (x) = (p) * pvs_factor_fresh_quotient
  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