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 ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ∧ 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) → 𝑃 = 1 9 3 )

Proof

Step Hyp Ref Expression
1 fmtno4prmfac ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ∧ 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) → ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) )
2 5nn ⊢ 5 ∈ ℕ
3 1nn0 ⊢ 1 ∈ ℕ0
4 3nn ⊢ 3 ∈ ℕ
5 3 4 decnncl ⊢ 1 3 ∈ ℕ
6 1lt5 ⊢ 1 < 5
7 1nn ⊢ 1 ∈ ℕ
8 3nn0 ⊢ 3 ∈ ℕ0
9 1lt10 ⊢ 1 < 1 0
10 7 8 3 9 declti ⊢ 1 < 1 3
11 eqid ⊢ ( 5 · 1 3 ) = ( 5 · 1 3 )
12 2 5 6 10 11 nprmi ⊢ ¬ ( 5 · 1 3 ) ∈ ℙ
13 id ⊢ ( 𝑃 = 6 5 → 𝑃 = 6 5 )
14 5nn0 ⊢ 5 ∈ ℕ0
15 eqid ⊢ 1 3 = 1 3
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 ) = 1 5
22 14 3 8 15 14 3 20 21 decmul2c ⊢ ( 5 · 1 3 ) = 6 5
23 13 22 eqtr4di ⊢ ( 𝑃 = 6 5 → 𝑃 = ( 5 · 1 3 ) )
24 23 eleq1d ⊢ ( 𝑃 = 6 5 → ( 𝑃 ∈ ℙ ↔ ( 5 · 1 3 ) ∈ ℙ ) )
25 12 24 mtbiri ⊢ ( 𝑃 = 6 5 → ¬ 𝑃 ∈ ℙ )
26 25 pm2.21d ⊢ ( 𝑃 = 6 5 → ( 𝑃 ∈ ℙ → 𝑃 = 1 9 3 ) )
27 4nn0 ⊢ 4 ∈ ℕ0
28 27 4 decnncl ⊢ 4 3 ∈ ℕ
29 4nn ⊢ 4 ∈ ℕ
30 29 8 3 9 declti ⊢ 1 < 4 3
31 1lt3 ⊢ 1 < 3
32 eqid ⊢ ( 4 3 · 3 ) = ( 4 3 · 3 )
33 28 4 30 31 32 nprmi ⊢ ¬ ( 4 3 · 3 ) ∈ ℙ
34 id ⊢ ( 𝑃 = 1 2 9 → 𝑃 = 1 2 9 )
35 eqid ⊢ 4 3 = 4 3
36 4t3e12 ⊢ ( 4 · 3 ) = 1 2
37 3t3e9 ⊢ ( 3 · 3 ) = 9
38 8 27 8 35 36 37 decmul1 ⊢ ( 4 3 · 3 ) = 1 2 9
39 34 38 eqtr4di ⊢ ( 𝑃 = 1 2 9 → 𝑃 = ( 4 3 · 3 ) )
40 39 eleq1d ⊢ ( 𝑃 = 1 2 9 → ( 𝑃 ∈ ℙ ↔ ( 4 3 · 3 ) ∈ ℙ ) )
41 33 40 mtbiri ⊢ ( 𝑃 = 1 2 9 → ¬ 𝑃 ∈ ℙ )
42 41 pm2.21d ⊢ ( 𝑃 = 1 2 9 → ( 𝑃 ∈ ℙ → 𝑃 = 1 9 3 ) )
43 ax-1 ⊢ ( 𝑃 = 1 9 3 → ( 𝑃 ∈ ℙ → 𝑃 = 1 9 3 ) )
44 26 42 43 3jaoi ⊢ ( ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) → ( 𝑃 ∈ ℙ → 𝑃 = 1 9 3 ) )
45 44 com12 ⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) → 𝑃 = 1 9 3 ) )
46 45 3ad2ant1 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ∧ 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) → ( ( 𝑃 = 6 5 ∨ 𝑃 = 1 2 9 ∨ 𝑃 = 1 9 3 ) → 𝑃 = 1 9 3 ) )
47 1 46 mpd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( FermatNo ‘ 4 ) ∧ 𝑃 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) → 𝑃 = 1 9 3 )