Theorem fmtnom1nn

Description: A Fermat number minus one is a power of a power of two. (Contributed by AV, 29-Jul-2021)

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

Proof

Step	Hyp	Ref	Expression
1		fmtno	⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) = ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) )
2	1	oveq1d	⊢ ( 𝑁 ∈ ℕ0 → ( ( FermatNo ‘ 𝑁 ) − 1 ) = ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) )
3		2nn0	⊢ 2 ∈ ℕ0
4	3	a1i	⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℕ0 )
5		id	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
6	4 5	nn0expcld	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℕ0 )
7	4 6	nn0expcld	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℕ0 )
8	7	nn0cnd	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℂ )
9		pncan1	⊢ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) ∈ ℂ → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) = ( 2 ↑ ( 2 ↑ 𝑁 ) ) )
10	8 9	syl	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 1 ) − 1 ) = ( 2 ↑ ( 2 ↑ 𝑁 ) ) )
11	2 10	eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( ( FermatNo ‘ 𝑁 ) − 1 ) = ( 2 ↑ ( 2 ↑ 𝑁 ) ) )