Metamath Proof Explorer


Theorem fmtno4prmfac

Description: If P was a (prime) factor of the fourth Fermat number less than the square root of the fourth Fermat number, it would be either 65 or 129 or 193. (Contributed by AV, 28-Jul-2021)

Ref Expression
Assertion fmtno4prmfac P P FermatNo 4 P FermatNo 4 P = 65 P = 129 P = 193

Proof

Step Hyp Ref Expression
1 2z 2
2 4z 4
3 2re 2
4 4re 4
5 2lt4 2 < 4
6 3 4 5 ltleii 2 4
7 eluz2 4 2 2 4 2 4
8 1 2 6 7 mpbir3an 4 2
9 fmtnoprmfac2 4 2 P P FermatNo 4 k P = k 2 4 + 2 + 1
10 8 9 mp3an1 P P FermatNo 4 k P = k 2 4 + 2 + 1
11 elnnuz k k 1
12 4nn 4
13 nnuz = 1
14 12 13 eleqtri 4 1
15 fzouzsplit 4 1 1 = 1 ..^ 4 4
16 14 15 ax-mp 1 = 1 ..^ 4 4
17 16 eleq2i k 1 k 1 ..^ 4 4
18 elun k 1 ..^ 4 4 k 1 ..^ 4 k 4
19 fzo1to4tp 1 ..^ 4 = 1 2 3
20 19 eleq2i k 1 ..^ 4 k 1 2 3
21 vex k V
22 21 eltp k 1 2 3 k = 1 k = 2 k = 3
23 20 22 bitri k 1 ..^ 4 k = 1 k = 2 k = 3
24 23 orbi1i k 1 ..^ 4 k 4 k = 1 k = 2 k = 3 k 4
25 18 24 bitri k 1 ..^ 4 4 k = 1 k = 2 k = 3 k 4
26 11 17 25 3bitri k k = 1 k = 2 k = 3 k 4
27 4p2e6 4 + 2 = 6
28 27 oveq2i 2 4 + 2 = 2 6
29 2exp6 2 6 = 64
30 28 29 eqtri 2 4 + 2 = 64
31 30 oveq2i k 2 4 + 2 = k 64
32 31 oveq1i k 2 4 + 2 + 1 = k 64 + 1
33 32 eqeq2i P = k 2 4 + 2 + 1 P = k 64 + 1
34 simpl P = k 64 + 1 k = 1 P = k 64 + 1
35 oveq1 k = 1 k 64 = 1 64
36 6nn0 6 0
37 4nn0 4 0
38 36 37 deccl 64 0
39 38 nn0cni 64
40 39 mulid2i 1 64 = 64
41 35 40 eqtrdi k = 1 k 64 = 64
42 41 oveq1d k = 1 k 64 + 1 = 64 + 1
43 4p1e5 4 + 1 = 5
44 eqid 64 = 64
45 36 37 43 44 decsuc 64 + 1 = 65
46 42 45 eqtrdi k = 1 k 64 + 1 = 65
47 46 adantl P = k 64 + 1 k = 1 k 64 + 1 = 65
48 34 47 eqtrd P = k 64 + 1 k = 1 P = 65
49 48 ex P = k 64 + 1 k = 1 P = 65
50 simpl P = k 64 + 1 k = 2 P = k 64 + 1
51 oveq1 k = 2 k 64 = 2 64
52 2nn0 2 0
53 6cn 6
54 2cn 2
55 6t2e12 6 2 = 12
56 53 54 55 mulcomli 2 6 = 12
57 56 eqcomi 12 = 2 6
58 4cn 4
59 4t2e8 4 2 = 8
60 58 54 59 mulcomli 2 4 = 8
61 60 eqcomi 8 = 2 4
62 36 37 52 57 61 decmul10add 2 64 = 120 + 8
63 51 62 eqtrdi k = 2 k 64 = 120 + 8
64 63 oveq1d k = 2 k 64 + 1 = 120 + 8 + 1
65 1nn0 1 0
66 65 52 deccl 12 0
67 8nn0 8 0
68 8p1e9 8 + 1 = 9
69 0nn0 0 0
70 eqid 120 = 120
71 8cn 8
72 71 addid2i 0 + 8 = 8
73 66 69 67 70 72 decaddi 120 + 8 = 128
74 66 67 68 73 decsuc 120 + 8 + 1 = 129
75 64 74 eqtrdi k = 2 k 64 + 1 = 129
76 75 adantl P = k 64 + 1 k = 2 k 64 + 1 = 129
77 50 76 eqtrd P = k 64 + 1 k = 2 P = 129
78 77 ex P = k 64 + 1 k = 2 P = 129
79 simpl P = k 64 + 1 k = 3 P = k 64 + 1
80 oveq1 k = 3 k 64 = 3 64
81 3nn0 3 0
82 6t3e18 6 3 = 18
83 3cn 3
84 53 83 mulcomi 6 3 = 3 6
85 82 84 eqtr3i 18 = 3 6
86 4t3e12 4 3 = 12
87 58 83 mulcomi 4 3 = 3 4
88 86 87 eqtr3i 12 = 3 4
89 36 37 81 85 88 decmul10add 3 64 = 180 + 12
90 80 89 eqtrdi k = 3 k 64 = 180 + 12
91 90 oveq1d k = 3 k 64 + 1 = 180 + 12 + 1
92 9nn0 9 0
93 65 92 deccl 19 0
94 2p1e3 2 + 1 = 3
95 65 67 deccl 18 0
96 eqid 180 = 180
97 eqid 12 = 12
98 eqid 18 = 18
99 65 67 68 98 decsuc 18 + 1 = 19
100 54 addid2i 0 + 2 = 2
101 95 69 65 52 96 97 99 100 decadd 180 + 12 = 192
102 93 52 94 101 decsuc 180 + 12 + 1 = 193
103 91 102 eqtrdi k = 3 k 64 + 1 = 193
104 103 adantl P = k 64 + 1 k = 3 k 64 + 1 = 193
105 79 104 eqtrd P = k 64 + 1 k = 3 P = 193
106 105 ex P = k 64 + 1 k = 3 P = 193
107 49 78 106 3orim123d P = k 64 + 1 k = 1 k = 2 k = 3 P = 65 P = 129 P = 193
108 107 a1i P FermatNo 4 P = k 64 + 1 k = 1 k = 2 k = 3 P = 65 P = 129 P = 193
109 108 com13 k = 1 k = 2 k = 3 P = k 64 + 1 P FermatNo 4 P = 65 P = 129 P = 193
110 fmtno4sqrt FermatNo 4 = 256
111 110 breq2i P FermatNo 4 P 256
112 breq1 P = k 64 + 1 P 256 k 64 + 1 256
113 112 adantl k 4 P = k 64 + 1 P 256 k 64 + 1 256
114 eluz2 k 4 4 k 4 k
115 6t4e24 6 4 = 24
116 53 58 115 mulcomli 4 6 = 24
117 52 37 43 116 decsuc 4 6 + 1 = 25
118 4t4e16 4 4 = 16
119 37 36 37 44 36 65 117 118 decmul2c 4 64 = 256
120 zre k k
121 38 nn0rei 64
122 36 12 decnncl 64
123 122 nngt0i 0 < 64
124 121 123 pm3.2i 64 0 < 64
125 124 a1i k 64 0 < 64
126 lemul1 4 k 64 0 < 64 4 k 4 64 k 64
127 4 120 125 126 mp3an2i k 4 k 4 64 k 64
128 127 biimpa k 4 k 4 64 k 64
129 119 128 eqbrtrrid k 4 k 256 k 64
130 5nn0 5 0
131 52 130 deccl 25 0
132 131 36 deccl 256 0
133 132 nn0zi 256
134 id k k
135 38 nn0zi 64
136 135 a1i k 64
137 134 136 zmulcld k k 64
138 137 adantr k 4 k k 64
139 zleltp1 256 k 64 256 k 64 256 < k 64 + 1
140 133 138 139 sylancr k 4 k 256 k 64 256 < k 64 + 1
141 129 140 mpbid k 4 k 256 < k 64 + 1
142 141 3adant1 4 k 4 k 256 < k 64 + 1
143 114 142 sylbi k 4 256 < k 64 + 1
144 132 nn0rei 256
145 144 a1i k 4 256
146 eluzelre k 4 k
147 121 a1i k 4 64
148 146 147 remulcld k 4 k 64
149 peano2re k 64 k 64 + 1
150 148 149 syl k 4 k 64 + 1
151 145 150 ltnled k 4 256 < k 64 + 1 ¬ k 64 + 1 256
152 143 151 mpbid k 4 ¬ k 64 + 1 256
153 152 pm2.21d k 4 k 64 + 1 256 P = 65 P = 129 P = 193
154 153 adantr k 4 P = k 64 + 1 k 64 + 1 256 P = 65 P = 129 P = 193
155 113 154 sylbid k 4 P = k 64 + 1 P 256 P = 65 P = 129 P = 193
156 111 155 syl5bi k 4 P = k 64 + 1 P FermatNo 4 P = 65 P = 129 P = 193
157 156 ex k 4 P = k 64 + 1 P FermatNo 4 P = 65 P = 129 P = 193
158 109 157 jaoi k = 1 k = 2 k = 3 k 4 P = k 64 + 1 P FermatNo 4 P = 65 P = 129 P = 193
159 158 adantr k = 1 k = 2 k = 3 k 4 P P FermatNo 4 P = k 64 + 1 P FermatNo 4 P = 65 P = 129 P = 193
160 33 159 syl5bi k = 1 k = 2 k = 3 k 4 P P FermatNo 4 P = k 2 4 + 2 + 1 P FermatNo 4 P = 65 P = 129 P = 193
161 160 ex k = 1 k = 2 k = 3 k 4 P P FermatNo 4 P = k 2 4 + 2 + 1 P FermatNo 4 P = 65 P = 129 P = 193
162 26 161 sylbi k P P FermatNo 4 P = k 2 4 + 2 + 1 P FermatNo 4 P = 65 P = 129 P = 193
163 162 com12 P P FermatNo 4 k P = k 2 4 + 2 + 1 P FermatNo 4 P = 65 P = 129 P = 193
164 163 rexlimdv P P FermatNo 4 k P = k 2 4 + 2 + 1 P FermatNo 4 P = 65 P = 129 P = 193
165 10 164 mpd P P FermatNo 4 P FermatNo 4 P = 65 P = 129 P = 193
166 165 3impia P P FermatNo 4 P FermatNo 4 P = 65 P = 129 P = 193