Metamath Proof Explorer

Theorem fmtno4prm

Description: The 4-th Fermat number (65537) is a prime (thefifth Fermat prime). (Contributed by AV, 28-Jul-2021)

Ref Expression
Assertion fmtno4prm ( FermatNo ‘ 4 ) ∈ ℙ

Proof

Step Hyp Ref Expression
1 4nn0 ⊢ 4 ∈ ℕ0
2 fmtno ⊢ ( 4 ∈ ℕ0 → ( FermatNo ‘ 4 ) = ( ( 2 ↑ ( 2 ↑ 4 ) ) + 1 ) )
3 1 2 ax-mp ⊢ ( FermatNo ‘ 4 ) = ( ( 2 ↑ ( 2 ↑ 4 ) ) + 1 )
4 2nn ⊢ 2 ∈ ℕ
5 2nn0 ⊢ 2 ∈ ℕ0
6 5 1 nn0expcli ⊢ ( 2 ↑ 4 ) ∈ ℕ0
7 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ ( 2 ↑ 4 ) ∈ ℕ0 ) → ( 2 ↑ ( 2 ↑ 4 ) ) ∈ ℕ )
8 4 6 7 mp2an ⊢ ( 2 ↑ ( 2 ↑ 4 ) ) ∈ ℕ
9 2re ⊢ 2 ∈ ℝ
10 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 4 ∈ ℕ0 ) → ( 2 ↑ 4 ) ∈ ℕ )
11 4 1 10 mp2an ⊢ ( 2 ↑ 4 ) ∈ ℕ
12 1lt2 ⊢ 1 < 2
13 expgt1 ⊢ ( ( 2 ∈ ℝ ∧ ( 2 ↑ 4 ) ∈ ℕ ∧ 1 < 2 ) → 1 < ( 2 ↑ ( 2 ↑ 4 ) ) )
14 9 11 12 13 mp3an ⊢ 1 < ( 2 ↑ ( 2 ↑ 4 ) )
15 eluz2b2 ⊢ ( ( 2 ↑ ( 2 ↑ 4 ) ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( 2 ↑ ( 2 ↑ 4 ) ) ∈ ℕ ∧ 1 < ( 2 ↑ ( 2 ↑ 4 ) ) ) )
16 8 14 15 mpbir2an ⊢ ( 2 ↑ ( 2 ↑ 4 ) ) ∈ ( ℤ≥ ‘ 2 )
17 peano2uz ⊢ ( ( 2 ↑ ( 2 ↑ 4 ) ) ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 ↑ ( 2 ↑ 4 ) ) + 1 ) ∈ ( ℤ≥ ‘ 2 ) )
18 16 17 ax-mp ⊢ ( ( 2 ↑ ( 2 ↑ 4 ) ) + 1 ) ∈ ( ℤ≥ ‘ 2 )
19 3 18 eqeltri ⊢ ( FermatNo ‘ 4 ) ∈ ( ℤ≥ ‘ 2 )
20 elinel2 ⊢ ( 𝑝 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) ∩ ℙ ) → 𝑝 ∈ ℙ )
21 20 adantr ⊢ ( ( 𝑝 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) ∩ ℙ ) ∧ 𝑝 ∥ ( FermatNo ‘ 4 ) ) → 𝑝 ∈ ℙ )
22 simpr ⊢ ( ( 𝑝 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) ∩ ℙ ) ∧ 𝑝 ∥ ( FermatNo ‘ 4 ) ) → 𝑝 ∥ ( FermatNo ‘ 4 ) )
23 elinel1 ⊢ ( 𝑝 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) ∩ ℙ ) → 𝑝 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) )
24 elfzle2 ⊢ ( 𝑝 ∈ ( 2 ... ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) → 𝑝 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) )
25 23 24 syl ⊢ ( 𝑝 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) ∩ ℙ ) → 𝑝 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) )
26 25 adantr ⊢ ( ( 𝑝 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) ∩ ℙ ) ∧ 𝑝 ∥ ( FermatNo ‘ 4 ) ) → 𝑝 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) )
27 fmtno4prmfac193 ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( FermatNo ‘ 4 ) ∧ 𝑝 ≤ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) → 𝑝 = 1 9 3 )
28 21 22 26 27 syl3anc ⊢ ( ( 𝑝 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) ∩ ℙ ) ∧ 𝑝 ∥ ( FermatNo ‘ 4 ) ) → 𝑝 = 1 9 3 )
29 fmtno4nprmfac193 ⊢ ¬ 1 9 3 ∥ ( FermatNo ‘ 4 )
30 breq1 ⊢ ( 𝑝 = 1 9 3 → ( 𝑝 ∥ ( FermatNo ‘ 4 ) ↔ 1 9 3 ∥ ( FermatNo ‘ 4 ) ) )
31 29 30 mtbiri ⊢ ( 𝑝 = 1 9 3 → ¬ 𝑝 ∥ ( FermatNo ‘ 4 ) )
32 28 31 syl ⊢ ( ( 𝑝 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) ∩ ℙ ) ∧ 𝑝 ∥ ( FermatNo ‘ 4 ) ) → ¬ 𝑝 ∥ ( FermatNo ‘ 4 ) )
33 32 pm2.01da ⊢ ( 𝑝 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) ∩ ℙ ) → ¬ 𝑝 ∥ ( FermatNo ‘ 4 ) )
34 33 rgen ⊢ ∀ 𝑝 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) ∩ ℙ ) ¬ 𝑝 ∥ ( FermatNo ‘ 4 )
35 isprm7 ⊢ ( ( FermatNo ‘ 4 ) ∈ ℙ ↔ ( ( FermatNo ‘ 4 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑝 ∈ ( ( 2 ... ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) ) ∩ ℙ ) ¬ 𝑝 ∥ ( FermatNo ‘ 4 ) ) )
36 19 34 35 mpbir2an ⊢ ( FermatNo ‘ 4 ) ∈ ℙ