Metamath Proof Explorer

Theorem fmtno3

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

Ref Expression
Assertion fmtno3 ( FermatNo ‘ 3 ) = 2 5 7

Proof

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