Metamath Proof Explorer

Theorem fmtnorec1

Description: The first recurrence relation for Fermat numbers, see Wikipedia "Fermat number", https://en.wikipedia.org/wiki/Fermat_number#Basic_properties , 22-Jul-2021. (Contributed by AV, 22-Jul-2021)

Ref Expression
Assertion fmtnorec1 ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ ( 𝑁 + 1 ) ) = ( ( ( ( FermatNo ‘ 𝑁 ) − 1 ) ↑ 2 ) + 1 ) )

Proof

Step Hyp Ref Expression
1 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
2 fmtno ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( FermatNo ‘ ( 𝑁 + 1 ) ) = ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) )
3 1 2 syl ⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ ( 𝑁 + 1 ) ) = ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) )
4 2nn0 ⊢ 2 ∈ ℕ0
5 nn0expcl ⊢ ( ( 2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℕ0 )
6 4 5 mpan ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℕ0 )
7 nn0expcl ⊢ ( ( 2 ∈ ℕ0 ∧ ( 2 ↑ 𝑁 ) ∈ ℕ0 ) → ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℕ0 )
8 7 nn0cnd ⊢ ( ( 2 ∈ ℕ0 ∧ ( 2 ↑ 𝑁 ) ∈ ℕ0 ) → ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℂ )
9 4 6 8 sylancr ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℂ )
10 pncan1 ⊢ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℂ → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) = ( 2 ↑ ( 2 ↑ 𝑁 ) ) )
11 9 10 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) = ( 2 ↑ ( 2 ↑ 𝑁 ) ) )
12 11 oveq1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) ↑ 2 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ↑ 2 ) )
13 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
14 6 nn0zd ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℤ )
15 2z ⊢ 2 ∈ ℤ
16 14 15 jctir ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ 𝑁 ) ∈ ℤ ∧ 2 ∈ ℤ ) )
17 expmulz ⊢ ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( ( 2 ↑ 𝑁 ) ∈ ℤ ∧ 2 ∈ ℤ ) ) → ( 2 ↑ ( ( 2 ↑ 𝑁 ) · 2 ) ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ↑ 2 ) )
18 13 16 17 sylancr ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( ( 2 ↑ 𝑁 ) · 2 ) ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ↑ 2 ) )
19 2cn ⊢ 2 ∈ ℂ
20 2ne0 ⊢ 2 ≠ 0
21 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
22 expp1z ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 2 ↑ ( 𝑁 + 1 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
23 19 20 21 22 mp3an12i ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( 𝑁 + 1 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
24 23 eqcomd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ 𝑁 ) · 2 ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
25 24 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( ( 2 ↑ 𝑁 ) · 2 ) ) = ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) )
26 12 18 25 3eqtr2rd ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) ↑ 2 ) )
27 26 oveq1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ ( 2 ↑ ( 𝑁 + 1 ) ) ) + 1 ) = ( ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) ↑ 2 ) + 1 ) )
28 fmtno ⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )
29 28 eqcomd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) = ( FermatNo ‘ 𝑁 ) )
30 29 oveq1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) = ( ( FermatNo ‘ 𝑁 ) − 1 ) )
31 30 oveq1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) ↑ 2 ) = ( ( ( FermatNo ‘ 𝑁 ) − 1 ) ↑ 2 ) )
32 31 oveq1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) ↑ 2 ) + 1 ) = ( ( ( ( FermatNo ‘ 𝑁 ) − 1 ) ↑ 2 ) + 1 ) )
33 3 27 32 3eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ ( 𝑁 + 1 ) ) = ( ( ( ( FermatNo ‘ 𝑁 ) − 1 ) ↑ 2 ) + 1 ) )