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 e. Prime

Proof

Step Hyp Ref Expression
1 2nn0 
 |-  2 e. NN0
2 5nn0 
 |-  5 e. NN0
3 1 2 deccl 
 |-  ; 2 5 e. NN0
4 7nn 
 |-  7 e. NN
5 3 4 decnncl 
 |-  ; ; 2 5 7 e. NN
6 8nn0 
 |-  8 e. NN0
7 4nn0 
 |-  4 e. NN0
8 7nn0 
 |-  7 e. NN0
9 1nn0 
 |-  1 e. NN0
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 e. NN
15 1 14 decnncl 
 |-  ; 2 5 e. NN
16 1lt10 
 |-  1 < ; 1 0
17 15 8 9 16 declti 
 |-  1 < ; ; 2 5 7
18 3nn0 
 |-  3 e. NN0
19 3t2e6 
 |-  ( 3 x. 2 ) = 6
20 df-7 
 |-  7 = ( 6 + 1 )
21 3 18 19 20 dec2dvds 
 |-  -. 2 || ; ; 2 5 7
22 3nn 
 |-  3 e. NN
23 2nn 
 |-  2 e. NN
24 3cn 
 |-  3 e. CC
25 24 mulridi 
 |-  ( 3 x. 1 ) = 3
26 25 oveq1i 
 |-  ( ( 3 x. 1 ) + 2 ) = ( 3 + 2 )
27 3p2e5 
 |-  ( 3 + 2 ) = 5
