BT003N · Bertrand theorem

euclid_prime_dvd_product

Stable checked-use theorem · independently kernel verified

A prime dividing a product divides at least one factor (Euclid's lemma).

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.

Statement with defined notation

∀ p. ∀ a. ∀ b. Prime(p) → Dvd(p,a · b) → Dvd(p,a) ∨ Dvd(p,b)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0003 Dvd PD0004 Prime

4 occurrences

In local proof propositions

PD0005 Coprime PD0006 IsGCD

4 occurrences

Exact expanded native-PA statement
forall p a b. (~(p = 1) /\ forall c d. p = c * d -> c = 1 \/ d = 1) -> (exists k. a * b = p * k) -> (exists u. a = p * u) \/ exists v. b = p * v

Proof neighborhood

Direct theorem prerequisites

BT003M prime_divisor_eq_one_or_self BT002V gcd_exists_relational BT0031 is_gcd_one_to_coprime BT0039 gauss_coprime_cancel

Direct theorem dependents

BT00QO prime_nondivisor_mul BT00VB factorial_prime_le_of_divides BT00VC choose_prime_divides_between

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

36 script commands · 14 reading checkpoints · 5 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 (4)
prime divisor eq one or selfgcd exists relationalis gcd one to coprimegauss coprime cancel
01Fix variables and assumptionsL1–5

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro hp
  5. L5
    intro hab
02Establish hgL6–7

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gcd exists relational.

  1. L6
    have hg : ∃ g. IsGCD(g,p,a)Definitions: IsGCD(g,p,a)Original native command in the exact edition
  2. L7
    apply gcd_exists_relational
03Separate the logical casesL8–8

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

  1. L8
    cases hg
04Establish hgfullL9–10

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

  1. L9
    have hgfull : IsGCD(x,p,a)Definitions: IsGCD(x,p,a)Original native command in the exact edition
  2. L10
    exact hg_witness
05Separate the logical casesL11–12

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

  1. L11
    cases hg_witness
  2. L12
    cases hg_witness_left
06Establish hfactorL13–18

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

  1. L13
    have hfactor : x = 1 \/ p = x
  2. L14
    specialize prime_divisor_eq_one_or_self p
  3. L15
    specialize prime_divisor_eq_one_or_self x
  4. L16
    apply prime_divisor_eq_one_or_self
  5. L17
    exact hp
  6. L18
    exact hg_witness_left_left
07Separate the logical casesL19–20

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

  1. L19
    cases hfactor
  2. L20
    right
08Use earlier factsL21–21

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

  1. L21
    apply gauss_coprime_cancel
09Establish hcopL22–23

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

  1. L22
  2. L23
    apply is_gcd_one_to_coprime
10Establish hg1L24–31

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

  1. L24
  2. L25
    rewrite <- hfactor_left
  3. L26
    rewrite <- hfactor_left
  4. L27
    rewrite <- hfactor_left
  5. L28
    exact hgfull
  6. L29
    exact hg1
  7. L30
    exact hcop
  8. L31
    exact hab
11Separate the logical casesL32–33

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

  1. L32
    left
  2. L33
    cases hg_witness_left_right
12Construct an explicit witnessL34–34

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

  1. L34
    exists x1
13Calculate and transport equalitiesL35–35

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

  1. L35
    rewrite hfactor_right
14Use earlier factsL36–36

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

  1. L36
    exact hg_witness_left_right_witness

Library-wide reading audit

Original defined command ledger · 36 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro hp
  5. 0005intro hab
  6. 0006have hg : ∃ g. IsGCD(g,p,a)
    Exact native replay linehave hg : exists g. (((exists x. p = g * x) /\ (exists y. a = g * y)) /\ forall c. (exists u. p = c * u) -> (exists v. a = c * v) -> exists w. g = c * w)
  7. 0007apply gcd_exists_relational
  8. 0008cases hg
  9. 0009have hgfull : IsGCD(x,p,a)
    Exact native replay linehave hgfull : (((exists u. p = x * u) /\ (exists v. a = x * v)) /\ forall c. (exists s. p = c * s) -> (exists t. a = c * t) -> exists w. x = c * w)
  10. 0010exact hg_witness
  11. 0011cases hg_witness
  12. 0012cases hg_witness_left
  13. 0013have hfactor : x = 1 \/ p = x
  14. 0014specialize prime_divisor_eq_one_or_self p
  15. 0015specialize prime_divisor_eq_one_or_self x
  16. 0016apply prime_divisor_eq_one_or_self
  17. 0017exact hp
  18. 0018exact hg_witness_left_left
  19. 0019cases hfactor
  20. 0020right
  21. 0021apply gauss_coprime_cancel
  22. 0022have hcop : Coprime(p,a)
    Exact native replay linehave hcop : forall d. (exists u. p = d * u) -> (exists v. a = d * v) -> d = 1
  23. 0023apply is_gcd_one_to_coprime
  24. 0024have hg1 : IsGCD(1,p,a)
    Exact native replay linehave hg1 : (((exists u. p = 1 * u) /\ (exists v. a = 1 * v)) /\ forall c. (exists s. p = c * s) -> (exists t. a = c * t) -> exists w. 1 = c * w)
  25. 0025rewrite <- hfactor_left
  26. 0026rewrite <- hfactor_left
  27. 0027rewrite <- hfactor_left
  28. 0028exact hgfull
  29. 0029exact hg1
  30. 0030exact hcop
  31. 0031exact hab
  32. 0032left
  33. 0033cases hg_witness_left_right
  34. 0034exists x1
  35. 0035rewrite hfactor_right
  36. 0036exact hg_witness_left_right_witness