BT00QO · Bertrand theorem

prime_nondivisor_mul

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

A prime dividing neither factor does not divide their product.

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) → ¬Dvd(p,b) → ¬Dvd(p,a · 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

PD0003 Dvd

2 occurrences

Exact expanded native-PA statement
forall p a b. ((~(p = 1) /\ forall frm_prime_left_bpd_prime frm_prime_right_bpd_prime. p = frm_prime_left_bpd_prime * frm_prime_right_bpd_prime -> frm_prime_left_bpd_prime = 1 \/ frm_prime_right_bpd_prime = 1)) -> ~(exists bpd_factor_nondivisor_left. a = (p) * bpd_factor_nondivisor_left) -> ~(exists bpd_factor_nondivisor_right. b = (p) * bpd_factor_nondivisor_right) -> ~(exists bpd_factor_nondivisor_product. a * b = (p) * bpd_factor_nondivisor_product)

Proof neighborhood

Direct theorem prerequisites

BT003N euclid_prime_dvd_product

Direct theorem dependents

BT00QQ power_valuation_mul_successor_not_divides

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

19 script commands · 4 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.

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 prime dvd product
01Fix variables and assumptionsL1–7

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 ha
  6. L6
    intro hb
  7. L7
    intro hab
02Establish hsplitL8–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclid prime dvd product.

  1. L8
    have hsplit : Dvd(p,a) ∨ Dvd(p,b)Definitions: Dvd(p,a)Dvd(p,b)Original native command in the exact edition
  2. L9
    specialize euclid_prime_dvd_product p
  3. L10
    specialize euclid_prime_dvd_product a
  4. L11
    specialize euclid_prime_dvd_product b
  5. L12
    apply euclid_prime_dvd_product
  6. L13
    exact hp
  7. L14
    exact hab
03Separate the logical casesL15–15

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

  1. L15
    cases hsplit
04Use earlier factsL16–19

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

  1. L16
    apply ha
  2. L17
    exact hsplit_left
  3. L18
    apply hb
  4. L19
    exact hsplit_right

Library-wide reading audit

Original defined command ledger · 19 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro hp
  5. 0005intro ha
  6. 0006intro hb
  7. 0007intro hab
  8. 0008have hsplit : Dvd(p,a) ∨ Dvd(p,b)
    Exact native replay linehave hsplit : (exists u. a = p * u) \/ exists v. b = p * v
  9. 0009specialize euclid_prime_dvd_product p
  10. 0010specialize euclid_prime_dvd_product a
  11. 0011specialize euclid_prime_dvd_product b
  12. 0012apply euclid_prime_dvd_product
  13. 0013exact hp
  14. 0014exact hab
  15. 0015cases hsplit
  16. 0016apply ha
  17. 0017exact hsplit_left
  18. 0018apply hb
  19. 0019exact hsplit_right