TF0010

euclid_three_common_multiple_exclusion

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

No prime dividing a nonzero common multiple can also divide its subtraction-free Euclid number 4c−1.

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 c d p. c = S d -> ((~(p = 1) /\ forall frm_prime_left_ptmf_prime frm_prime_right_ptmf_prime. p = frm_prime_left_ptmf_prime * frm_prime_right_ptmf_prime -> frm_prime_left_ptmf_prime = 1 \/ frm_prime_right_ptmf_prime = 1)) -> (exists ff_quotient_ptmf_common. (c) = (p) * ff_quotient_ptmf_common) -> (exists ff_quotient_ptmf_euclid. (4 * d + 3) = (p) * ff_quotient_ptmf_euclid) -> false

Constructive proof overview

Generated structural guide

No prime dividing a nonzero common multiple can also divide its subtraction-free Euclid number 4c−1.

The unchanged tactic script uses 5 declared prerequisites and contains 35 exact native proof lines.

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

Proof neighborhood

Direct dependencies

multiple_mul_left Stable theorem; checked-use authorized divides_remainder Stable theorem; checked-use authorized mul_one Stable theorem; checked-use authorized TF000E euclid_three_number_successor_balance divisor_one Stable theorem; checked-use authorized

Direct dependents

TF0011 euclid_three_prime_divisor_exceeds_bound

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

35 script commands · 9 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.

Named ingredients (1)
euclid three number successor balance
01Fix variables and assumptionsL1–7

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

  1. L1
    intro c
  2. L2
    intro d
  3. L3
    intro p
  4. L4
    intro hpredecessor
  5. L5
    intro hprime
  6. L6
    intro hcommon
  7. L7
    intro heuclid
02Establish hfourL8–13

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

  1. L8
    have hfour : exists q. 4 * c = p * q
  2. L9
    specialize multiple_mul_left p
  3. L10
    specialize multiple_mul_left c
  4. L11
    specialize multiple_mul_left 4
  5. L12
    apply multiple_mul_left
  6. L13
    exact hcommon
03Establish honeL14–23

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

  1. L14
    have hone : exists q. 1 = p * q
  2. L15
    specialize divides_remainder p
  3. L16
    specialize divides_remainder (4 * c)
  4. L17
    specialize divides_remainder (4 * d + 3)
  5. L18
    specialize divides_remainder 1
  6. L19
    specialize divides_remainder 1
  7. L20
    apply divides_remainder
  8. L21
    exact hfour
  9. L22
    exact heuclid
  10. L23
    rewrite hpredecessor
04Use earlier factsL24–24

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

  1. L24
    specialize mul_one (4 * d + 3)
05Calculate and transport equalitiesL25–26

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

  1. L25
    rewrite mul_one
  2. L26
    symm
06Use earlier factsL27–28

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

  1. L27
    specialize euclid_three_number_successor_balance d
  2. L28
    exact euclid_three_number_successor_balance
07Establish hunitL29–32

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

  1. L29
    have hunit : p = 1
  2. L30
    specialize divisor_one p
  3. L31
    apply divisor_one
  4. L32
    exact hone
08Separate the logical casesL33–33

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

  1. L33
    cases hprime
09Use earlier factsL34–35

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

  1. L34
    apply hprime_left
  2. L35
    exact hunit

Library-wide reading audit

Original exact command ledger · 35 lines
  1. 0001intro c
  2. 0002intro d
  3. 0003intro p
  4. 0004intro hpredecessor
  5. 0005intro hprime
  6. 0006intro hcommon
  7. 0007intro heuclid
  8. 0008have hfour : exists q. 4 * c = p * q
  9. 0009specialize multiple_mul_left p
  10. 0010specialize multiple_mul_left c
  11. 0011specialize multiple_mul_left 4
  12. 0012apply multiple_mul_left
  13. 0013exact hcommon
  14. 0014have hone : exists q. 1 = p * q
  15. 0015specialize divides_remainder p
  16. 0016specialize divides_remainder (4 * c)
  17. 0017specialize divides_remainder (4 * d + 3)
  18. 0018specialize divides_remainder 1
  19. 0019specialize divides_remainder 1
  20. 0020apply divides_remainder
  21. 0021exact hfour
  22. 0022exact heuclid
  23. 0023rewrite hpredecessor
  24. 0024specialize mul_one (4 * d + 3)
  25. 0025rewrite mul_one
  26. 0026symm
  27. 0027specialize euclid_three_number_successor_balance d
  28. 0028exact euclid_three_number_successor_balance
  29. 0029have hunit : p = 1
  30. 0030specialize divisor_one p
  31. 0031apply divisor_one
  32. 0032exact hone
  33. 0033cases hprime
  34. 0034apply hprime_left
  35. 0035exact hunit