Metamath Proof Explorer

Theorem 257prm

Description: 257 is a prime number (thefourth Fermat prime). (Contributed by AV, 15-Jun-2021)

Ref Expression
Assertion 257prm 2 5 7 ∈ ℙ

Proof

Step Hyp Ref Expression
1 2nn0 ⊢ 2 ∈ ℕ0
2 5nn0 ⊢ 5 ∈ ℕ0
3 1 2 deccl ⊢ 2 5 ∈ ℕ0
4 7nn ⊢ 7 ∈ ℕ
5 3 4 decnncl ⊢ 2 5 7 ∈ ℕ
6 8nn0 ⊢ 8 ∈ ℕ0
7 4nn0 ⊢ 4 ∈ ℕ0
8 7nn0 ⊢ 7 ∈ ℕ0
9 1nn0 ⊢ 1 ∈ ℕ0
10 2lt8 ⊢ 2 < 8
11 5lt10 ⊢ 5 < 1 0
12 7lt10 ⊢ 7 < 1 0
13 1 6 2 7 8 9 10 11 12 3decltc ⊢ 2 5 7 < 8 4 1
14 5nn ⊢ 5 ∈ ℕ
15 1 14 decnncl ⊢ 2 5 ∈ ℕ
16 1lt10 ⊢ 1 < 1 0
17 15 8 9 16 declti ⊢ 1 < 2 5 7
18 3nn0 ⊢ 3 ∈ ℕ0
19 3t2e6 ⊢ ( 3 · 2 ) = 6
20 df-7 ⊢ 7 = ( 6 + 1 )
21 3 18 19 20 dec2dvds ⊢ ¬ 2 ∥ 2 5 7
22 3nn ⊢ 3 ∈ ℕ
23 2nn ⊢ 2 ∈ ℕ
24 3cn ⊢ 3 ∈ ℂ
25 24 mulid1i ⊢ ( 3 · 1 ) = 3
26 25 oveq1i ⊢ ( ( 3 · 1 ) + 2 ) = ( 3 + 2 )
27 3p2e5 ⊢ ( 3 + 2 ) = 5
28 26 27 eqtri ⊢ ( ( 3 · 1 ) + 2 ) = 5
29 2lt3 ⊢ 2 < 3
30 22 9 23 28 29 ndvdsi ⊢ ¬ 3 ∥ 5
31 1 2 8 3dvds2dec ⊢ ( 3 ∥ 2 5 7 ↔ 3 ∥ ( ( 2 + 5 ) + 7 ) )
32 5cn ⊢ 5 ∈ ℂ
33 2cn ⊢ 2 ∈ ℂ
34 5p2e7 ⊢ ( 5 + 2 ) = 7
35 32 33 34 addcomli ⊢ ( 2 + 5 ) = 7
36 35 oveq1i ⊢ ( ( 2 + 5 ) + 7 ) = ( 7 + 7 )
37 7p7e14 ⊢ ( 7 + 7 ) = 1 4
38 36 37 eqtri ⊢ ( ( 2 + 5 ) + 7 ) = 1 4
39 38 breq2i ⊢ ( 3 ∥ ( ( 2 + 5 ) + 7 ) ↔ 3 ∥ 1 4 )
40 9 7 3dvdsdec ⊢ ( 3 ∥ 1 4 ↔ 3 ∥ ( 1 + 4 ) )
41 4cn ⊢ 4 ∈ ℂ
42 ax-1cn ⊢ 1 ∈ ℂ
43 4p1e5 ⊢ ( 4 + 1 ) = 5
44 41 42 43 addcomli ⊢ ( 1 + 4 ) = 5
45 44 breq2i ⊢ ( 3 ∥ ( 1 + 4 ) ↔ 3 ∥ 5 )
46 40 45 bitri ⊢ ( 3 ∥ 1 4 ↔ 3 ∥ 5 )
47 31 39 46 3bitri ⊢ ( 3 ∥ 2 5 7 ↔ 3 ∥ 5 )
48 30 47 mtbir ⊢ ¬ 3 ∥ 2 5 7
49 2lt5 ⊢ 2 < 5
50 3 23 49 34 dec5dvds2 ⊢ ¬ 5 ∥ 2 5 7
51 6nn0 ⊢ 6 ∈ ℕ0
52 18 51 deccl ⊢ 3 6 ∈ ℕ0
53 eqid ⊢ 3 6 = 3 6
54 7t3e21 ⊢ ( 7 · 3 ) = 2 1
55 1 9 7 54 44 decaddi ⊢ ( ( 7 · 3 ) + 4 ) = 2 5
56 7t6e42 ⊢ ( 7 · 6 ) = 4 2
57 8 18 51 53 1 7 55 56 decmul2c ⊢ ( 7 · 3 6 ) = 2 5 2
58 3 1 2 57 35 decaddi ⊢ ( ( 7 · 3 6 ) + 5 ) = 2 5 7
59 5lt7 ⊢ 5 < 7
60 4 52 14 58 59 ndvdsi ⊢ ¬ 7 ∥ 2 5 7
61 1nn ⊢ 1 ∈ ℕ
62 9 61 decnncl ⊢ 1 1 ∈ ℕ
63 1 18 deccl ⊢ 2 3 ∈ ℕ0
64 4nn ⊢ 4 ∈ ℕ
65 9 9 deccl ⊢ 1 1 ∈ ℕ0
66 eqid ⊢ 2 3 = 2 3
67 65 nn0cni ⊢ 1 1 ∈ ℂ
68 67 33 mulcomi ⊢ ( 1 1 · 2 ) = ( 2 · 1 1 )
69 68 oveq1i ⊢ ( ( 1 1 · 2 ) + 3 ) = ( ( 2 · 1 1 ) + 3 )
70 1 11multnc ⊢ ( 2 · 1 1 ) = 2 2
71 24 33 27 addcomli ⊢ ( 2 + 3 ) = 5
72 1 1 18 70 71 decaddi ⊢ ( ( 2 · 1 1 ) + 3 ) = 2 5
73 69 72 eqtri ⊢ ( ( 1 1 · 2 ) + 3 ) = 2 5
74 18 11multnc ⊢ ( 3 · 1 1 ) = 3 3
75 24 67 74 mulcomli ⊢ ( 1 1 · 3 ) = 3 3
76 65 1 18 66 18 18 73 75 decmul2c ⊢ ( 1 1 · 2 3 ) = 2 5 3
77 4p3e7 ⊢ ( 4 + 3 ) = 7
78 41 24 77 addcomli ⊢ ( 3 + 4 ) = 7
79 3 18 7 76 78 decaddi ⊢ ( ( 1 1 · 2 3 ) + 4 ) = 2 5 7
80 4lt10 ⊢ 4 < 1 0
81 61 9 7 80 declti ⊢ 4 < 1 1
82 62 63 64 79 81 ndvdsi ⊢ ¬ 1 1 ∥ 2 5 7
83 9 22 decnncl ⊢ 1 3 ∈ ℕ
84 9nn0 ⊢ 9 ∈ ℕ0
85 9 84 deccl ⊢ 1 9 ∈ ℕ0
86 10nn ⊢ 1 0 ∈ ℕ
87 9 18 deccl ⊢ 1 3 ∈ ℕ0
88 87 nn0cni ⊢ 1 3 ∈ ℂ
89 85 nn0cni ⊢ 1 9 ∈ ℂ
90 88 89 mulcomi ⊢ ( 1 3 · 1 9 ) = ( 1 9 · 1 3 )
91 90 oveq1i ⊢ ( ( 1 3 · 1 9 ) + 1 0 ) = ( ( 1 9 · 1 3 ) + 1 0 )
92 0nn0 ⊢ 0 ∈ ℕ0
93 eqid ⊢ 1 9 = 1 9
94 eqid ⊢ 1 0 = 1 0
95 88 mulid2i ⊢ ( 1 · 1 3 ) = 1 3
96 1p1e2 ⊢ ( 1 + 1 ) = 2
97 eqid ⊢ 1 1 = 1 1
98 9 9 96 97 decsuc ⊢ ( 1 1 + 1 ) = 1 2
99 67 42 98 addcomli ⊢ ( 1 + 1 1 ) = 1 2
100 9 18 9 1 95 99 96 27 decadd ⊢ ( ( 1 · 1 3 ) + ( 1 + 1 1 ) ) = 2 5
101 eqid ⊢ 1 3 = 1 3
102 9cn ⊢ 9 ∈ ℂ
103 102 mulid1i ⊢ ( 9 · 1 ) = 9
104 103 oveq1i ⊢ ( ( 9 · 1 ) + 2 ) = ( 9 + 2 )
105 9p2e11 ⊢ ( 9 + 2 ) = 1 1
106 104 105 eqtri ⊢ ( ( 9 · 1 ) + 2 ) = 1 1
107 9t3e27 ⊢ ( 9 · 3 ) = 2 7
108 84 9 18 101 8 1 106 107 decmul2c ⊢ ( 9 · 1 3 ) = 1 1 7
109 108 oveq1i ⊢ ( ( 9 · 1 3 ) + 0 ) = ( 1 1 7 + 0 )
110 65 8 deccl ⊢ 1 1 7 ∈ ℕ0
111 110 nn0cni ⊢ 1 1 7 ∈ ℂ
112 111 addid1i ⊢ ( 1 1 7 + 0 ) = 1 1 7
113 109 112 eqtri ⊢ ( ( 9 · 1 3 ) + 0 ) = 1 1 7
114 9 84 9 92 93 94 87 8 65 100 113 decmac ⊢ ( ( 1 9 · 1 3 ) + 1 0 ) = 2 5 7
115 91 114 eqtri ⊢ ( ( 1 3 · 1 9 ) + 1 0 ) = 2 5 7
116 3pos ⊢ 0 < 3
117 9 92 22 116 declt ⊢ 1 0 < 1 3
118 83 85 86 115 117 ndvdsi ⊢ ¬ 1 3 ∥ 2 5 7
119 9 4 decnncl ⊢ 1 7 ∈ ℕ
120 9 2 deccl ⊢ 1 5 ∈ ℕ0
121 9 8 deccl ⊢ 1 7 ∈ ℕ0
122 eqid ⊢ 1 5 = 1 5
123 121 nn0cni ⊢ 1 7 ∈ ℂ
124 123 mulid1i ⊢ ( 1 7 · 1 ) = 1 7
125 8cn ⊢ 8 ∈ ℂ
126 7cn ⊢ 7 ∈ ℂ
127 8p7e15 ⊢ ( 8 + 7 ) = 1 5
128 125 126 127 addcomli ⊢ ( 7 + 8 ) = 1 5
129 9 8 6 124 96 2 128 decaddci ⊢ ( ( 1 7 · 1 ) + 8 ) = 2 5
130 eqid ⊢ 1 7 = 1 7
131 32 mulid2i ⊢ ( 1 · 5 ) = 5
132 131 oveq1i ⊢ ( ( 1 · 5 ) + 3 ) = ( 5 + 3 )
133 5p3e8 ⊢ ( 5 + 3 ) = 8
134 132 133 eqtri ⊢ ( ( 1 · 5 ) + 3 ) = 8
135 7t5e35 ⊢ ( 7 · 5 ) = 3 5
136 2 9 8 130 2 18 134 135 decmul1c ⊢ ( 1 7 · 5 ) = 8 5
137 121 9 2 122 2 6 129 136 decmul2c ⊢ ( 1 7 · 1 5 ) = 2 5 5
138 3 2 1 137 34 decaddi ⊢ ( ( 1 7 · 1 5 ) + 2 ) = 2 5 7
139 2lt10 ⊢ 2 < 1 0
140 61 8 1 139 declti ⊢ 2 < 1 7
141 119 120 23 138 140 ndvdsi ⊢ ¬ 1 7 ∥ 2 5 7
142 9nn ⊢ 9 ∈ ℕ
143 9 142 decnncl ⊢ 1 9 ∈ ℕ
144 9pos ⊢ 0 < 9
145 9 92 142 144 declt ⊢ 1 0 < 1 9
146 143 87 86 114 145 ndvdsi ⊢ ¬ 1 9 ∥ 2 5 7
147 1 22 decnncl ⊢ 2 3 ∈ ℕ
148 65 1 18 66 18 18 72 74 decmul1c ⊢ ( 2 3 · 1 1 ) = 2 5 3
149 3 18 7 148 78 decaddi ⊢ ( ( 2 3 · 1 1 ) + 4 ) = 2 5 7
150 23 18 7 80 declti ⊢ 4 < 2 3
151 147 65 64 149 150 ndvdsi ⊢ ¬ 2 3 ∥ 2 5 7
152 5 13 17 21 48 50 60 82 118 141 146 151 prmlem2 ⊢ 2 5 7 ∈ ℙ