BT008Q · Bertrand theorem

prime_coprime_or_divides

Stable checked-use theorem · independently kernel verified

A prime is constructively either coprime to a natural or divides it.

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. Prime(p) → Coprime(p,a) ∨ Dvd(p,a)

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 PD0005 Coprime

3 occurrences

In local proof propositions

PD0006 IsGCD

3 occurrences

Exact expanded native-PA statement
forall p a. (~(p = 1) /\ forall c e. p = c * e -> c = 1 \/ e = 1) -> (forall d. (exists x. p = d * x) -> (exists y. a = d * y) -> d = 1) \/ exists k. a = p * k

Proof neighborhood

Direct theorem prerequisites

BT002V gcd_exists_relational BT003M prime_divisor_eq_one_or_self BT0031 is_gcd_one_to_coprime

Direct theorem dependents

BT008R prime_not_divides_coprime

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

30 script commands · 13 reading checkpoints · 4 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 (3)
gcd exists relationalprime divisor eq one or selfis gcd one to coprime
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro hp
02Establish hgL4–5

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

  1. L4
    have hg : ∃ g. IsGCD(g,p,a)Definitions: IsGCD(g,p,a)Original native command in the exact edition
  2. L5
    apply gcd_exists_relational
03Separate the logical casesL6–6

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

  1. L6
    cases hg
04Establish hgfullL7–8

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

  1. L7
    have hgfull : IsGCD(x,p,a)Definitions: IsGCD(x,p,a)Original native command in the exact edition
  2. L8
    exact hg_witness
05Separate the logical casesL9–10

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

  1. L9
    cases hg_witness
  2. L10
    cases hg_witness_left
06Establish hfactorL11–16

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. L11
    have hfactor : x = 1 \/ p = x
  2. L12
    specialize prime_divisor_eq_one_or_self p
  3. L13
    specialize prime_divisor_eq_one_or_self x
  4. L14
    apply prime_divisor_eq_one_or_self
  5. L15
    exact hp
  6. L16
    exact hg_witness_left_left
07Separate the logical casesL17–18

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

  1. L17
    cases hfactor
  2. L18
    left
08Use earlier factsL19–19

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

  1. L19
    apply is_gcd_one_to_coprime
09Establish hg1L20–25

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

  1. L20
  2. L21
    rewrite <- hfactor_left
  3. L22
    rewrite <- hfactor_left
  4. L23
    rewrite <- hfactor_left
  5. L24
    exact hgfull
  6. L25
    exact hg1
10Separate the logical casesL26–27

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

  1. L26
    right
  2. L27
    cases hg_witness_left_right
11Construct an explicit witnessL28–28

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

  1. L28
    exists x1
12Calculate and transport equalitiesL29–29

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

  1. L29
    rewrite hfactor_right
13Use earlier factsL30–30

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

  1. L30
    exact hg_witness_left_right_witness

Library-wide reading audit

Original defined command ledger · 30 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro hp
  4. 0004have 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)
  5. 0005apply gcd_exists_relational
  6. 0006cases hg
  7. 0007have 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)
  8. 0008exact hg_witness
  9. 0009cases hg_witness
  10. 0010cases hg_witness_left
  11. 0011have hfactor : x = 1 \/ p = x
  12. 0012specialize prime_divisor_eq_one_or_self p
  13. 0013specialize prime_divisor_eq_one_or_self x
  14. 0014apply prime_divisor_eq_one_or_self
  15. 0015exact hp
  16. 0016exact hg_witness_left_left
  17. 0017cases hfactor
  18. 0018left
  19. 0019apply is_gcd_one_to_coprime
  20. 0020have 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)
  21. 0021rewrite <- hfactor_left
  22. 0022rewrite <- hfactor_left
  23. 0023rewrite <- hfactor_left
  24. 0024exact hgfull
  25. 0025exact hg1
  26. 0026right
  27. 0027cases hg_witness_left_right
  28. 0028exists x1
  29. 0029rewrite hfactor_right
  30. 0030exact hg_witness_left_right_witness