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	mullidi	$$⊢1\cdot 64=64$$
41	35 40	eqtrdi	$$⊢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	eqtrdi	$$⊢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		2t4e8	$$⊢2\cdot 4=8$$
59	58	eqcomi	$$⊢8=2\cdot 4$$
60	36 37 52 57 59	decmul10add	$$⊢2\cdot 64=120+8$$
61	51 60	eqtrdi	$$⊢k=2\to k\cdot 64=120+8$$
62	61	oveq1d	$$⊢k=2\to k\cdot 64+1=120+8+1$$
63		1nn0	$$⊢1\in {\mathbb{N}}_0$$
64	63 52	deccl	$$⊢12\in {\mathbb{N}}_0$$
65		8nn0	$$⊢8\in {\mathbb{N}}_0$$
66		8p1e9	$$⊢8+1=9$$
67		0nn0	$$⊢0\in {\mathbb{N}}_0$$
68		eqid	$$⊢120=120$$
69		8cn	$$⊢8\in ℂ$$
70	69	addlidi	$$⊢0+8=8$$
71	64 67 65 68 70	decaddi	$$⊢120+8=128$$
72	64 65 66 71	decsuc	$$⊢120+8+1=129$$
73	62 72	eqtrdi	$$⊢k=2\to k\cdot 64+1=129$$
74	73	adantl	$$⊢\left(P=k\cdot 64+1\wedge k=2\right)\to k\cdot 64+1=129$$
75	50 74	eqtrd	$$⊢\left(P=k\cdot 64+1\wedge k=2\right)\to P=129$$
76	75	ex	$$⊢P=k\cdot 64+1\to \left(k=2\to P=129\right)$$
77		simpl	$$⊢\left(P=k\cdot 64+1\wedge k=3\right)\to P=k\cdot 64+1$$
78		oveq1	$$⊢k=3\to k\cdot 64=3\cdot 64$$
79		3nn0	$$⊢3\in {\mathbb{N}}_0$$
80		6t3e18	$$⊢6\cdot 3=18$$
81		3cn	$$⊢3\in ℂ$$
82	53 81	mulcomi	$$⊢6\cdot 3=3\cdot 6$$
83	80 82	eqtr3i	$$⊢18=3\cdot 6$$
84		4t3e12	$$⊢4\cdot 3=12$$
85		4cn	$$⊢4\in ℂ$$
86	85 81	mulcomi	$$⊢4\cdot 3=3\cdot 4$$
87	84 86	eqtr3i	$$⊢12=3\cdot 4$$
88	36 37 79 83 87	decmul10add	$$⊢3\cdot 64=180+12$$
89	78 88	eqtrdi	$$⊢k=3\to k\cdot 64=180+12$$
90	89	oveq1d	$$⊢k=3\to k\cdot 64+1=180+12+1$$
91		9nn0	$$⊢9\in {\mathbb{N}}_0$$
92	63 91	deccl	$$⊢19\in {\mathbb{N}}_0$$
93		2p1e3	$$⊢2+1=3$$
94	63 65	deccl	$$⊢18\in {\mathbb{N}}_0$$
95		eqid	$$⊢180=180$$
96		eqid	$$⊢12=12$$
97		eqid	$$⊢18=18$$
98	63 65 66 97	decsuc	$$⊢18+1=19$$
99	54	addlidi	$$⊢0+2=2$$
100	94 67 63 52 95 96 98 99	decadd	$$⊢180+12=192$$
101	92 52 93 100	decsuc	$$⊢180+12+1=193$$
102	90 101	eqtrdi	$$⊢k=3\to k\cdot 64+1=193$$
103	102	adantl	$$⊢\left(P=k\cdot 64+1\wedge k=3\right)\to k\cdot 64+1=193$$
104	77 103	eqtrd	$$⊢\left(P=k\cdot 64+1\wedge k=3\right)\to P=193$$
105	104	ex	$$⊢P=k\cdot 64+1\to \left(k=3\to P=193\right)$$
106	49 76 105	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)$$
107	106	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)$$
108	107	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)$$
109		fmtno4sqrt	$$⊢⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋=256$$
110	109	breq2i	$$⊢P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\leftrightarrow P\le 256$$
111		breq1	$$⊢P=k\cdot 64+1\to \left(P\le 256\leftrightarrow k\cdot 64+1\le 256\right)$$
112	111	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)$$
113		eluz2	$$⊢k\in {\mathbb{Z}}_{\ge 4}\leftrightarrow \left(4\in \mathbb{Z}\wedge k\in \mathbb{Z}\wedge 4\le k\right)$$
114		6t4e24	$$⊢6\cdot 4=24$$
115	53 85 114	mulcomli	$$⊢4\cdot 6=24$$
116	52 37 43 115	decsuc	$$⊢4\cdot 6+1=25$$
117		4t4e16	$$⊢4\cdot 4=16$$
118	37 36 37 44 36 63 116 117	decmul2c	$$⊢4\cdot 64=256$$
119		zre	$$⊢k\in \mathbb{Z}\to k\in ℝ$$
120	38	nn0rei	$$⊢64\in ℝ$$
121	36 12	decnncl	$$⊢64\in \mathbb{N}$$
122	121	nngt0i	$$⊢0<64$$
123	120 122	pm3.2i	$$⊢\left(64\in ℝ\wedge 0<64\right)$$
124	123	a1i	$$⊢k\in \mathbb{Z}\to \left(64\in ℝ\wedge 0<64\right)$$
125		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)$$
126	4 119 124 125	mp3an2i	$$⊢k\in \mathbb{Z}\to \left(4\le k\leftrightarrow 4\cdot 64\le k\cdot 64\right)$$
127	126	biimpa	$$⊢\left(k\in \mathbb{Z}\wedge 4\le k\right)\to 4\cdot 64\le k\cdot 64$$
128	118 127	eqbrtrrid	$$⊢\left(k\in \mathbb{Z}\wedge 4\le k\right)\to 256\le k\cdot 64$$
129		5nn0	$$⊢5\in {\mathbb{N}}_0$$
130	52 129	deccl	$$⊢25\in {\mathbb{N}}_0$$
131	130 36	deccl	$$⊢256\in {\mathbb{N}}_0$$
132	131	nn0zi	$$⊢256\in \mathbb{Z}$$
133		id	$$⊢k\in \mathbb{Z}\to k\in \mathbb{Z}$$
134	38	nn0zi	$$⊢64\in \mathbb{Z}$$
135	134	a1i	$$⊢k\in \mathbb{Z}\to 64\in \mathbb{Z}$$
136	133 135	zmulcld	$$⊢k\in \mathbb{Z}\to k\cdot 64\in \mathbb{Z}$$
137	136	adantr	$$⊢\left(k\in \mathbb{Z}\wedge 4\le k\right)\to k\cdot 64\in \mathbb{Z}$$
138		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)$$
139	132 137 138	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)$$
140	128 139	mpbid	$$⊢\left(k\in \mathbb{Z}\wedge 4\le k\right)\to 256<k\cdot 64+1$$
141	140	3adant1	$$⊢\left(4\in \mathbb{Z}\wedge k\in \mathbb{Z}\wedge 4\le k\right)\to 256<k\cdot 64+1$$
142	113 141	sylbi	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to 256<k\cdot 64+1$$
143	131	nn0rei	$$⊢256\in ℝ$$
144	143	a1i	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to 256\in ℝ$$
145		eluzelre	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to k\in ℝ$$
146	120	a1i	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to 64\in ℝ$$
147	145 146	remulcld	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to k\cdot 64\in ℝ$$
148		peano2re	$$⊢k\cdot 64\in ℝ\to k\cdot 64+1\in ℝ$$
149	147 148	syl	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to k\cdot 64+1\in ℝ$$
150	144 149	ltnled	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to \left(256<k\cdot 64+1\leftrightarrow \neg k\cdot 64+1\le 256\right)$$
151	142 150	mpbid	$$⊢k\in {\mathbb{Z}}_{\ge 4}\to \neg k\cdot 64+1\le 256$$
152	151	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)$$
153	152	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)$$
154	112 153	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)$$
155	110 154	biimtrid	$$⊢\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)$$
156	155	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)$$
157	108 156	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)$$
158	157	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)$$
159	33 158	biimtrid	$$⊢\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)$$
160	159	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)$$
161	26 160	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)$$
162	161	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)$$
163	162	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)$$
164	10 163	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)$$
165	164	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)$$