Theorem fmtno4prmfac193

Description: If P was a (prime) factor of the fourth Fermat number, it would be 193. (Contributed by AV, 28-Jul-2021)

	Ref	Expression
Assertion	fmtno4prmfac193	$$⊢\left(P\in \mathbb{P}\wedge P\parallel \mathrm{FermatNo}\left(4\right)\wedge P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\right)\to P=193$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2		5nn	$$⊢5\in \mathbb{N}$$
3		1nn0	$$⊢1\in {\mathbb{N}}_0$$
4		3nn	$$⊢3\in \mathbb{N}$$
5	3 4	decnncl	$$⊢13\in \mathbb{N}$$
6		1lt5	$$⊢1<5$$
7		1nn	$$⊢1\in \mathbb{N}$$
8		3nn0	$$⊢3\in {\mathbb{N}}_0$$
9		1lt10	$$⊢1<10$$
10	7 8 3 9	declti	$$⊢1<13$$
11		eqid	$$⊢5\cdot 13=5\cdot 13$$
12	2 5 6 10 11	nprmi	$$⊢\neg 5\cdot 13\in \mathbb{P}$$
13		id	$$⊢P=65\to P=65$$
14		5nn0	$$⊢5\in {\mathbb{N}}_0$$
15		eqid	$$⊢13=13$$
16		5cn	$$⊢5\in ℂ$$
17	16	mulridi	$$⊢5\cdot 1=5$$
18	17	oveq1i	$$⊢5\cdot 1+1=5+1$$
19		5p1e6	$$⊢5+1=6$$
20	18 19	eqtri	$$⊢5\cdot 1+1=6$$
21		5t3e15	$$⊢5\cdot 3=15$$
22	14 3 8 15 14 3 20 21	decmul2c	$$⊢5\cdot 13=65$$
23	13 22	eqtr4di	$$⊢P=65\to P=5\cdot 13$$
24	23	eleq1d	$$⊢P=65\to \left(P\in \mathbb{P}\leftrightarrow 5\cdot 13\in \mathbb{P}\right)$$
25	12 24	mtbiri	$$⊢P=65\to \neg P\in \mathbb{P}$$
26	25	pm2.21d	$$⊢P=65\to \left(P\in \mathbb{P}\to P=193\right)$$
27		4nn0	$$⊢4\in {\mathbb{N}}_0$$
28	27 4	decnncl	$$⊢43\in \mathbb{N}$$
29		4nn	$$⊢4\in \mathbb{N}$$
30	29 8 3 9	declti	$$⊢1<43$$
31		1lt3	$$⊢1<3$$
32		eqid	$$⊢43\cdot 3=43\cdot 3$$
33	28 4 30 31 32	nprmi	$$⊢\neg 43\cdot 3\in \mathbb{P}$$
34		id	$$⊢P=129\to P=129$$
35		eqid	$$⊢43=43$$
36		4t3e12	$$⊢4\cdot 3=12$$
37		3t3e9	$$⊢3\cdot 3=9$$
38	8 27 8 35 36 37	decmul1	$$⊢43\cdot 3=129$$
39	34 38	eqtr4di	$$⊢P=129\to P=43\cdot 3$$
40	39	eleq1d	$$⊢P=129\to \left(P\in \mathbb{P}\leftrightarrow 43\cdot 3\in \mathbb{P}\right)$$
41	33 40	mtbiri	$$⊢P=129\to \neg P\in \mathbb{P}$$
42	41	pm2.21d	$$⊢P=129\to \left(P\in \mathbb{P}\to P=193\right)$$
43		ax-1	$$⊢P=193\to \left(P\in \mathbb{P}\to P=193\right)$$
44	26 42 43	3jaoi	$$⊢\left(P=65\vee P=129\vee P=193\right)\to \left(P\in \mathbb{P}\to P=193\right)$$
45	44	com12	$$⊢P\in \mathbb{P}\to \left(\left(P=65\vee P=129\vee P=193\right)\to P=193\right)$$
46	45	3ad2ant1	$$⊢\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(\left(P=65\vee P=129\vee P=193\right)\to P=193\right)$$
47	1 46	mpd	$$⊢\left(P\in \mathbb{P}\wedge P\parallel \mathrm{FermatNo}\left(4\right)\wedge P\le ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋\right)\to P=193$$