BT011B

nonzero_remainder_not_multiple

Alpha body-checked · checked-use disabled

A nonzero proper remainder refutes divisibility.

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 this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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