PA0039

divisor_le_nonzero

Stable checked-use theorem · independently closed

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

Generated structural guide

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

Use the direct prerequisites one_le_of_ne_zero as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (3), equality transport (1), certified simplification (1).

Referenced ingredients

PA002L one_le_of_ne_zero

Proof neighborhood

Direct dependencies

PA002L one_le_of_ne_zero

Direct dependents

PA0063 prime_bounded_nonzero_mod_inverse PA0072 gauss_half_range_signed_choices PA0082 prime_positive_bounded_product_coprime PA0089 bounded_nonzero_not_divides PA008B prime_mul_index_map_exists_up_to PA008K prime_range_product_coprime PA009C prime_scaled_inverse_unique PA00AG prime_bounded_square_one_cases PA00D8 distinct_odd_prime_half_products_ne PA00DN prime_nondivisor_bounded_scaled_remainder_nonzero

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  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