Theorem fmtno

Description: The N th Fermat number. (Contributed by AV, 13-Jun-2021)

	Ref	Expression
Assertion	fmtno	|- ( N e. NN0 -> ( FermatNo ` N ) = ( ( 2 ^ ( 2 ^ N ) ) + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		df-fmtno	|- FermatNo = ( n e. NN0 |-> ( ( 2 ^ ( 2 ^ n ) ) + 1 ) )
2		oveq2	|- ( n = N -> ( 2 ^ n ) = ( 2 ^ N ) )
3	2	oveq2d	|- ( n = N -> ( 2 ^ ( 2 ^ n ) ) = ( 2 ^ ( 2 ^ N ) ) )
4	3	oveq1d	|- ( n = N -> ( ( 2 ^ ( 2 ^ n ) ) + 1 ) = ( ( 2 ^ ( 2 ^ N ) ) + 1 ) )
5		id	|- ( N e. NN0 -> N e. NN0 )
6		ovexd	|- ( N e. NN0 -> ( ( 2 ^ ( 2 ^ N ) ) + 1 ) e. _V )
7	1 4 5 6	fvmptd3	|- ( N e. NN0 -> ( FermatNo ` N ) = ( ( 2 ^ ( 2 ^ N ) ) + 1 ) )