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		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	addlidi	⊢ ( 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	addlidi	⊢ ( 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	biimtrid	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 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	biimtrid	⊢ ( ( ( ( 𝑘 = 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 ) )