Metamath Proof Explorer

Theorem fmtno5

Description: The 5 th Fermat number. (Contributed by AV, 30-Jul-2021)

Ref Expression
Assertion fmtno5 
|- ( FermatNo ` 5 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 7

Proof

Step Hyp Ref Expression
1 df-5 
 |-  5 = ( 4 + 1 )
2 1 fveq2i 
 |-  ( FermatNo ` 5 ) = ( FermatNo ` ( 4 + 1 ) )
3 4nn0 
 |-  4 e. NN0
4 fmtnorec1 
 |-  ( 4 e. NN0 -> ( FermatNo ` ( 4 + 1 ) ) = ( ( ( ( FermatNo ` 4 ) - 1 ) ^ 2 ) + 1 ) )
5 3 4 ax-mp 
 |-  ( FermatNo ` ( 4 + 1 ) ) = ( ( ( ( FermatNo ` 4 ) - 1 ) ^ 2 ) + 1 )
6 2 5 eqtri 
 |-  ( FermatNo ` 5 ) = ( ( ( ( FermatNo ` 4 ) - 1 ) ^ 2 ) + 1 )
7 2nn0 
 |-  2 e. NN0
8 3 7 deccl 
 |-  ; 4 2 e. NN0
9 9nn0 
 |-  9 e. NN0
10 8 9 deccl 
 |-  ; ; 4 2 9 e. NN0
11 10 3 deccl 
 |-  ; ; ; 4 2 9 4 e. NN0
12 11 9 deccl 
 |-  ; ; ; ; 4 2 9 4 9 e. NN0
13 6nn0 
 |-  6 e. NN0
14 12 13 deccl 
 |-  ; ; ; ; ; 4 2 9 4 9 6 e. NN0
15 7nn0 
 |-  7 e. NN0
16 14 15 deccl 
 |-  ; ; ; ; ; ; 4 2 9 4 9 6 7 e. NN0
17 16 7 deccl 
 |-  ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 e. NN0
18 17 9 deccl 
 |-  ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 e. NN0
19 6p1e7 
 |-  ( 6 + 1 ) = 7
20 5nn0 
 |-  5 e. NN0
21 13 20 deccl 
 |-  ; 6 5 e. NN0
22 21 20 deccl 
 |-  ; ; 6 5 5 e. NN0
23 3nn0 
 |-  3 e. NN0
24 22 23 deccl 
 |-  ; ; ; 6 5 5 3 e. NN0
25 1nn0 
 |-  1 e. NN0
26 fmtno4 
 |-  ( FermatNo ` 4 ) = ; ; ; ; 6 5 5 3 7
27 3p1e4 
 |-  ( 3 + 1 ) = 4
28 eqid 
 |-  ; ; ; 6 5 5 3 = ; ; ; 6 5 5 3
29 22 23 27 28 decsuc 
 |-  ( ; ; ; 6 5 5 3 + 1 ) = ; ; ; 6 5 5 4
30 6cn 
 |-  6 e. CC
31 ax-1cn 
 |-  1 e. CC
32 df-7 
 |-  7 = ( 6 + 1 )
33 30 31 32 mvrraddi 
 |-  ( 7 - 1 ) = 6
34 24 15 25 26 29 33 decsubi 
 |-  ( ( FermatNo ` 4 ) - 1 ) = ; ; ; ; 6 5 5 3 6
35 34 oveq1i 
 |-  ( ( ( FermatNo ` 4 ) - 1 ) ^ 2 ) = ( ; ; ; ; 6 5 5 3 6 ^ 2 )
36 fmtno5lem4 
 |-  ( ; ; ; ; 6 5 5 3 6 ^ 2 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 6
37 35 36 eqtri 
 |-  ( ( ( FermatNo ` 4 ) - 1 ) ^ 2 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 6
38 18 13 19 37 decsuc 
 |-  ( ( ( ( FermatNo ` 4 ) - 1 ) ^ 2 ) + 1 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 7
39 6 38 eqtri 
 |-  ( FermatNo ` 5 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 7