Metamath Proof Explorer

Theorem fmtno4

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

Ref Expression
Assertion fmtno4 
|- ( FermatNo ` 4 ) = ; ; ; ; 6 5 5 3 7

Proof

Step Hyp Ref Expression
1 4nn0 
 |-  4 e. NN0
2 fmtno 
 |-  ( 4 e. NN0 -> ( FermatNo ` 4 ) = ( ( 2 ^ ( 2 ^ 4 ) ) + 1 ) )
3 1 2 ax-mp 
 |-  ( FermatNo ` 4 ) = ( ( 2 ^ ( 2 ^ 4 ) ) + 1 )
4 2exp4 
 |-  ( 2 ^ 4 ) = ; 1 6
5 4 oveq2i 
 |-  ( 2 ^ ( 2 ^ 4 ) ) = ( 2 ^ ; 1 6 )
6 5 oveq1i 
 |-  ( ( 2 ^ ( 2 ^ 4 ) ) + 1 ) = ( ( 2 ^ ; 1 6 ) + 1 )
7 2exp16 
 |-  ( 2 ^ ; 1 6 ) = ; ; ; ; 6 5 5 3 6
8 7 oveq1i 
 |-  ( ( 2 ^ ; 1 6 ) + 1 ) = ( ; ; ; ; 6 5 5 3 6 + 1 )
9 6nn0 
 |-  6 e. NN0
10 5nn0 
 |-  5 e. NN0
11 9 10 deccl 
 |-  ; 6 5 e. NN0
12 11 10 deccl 
 |-  ; ; 6 5 5 e. NN0
13 3nn0 
 |-  3 e. NN0
14 12 13 deccl 
 |-  ; ; ; 6 5 5 3 e. NN0
15 6p1e7 
 |-  ( 6 + 1 ) = 7
16 eqid 
 |-  ; ; ; ; 6 5 5 3 6 = ; ; ; ; 6 5 5 3 6
17 14 9 15 16 decsuc 
 |-  ( ; ; ; ; 6 5 5 3 6 + 1 ) = ; ; ; ; 6 5 5 3 7
18 6 8 17 3eqtri 
 |-  ( ( 2 ^ ( 2 ^ 4 ) ) + 1 ) = ; ; ; ; 6 5 5 3 7
19 3 18 eqtri 
 |-  ( FermatNo ` 4 ) = ; ; ; ; 6 5 5 3 7