BT008Q

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.

Exact expanded 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

Structural proof guide

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

Direct prerequisites: gcd_exists_relational, prime_divisor_eq_one_or_self, is_gcd_one_to_coprime. The authored body proceeds by case analysis (5), intermediate claims (4), equality transport (4).

Proof neighborhood

Direct dependencies

BT002V gcd_exists_relational BT003M prime_divisor_eq_one_or_self BT0031 is_gcd_one_to_coprime

Direct dependents

BT008R prime_not_divides_coprime

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

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.

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 : 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)
  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 : (((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)
  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
    have 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)
  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 exact command ledger · 30 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro hp
  4. 0004have 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 : (((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 : (((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