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 e. NN0
2 fmtno
 |-  ( 3 e. NN0 -> ( 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 e. NN0
10 5nn0
 |-  5 e. NN0
11 9 10 deccl
 |-  ; 2 5 e. NN0
12 6nn0
 |-  6 e. NN0
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