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 ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ∧ 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) )

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 ) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 4 + 2 ) ) ) + 1 ) )
10 8 9 mp3an1 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) → ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 4 + 2 ) ) ) + 1 ) )
11 elnnuz ⊢ ( 𝑘 ∈ ℕ ↔ 𝑘 ∈ ( ℤ≥ ‘ 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 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) ↔ 𝑘 ∈ ( ( 1 ..^ 4 ) ∪ ( ℤ≥ ‘ 4 ) ) )
18 elun ⊢ ( 𝑘 ∈ ( ( 1 ..^ 4 ) ∪ ( ℤ≥ ‘ 4 ) ) ↔ ( 𝑘 ∈ ( 1 ..^ 4 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) )
19 fzo1to4tp ⊢ ( 1 ..^ 4 ) = { 1 , 2 , 3 }
20 19 eleq2i ⊢ ( 𝑘 ∈ ( 1 ..^ 4 ) ↔ 𝑘 ∈ { 1 , 2 , 3 } )
21 vex ⊢ 𝑘 ∈ V
22 21 eltp ⊢ ( 𝑘 ∈ { 1 , 2 , 3 } ↔ ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) )
23 20 22 bitri ⊢ ( 𝑘 ∈ ( 1 ..^ 4 ) ↔ ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) )
24 23 orbi1i ⊢ ( ( 𝑘 ∈ ( 1 ..^ 4 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) ↔ ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) )
25 18 24 bitri ⊢ ( 𝑘 ∈ ( ( 1 ..^ 4 ) ∪ ( ℤ≥ ‘ 4 ) ) ↔ ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) )
26 11 17 25 3bitri ⊢ ( 𝑘 ∈ ℕ ↔ ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 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 ⊢ ( 𝑘 · ( 2 ↑ ( 4 + 2 ) ) ) = ( 𝑘 · 6 4 )
32 31 oveq1i ⊢ ( ( 𝑘 · ( 2 ↑ ( 4 + 2 ) ) ) + 1 ) = ( ( 𝑘 · 6 4 ) + 1 )
33 32 eqeq2i ⊢ ( 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 4 + 2 ) ) ) + 1 ) ↔ 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) )
34 simpl ⊢ ( ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ∧ 𝑘 = 1 ) → 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) )
35 oveq1 ⊢ ( 𝑘 = 1 → ( 𝑘 · 6 4 ) = ( 1 · 6 4 ) )
36 6nn0 ⊢ 6 ∈ ℕ0
37 4nn0 ⊢ 4 ∈ ℕ0
38 36 37 deccl ⊢ 6 4 ∈ ℕ0
39 38 nn0cni ⊢ 6 4 ∈ ℂ
40 39 mulid2i ⊢ ( 1 · 6 4 ) = 6 4
41 35 40 eqtrdi ⊢ ( 𝑘 = 1 → ( 𝑘 · 6 4 ) = 6 4 )
42 41 oveq1d ⊢ ( 𝑘 = 1 → ( ( 𝑘 · 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 ⊢ ( 𝑘 = 1 → ( ( 𝑘 · 6 4 ) + 1 ) = 6 5 )
47 46 adantl ⊢ ( ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ∧ 𝑘 = 1 ) → ( ( 𝑘 · 6 4 ) + 1 ) = 6 5 )
48 34 47 eqtrd ⊢ ( ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ∧ 𝑘 = 1 ) → 𝑃 = 6 5 )
49 48 ex ⊢ ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( 𝑘 = 1 → 𝑃 = 6 5 ) )
50 simpl ⊢ ( ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ∧ 𝑘 = 2 ) → 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) )
51 oveq1 ⊢ ( 𝑘 = 2 → ( 𝑘 · 6 4 ) = ( 2 · 6 4 ) )
52 2nn0 ⊢ 2 ∈ ℕ0
53 6cn ⊢ 6 ∈ ℂ
54 2cn ⊢ 2 ∈ ℂ
55 6t2e12 ⊢ ( 6 · 2 ) = 1 2
56 53 54 55 mulcomli ⊢ ( 2 · 6 ) = 1 2
57 56 eqcomi ⊢ 1 2 = ( 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 · 6 4 ) = ( 1 2 0 + 8 )
63 51 62 eqtrdi ⊢ ( 𝑘 = 2 → ( 𝑘 · 6 4 ) = ( 1 2 0 + 8 ) )
64 63 oveq1d ⊢ ( 𝑘 = 2 → ( ( 𝑘 · 6 4 ) + 1 ) = ( ( 1 2 0 + 8 ) + 1 ) )
65 1nn0 ⊢ 1 ∈ ℕ0
66 65 52 deccl ⊢ 1 2 ∈ ℕ0
67 8nn0 ⊢ 8 ∈ ℕ0
68 8p1e9 ⊢ ( 8 + 1 ) = 9
69 0nn0 ⊢ 0 ∈ ℕ0
70 eqid ⊢ 1 2 0 = 1 2 0
71 8cn ⊢ 8 ∈ ℂ
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 ⊢ ( 𝑘 = 2 → ( ( 𝑘 · 6 4 ) + 1 ) = 1 2 9 )
76 75 adantl ⊢ ( ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ∧ 𝑘 = 2 ) → ( ( 𝑘 · 6 4 ) + 1 ) = 1 2 9 )
77 50 76 eqtrd ⊢ ( ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ∧ 𝑘 = 2 ) → 𝑃 = 1 2 9 )
78 77 ex ⊢ ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( 𝑘 = 2 → 𝑃 = 1 2 9 ) )
79 simpl ⊢ ( ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ∧ 𝑘 = 3 ) → 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) )
80 oveq1 ⊢ ( 𝑘 = 3 → ( 𝑘 · 6 4 ) = ( 3 · 6 4 ) )
81 3nn0 ⊢ 3 ∈ ℕ0
82 6t3e18 ⊢ ( 6 · 3 ) = 1 8
83 3cn ⊢ 3 ∈ ℂ
84 53 83 mulcomi ⊢ ( 6 · 3 ) = ( 3 · 6 )
85 82 84 eqtr3i ⊢ 1 8 = ( 3 · 6 )
86 4t3e12 ⊢ ( 4 · 3 ) = 1 2
87 58 83 mulcomi ⊢ ( 4 · 3 ) = ( 3 · 4 )
88 86 87 eqtr3i ⊢ 1 2 = ( 3 · 4 )
89 36 37 81 85 88 decmul10add ⊢ ( 3 · 6 4 ) = ( 1 8 0 + 1 2 )
90 80 89 eqtrdi ⊢ ( 𝑘 = 3 → ( 𝑘 · 6 4 ) = ( 1 8 0 + 1 2 ) )
91 90 oveq1d ⊢ ( 𝑘 = 3 → ( ( 𝑘 · 6 4 ) + 1 ) = ( ( 1 8 0 + 1 2 ) + 1 ) )
92 9nn0 ⊢ 9 ∈ ℕ0
93 65 92 deccl ⊢ 1 9 ∈ ℕ0
94 2p1e3 ⊢ ( 2 + 1 ) = 3
95 65 67 deccl ⊢ 1 8 ∈ ℕ0
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 ⊢ ( 𝑘 = 3 → ( ( 𝑘 · 6 4 ) + 1 ) = 1 9 3 )
104 103 adantl ⊢ ( ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ∧ 𝑘 = 3 ) → ( ( 𝑘 · 6 4 ) + 1 ) = 1 9 3 )
105 79 104 eqtrd ⊢ ( ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ∧ 𝑘 = 3 ) → 𝑃 = 1 9 3 )
106 105 ex ⊢ ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( 𝑘 = 3 → 𝑃 = 1 9 3 ) )
107 49 78 106 3orim123d ⊢ ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) )
108 107 a1i ⊢ ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) )
109 108 com13 ⊢ ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) → ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) )
110 fmtno4sqrt ⊢ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) = 2 5 6
111 110 breq2i ⊢ ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ↔ 𝑃 ≤ 2 5 6 )
112 breq1 ⊢ ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( 𝑃 ≤ 2 5 6 ↔ ( ( 𝑘 · 6 4 ) + 1 ) ≤ 2 5 6 ) )
113 112 adantl ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ) → ( 𝑃 ≤ 2 5 6 ↔ ( ( 𝑘 · 6 4 ) + 1 ) ≤ 2 5 6 ) )
114 eluz2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ↔ ( 4 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 4 ≤ 𝑘 ) )
115 6t4e24 ⊢ ( 6 · 4 ) = 2 4
116 53 58 115 mulcomli ⊢ ( 4 · 6 ) = 2 4
117 52 37 43 116 decsuc ⊢ ( ( 4 · 6 ) + 1 ) = 2 5
118 4t4e16 ⊢ ( 4 · 4 ) = 1 6
119 37 36 37 44 36 65 117 118 decmul2c ⊢ ( 4 · 6 4 ) = 2 5 6
120 zre ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
121 38 nn0rei ⊢ 6 4 ∈ ℝ
122 36 12 decnncl ⊢ 6 4 ∈ ℕ
123 122 nngt0i ⊢ 0 < 6 4
124 121 123 pm3.2i ⊢ ( 6 4 ∈ ℝ ∧ 0 < 6 4 )
125 124 a1i ⊢ ( 𝑘 ∈ ℤ → ( 6 4 ∈ ℝ ∧ 0 < 6 4 ) )
126 lemul1 ⊢ ( ( 4 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ ( 6 4 ∈ ℝ ∧ 0 < 6 4 ) ) → ( 4 ≤ 𝑘 ↔ ( 4 · 6 4 ) ≤ ( 𝑘 · 6 4 ) ) )
127 4 120 125 126 mp3an2i ⊢ ( 𝑘 ∈ ℤ → ( 4 ≤ 𝑘 ↔ ( 4 · 6 4 ) ≤ ( 𝑘 · 6 4 ) ) )
128 127 biimpa ⊢ ( ( 𝑘 ∈ ℤ ∧ 4 ≤ 𝑘 ) → ( 4 · 6 4 ) ≤ ( 𝑘 · 6 4 ) )
129 119 128 eqbrtrrid ⊢ ( ( 𝑘 ∈ ℤ ∧ 4 ≤ 𝑘 ) → 2 5 6 ≤ ( 𝑘 · 6 4 ) )
130 5nn0 ⊢ 5 ∈ ℕ0
131 52 130 deccl ⊢ 2 5 ∈ ℕ0
132 131 36 deccl ⊢ 2 5 6 ∈ ℕ0
133 132 nn0zi ⊢ 2 5 6 ∈ ℤ
134 id ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℤ )
135 38 nn0zi ⊢ 6 4 ∈ ℤ
136 135 a1i ⊢ ( 𝑘 ∈ ℤ → 6 4 ∈ ℤ )
137 134 136 zmulcld ⊢ ( 𝑘 ∈ ℤ → ( 𝑘 · 6 4 ) ∈ ℤ )
138 137 adantr ⊢ ( ( 𝑘 ∈ ℤ ∧ 4 ≤ 𝑘 ) → ( 𝑘 · 6 4 ) ∈ ℤ )
139 zleltp1 ⊢ ( ( 2 5 6 ∈ ℤ ∧ ( 𝑘 · 6 4 ) ∈ ℤ ) → ( 2 5 6 ≤ ( 𝑘 · 6 4 ) ↔ 2 5 6 < ( ( 𝑘 · 6 4 ) + 1 ) ) )
140 133 138 139 sylancr ⊢ ( ( 𝑘 ∈ ℤ ∧ 4 ≤ 𝑘 ) → ( 2 5 6 ≤ ( 𝑘 · 6 4 ) ↔ 2 5 6 < ( ( 𝑘 · 6 4 ) + 1 ) ) )
141 129 140 mpbid ⊢ ( ( 𝑘 ∈ ℤ ∧ 4 ≤ 𝑘 ) → 2 5 6 < ( ( 𝑘 · 6 4 ) + 1 ) )
142 141 3adant1 ⊢ ( ( 4 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 4 ≤ 𝑘 ) → 2 5 6 < ( ( 𝑘 · 6 4 ) + 1 ) )
143 114 142 sylbi ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → 2 5 6 < ( ( 𝑘 · 6 4 ) + 1 ) )
144 132 nn0rei ⊢ 2 5 6 ∈ ℝ
145 144 a1i ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → 2 5 6 ∈ ℝ )
146 eluzelre ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → 𝑘 ∈ ℝ )
147 121 a1i ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → 6 4 ∈ ℝ )
148 146 147 remulcld ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑘 · 6 4 ) ∈ ℝ )
149 peano2re ⊢ ( ( 𝑘 · 6 4 ) ∈ ℝ → ( ( 𝑘 · 6 4 ) + 1 ) ∈ ℝ )
150 148 149 syl ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → ( ( 𝑘 · 6 4 ) + 1 ) ∈ ℝ )
151 145 150 ltnled ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → ( 2 5 6 < ( ( 𝑘 · 6 4 ) + 1 ) ↔ ¬ ( ( 𝑘 · 6 4 ) + 1 ) ≤ 2 5 6 ) )
152 143 151 mpbid ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → ¬ ( ( 𝑘 · 6 4 ) + 1 ) ≤ 2 5 6 )
153 152 pm2.21d ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → ( ( ( 𝑘 · 6 4 ) + 1 ) ≤ 2 5 6 → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) )
154 153 adantr ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ) → ( ( ( 𝑘 · 6 4 ) + 1 ) ≤ 2 5 6 → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) )
155 113 154 sylbid ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ) → ( 𝑃 ≤ 2 5 6 → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) )
156 111 155 syl5bi ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) )
157 156 ex ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) )
158 109 157 jaoi ⊢ ( ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) )
159 158 adantr ⊢ ( ( ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) )
160 33 159 syl5bi ⊢ ( ( ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 4 + 2 ) ) ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) )
161 160 ex ⊢ ( ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) → ( 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 4 + 2 ) ) ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) ) )
162 26 161 sylbi ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) → ( 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 4 + 2 ) ) ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) ) )
163 162 com12 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) → ( 𝑘 ∈ ℕ → ( 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 4 + 2 ) ) ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) ) )
164 163 rexlimdv ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) → ( ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 4 + 2 ) ) ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) )
165 10 164 mpd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) )
166 165 3impia ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ∧ 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) )