Theorem fmtno4nprmfac193

Description: 193 is not a (prime) factor of the fourth Fermat number. (Contributed by AV, 24-Jul-2021)

	Ref	Expression
Assertion	fmtno4nprmfac193	|- -. ; ; 1 9 3 || ( FermatNo ` 4 )

Proof

Step	Hyp	Ref	Expression
1		1nn0	|- 1 e. NN0
2		9nn0	|- 9 e. NN0
3	1 2	deccl	|- ; 1 9 e. NN0
4		3nn	|- 3 e. NN
5	3 4	decnncl	|- ; ; 1 9 3 e. NN
6		3nn0	|- 3 e. NN0
7	6 6	deccl	|- ; 3 3 e. NN0
8	7 2	deccl	|- ; ; 3 3 9 e. NN0
9		1nn	|- 1 e. NN
10	1 9	decnncl	|- ; 1 1 e. NN
11	10	decnncl2	|- ; ; 1 1 0 e. NN
12		6nn0	|- 6 e. NN0
13		5nn0	|- 5 e. NN0
14	12 13	deccl	|- ; 6 5 e. NN0
15		4nn0	|- 4 e. NN0
16	14 15	deccl	|- ; ; 6 5 4 e. NN0
17		2nn0	|- 2 e. NN0
18	16 17	deccl	|- ; ; ; 6 5 4 2 e. NN0
19		7nn0	|- 7 e. NN0
20	1 1	deccl	|- ; 1 1 e. NN0
21		0nn0	|- 0 e. NN0
22	3 6	deccl	|- ; ; 1 9 3 e. NN0
23		eqid	|- ; ; 3 3 9 = ; ; 3 3 9
24	1 19	deccl	|- ; 1 7 e. NN0
25	24 6	deccl	|- ; ; 1 7 3 e. NN0
26		eqid	|- ; 3 3 = ; 3 3
27		eqid	|- ; ; 1 7 3 = ; ; 1 7 3
28		8nn0	|- 8 e. NN0
29	13 28	deccl	|- ; 5 8 e. NN0
30	13 19	deccl	|- ; 5 7 e. NN0
31		eqid	|- ; ; 1 9 3 = ; ; 1 9 3
32		eqid	|- ; 1 9 = ; 1 9
33		3cn	|- 3 e. CC
34	33	mulid2i	|- ( 1 x. 3 ) = 3
35	34	oveq1i	|- ( ( 1 x. 3 ) + 2 ) = ( 3 + 2 )
36		3p2e5	|- ( 3 + 2 ) = 5
37	35 36	eqtri	|- ( ( 1 x. 3 ) + 2 ) = 5
38		9t3e27	|- ( 9 x. 3 ) = ; 2 7
39	6 1 2 32 19 17 37 38	decmul1c	|- ( ; 1 9 x. 3 ) = ; 5 7
40		3t3e9	|- ( 3 x. 3 ) = 9
41	6 3 6 31 39 40	decmul1	|- ( ; ; 1 9 3 x. 3 ) = ; ; 5 7 9
42		eqid	|- ; 1 7 = ; 1 7
43		eqid	|- ; 5 8 = ; 5 8
44		5cn	|- 5 e. CC
45		ax-1cn	|- 1 e. CC
46		5p1e6	|- ( 5 + 1 ) = 6
47	44 45 46	addcomli	|- ( 1 + 5 ) = 6
48	47	oveq1i	|- ( ( 1 + 5 ) + 1 ) = ( 6 + 1 )
49		6p1e7	|- ( 6 + 1 ) = 7
50	48 49	eqtri	|- ( ( 1 + 5 ) + 1 ) = 7
51		8cn	|- 8 e. CC
52		7cn	|- 7 e. CC
53		8p7e15	|- ( 8 + 7 ) = ; 1 5
54	51 52 53	addcomli	|- ( 7 + 8 ) = ; 1 5
55	1 19 13 28 42 43 50 13 54	decaddc	|- ( ; 1 7 + ; 5 8 ) = ; 7 5
56		4p1e5	|- ( 4 + 1 ) = 5
57		eqid	|- ; 5 7 = ; 5 7
58		7p7e14	|- ( 7 + 7 ) = ; 1 4
59	13 19 19 57 46 15 58	decaddci	|- ( ; 5 7 + 7 ) = ; 6 4
60	12 15 56 59	decsuc	|- ( ( ; 5 7 + 7 ) + 1 ) = ; 6 5
61		9p5e14	|- ( 9 + 5 ) = ; 1 4
62	30 2 19 13 41 55 60 15 61	decaddc	|- ( ( ; ; 1 9 3 x. 3 ) + ( ; 1 7 + ; 5 8 ) ) = ; ; 6 5 4
63		7p1e8	|- ( 7 + 1 ) = 8
64	13 19 63 57	decsuc	|- ( ; 5 7 + 1 ) = ; 5 8
65		9p3e12	|- ( 9 + 3 ) = ; 1 2
66	30 2 6 41 64 17 65	decaddci	|- ( ( ; ; 1 9 3 x. 3 ) + 3 ) = ; ; 5 8 2
67	6 6 24 6 26 27 22 17 29 62 66	decma2c	|- ( ( ; ; 1 9 3 x. ; 3 3 ) + ; ; 1 7 3 ) = ; ; ; 6 5 4 2
68		9cn	|- 9 e. CC
69	68	mulid2i	|- ( 1 x. 9 ) = 9
70	69	oveq1i	|- ( ( 1 x. 9 ) + 8 ) = ( 9 + 8 )
71		9p8e17	|- ( 9 + 8 ) = ; 1 7
72	70 71	eqtri	|- ( ( 1 x. 9 ) + 8 ) = ; 1 7
73		9t9e81	|- ( 9 x. 9 ) = ; 8 1
74	2 1 2 32 1 28 72 73	decmul1c	|- ( ; 1 9 x. 9 ) = ; ; 1 7 1
75		1p2e3	|- ( 1 + 2 ) = 3
76	24 1 17 74 75	decaddi	|- ( ( ; 1 9 x. 9 ) + 2 ) = ; ; 1 7 3
77	68 33 38	mulcomli	|- ( 3 x. 9 ) = ; 2 7
78	2 3 6 31 19 17 76 77	decmul1c	|- ( ; ; 1 9 3 x. 9 ) = ; ; ; 1 7 3 7
79	22 7 2 23 19 25 67 78	decmul2c	|- ( ; ; 1 9 3 x. ; ; 3 3 9 ) = ; ; ; ; 6 5 4 2 7
80		eqid	|- ; ; 1 1 0 = ; ; 1 1 0
81		eqid	|- ; ; ; 6 5 4 2 = ; ; ; 6 5 4 2
82		eqid	|- ; 1 1 = ; 1 1
83		eqid	|- ; ; 6 5 4 = ; ; 6 5 4
84	14 15 56 83	decsuc	|- ( ; ; 6 5 4 + 1 ) = ; ; 6 5 5
85		2p1e3	|- ( 2 + 1 ) = 3
86	16 17 1 1 81 82 84 85	decadd	|- ( ; ; ; 6 5 4 2 + ; 1 1 ) = ; ; ; 6 5 5 3
87	52	addid1i	|- ( 7 + 0 ) = 7
88	18 19 20 21 79 80 86 87	decadd	|- ( ( ; ; 1 9 3 x. ; ; 3 3 9 ) + ; ; 1 1 0 ) = ; ; ; ; 6 5 5 3 7
89		10pos	|- 0 < ; 1 0
90		9nn	|- 9 e. NN
91		1lt9	|- 1 < 9
92	1 1 90 91	declt	|- ; 1 1 < ; 1 9
93	20 3 21 6 89 92	decltc	|- ; ; 1 1 0 < ; ; 1 9 3
94	5 8 11 88 93	ndvdsi	|- -. ; ; 1 9 3 || ; ; ; ; 6 5 5 3 7
95		fmtno4	|- ( FermatNo ` 4 ) = ; ; ; ; 6 5 5 3 7
96	95	breq2i	|- ( ; ; 1 9 3 || ( FermatNo ` 4 ) <-> ; ; 1 9 3 || ; ; ; ; 6 5 5 3 7 )
97	94 96	mtbir	|- -. ; ; 1 9 3 || ( FermatNo ` 4 )