Metamath Proof Explorer

Theorem fmtnoodd

Description: Each Fermat number is odd. (Contributed by AV, 26-Jul-2021)

Ref Expression
Assertion fmtnoodd ( 𝑁 ∈ ℕ0 → ¬ 2 ∥ ( FermatNo ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 2nn ⊢ 2 ∈ ℕ
2 1 a1i ⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℕ )
3 id ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
4 2 3 nnexpcld ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℕ )
5 nnm1nn0 ⊢ ( ( 2 ↑ 𝑁 ) ∈ ℕ → ( ( 2 ↑ 𝑁 ) − 1 ) ∈ ℕ0 )
6 4 5 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ 𝑁 ) − 1 ) ∈ ℕ0 )
7 2 6 nnexpcld ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( ( 2 ↑ 𝑁 ) − 1 ) ) ∈ ℕ )
8 7 nnzd ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( ( 2 ↑ 𝑁 ) − 1 ) ) ∈ ℤ )
9 oveq2 ⊢ ( 𝑘 = ( 2 ↑ ( ( 2 ↑ 𝑁 ) − 1 ) ) → ( 2 · 𝑘 ) = ( 2 · ( 2 ↑ ( ( 2 ↑ 𝑁 ) − 1 ) ) ) )
10 9 oveq1d ⊢ ( 𝑘 = ( 2 ↑ ( ( 2 ↑ 𝑁 ) − 1 ) ) → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · ( 2 ↑ ( ( 2 ↑ 𝑁 ) − 1 ) ) ) + 1 ) )
11 fmtno ⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )
12 10 11 eqeqan12rd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 = ( 2 ↑ ( ( 2 ↑ 𝑁 ) − 1 ) ) ) → ( ( ( 2 · 𝑘 ) + 1 ) = ( FermatNo ‘ 𝑁 ) ↔ ( ( 2 · ( 2 ↑ ( ( 2 ↑ 𝑁 ) − 1 ) ) ) + 1 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) ) )
13 2cnd ⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℂ )
14 7 nncnd ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( ( 2 ↑ 𝑁 ) − 1 ) ) ∈ ℂ )
15 13 14 mulcomd ⊢ ( 𝑁 ∈ ℕ0 → ( 2 · ( 2 ↑ ( ( 2 ↑ 𝑁 ) − 1 ) ) ) = ( ( 2 ↑ ( ( 2 ↑ 𝑁 ) − 1 ) ) · 2 ) )
16 expm1t ⊢ ( ( 2 ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ∈ ℕ ) → ( 2 ↑ ( 2 ↑ 𝑁 ) ) = ( ( 2 ↑ ( ( 2 ↑ 𝑁 ) − 1 ) ) · 2 ) )
17 13 4 16 syl2anc ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ 𝑁 ) ) = ( ( 2 ↑ ( ( 2 ↑ 𝑁 ) − 1 ) ) · 2 ) )
18 15 17 eqtr4d ⊢ ( 𝑁 ∈ ℕ0 → ( 2 · ( 2 ↑ ( ( 2 ↑ 𝑁 ) − 1 ) ) ) = ( 2 ↑ ( 2 ↑ 𝑁 ) ) )
19 18 oveq1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 · ( 2 ↑ ( ( 2 ↑ 𝑁 ) − 1 ) ) ) + 1 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )
20 8 12 19 rspcedvd ⊢ ( 𝑁 ∈ ℕ0 → ∃ 𝑘 ∈ ℤ ( ( 2 · 𝑘 ) + 1 ) = ( FermatNo ‘ 𝑁 ) )
21 fmtnonn ⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) ∈ ℕ )
22 21 nnzd ⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) ∈ ℤ )
23 odd2np1 ⊢ ( ( FermatNo ‘ 𝑁 ) ∈ ℤ → ( ¬ 2 ∥ ( FermatNo ‘ 𝑁 ) ↔ ∃ 𝑘 ∈ ℤ ( ( 2 · 𝑘 ) + 1 ) = ( FermatNo ‘ 𝑁 ) ) )
24 22 23 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ¬ 2 ∥ ( FermatNo ‘ 𝑁 ) ↔ ∃ 𝑘 ∈ ℤ ( ( 2 · 𝑘 ) + 1 ) = ( FermatNo ‘ 𝑁 ) ) )
25 20 24 mpbird ⊢ ( 𝑁 ∈ ℕ0 → ¬ 2 ∥ ( FermatNo ‘ 𝑁 ) )