BT003B

multiple_decidable_nonzero

Stable · empty-context checked

Divisibility by a nonzero natural is constructively decidable.

Exact expanded PA statement

forall d n. ~(d = 0) -> (exists q. n = d * q) \/ ~(exists q. n = d * q)

Structural proof guide

Divisibility by a nonzero natural is constructively decidable.

Direct prerequisites: eq_decidable, division_remainder_exists, multiple_has_zero_remainder, division_remainder_unique. The authored body proceeds by case analysis (9), intermediate claims (4), equality transport (2).

Proof neighborhood

Direct dependencies

BT003A eq_decidable BT001P division_remainder_exists BT001W multiple_has_zero_remainder BT001U division_remainder_unique

Direct dependents

BT003C multiple_decidable BT003E factor_search_up_to

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 hd
  4. 0004have hdiv : exists q r. n = d * q + r /\ S r <= d
  5. 0005apply division_remainder_exists
  6. 0006exact hd
  7. 0007cases hdiv
  8. 0008cases hdiv_witness
  9. 0009cases hdiv_witness_witness
  10. 0010specialize eq_decidable x1
  11. 0011specialize eq_decidable 0
  12. 0012have hr : x1 = 0 \/ ~(x1 = 0)
  13. 0013apply eq_decidable
  14. 0014cases hr
  15. 0015left
  16. 0016exists x
  17. 0017rewrite hr_left at hdiv_witness_witness_left
  18. 0018rewrite PA3 at hdiv_witness_witness_left
  19. 0019exact hdiv_witness_witness_left
  20. 0020right
  21. 0021intro hmul
  22. 0022have hzero : exists q r. ((n = d * q + r /\ r = 0) /\ S r <= d)
  23. 0023apply multiple_has_zero_remainder
  24. 0024exact hd
  25. 0025exact hmul
  26. 0026cases hzero
  27. 0027cases hzero_witness
  28. 0028cases hzero_witness_witness
  29. 0029cases hzero_witness_witness_left
  30. 0030have huniq : x = x2 /\ x1 = x3
  31. 0031apply division_remainder_unique
  32. 0032exact hdiv_witness_witness_left
  33. 0033exact hdiv_witness_witness_right
  34. 0034exact hzero_witness_witness_left_left
  35. 0035exact hzero_witness_witness_right
  36. 0036cases huniq
  37. 0037apply hr_right
  38. 0038trans x3
  39. 0039exact huniq_right
  40. 0040exact hzero_witness_witness_left_right