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 mullidi ⊢ ( 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 mullidi ⊢ ( 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 addridi ⊢ ( 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 )