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 e. Prime /\ P || ( FermatNo ` 4 ) /\ P <_ ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) ) -> ( P = ; 6 5 \/ P = ; ; 1 2 9 \/ P = ; ; 1 9 3 ) )

Proof

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