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 ) |
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 ) |