BT011B · Bertrand theorem

nonzero_remainder_not_multiple

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

A nonzero proper remainder refutes divisibility.

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. ∀ q. ∀ r. n = d · q + r → ¬r = 0 → Lt(r,d) → ¬Dvd(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

PD0002 Lt PD0003 Dvd

2 occurrences

In local proof propositions

PD0001 Le PD0003 Dvd

3 occurrences

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

Proof neighborhood

Direct theorem prerequisites

BT0028 multiple_refl BT002H divides_remainder BT002D divisor_le_nonzero BT001I lt_not_le

Direct theorem dependents

BT011F prime_five BT011G prime_seven BT011H prime_thirteen BT011I prime_twenty_three BT011J prime_forty_three BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen BT011N prime_five_hundred_twenty_one

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

32 script commands · 5 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 (4)
multiple refldivides remainderdivisor le nonzerolt not le
01Fix variables and assumptionsL1–8

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

  1. L1
    intro d
  2. L2
    intro n
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro heq
  6. L6
    intro hr0
  7. L7
    intro hlt
  8. L8
    intro hdivides
02Establish hselfL9–11

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

  1. L9
  2. L10
    specialize multiple_refl d
  3. L11
    exact multiple_refl
03Establish hremL12–21

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

  1. L12
  2. L13
    specialize divides_remainder d
  3. L14
    specialize divides_remainder n
  4. L15
    specialize divides_remainder d
  5. L16
    specialize divides_remainder q
  6. L17
    specialize divides_remainder r
  7. L18
    apply divides_remainder
  8. L19
    exact hdivides
  9. L20
    exact hself
  10. L21
    exact heq
04Establish hleL22–31

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

  1. L22
  2. L23
    specialize divisor_le_nonzero d
  3. L24
    specialize divisor_le_nonzero r
  4. L25
    apply divisor_le_nonzero
  5. L26
    exact hr0
  6. L27
    exact hrem
  7. L28
    specialize lt_not_le r
  8. L29
    specialize lt_not_le d
  9. L30
    apply lt_not_le
  10. L31
    exact hlt
05Use earlier factsL32–32

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

  1. L32
    exact hle

Library-wide reading audit

Original defined command ledger · 32 lines
  1. 0001intro d
  2. 0002intro n
  3. 0003intro q
  4. 0004intro r
  5. 0005intro heq
  6. 0006intro hr0
  7. 0007intro hlt
  8. 0008intro hdivides
  9. 0009have hself : Dvd(d,d)
    Exact native replay linehave hself : exists u. d = d * u
  10. 0010specialize multiple_refl d
  11. 0011exact multiple_refl
  12. 0012have hrem : Dvd(d,r)
    Exact native replay linehave hrem : exists u. r = d * u
  13. 0013specialize divides_remainder d
  14. 0014specialize divides_remainder n
  15. 0015specialize divides_remainder d
  16. 0016specialize divides_remainder q
  17. 0017specialize divides_remainder r
  18. 0018apply divides_remainder
  19. 0019exact hdivides
  20. 0020exact hself
  21. 0021exact heq
  22. 0022have hle : Le(d,r)
    Exact native replay linehave hle : exists k. k + d = r
  23. 0023specialize divisor_le_nonzero d
  24. 0024specialize divisor_le_nonzero r
  25. 0025apply divisor_le_nonzero
  26. 0026exact hr0
  27. 0027exact hrem
  28. 0028specialize lt_not_le r
  29. 0029specialize lt_not_le d
  30. 0030apply lt_not_le
  31. 0031exact hlt
  32. 0032exact hle