Metamath Proof Explorer

Theorem fmtno2

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

Ref Expression
Assertion fmtno2 ( FermatNo ‘ 2 ) = 1 7

Proof

Step Hyp Ref Expression
1 2nn0 ⊢ 2 ∈ ℕ0
2 fmtno ⊢ ( 2 ∈ ℕ0 → ( FermatNo ‘ 2 ) = ( ( 2 ↑ ( 2 ↑ 2 ) ) + 1 ) )
3 1 2 ax-mp ⊢ ( FermatNo ‘ 2 ) = ( ( 2 ↑ ( 2 ↑ 2 ) ) + 1 )
4 sq2 ⊢ ( 2 ↑ 2 ) = 4
5 4 oveq2i ⊢ ( 2 ↑ ( 2 ↑ 2 ) ) = ( 2 ↑ 4 )
6 5 oveq1i ⊢ ( ( 2 ↑ ( 2 ↑ 2 ) ) + 1 ) = ( ( 2 ↑ 4 ) + 1 )
7 2exp4 ⊢ ( 2 ↑ 4 ) = 1 6
8 7 oveq1i ⊢ ( ( 2 ↑ 4 ) + 1 ) = ( 1 6 + 1 )
9 1nn0 ⊢ 1 ∈ ℕ0
10 6nn0 ⊢ 6 ∈ ℕ0
11 6p1e7 ⊢ ( 6 + 1 ) = 7
12 eqid ⊢ 1 6 = 1 6
13 9 10 11 12 decsuc ⊢ ( 1 6 + 1 ) = 1 7
14 6 8 13 3eqtri ⊢ ( ( 2 ↑ ( 2 ↑ 2 ) ) + 1 ) = 1 7
15 3 14 eqtri ⊢ ( FermatNo ‘ 2 ) = 1 7