BT006N

prime_three

Stable · empty-context checked

Three is prime in the expanded first-order prime predicate.

Exact expanded PA statement

~(3 = 1) /\ forall a b. 3 = a * b -> a = 1 \/ b = 1

Structural proof guide

Three is prime in the expanded first-order prime predicate.

Direct prerequisites: mul_succ_left, mul_eq_one_components, add_eq_zero_left, mul_eq_zero, mul_zero_left, zero_or_succ. The authored body proceeds by structural induction (4), case analysis (4), intermediate claims (11), equality transport (11).

Proof neighborhood

Direct dependencies

BT0005 mul_succ_left BT0020 mul_eq_one_components BT001X add_eq_zero_left BT000M mul_eq_zero BT0004 mul_zero_left BT000Q zero_or_succ

Direct dependents

BT0124 bertrand_small_closed_upper

Formal native tactic body

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

  1. 0001have hlarge : forall x y. ~(3 = S (S x) * S (S y))
  2. 0002intro x
  3. 0003intro y
  4. 0004intro hlarge_eq
  5. 0005specialize mul_succ_left (S x)
  6. 0006specialize mul_succ_left (S (S y))
  7. 0007rewrite mul_succ_left at hlarge_eq
  8. 0008rewrite PA4 at hlarge_eq
  9. 0009rewrite PA4 at hlarge_eq
  10. 0010have hone : 1 = S x * S (S y) + y
  11. 0011apply PA2
  12. 0012apply PA2
  13. 0013exact hlarge_eq
  14. 0014have hysplit : y = 0 \/ exists z. y = S z
  15. 0015specialize zero_or_succ y
  16. 0016exact zero_or_succ
  17. 0017cases hysplit
  18. 0018rewrite hysplit_left at hone
  19. 0019rewrite hysplit_left at hone
  20. 0020rewrite PA3 at hone
  21. 0021have hprod_one : S x * S (S 0) = 1
  22. 0022symm
  23. 0023exact hone
  24. 0024have hcomponents : S x = 1 /\ S (S 0) = 1
  25. 0025specialize mul_eq_one_components (S x)
  26. 0026specialize mul_eq_one_components (S (S 0))
  27. 0027apply mul_eq_one_components
  28. 0028exact hprod_one
  29. 0029cases hcomponents
  30. 0030have h10 : 1 = 0
  31. 0031apply PA2
  32. 0032exact hcomponents_right
  33. 0033apply PA1
  34. 0034exact h10
  35. 0035cases hysplit_right
  36. 0036rewrite hysplit_right_witness at hone
  37. 0037rewrite hysplit_right_witness at hone
  38. 0038rewrite PA4 at hone
  39. 0039have hzero : 0 = S x * S (S (S x1)) + x1
  40. 0040apply PA2
  41. 0041exact hone
  42. 0042have hsumzero : S x * S (S (S x1)) + x1 = 0
  43. 0043symm
  44. 0044exact hzero
  45. 0045have hprodzero : S x * S (S (S x1)) = 0
  46. 0046specialize add_eq_zero_left (S x * S (S (S x1)))
  47. 0047specialize add_eq_zero_left x1
  48. 0048apply add_eq_zero_left
  49. 0049exact hsumzero
  50. 0050have hfactors : S x = 0 \/ S (S (S x1)) = 0
  51. 0051specialize mul_eq_zero (S x)
  52. 0052specialize mul_eq_zero (S (S (S x1)))
  53. 0053apply mul_eq_zero
  54. 0054exact hprodzero
  55. 0055cases hfactors
  56. 0056apply PA1
  57. 0057exact hfactors_left
  58. 0058apply PA1
  59. 0059exact hfactors_right
  60. 0060split
  61. 0061intro h31
  62. 0062have h20 : 2 = 0
  63. 0063apply PA2
  64. 0064exact h31
  65. 0065apply PA1
  66. 0066exact h20
  67. 0067intro a
  68. 0068induction b
  69. 0069intro hab
  70. 0070rewrite PA5 at hab
  71. 0071exfalso
  72. 0072apply PA1
  73. 0073exact hab
  74. 0074induction b
  75. 0075intro hab
  76. 0076right
  77. 0077refl
  78. 0078induction a
  79. 0079intro hab
  80. 0080specialize mul_zero_left (S (S b))
  81. 0081rewrite mul_zero_left at hab
  82. 0082exfalso
  83. 0083apply PA1
  84. 0084exact hab
  85. 0085induction a
  86. 0086intro hab
  87. 0087left
  88. 0088refl
  89. 0089intro hab
  90. 0090exfalso
  91. 0091specialize hlarge a
  92. 0092specialize hlarge b
  93. 0093apply hlarge
  94. 0094exact hab