BT002D · Bertrand theorem

divisor_le_nonzero

Stable checked-use theorem · independently kernel verified

A divisor of a nonzero natural is bounded by that natural.

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

∀ d. ∀ n. ¬n = 0 → Dvd(d,n) → Le(d,n)

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

PD0001 Le PD0003 Dvd

2 occurrences

In local proof propositions

PD0002 Lt

1 occurrences

Exact expanded native-PA statement
forall d n. ~(n = 0) -> (exists q. n = d * q) -> exists k. k + d = n

Proof neighborhood

Direct theorem prerequisites

BT0010 one_le_of_ne_zero

Direct theorem dependents

BT003F prime_or_composite BT003J proper_factor_lt BT00QG prime_power_divides_exponent_le_value BT00VB factorial_prime_le_of_divides BT00VI primorial_even_interval_le_central BT00VJ primorial_odd_interval_le_middle BT0118 nonprime_has_small_prime_divisor_below_square BT011B nonzero_remainder_not_multiple

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

31 script commands · 13 reading checkpoints · 3 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)
one le of ne zero
01Fix variables and assumptionsL1–4

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

  1. L1
    intro d
  2. L2
    intro n
  3. L3
    intro hn
  4. L4
    intro hd
02Separate the logical casesL5–5

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

  1. L5
    cases hd
03Establish hqL6–13

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

  1. L6
    have hq : ~(x = 0)
  2. L7
    intro hx
  3. L8
    apply hn
  4. L9
    trans d * x
  5. L10
    exact hd_witness
  6. L11
    rewrite hx
  7. L12
    apply PA5
  8. L13
    specialize one_le_of_ne_zero x
04Establish h1qL14–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply one le of ne zero.

  1. L14
  2. L15
    apply one_le_of_ne_zero
  3. L16
    exact hq
05Separate the logical casesL17–17

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

  1. L17
    cases h1q
06Establish hsL18–21

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

  1. L18
    have hs : S x1 = x
  2. L19
    trans x1 + 1
  3. L20
    simp
  4. L21
    exact h1q_witness
07Construct an explicit witnessL22–22

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

  1. L22
    exists d * x1
08Calculate and transport equalitiesL23–24

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

  1. L23
    trans d * S x1
  2. L24
    symm
09Use earlier factsL25–25

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

  1. L25
    apply PA6
10Calculate and transport equalitiesL26–28

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

  1. L26
    trans d * x
  2. L27
    congr
  3. L28
    refl
11Use earlier factsL29–29

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

  1. L29
    exact hs
12Calculate and transport equalitiesL30–30

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

  1. L30
    symm
13Use earlier factsL31–31

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

  1. L31
    exact hd_witness

Library-wide reading audit

Original defined command ledger · 31 lines
  1. 0001intro d
  2. 0002intro n
  3. 0003intro hn
  4. 0004intro hd
  5. 0005cases hd
  6. 0006have hq : ~(x = 0)
  7. 0007intro hx
  8. 0008apply hn
  9. 0009trans d * x
  10. 0010exact hd_witness
  11. 0011rewrite hx
  12. 0012apply PA5
  13. 0013specialize one_le_of_ne_zero x
  14. 0014have h1q : Lt(0,x)
    Exact native replay linehave h1q : exists k. k + 1 = x
  15. 0015apply one_le_of_ne_zero
  16. 0016exact hq
  17. 0017cases h1q
  18. 0018have hs : S x1 = x
  19. 0019trans x1 + 1
  20. 0020simp
  21. 0021exact h1q_witness
  22. 0022exists d * x1
  23. 0023trans d * S x1
  24. 0024symm
  25. 0025apply PA6
  26. 0026trans d * x
  27. 0027congr
  28. 0028refl
  29. 0029exact hs
  30. 0030symm
  31. 0031exact hd_witness