BT003M

prime_divisor_eq_one_or_self

Stable checked-use theorem · independently kernel verified

Every divisor of a prime is one or the prime itself.

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 g. (~(p = 1) /\ forall c d. p = c * d -> c = 1 \/ d = 1) -> (exists x. p = g * x) -> g = 1 \/ p = g

Structural proof guide

Every divisor of a prime is one or the prime itself.

Direct prerequisites: mul_one. The authored body proceeds by case analysis (3), intermediate claims (1), equality transport (1).

Proof neighborhood

Direct dependencies

BT000A mul_one

Direct dependents

BT003N euclid_prime_dvd_product BT008Q prime_coprime_or_divides BT008S distinct_primes_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

19 script commands · 11 reading checkpoints · 1 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)
mul one
01Fix variables and assumptionsL1–4

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

  1. L1
    intro p
  2. L2
    intro g
  3. L3
    intro hp
  4. L4
    intro hdiv
02Separate the logical casesL5–6

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

  1. L5
    cases hp
  2. L6
    cases hdiv
03Use earlier factsL7–8

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

  1. L7
    specialize hp_right g
  2. L8
    specialize hp_right x
04Establish hfactorL9–11

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

  1. L9
    have hfactor : g = 1 \/ x = 1
  2. L10
    apply hp_right
  3. L11
    exact hdiv_witness
05Separate the logical casesL12–13

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

  1. L12
    cases hfactor
  2. L13
    left
06Use earlier factsL14–14

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

  1. L14
    exact hfactor_left
07Separate the logical casesL15–15

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

  1. L15
    right
08Calculate and transport equalitiesL16–16

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

  1. L16
    trans g * x
09Use earlier factsL17–17

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

  1. L17
    exact hdiv_witness
10Calculate and transport equalitiesL18–18

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

  1. L18
    rewrite hfactor_right
11Use earlier factsL19–19

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

  1. L19
    apply mul_one

Library-wide reading audit

Original exact command ledger · 19 lines
  1. 0001intro p
  2. 0002intro g
  3. 0003intro hp
  4. 0004intro hdiv
  5. 0005cases hp
  6. 0006cases hdiv
  7. 0007specialize hp_right g
  8. 0008specialize hp_right x
  9. 0009have hfactor : g = 1 \/ x = 1
  10. 0010apply hp_right
  11. 0011exact hdiv_witness
  12. 0012cases hfactor
  13. 0013left
  14. 0014exact hfactor_left
  15. 0015right
  16. 0016trans g * x
  17. 0017exact hdiv_witness
  18. 0018rewrite hfactor_right
  19. 0019apply mul_one