prime_seven

Proof neighborhood

Direct dependencies

Direct dependents

Formal native tactic body

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

1. 0001have hn0 : ~(7 = 0)
2. 0002intro hzero
3. 0003apply PA1
4. 0004exact hzero
5. 0005have hn1 : ~(7 = 1)
6. 0006intro hone
7. 0007apply PA1
8. 0008apply PA2
9. 0009exact hone
10. 0010have hsquare : exists bpr_gap_bb8cert_prime_seven_square. bpr_gap_bb8cert_prime_seven_square + S (7) = S 2 * S 2
11. 0011exists 1
12. 0012norm_num
13. 0013specialize prime_of_no_small_prime_divisor_below_square 2
14. 0014specialize prime_of_no_small_prime_divisor_below_square (7)
15. 0015apply prime_of_no_small_prime_divisor_below_square
16. 0016exact hn0
17. 0017exact hn1
18. 0018exact hsquare
19. 0019intro p
20. 0020intro hp
21. 0021intro hp_bound
22. 0022intro hdivides
23. 0023have hbound_22 : exists k. k + 2 = 22
24. 0024exists 20
25. 0025norm_num
26. 0026have hp_22 : exists k. k + p = 22
27. 0027specialize le_trans p
28. 0028specialize le_trans 2
29. 0029specialize le_trans 22
30. 0030apply le_trans
31. 0031exact hp_bound
32. 0032exact hbound_22
33. 0033have hcases : p = 2 \/ (p = 3 \/ (p = 5 \/ (p = 7 \/ (p = 11 \/ (p = 13 \/ (p = 17 \/ (p = 19)))))))
34. 0034specialize prime_le_twenty_two_cases p
35. 0035apply prime_le_twenty_two_cases
36. 0036exact hp
37. 0037exact hp_22
38. 0038cases hcases
39. 0039rewrite hcases_left at hdivides
40. 0040specialize nonzero_remainder_not_multiple 2
41. 0041specialize nonzero_remainder_not_multiple (7)
42. 0042specialize nonzero_remainder_not_multiple 3
43. 0043specialize nonzero_remainder_not_multiple 1
44. 0044apply nonzero_remainder_not_multiple
45. 0045norm_num
46. 0046intro hrem_2_zero
47. 0047apply PA1
48. 0048exact hrem_2_zero
49. 0049exists 0
50. 0050norm_num
51. 0051exact hdivides
52. 0052cases hcases_right
53. 0053have htoo_large_3 : exists k. k + S 2 = 3
54. 0054exists 0
55. 0055norm_num
56. 0056specialize lt_not_le 2
57. 0057specialize lt_not_le 3
58. 0058apply lt_not_le
59. 0059exact htoo_large_3
60. 0060rewrite hcases_right_left at hp_bound
61. 0061exact hp_bound
62. 0062cases hcases_right_right
63. 0063have htoo_large_5 : exists k. k + S 2 = 5
64. 0064exists 2
65. 0065norm_num
66. 0066specialize lt_not_le 2
67. 0067specialize lt_not_le 5
68. 0068apply lt_not_le
69. 0069exact htoo_large_5
70. 0070rewrite hcases_right_right_left at hp_bound
71. 0071exact hp_bound
72. 0072cases hcases_right_right_right
73. 0073have htoo_large_7 : exists k. k + S 2 = 7
74. 0074exists 4
75. 0075norm_num
76. 0076specialize lt_not_le 2
77. 0077specialize lt_not_le 7
78. 0078apply lt_not_le
79. 0079exact htoo_large_7
80. 0080rewrite hcases_right_right_right_left at hp_bound
81. 0081exact hp_bound
82. 0082cases hcases_right_right_right_right
83. 0083have htoo_large_11 : exists k. k + S 2 = 11
84. 0084exists 8
85. 0085norm_num
86. 0086specialize lt_not_le 2
87. 0087specialize lt_not_le 11
88. 0088apply lt_not_le
89. 0089exact htoo_large_11
90. 0090rewrite hcases_right_right_right_right_left at hp_bound
91. 0091exact hp_bound
92. 0092cases hcases_right_right_right_right_right
93. 0093have htoo_large_13 : exists k. k + S 2 = 13
94. 0094exists 10
95. 0095norm_num
96. 0096specialize lt_not_le 2
97. 0097specialize lt_not_le 13
98. 0098apply lt_not_le
99. 0099exact htoo_large_13
100. 0100rewrite hcases_right_right_right_right_right_left at hp_bound
101. 0101exact hp_bound
102. 0102cases hcases_right_right_right_right_right_right
103. 0103have htoo_large_17 : exists k. k + S 2 = 17
104. 0104exists 14
105. 0105norm_num
106. 0106specialize lt_not_le 2
107. 0107specialize lt_not_le 17
108. 0108apply lt_not_le
109. 0109exact htoo_large_17
110. 0110rewrite hcases_right_right_right_right_right_right_left at hp_bound
111. 0111exact hp_bound
112. 0112have htoo_large_19 : exists k. k + S 2 = 19
113. 0113exists 16
114. 0114norm_num
115. 0115specialize lt_not_le 2
116. 0116specialize lt_not_le 19
117. 0117apply lt_not_le
118. 0118exact htoo_large_19
119. 0119rewrite hcases_right_right_right_right_right_right_right at hp_bound
120. 0120exact hp_bound