BT003J

proper_factor_lt

Stable · empty-context checked

A factor with a nonunit cofactor is strictly smaller than a nonzero product.

Exact expanded PA statement

forall n c d. ~(n = 0) -> n = c * d -> ~(d = 1) -> exists k. k + S c = n

Structural proof guide

A factor with a nonunit cofactor is strictly smaller than a nonzero product.

Direct prerequisites: divisor_le_nonzero, le_eq_or_lt, mul_left_cancel_nonzero, mul_one. The authored body proceeds by case analysis (1), intermediate claims (3).

Proof neighborhood

Direct dependencies

BT002D divisor_le_nonzero BT001C le_eq_or_lt BT0022 mul_left_cancel_nonzero BT000A mul_one

Direct dependents

BT003K prime_divisor_exists_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 n
  2. 0002intro c
  3. 0003intro d
  4. 0004intro hn
  5. 0005intro hfactor
  6. 0006intro hd
  7. 0007have hle : exists k. k + c = n
  8. 0008specialize divisor_le_nonzero c
  9. 0009specialize divisor_le_nonzero n
  10. 0010apply divisor_le_nonzero
  11. 0011exact hn
  12. 0012exists d
  13. 0013exact hfactor
  14. 0014have hcases : c = n \/ exists k. k + S c = n
  15. 0015specialize le_eq_or_lt c
  16. 0016specialize le_eq_or_lt n
  17. 0017apply le_eq_or_lt
  18. 0018exact hle
  19. 0019cases hcases
  20. 0020exfalso
  21. 0021apply hd
  22. 0022have hc : ~(c = 0)
  23. 0023intro hc0
  24. 0024apply hn
  25. 0025trans c
  26. 0026symm
  27. 0027exact hcases_left
  28. 0028exact hc0
  29. 0029specialize mul_left_cancel_nonzero c
  30. 0030specialize mul_left_cancel_nonzero d
  31. 0031specialize mul_left_cancel_nonzero 1
  32. 0032apply mul_left_cancel_nonzero
  33. 0033exact hc
  34. 0034trans n
  35. 0035symm
  36. 0036exact hfactor
  37. 0037trans c
  38. 0038symm
  39. 0039exact hcases_left
  40. 0040symm
  41. 0041specialize mul_one c
  42. 0042exact mul_one
  43. 0043exact hcases_right