BT003K

prime_divisor_exists_up_to

Stable · empty-context checked

Bounded strong induction constructs a prime divisor of every nonzero nonunit natural.

Exact expanded PA statement

forall B n. (exists t. t + n = B) -> ~(n = 0) -> ~(n = 1) -> exists p. ((~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) /\ exists k. n = p * k)

Structural proof guide

Bounded strong induction constructs a prime divisor of every nonzero nonunit natural.

Direct prerequisites: mul_zero_left, le_zero, lt_of_lt_of_le, le_of_succ_le_succ, multiple_refl, multiple_trans, prime_or_composite, proper_factor_lt. The authored body proceeds by structural induction (1), case analysis (7), intermediate claims (6), equality transport (1).

Proof neighborhood

Direct dependencies

BT0004 mul_zero_left BT000Y le_zero BT001D lt_of_lt_of_le BT0017 le_of_succ_le_succ BT0028 multiple_refl BT002C multiple_trans BT003F prime_or_composite BT003J proper_factor_lt

Direct dependents

BT003L prime_divisor_exists

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro B
  2. 0002induction B
  3. 0003intro n
  4. 0004intro hnB
  5. 0005intro hn0
  6. 0006intro hn1
  7. 0007exfalso
  8. 0008apply hn0
  9. 0009apply le_zero
  10. 0010exact hnB
  11. 0011intro n
  12. 0012intro hnB
  13. 0013intro hn0
  14. 0014intro hn1
  15. 0015specialize prime_or_composite n
  16. 0016have hpc : (~(n = 1) /\ forall a b. n = a * b -> a = 1 \/ b = 1) \/ exists c d. ((~(c = 1) /\ ~(d = 1)) /\ n = c * d)
  17. 0017apply prime_or_composite
  18. 0018exact hn0
  19. 0019exact hn1
  20. 0020cases hpc
  21. 0021exists n
  22. 0022split
  23. 0023exact hpc_left
  24. 0024apply multiple_refl
  25. 0025cases hpc_right
  26. 0026cases hpc_right_witness
  27. 0027cases hpc_right_witness_witness
  28. 0028cases hpc_right_witness_witness_left
  29. 0029have hc0 : ~(x = 0)
  30. 0030intro hc
  31. 0031apply hn0
  32. 0032trans x * x1
  33. 0033exact hpc_right_witness_witness_right
  34. 0034rewrite hc
  35. 0035apply mul_zero_left
  36. 0036have hcn : exists k. k + S x = n
  37. 0037specialize proper_factor_lt n
  38. 0038specialize proper_factor_lt x
  39. 0039specialize proper_factor_lt x1
  40. 0040apply proper_factor_lt
  41. 0041exact hn0
  42. 0042exact hpc_right_witness_witness_right
  43. 0043exact hpc_right_witness_witness_left_right
  44. 0044have hcSB : exists k. k + S x = S B
  45. 0045specialize lt_of_lt_of_le x
  46. 0046specialize lt_of_lt_of_le n
  47. 0047specialize lt_of_lt_of_le (S B)
  48. 0048apply lt_of_lt_of_le
  49. 0049exact hcn
  50. 0050exact hnB
  51. 0051have hcB : exists k. k + x = B
  52. 0052apply le_of_succ_le_succ
  53. 0053exact hcSB
  54. 0054specialize IH x
  55. 0055have hp : exists p. ((~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) /\ exists k. x = p * k)
  56. 0056apply IH
  57. 0057exact hcB
  58. 0058exact hc0
  59. 0059exact hpc_right_witness_witness_left_left
  60. 0060cases hp
  61. 0061cases hp_witness
  62. 0062exists x2
  63. 0063split
  64. 0064exact hp_witness_left
  65. 0065specialize multiple_trans x
  66. 0066specialize multiple_trans x2
  67. 0067specialize multiple_trans n
  68. 0068apply multiple_trans
  69. 0069exists x1
  70. 0070exact hpc_right_witness_witness_right
  71. 0071exact hp_witness_right