Metamath Proof Explorer

Theorem fmtno1

Description: The 1 st Fermat number, see remark in ApostolNT p. 7. (Contributed by AV, 13-Jun-2021)

Ref Expression
Assertion fmtno1 
|- ( FermatNo ` 1 ) = 5

Proof

Step Hyp Ref Expression
1 1nn0 
 |-  1 e. NN0
2 fmtno 
 |-  ( 1 e. NN0 -> ( FermatNo ` 1 ) = ( ( 2 ^ ( 2 ^ 1 ) ) + 1 ) )
3 1 2 ax-mp 
 |-  ( FermatNo ` 1 ) = ( ( 2 ^ ( 2 ^ 1 ) ) + 1 )
4 2cn 
 |-  2 e. CC
5 exp1 
 |-  ( 2 e. CC -> ( 2 ^ 1 ) = 2 )
6 4 5 ax-mp 
 |-  ( 2 ^ 1 ) = 2
7 6 oveq2i 
 |-  ( 2 ^ ( 2 ^ 1 ) ) = ( 2 ^ 2 )
8 7 oveq1i 
 |-  ( ( 2 ^ ( 2 ^ 1 ) ) + 1 ) = ( ( 2 ^ 2 ) + 1 )
9 sq2 
 |-  ( 2 ^ 2 ) = 4
10 9 oveq1i 
 |-  ( ( 2 ^ 2 ) + 1 ) = ( 4 + 1 )
11 4p1e5 
 |-  ( 4 + 1 ) = 5
12 8 10 11 3eqtri 
 |-  ( ( 2 ^ ( 2 ^ 1 ) ) + 1 ) = 5
13 3 12 eqtri 
 |-  ( FermatNo ` 1 ) = 5