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 mullidi ⊢ ( 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 2t4e8 ⊢ ( 2 · 4 ) = 8
59 58 eqcomi ⊢ 8 = ( 2 · 4 )
60 36 37 52 57 59 decmul10add ⊢ ( 2 · 6 4 ) = ( 1 2 0 + 8 )
61 51 60 eqtrdi ⊢ ( 𝑘 = 2 → ( 𝑘 · 6 4 ) = ( 1 2 0 + 8 ) )
62 61 oveq1d ⊢ ( 𝑘 = 2 → ( ( 𝑘 · 6 4 ) + 1 ) = ( ( 1 2 0 + 8 ) + 1 ) )
63 1nn0 ⊢ 1 ∈ ℕ0
64 63 52 deccl ⊢ 1 2 ∈ ℕ0
65 8nn0 ⊢ 8 ∈ ℕ0
66 8p1e9 ⊢ ( 8 + 1 ) = 9
67 0nn0 ⊢ 0 ∈ ℕ0
68 eqid ⊢ 1 2 0 = 1 2 0
69 8cn ⊢ 8 ∈ ℂ
70 69 addlidi ⊢ ( 0 + 8 ) = 8
71 64 67 65 68 70 decaddi ⊢ ( 1 2 0 + 8 ) = 1 2 8
72 64 65 66 71 decsuc ⊢ ( ( 1 2 0 + 8 ) + 1 ) = 1 2 9
73 62 72 eqtrdi ⊢ ( 𝑘 = 2 → ( ( 𝑘 · 6 4 ) + 1 ) = 1 2 9 )
74 73 adantl ⊢ ( ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ∧ 𝑘 = 2 ) → ( ( 𝑘 · 6 4 ) + 1 ) = 1 2 9 )
75 50 74 eqtrd ⊢ ( ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ∧ 𝑘 = 2 ) → 𝑃 = 1 2 9 )
76 75 ex ⊢ ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( 𝑘 = 2 → 𝑃 = 1 2 9 ) )
77 simpl ⊢ ( ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ∧ 𝑘 = 3 ) → 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) )
78 oveq1 ⊢ ( 𝑘 = 3 → ( 𝑘 · 6 4 ) = ( 3 · 6 4 ) )
79 3nn0 ⊢ 3 ∈ ℕ0
80 6t3e18 ⊢ ( 6 · 3 ) = 1 8
81 3cn ⊢ 3 ∈ ℂ
82 53 81 mulcomi ⊢ ( 6 · 3 ) = ( 3 · 6 )
83 80 82 eqtr3i ⊢ 1 8 = ( 3 · 6 )
84 4t3e12 ⊢ ( 4 · 3 ) = 1 2
85 4cn ⊢ 4 ∈ ℂ
86 85 81 mulcomi ⊢ ( 4 · 3 ) = ( 3 · 4 )
87 84 86 eqtr3i ⊢ 1 2 = ( 3 · 4 )
88 36 37 79 83 87 decmul10add ⊢ ( 3 · 6 4 ) = ( 1 8 0 + 1 2 )
89 78 88 eqtrdi ⊢ ( 𝑘 = 3 → ( 𝑘 · 6 4 ) = ( 1 8 0 + 1 2 ) )
90 89 oveq1d ⊢ ( 𝑘 = 3 → ( ( 𝑘 · 6 4 ) + 1 ) = ( ( 1 8 0 + 1 2 ) + 1 ) )
91 9nn0 ⊢ 9 ∈ ℕ0
92 63 91 deccl ⊢ 1 9 ∈ ℕ0
93 2p1e3 ⊢ ( 2 + 1 ) = 3
94 63 65 deccl ⊢ 1 8 ∈ ℕ0
95 eqid ⊢ 1 8 0 = 1 8 0
96 eqid ⊢ 1 2 = 1 2
97 eqid ⊢ 1 8 = 1 8
98 63 65 66 97 decsuc ⊢ ( 1 8 + 1 ) = 1 9
99 54 addlidi ⊢ ( 0 + 2 ) = 2
100 94 67 63 52 95 96 98 99 decadd ⊢ ( 1 8 0 + 1 2 ) = 1 9 2
101 92 52 93 100 decsuc ⊢ ( ( 1 8 0 + 1 2 ) + 1 ) = 1 9 3
102 90 101 eqtrdi ⊢ ( 𝑘 = 3 → ( ( 𝑘 · 6 4 ) + 1 ) = 1 9 3 )
103 102 adantl ⊢ ( ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ∧ 𝑘 = 3 ) → ( ( 𝑘 · 6 4 ) + 1 ) = 1 9 3 )
104 77 103 eqtrd ⊢ ( ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ∧ 𝑘 = 3 ) → 𝑃 = 1 9 3 )
105 104 ex ⊢ ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( 𝑘 = 3 → 𝑃 = 1 9 3 ) )
106 49 76 105 3orim123d ⊢ ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) )
107 106 a1i ⊢ ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) )
108 107 com13 ⊢ ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) → ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) )
109 fmtno4sqrt ⊢ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) = 2 5 6
110 109 breq2i ⊢ ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ↔ 𝑃 ≤ 2 5 6 )
111 breq1 ⊢ ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( 𝑃 ≤ 2 5 6 ↔ ( ( 𝑘 · 6 4 ) + 1 ) ≤ 2 5 6 ) )
112 111 adantl ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ) → ( 𝑃 ≤ 2 5 6 ↔ ( ( 𝑘 · 6 4 ) + 1 ) ≤ 2 5 6 ) )
113 eluz2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ↔ ( 4 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 4 ≤ 𝑘 ) )
114 6t4e24 ⊢ ( 6 · 4 ) = 2 4
115 53 85 114 mulcomli ⊢ ( 4 · 6 ) = 2 4
116 52 37 43 115 decsuc ⊢ ( ( 4 · 6 ) + 1 ) = 2 5
117 4t4e16 ⊢ ( 4 · 4 ) = 1 6
118 37 36 37 44 36 63 116 117 decmul2c ⊢ ( 4 · 6 4 ) = 2 5 6
119 zre ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
120 38 nn0rei ⊢ 6 4 ∈ ℝ
121 36 12 decnncl ⊢ 6 4 ∈ ℕ
122 121 nngt0i ⊢ 0 < 6 4
123 120 122 pm3.2i ⊢ ( 6 4 ∈ ℝ ∧ 0 < 6 4 )
124 123 a1i ⊢ ( 𝑘 ∈ ℤ → ( 6 4 ∈ ℝ ∧ 0 < 6 4 ) )
125 lemul1 ⊢ ( ( 4 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ ( 6 4 ∈ ℝ ∧ 0 < 6 4 ) ) → ( 4 ≤ 𝑘 ↔ ( 4 · 6 4 ) ≤ ( 𝑘 · 6 4 ) ) )
126 4 119 124 125 mp3an2i ⊢ ( 𝑘 ∈ ℤ → ( 4 ≤ 𝑘 ↔ ( 4 · 6 4 ) ≤ ( 𝑘 · 6 4 ) ) )
127 126 biimpa ⊢ ( ( 𝑘 ∈ ℤ ∧ 4 ≤ 𝑘 ) → ( 4 · 6 4 ) ≤ ( 𝑘 · 6 4 ) )
128 118 127 eqbrtrrid ⊢ ( ( 𝑘 ∈ ℤ ∧ 4 ≤ 𝑘 ) → 2 5 6 ≤ ( 𝑘 · 6 4 ) )
129 5nn0 ⊢ 5 ∈ ℕ0
130 52 129 deccl ⊢ 2 5 ∈ ℕ0
131 130 36 deccl ⊢ 2 5 6 ∈ ℕ0
132 131 nn0zi ⊢ 2 5 6 ∈ ℤ
133 id ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℤ )
134 38 nn0zi ⊢ 6 4 ∈ ℤ
135 134 a1i ⊢ ( 𝑘 ∈ ℤ → 6 4 ∈ ℤ )
136 133 135 zmulcld ⊢ ( 𝑘 ∈ ℤ → ( 𝑘 · 6 4 ) ∈ ℤ )
137 136 adantr ⊢ ( ( 𝑘 ∈ ℤ ∧ 4 ≤ 𝑘 ) → ( 𝑘 · 6 4 ) ∈ ℤ )
138 zleltp1 ⊢ ( ( 2 5 6 ∈ ℤ ∧ ( 𝑘 · 6 4 ) ∈ ℤ ) → ( 2 5 6 ≤ ( 𝑘 · 6 4 ) ↔ 2 5 6 < ( ( 𝑘 · 6 4 ) + 1 ) ) )
139 132 137 138 sylancr ⊢ ( ( 𝑘 ∈ ℤ ∧ 4 ≤ 𝑘 ) → ( 2 5 6 ≤ ( 𝑘 · 6 4 ) ↔ 2 5 6 < ( ( 𝑘 · 6 4 ) + 1 ) ) )
140 128 139 mpbid ⊢ ( ( 𝑘 ∈ ℤ ∧ 4 ≤ 𝑘 ) → 2 5 6 < ( ( 𝑘 · 6 4 ) + 1 ) )
141 140 3adant1 ⊢ ( ( 4 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 4 ≤ 𝑘 ) → 2 5 6 < ( ( 𝑘 · 6 4 ) + 1 ) )
142 113 141 sylbi ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → 2 5 6 < ( ( 𝑘 · 6 4 ) + 1 ) )
143 131 nn0rei ⊢ 2 5 6 ∈ ℝ
144 143 a1i ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → 2 5 6 ∈ ℝ )
145 eluzelre ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → 𝑘 ∈ ℝ )
146 120 a1i ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → 6 4 ∈ ℝ )
147 145 146 remulcld ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑘 · 6 4 ) ∈ ℝ )
148 peano2re ⊢ ( ( 𝑘 · 6 4 ) ∈ ℝ → ( ( 𝑘 · 6 4 ) + 1 ) ∈ ℝ )
149 147 148 syl ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → ( ( 𝑘 · 6 4 ) + 1 ) ∈ ℝ )
150 144 149 ltnled ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → ( 2 5 6 < ( ( 𝑘 · 6 4 ) + 1 ) ↔ ¬ ( ( 𝑘 · 6 4 ) + 1 ) ≤ 2 5 6 ) )
151 142 150 mpbid ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → ¬ ( ( 𝑘 · 6 4 ) + 1 ) ≤ 2 5 6 )
152 151 pm2.21d ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → ( ( ( 𝑘 · 6 4 ) + 1 ) ≤ 2 5 6 → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) )
153 152 adantr ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ) → ( ( ( 𝑘 · 6 4 ) + 1 ) ≤ 2 5 6 → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) )
154 112 153 sylbid ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ) → ( 𝑃 ≤ 2 5 6 → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) )
155 110 154 biimtrid ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) )
156 155 ex ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) )
157 108 156 jaoi ⊢ ( ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) )
158 157 adantr ⊢ ( ( ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = ( ( 𝑘 · 6 4 ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) )
159 33 158 biimtrid ⊢ ( ( ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 4 + 2 ) ) ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) )
160 159 ex ⊢ ( ( ( 𝑘 = 1 ∨ 𝑘 = 2 ∨ 𝑘 = 3 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) → ( 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 4 + 2 ) ) ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) ) )
161 26 160 sylbi ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) → ( 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 4 + 2 ) ) ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) ) )
162 161 com12 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) → ( 𝑘 ∈ ℕ → ( 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 4 + 2 ) ) ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) ) )
163 162 rexlimdv ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) → ( ∃ 𝑘 ∈ ℕ 𝑃 = ( ( 𝑘 · ( 2 ↑ ( 4 + 2 ) ) ) + 1 ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) ) )
164 10 163 mpd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ) → ( 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) ) )
165 164 3impia ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ∧ 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) )