28 26 27 eqtri 
 |-  ( ( 3 x. 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 e. CC
33 2cn 
 |-  2 e. CC
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 e. CC
42 ax-1cn 
 |-  1 e. CC
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 e. NN0
52 18 51 deccl 
 |-  ; 3 6 e. NN0
53 eqid 
 |-  ; 3 6 = ; 3 6
54 7t3e21 
 |-  ( 7 x. 3 ) = ; 2 1
55 1 9 7 54 44 decaddi 
 |-  ( ( 7 x. 3 ) + 4 ) = ; 2 5
56 7t6e42 
 |-  ( 7 x. 6 ) = ; 4 2
57 8 18 51 53 1 7 55 56 decmul2c 
 |-  ( 7 x. ; 3 6 ) = ; ; 2 5 2
58 3 1 2 57 35 decaddi 
 |-  ( ( 7 x. ; 3 6 ) + 5 ) = ; ; 2 5 7
59 5lt7 
 |-  5 < 7
60 4 52 14 58 59 ndvdsi 
 |-  -. 7 || ; ; 2 5 7
61 1nn 
 |-  1 e. NN
62 9 61 decnncl 
 |-  ; 1 1 e. NN
63 1 18 deccl 
 |-  ; 2 3 e. NN0
64 4nn 
 |-  4 e. NN
65 9 9 deccl 
 |-  ; 1 1 e. NN0
66 eqid 
 |-  ; 2 3 = ; 2 3
67 65 nn0cni 
 |-  ; 1 1 e. CC
68 67 33 mulcomi 
 |-  ( ; 1 1 x. 2 ) = ( 2 x. ; 1 1 )
69 68 oveq1i 
 |-  ( ( ; 1 1 x. 2 ) + 3 ) = ( ( 2 x. ; 1 1 ) + 3 )
70 1 11multnc 
 |-  ( 2 x. ; 1 1 ) = ; 2 2
71 24 33 27 addcomli 
 |-  ( 2 + 3 ) = 5
72 1 1 18 70 71 decaddi 
 |-  ( ( 2 x. ; 1 1 ) + 3 ) = ; 2 5
73 69 72 eqtri 
 |-  ( ( ; 1 1 x. 2 ) + 3 ) = ; 2 5
74 18 11multnc 
 |-  ( 3 x. ; 1 1 ) = ; 3 3
75 24 67 74 mulcomli 
 |-  ( ; 1 1 x. 3 ) = ; 3 3
76 65 1 18 66 18 18 73 75 decmul2c 
 |-  ( ; 1 1 x. ; 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 x. ; 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 e. NN
84 9nn0 
 |-  9 e. NN0
85 9 84 deccl 
 |-  ; 1 9 e. NN0
86 10nn 
 |-  ; 1 0 e. NN
87 9 18 deccl 
 |-  ; 1 3 e. NN0
88 87 nn0cni 
 |-  ; 1 3 e. CC
89 85 nn0cni 
 |-  ; 1 9 e. CC
90 88 89 mulcomi 
 |-  ( ; 1 3 x. ; 1 9 ) = ( ; 1 9 x. ; 1 3 )
91 90 oveq1i 
 |-  ( ( ; 1 3 x. ; 1 9 ) + ; 1 0 ) = ( ( ; 1 9 x. ; 1 3 ) + ; 1 0 )
92 0nn0 
 |-  0 e. NN0
93 eqid 
 |-  ; 1 9 = ; 1 9
94 eqid 
 |-  ; 1 0 = ; 1 0
95 88 mullidi 
 |-  ( 1 x. ; 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 x. ; 1 3 ) + ( 1 + ; 1 1 ) ) = ; 2 5
101 eqid 
 |-  ; 1 3 = ; 1 3
102 9cn 
 |-  9 e. CC
103 102 mulridi 
 |-  ( 9 x. 1 ) = 9
104 103 oveq1i 
 |-  ( ( 9 x. 1 ) + 2 ) = ( 9 + 2 )
105 9p2e11 
 |-  ( 9 + 2 ) = ; 1 1
106 104 105 eqtri 
 |-  ( ( 9 x. 1 ) + 2 ) = ; 1 1
107 9t3e27 
 |-  ( 9 x. 3 ) = ; 2 7
108 84 9 18 101 8 1 106 107 decmul2c 
 |-  ( 9 x. ; 1 3 ) = ; ; 1 1 7
109 108 oveq1i 
 |-  ( ( 9 x. ; 1 3 ) + 0 ) = ( ; ; 1 1 7 + 0 )
110 65 8 deccl 
 |-  ; ; 1 1 7 e. NN0
111 110 nn0cni 
 |-  ; ; 1 1 7 e. CC
112 111 addridi 
 |-  ( ; ; 1 1 7 + 0 ) = ; ; 1 1 7
113 109 112 eqtri 
 |-  ( ( 9 x. ; 1 3 ) + 0 ) = ; ; 1 1 7
114 9 84 9 92 93 94 87 8 65 100 113 decmac 
 |-  ( ( ; 1 9 x. ; 1 3 ) + ; 1 0 ) = ; ; 2 5 7
115 91 114 eqtri 
 |-  ( ( ; 1 3 x. ; 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 e. NN
120 9 2 deccl 
 |-  ; 1 5 e. NN0
121 9 8 deccl 
 |-  ; 1 7 e. NN0
122 eqid 
 |-  ; 1 5 = ; 1 5
123 121 nn0cni 
 |-  ; 1 7 e. CC
124 123 mulridi 
 |-  ( ; 1 7 x. 1 ) = ; 1 7
125 8cn 
 |-  8 e. CC
126 7cn 
 |-  7 e. CC
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 x. 1 ) + 8 ) = ; 2 5
130 eqid 
 |-  ; 1 7 = ; 1 7
131 32 mullidi 
 |-  ( 1 x. 5 ) = 5
132 131 oveq1i 
 |-  ( ( 1 x. 5 ) + 3 ) = ( 5 + 3 )
133 5p3e8 
 |-  ( 5 + 3 ) = 8
134 132 133 eqtri 
 |-  ( ( 1 x. 5 ) + 3 ) = 8
135 7t5e35 
 |-  ( 7 x. 5 ) = ; 3 5
136 2 9 8 130 2 18 134 135 decmul1c 
 |-  ( ; 1 7 x. 5 ) = ; 8 5
137 121 9 2 122 2 6 129 136 decmul2c 
 |-  ( ; 1 7 x. ; 1 5 ) = ; ; 2 5 5
138 3 2 1 137 34 decaddi 
 |-  ( ( ; 1 7 x. ; 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 e. NN
143 9 142 decnncl 
 |-  ; 1 9 e. NN
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 e. NN
148 65 1 18 66 18 18 72 74 decmul1c 
 |-  ( ; 2 3 x. ; 1 1 ) = ; ; 2 5 3
149 3 18 7 148 78 decaddi 
 |-  ( ( ; 2 3 x. ; 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 e. Prime