TF0010

euclid_three_common_multiple_exclusion

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

Alpha v34 checked-use · first admitted v23 · 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. Exact original first-admission records.

The exact G025 progression-prime milestone is fully proved in unchanged constructive arithmetic; Mod4Three deliberately reuses its existing Quadratic Reciprocity definition PD0012. The much stronger full Dirichlet progression-prime milestone G030 remains open.

Exact theorem in conservative defined notation

∀ c. ∀ d. ∀ p. c = S d → Prime(p) → Dvd(p,c) → ¬Dvd(p,4 · d + 3)

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

Definition DAG

Dvd(d,n) · 2Prime(p) · 1

Actual proof prerequisites

multiple_mul_left · checked external prerequisitedivides_remainder · checked external prerequisitemul_one · checked external prerequisiteeuclid_three_number_successor_balancedivisor_one · checked external prerequisite
Original expanded first-order 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

Complete unchanged native tactic proof

All 35 lines are the exact independently kernel-checked original script.

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.

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)
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 defined 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