BT002D

divisor_le_nonzero

Stable · empty-context checked

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

Exact expanded PA statement

forall d n. ~(n = 0) -> (exists q. n = d * q) -> exists k. k + d = n

Structural proof guide

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

Direct prerequisites: one_le_of_ne_zero. The authored body proceeds by case analysis (2), intermediate claims (3), equality transport (1).

Proof neighborhood

Direct dependencies

BT0010 one_le_of_ne_zero

Direct 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

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 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 : 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