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 ∈ ℕ0
2 fmtno ( 1 ∈ ℕ0 → ( FermatNo ‘ 1 ) = ( ( 2 ↑ ( 2 ↑ 1 ) ) + 1 ) )
3 1 2 ax-mp ( FermatNo ‘ 1 ) = ( ( 2 ↑ ( 2 ↑ 1 ) ) + 1 )
4 2cn 2 ∈ ℂ
5 exp1 ( 2 ∈ ℂ → ( 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