BT011B

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.

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

Structural proof guide

A nonzero proper remainder refutes divisibility.

Direct prerequisites: multiple_refl, divides_remainder, divisor_le_nonzero, lt_not_le. The authored body proceeds by intermediate claims (3).

Proof neighborhood

Direct dependencies

BT0028 multiple_refl BT002H divides_remainder BT002D divisor_le_nonzero BT001I lt_not_le

Direct 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

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

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.

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
    have hself : exists u. d = d * u
  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
    have hrem : exists u. r = d * u
  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
    have hle : exists k. k + d = r
  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 exact 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 : exists u. d = d * u
  10. 0010specialize multiple_refl d
  11. 0011exact multiple_refl
  12. 0012have 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 : 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