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	$$⊢\left(P\in \mathbb{P}\wedge P\parallel \mathrm{FermatNo}\left(4\right)\wedge P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\right)\to \left(P=65\vee P=129\vee P=193\right)$$

Proof

Step	Hyp	Ref	Expression
1		2z	$$⊢2\in \mathbb{Z}$$
2		4z	$$⊢4\in \mathbb{Z}$$
3		2re	$$⊢2\in ℝ$$
4		4re	$$⊢4\in ℝ$$
5		2lt4	$$⊢2<4$$
6	3 4 5	ltleii	$$⊢2\le 4$$
7		eluz2	$$⊢4\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(2\in \mathbb{Z}\wedge 4\in \mathbb{Z}\wedge 2\le 4\right)$$
8	1 2 6 7	mpbir3an	$$⊢4\in {\mathbb{Z}}_{\ge 2}$$
9		fmtnoprmfac2	$$⊢\left(4\in {\mathbb{Z}}_{\ge 2}\wedge P\in \mathbb{P}\wedge P\parallel \mathrm{FermatNo}\left(4\right)\right)\to \exists k\in \mathbb{N}P=k{2}^{4+2}+1$$
10	8 9	mp3an1	$$⊢\left(P\in \mathbb{P}\wedge P\parallel \mathrm{FermatNo}\left(4\right)\right)\to \exists k\in \mathbb{N}P=k{2}^{4+2}+1$$
11		elnnuz	$$⊢k\in \mathbb{N}\leftrightarrow k\in {\mathbb{Z}}_{\ge 1}$$
12		4nn	$$⊢4\in \mathbb{N}$$
13		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
14	12 13	eleqtri	$$⊢4\in {\mathbb{Z}}_{\ge 1}$$
15		fzouzsplit	$$⊢4\in {\mathbb{Z}}_{\ge 1}\to {\mathbb{Z}}_{\ge 1}=\left(1..^4\right)\cup {\mathbb{Z}}_{\ge 4}$$
16	14 15	ax-mp	$$⊢{\mathbb{Z}}_{\ge 1}=\left(1..^4\right)\cup {\mathbb{Z}}_{\ge 4}$$
17	16	eleq2i	$$⊢k\in {\mathbb{Z}}_{\ge 1}\leftrightarrow k\in \left(\left(1..^4\right)\cup {\mathbb{Z}}_{\ge 4}\right)$$
18		elun	$$⊢k\in \left(\left(1..^4\right)\cup {\mathbb{Z}}_{\ge 4}\right)\leftrightarrow \left(k\in \left(1..^4\right)\vee k\in {\mathbb{Z}}_{\ge 4}\right)$$
19		fzo1to4tp	$$⊢\left(1..^4\right)=\left\{1,2,3\right\}$$
20	19	eleq2i	$$⊢k\in \left(1..^4\right)\leftrightarrow k\in \left\{1,2,3\right\}$$
21		vex	$$⊢k\in \mathrm{V}$$
22	21	eltp	$$⊢k\in \left\{1,2,3\right\}\leftrightarrow \left(k=1\vee k=2\vee k=3\right)$$
23	20 22	bitri	$$⊢k\in \left(1..^4\right)\leftrightarrow \left(k=1\vee k=2\vee k=3\right)$$
24	23	orbi1i	$$⊢\left(k\in \left(1..^4\right)\vee k\in {\mathbb{Z}}_{\ge 4}\right)\leftrightarrow \left(\left(k=1\vee k=2\vee k=3\right)\vee k\in {\mathbb{Z}}_{\ge 4}\right)$$
25	18 24	bitri	$$⊢k\in \left(\left(1..^4\right)\cup {\mathbb{Z}}_{\ge 4}\right)\leftrightarrow \left(\left(k=1\vee k=2\vee k=3\right)\vee k\in {\mathbb{Z}}_{\ge 4}\right)$$
26	11 17 25	3bitri	$$⊢k\in \mathbb{N}\leftrightarrow \left(\left(k=1\vee k=2\vee k=3\right)\vee k\in {\mathbb{Z}}_{\ge 4}\right)$$
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\cdot 64$$
32	31	oveq1i	$$⊢k{2}^{4+2}+1=k\cdot 64+1$$
33	32	eqeq2i	$$⊢P=k{2}^{4+2}+1\leftrightarrow P=k\cdot 64+1$$
34		simpl	$$⊢\left(P=k\cdot 64+1\wedge k=1\right)\to P=k\cdot 64+1$$
35		oveq1	$$⊢k=1\to k\cdot 64=1\cdot 64$$
36		6nn0	$$⊢6\in {\mathbb{N}}_0$$
37		4nn0	$$⊢4\in {\mathbb{N}}_0$$
38	36 37	deccl	$$⊢64\in {\mathbb{N}}_0$$
39	38	nn0cni	$$⊢64\in ℂ$$
40	39	mulid2i	$$⊢1\cdot 64=64$$
41	35 40	syl6eq	$$⊢k=1\to k\cdot 64=64$$
42	41	oveq1d	$$⊢k=1\to k\cdot 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	syl6eq	$$⊢k=1\to k\cdot 64+1=65$$
47	46	adantl	$$⊢\left(P=k\cdot 64+1\wedge k=1\right)\to k\cdot 64+1=65$$
48	34 47	eqtrd	$$⊢\left(P=k\cdot 64+1\wedge k=1\right)\to P=65$$
49	48	ex	$$⊢P=k\cdot 64+1\to \left(k=1\to P=65\right)$$
50		simpl	$$⊢\left(P=k\cdot 64+1\wedge k=2\right)\to P=k\cdot 64+1$$
51		oveq1	$$⊢k=2\to k\cdot 64=2\cdot 64$$
52		2nn0	$$⊢2\in {\mathbb{N}}_0$$
53		6cn	$$⊢6\in ℂ$$
54		2cn	$$⊢2\in ℂ$$
55		6t2e12	$$⊢6\cdot 2=12$$
56	53 54 55	mulcomli	$$⊢2\cdot 6=12$$
57	56	eqcomi	$$⊢12=2\cdot 6$$
58		4cn	$$⊢4\in ℂ$$
59		4t2e8	$$⊢4\cdot 2=8$$
60	58 54 59	mulcomli	$$⊢2\cdot 4=8$$
61	60	eqcomi	$$⊢8=2\cdot 4$$
62	36 37 52 57 61	decmul10add	$$⊢2\cdot 64=120+8$$
63	51 62	syl6eq	$$⊢k=2\to k\cdot 64=120+8$$
64	63	oveq1d	$$⊢k=2\to k\cdot 64+1=120+8+1$$
65		1nn0	$$⊢1\in {\mathbb{N}}_0$$
66	65 52	deccl	$$⊢12\in {\mathbb{N}}_0$$
67		8nn0	$$⊢8\in {\mathbb{N}}_0$$
68		8p1e9	$$⊢8+1=9$$
69		0nn0	$$⊢0\in {\mathbb{N}}_0$$
70		eqid	$$⊢120=120$$
71		8cn	$$⊢8\in ℂ$$
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	syl6eq	$$⊢k=2\to k\cdot 64+1=129$$
76	75	adantl	$$⊢\left(P=k\cdot 64+1\wedge k=2\right)\to k\cdot 64+1=129$$
77	50 76	eqtrd	$$⊢\left(P=k\cdot 64+1\wedge k=2\right)\to P=129$$
78	77	ex	$$⊢P=k\cdot 64+1\to \left(k=2\to P=129\right)$$
79		simpl	$$⊢\left(P=k\cdot 64+1\wedge k=3\right)\to P=k\cdot 64+1$$
80		oveq1	$$⊢k=3\to k\cdot 64=3\cdot 64$$
81		3nn0	$$⊢3\in {\mathbb{N}}_0$$
82		6t3e18	$$⊢6\cdot 3=18$$
83		3cn	$$⊢3\in ℂ$$
84	53 83	mulcomi	$$⊢6\cdot 3=3\cdot 6$$
85	82 84	eqtr3i	$$⊢18=3\cdot 6$$
86		4t3e12	$$⊢4\cdot 3=12$$
87	58 83	mulcomi	$$⊢4\cdot 3=3\cdot 4$$
88	86 87	eqtr3i	$$⊢12=3\cdot 4$$
89	36 37 81 85 88	decmul10add	$$⊢3\cdot 64=180+12$$
90	80 89	syl6eq	$$⊢k=3\to k\cdot 64=180+12$$
91	90	oveq1d	$$⊢k=3\to k\cdot 64+1=180+12+1$$
92		9nn0	$$⊢9\in {\mathbb{N}}_0$$
93	65 92	deccl	$$⊢19\in {\mathbb{N}}_0$$
94		2p1e3	$$⊢2+1=3$$
95	65 67	deccl	$$⊢18\in {\mathbb{N}}_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	syl6eq	$$⊢k=3\to k\cdot 64+1=193$$
104	103	adantl	$$⊢\left(P=k\cdot 64+1\wedge k=3\right)\to k\cdot 64+1=193$$
105	79 104	eqtrd	$$⊢\left(P=k\cdot 64+1\wedge k=3\right)\to P=193$$
106	105	ex	$$⊢P=k\cdot 64+1\to \left(k=3\to P=193\right)$$
107	49 78 106	3orim123d	$$⊢P=k\cdot 64+1\to \left(\left(k=1\vee k=2\vee k=3\right)\to \left(P=65\vee P=129\vee P=193\right)\right)$$
108	107	a1i	$$⊢P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\to \left(P=k\cdot 64+1\to \left(\left(k=1\vee k=2\vee k=3\right)\to \left(P=65\vee P=129\vee P=193\right)\right)\right)$$
109	108	com13	$$⊢\left(k=1\vee k=2\vee k=3\right)\to \left(P=k\cdot 64+1\to \left(P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\to \left(P=65\vee P=129\vee P=193\right)\right)\right)$$
110		fmtno4sqrt	$$⊢⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋=256$$
111	110	breq2i	$$⊢P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\leftrightarrow P\le 256$$
112		breq1	$$⊢P=k\cdot 64+1\to \left(P\le 256\leftrightarrow k\cdot 64+1\le 256\right)$$
113	112	adantl	$$⊢\left(k\in {\mathbb{Z}}_{\ge 4}\wedge P=k\cdot 64+1\right)\to \left(P\le 256\leftrightarrow k\cdot 64+1\le 256\right)$$
114		eluz2	$$⊢k\in {\mathbb{Z}}_{\ge 4}\leftrightarrow \left(4\in \mathbb{Z}\wedge k\in \mathbb{Z}\wedge 4\le k\right)$$
115		6t4e24	$$⊢6\cdot 4=24$$
116	53 58 115	mulcomli	$$⊢4\cdot 6=24$$
117	52 37 43 116	decsuc	$$⊢4\cdot 6+1=25$$
118		4t4e16	$$⊢4\cdot 4=16$$
119	37 36 37 44 36 65 117 118	decmul2c	$$⊢4\cdot 64=256$$
120		zre	$$⊢k\in \mathbb{Z}\to k\in ℝ$$
121	38	nn0rei	$$⊢64\in ℝ$$
122	36 12	decnncl	$$⊢64\in \mathbb{N}$$
123	122	nngt0i	$$⊢0<64$$
124	121 123	pm3.2i	$$⊢\left(64\in ℝ\wedge 0<64\right)$$
125	124	a1i	$$⊢k\in \mathbb{Z}\to \left(64\in ℝ\wedge 0<64\right)$$
126		lemul1	$$⊢\left(4\in ℝ\wedge k\in ℝ\wedge \left(64\in ℝ\wedge 0<64\right)\right)\to \left(4\le k\leftrightarrow 4\cdot 64\le k\cdot 64\right)$$
127	4 120 125 126	mp3an2i	$$⊢k\in \mathbb{Z}\to \left(4\le k\leftrightarrow 4\cdot 64\le k\cdot 64\right)$$
128	127	biimpa	$$⊢\left(k\in \mathbb{Z}\wedge 4\le k\right)\to 4\cdot 64\le k\cdot 64$$
129	119 128	eqbrtrrid	$$⊢\left(k\in \mathbb{Z}\wedge 4\le k\right)\to 256\le k\cdot 64$$
130		5nn0	$$⊢5\in {\mathbb{N}}_0$$
131	52 130	deccl	$$⊢25\in {\mathbb{N}}_0$$
132	131 36	deccl	$$⊢256\in {\mathbb{N}}_0$$
133	132	nn0zi	$$⊢256\in \mathbb{Z}$$
134		id	$$⊢k\in \mathbb{Z}\to k\in \mathbb{Z}$$
135	38	nn0zi	$$⊢64\in \mathbb{Z}$$
136	135	a1i	$$⊢k\in \mathbb{Z}\to 64\in \mathbb{Z}$$
137	134 136	zmulcld	$$⊢k\in \mathbb{Z}\to k\cdot 64\in \mathbb{Z}$$
138	137	adantr	$$⊢\left(k\in \mathbb{Z}\wedge 4\le k\right)\to k\cdot 64\in \mathbb{Z}$$
139		zleltp1	$$⊢\left(256\in \mathbb{Z}\wedge k\cdot 64\in \mathbb{Z}\right)\to \left(256\le k\cdot 64\leftrightarrow 256<k\cdot 64+1\right)$$
140	133 138 139	sylancr	$$⊢\left(k\in \mathbb{Z}\wedge 4\le k\right)\to \left(256\le k\cdot 64\leftrightarrow 256<k\cdot 64+1\right)$$
141	129 140	mpbid	$$⊢\left(k\in \mathbb{Z}\wedge 4\le k\right)\to 256<k\cdot 64+1$$
142	141	3adant1	$$⊢\left(4\in \mathbb{Z}\wedge k\in \mathbb{Z}\wedge 4\le k\right)\to 256<k\cdot 64+1$$
143	114 142	sylbi	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to 256<k\cdot 64+1$$
144	132	nn0rei	$$⊢256\in ℝ$$
145	144	a1i	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to 256\in ℝ$$
146		eluzelre	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to k\in ℝ$$
147	121	a1i	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to 64\in ℝ$$
148	146 147	remulcld	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to k\cdot 64\in ℝ$$
149		peano2re	$$⊢k\cdot 64\in ℝ\to k\cdot 64+1\in ℝ$$
150	148 149	syl	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to k\cdot 64+1\in ℝ$$
151	145 150	ltnled	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to \left(256<k\cdot 64+1\leftrightarrow \neg k\cdot 64+1\le 256\right)$$
152	143 151	mpbid	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to \neg k\cdot 64+1\le 256$$
153	152	pm2.21d	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to \left(k\cdot 64+1\le 256\to \left(P=65\vee P=129\vee P=193\right)\right)$$
154	153	adantr	$$⊢\left(k\in {\mathbb{Z}}_{\ge 4}\wedge P=k\cdot 64+1\right)\to \left(k\cdot 64+1\le 256\to \left(P=65\vee P=129\vee P=193\right)\right)$$
155	113 154	sylbid	$$⊢\left(k\in {\mathbb{Z}}_{\ge 4}\wedge P=k\cdot 64+1\right)\to \left(P\le 256\to \left(P=65\vee P=129\vee P=193\right)\right)$$
156	111 155	syl5bi	$$⊢\left(k\in {\mathbb{Z}}_{\ge 4}\wedge P=k\cdot 64+1\right)\to \left(P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\to \left(P=65\vee P=129\vee P=193\right)\right)$$
157	156	ex	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to \left(P=k\cdot 64+1\to \left(P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\to \left(P=65\vee P=129\vee P=193\right)\right)\right)$$
158	109 157	jaoi	$$⊢\left(\left(k=1\vee k=2\vee k=3\right)\vee k\in {\mathbb{Z}}_{\ge 4}\right)\to \left(P=k\cdot 64+1\to \left(P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\to \left(P=65\vee P=129\vee P=193\right)\right)\right)$$
159	158	adantr	$$⊢\left(\left(\left(k=1\vee k=2\vee k=3\right)\vee k\in {\mathbb{Z}}_{\ge 4}\right)\wedge \left(P\in \mathbb{P}\wedge P\parallel \mathrm{FermatNo}\left(4\right)\right)\right)\to \left(P=k\cdot 64+1\to \left(P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\to \left(P=65\vee P=129\vee P=193\right)\right)\right)$$
160	33 159	syl5bi	$$⊢\left(\left(\left(k=1\vee k=2\vee k=3\right)\vee k\in {\mathbb{Z}}_{\ge 4}\right)\wedge \left(P\in \mathbb{P}\wedge P\parallel \mathrm{FermatNo}\left(4\right)\right)\right)\to \left(P=k{2}^{4+2}+1\to \left(P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\to \left(P=65\vee P=129\vee P=193\right)\right)\right)$$
161	160	ex	$$⊢\left(\left(k=1\vee k=2\vee k=3\right)\vee k\in {\mathbb{Z}}_{\ge 4}\right)\to \left(\left(P\in \mathbb{P}\wedge P\parallel \mathrm{FermatNo}\left(4\right)\right)\to \left(P=k{2}^{4+2}+1\to \left(P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\to \left(P=65\vee P=129\vee P=193\right)\right)\right)\right)$$
162	26 161	sylbi	$$⊢k\in \mathbb{N}\to \left(\left(P\in \mathbb{P}\wedge P\parallel \mathrm{FermatNo}\left(4\right)\right)\to \left(P=k{2}^{4+2}+1\to \left(P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\to \left(P=65\vee P=129\vee P=193\right)\right)\right)\right)$$
163	162	com12	$$⊢\left(P\in \mathbb{P}\wedge P\parallel \mathrm{FermatNo}\left(4\right)\right)\to \left(k\in \mathbb{N}\to \left(P=k{2}^{4+2}+1\to \left(P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\to \left(P=65\vee P=129\vee P=193\right)\right)\right)\right)$$
164	163	rexlimdv	$$⊢\left(P\in \mathbb{P}\wedge P\parallel \mathrm{FermatNo}\left(4\right)\right)\to \left(\exists k\in \mathbb{N}P=k{2}^{4+2}+1\to \left(P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\to \left(P=65\vee P=129\vee P=193\right)\right)\right)$$
165	10 164	mpd	$$⊢\left(P\in \mathbb{P}\wedge P\parallel \mathrm{FermatNo}\left(4\right)\right)\to \left(P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\to \left(P=65\vee P=129\vee P=193\right)\right)$$
166	165	3impia	$$⊢\left(P\in \mathbb{P}\wedge P\parallel \mathrm{FermatNo}\left(4\right)\wedge P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\right)\to \left(P=65\vee P=129\vee P=193\right)$$