Metamath Proof Explorer


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 ∈ ℕ0
2 9nn0 9 ∈ ℕ0
3 1 2 deccl 1 9 ∈ ℕ0
4 3nn 3 ∈ ℕ
5 3 4 decnncl 1 9 3 ∈ ℕ
6 3nn0 3 ∈ ℕ0
7 6 6 deccl 3 3 ∈ ℕ0
8 7 2 deccl 3 3 9 ∈ ℕ0
9 1nn 1 ∈ ℕ
10 1 9 decnncl 1 1 ∈ ℕ
11 10 decnncl2 1 1 0 ∈ ℕ
12 6nn0 6 ∈ ℕ0
13 5nn0 5 ∈ ℕ0
14 12 13 deccl 6 5 ∈ ℕ0
15 4nn0 4 ∈ ℕ0
16 14 15 deccl 6 5 4 ∈ ℕ0
17 2nn0 2 ∈ ℕ0
18 16 17 deccl 6 5 4 2 ∈ ℕ0
19 7nn0 7 ∈ ℕ0
20 1 1 deccl 1 1 ∈ ℕ0
21 0nn0 0 ∈ ℕ0
22 3 6 deccl 1 9 3 ∈ ℕ0
23 eqid 3 3 9 = 3 3 9
24 1 19 deccl 1 7 ∈ ℕ0
25 24 6 deccl 1 7 3 ∈ ℕ0
26 eqid 3 3 = 3 3
27 eqid 1 7 3 = 1 7 3
28 8nn0 8 ∈ ℕ0
29 13 28 deccl 5 8 ∈ ℕ0
30 13 19 deccl 5 7 ∈ ℕ0
31 eqid 1 9 3 = 1 9 3
32 eqid 1 9 = 1 9
33 3cn 3 ∈ ℂ
34 33 mulid2i ( 1 · 3 ) = 3
35 34 oveq1i ( ( 1 · 3 ) + 2 ) = ( 3 + 2 )
36 3p2e5 ( 3 + 2 ) = 5
37 35 36 eqtri ( ( 1 · 3 ) + 2 ) = 5
38 9t3e27 ( 9 · 3 ) = 2 7
39 6 1 2 32 19 17 37 38 decmul1c ( 1 9 · 3 ) = 5 7
40 3t3e9 ( 3 · 3 ) = 9
41 6 3 6 31 39 40 decmul1 ( 1 9 3 · 3 ) = 5 7 9
42 eqid 1 7 = 1 7
43 eqid 5 8 = 5 8
44 5cn 5 ∈ ℂ
45 ax-1cn 1 ∈ ℂ
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 ∈ ℂ
52 7cn 7 ∈ ℂ
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 · 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 · 3 ) + 3 ) = 5 8 2
67 6 6 24 6 26 27 22 17 29 62 66 decma2c ( ( 1 9 3 · 3 3 ) + 1 7 3 ) = 6 5 4 2
68 9cn 9 ∈ ℂ
69 68 mulid2i ( 1 · 9 ) = 9
70 69 oveq1i ( ( 1 · 9 ) + 8 ) = ( 9 + 8 )
71 9p8e17 ( 9 + 8 ) = 1 7
72 70 71 eqtri ( ( 1 · 9 ) + 8 ) = 1 7
73 9t9e81 ( 9 · 9 ) = 8 1
74 2 1 2 32 1 28 72 73 decmul1c ( 1 9 · 9 ) = 1 7 1
75 1p2e3 ( 1 + 2 ) = 3
76 24 1 17 74 75 decaddi ( ( 1 9 · 9 ) + 2 ) = 1 7 3
77 68 33 38 mulcomli ( 3 · 9 ) = 2 7
78 2 3 6 31 19 17 76 77 decmul1c ( 1 9 3 · 9 ) = 1 7 3 7
79 22 7 2 23 19 25 67 78 decmul2c ( 1 9 3 · 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 · 3 3 9 ) + 1 1 0 ) = 6 5 5 3 7
89 10pos 0 < 1 0
90 9nn 9 ∈ ℕ
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 )