Metamath Proof Explorer

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 ⊢ P ∈ ℙ ∧ P ∥ FermatNo ⁡ 4 ∧ P ≤ FermatNo ⁡ 4 → P = 193

Proof

Step Hyp Ref Expression
1 fmtno4prmfac ⊢ P ∈ ℙ ∧ P ∥ FermatNo ⁡ 4 ∧ P ≤ FermatNo ⁡ 4 → P = 65 ∨ P = 129 ∨ P = 193
2 5nn ⊢ 5 ∈ ℕ
3 1nn0 ⊢ 1 ∈ ℕ 0
4 3nn ⊢ 3 ∈ ℕ
5 3 4 decnncl ⊢ 13 ∈ ℕ
6 1lt5 ⊢ 1 < 5
7 1nn ⊢ 1 ∈ ℕ
8 3nn0 ⊢ 3 ∈ ℕ 0
9 1lt10 ⊢ 1 < 10
10 7 8 3 9 declti ⊢ 1 < 13
11 eqid ⊢ 5 ⋅ 13 = 5 ⋅ 13
12 2 5 6 10 11 nprmi ⊢ ¬ 5 ⋅ 13 ∈ ℙ
13 id ⊢ P = 65 → P = 65
14 5nn0 ⊢ 5 ∈ ℕ 0
15 eqid ⊢ 13 = 13
16 5cn ⊢ 5 ∈ ℂ
17 16 mulid1i ⊢ 5 ⋅ 1 = 5
18 17 oveq1i ⊢ 5 ⋅ 1 + 1 = 5 + 1
19 5p1e6 ⊢ 5 + 1 = 6
20 18 19 eqtri ⊢ 5 ⋅ 1 + 1 = 6
21 5t3e15 ⊢ 5 ⋅ 3 = 15
22 14 3 8 15 14 3 20 21 decmul2c ⊢ 5 ⋅ 13 = 65
23 13 22 eqtr4di ⊢ P = 65 → P = 5 ⋅ 13
24 23 eleq1d ⊢ P = 65 → P ∈ ℙ ↔ 5 ⋅ 13 ∈ ℙ
25 12 24 mtbiri ⊢ P = 65 → ¬ P ∈ ℙ
26 25 pm2.21d ⊢ P = 65 → P ∈ ℙ → P = 193
27 4nn0 ⊢ 4 ∈ ℕ 0
28 27 4 decnncl ⊢ 43 ∈ ℕ
29 4nn ⊢ 4 ∈ ℕ
30 29 8 3 9 declti ⊢ 1 < 43
31 1lt3 ⊢ 1 < 3
32 eqid ⊢ 43 ⋅ 3 = 43 ⋅ 3
33 28 4 30 31 32 nprmi ⊢ ¬ 43 ⋅ 3 ∈ ℙ
34 id ⊢ P = 129 → P = 129
35 eqid ⊢ 43 = 43
36 4t3e12 ⊢ 4 ⋅ 3 = 12
37 3t3e9 ⊢ 3 ⋅ 3 = 9
38 8 27 8 35 36 37 decmul1 ⊢ 43 ⋅ 3 = 129
39 34 38 eqtr4di ⊢ P = 129 → P = 43 ⋅ 3
40 39 eleq1d ⊢ P = 129 → P ∈ ℙ ↔ 43 ⋅ 3 ∈ ℙ
41 33 40 mtbiri ⊢ P = 129 → ¬ P ∈ ℙ
42 41 pm2.21d ⊢ P = 129 → P ∈ ℙ → P = 193
43 ax-1 ⊢ P = 193 → P ∈ ℙ → P = 193
44 26 42 43 3jaoi ⊢ P = 65 ∨ P = 129 ∨ P = 193 → P ∈ ℙ → P = 193
45 44 com12 ⊢ P ∈ ℙ → P = 65 ∨ P = 129 ∨ P = 193 → P = 193
46 45 3ad2ant1 ⊢ P ∈ ℙ ∧ P ∥ FermatNo ⁡ 4 ∧ P ≤ FermatNo ⁡ 4 → P = 65 ∨ P = 129 ∨ P = 193 → P = 193
47 1 46 mpd ⊢ P ∈ ℙ ∧ P ∥ FermatNo ⁡ 4 ∧ P ≤ FermatNo ⁡ 4 → P = 193