Metamath Proof Explorer

Theorem fmtnorec2

Description: The second recurrence relation for Fermat numbers, see ProofWiki "Product of Sequence of Fermat Numbers plus 2", 29-Jul-2021, https://proofwiki.org/wiki/Product_of_Sequence_of_Fermat_Numbers_plus_2 or Wikipedia "Fermat number", 29-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties . (Contributed by AV, 29-Jul-2021)

Ref Expression
Assertion fmtnorec2 
|- ( N e. NN0 -> ( FermatNo ` ( N + 1 ) ) = ( prod_ n e. ( 0 ... N ) ( FermatNo ` n ) + 2 ) )

Proof

Step Hyp Ref Expression
1 fvoveq1 
 |-  ( x = 0 -> ( FermatNo ` ( x + 1 ) ) = ( FermatNo ` ( 0 + 1 ) ) )
2 oveq2 
 |-  ( x = 0 -> ( 0 ... x ) = ( 0 ... 0 ) )
3 2 prodeq1d 
 |-  ( x = 0 -> prod_ n e. ( 0 ... x ) ( FermatNo ` n ) = prod_ n e. ( 0 ... 0 ) ( FermatNo ` n ) )
4 3 oveq1d 
 |-  ( x = 0 -> ( prod_ n e. ( 0 ... x ) ( FermatNo ` n ) + 2 ) = ( prod_ n e. ( 0 ... 0 ) ( FermatNo ` n ) + 2 ) )
5 1 4 eqeq12d 
 |-  ( x = 0 -> ( ( FermatNo ` ( x + 1 ) ) = ( prod_ n e. ( 0 ... x ) ( FermatNo ` n ) + 2 ) <-> ( FermatNo ` ( 0 + 1 ) ) = ( prod_ n e. ( 0 ... 0 ) ( FermatNo ` n ) + 2 ) ) )
6 fvoveq1 
 |-  ( x = y -> ( FermatNo ` ( x + 1 ) ) = ( FermatNo ` ( y + 1 ) ) )
7 oveq2 
 |-  ( x = y -> ( 0 ... x ) = ( 0 ... y ) )
8 7 prodeq1d 
 |-  ( x = y -> prod_ n e. ( 0 ... x ) ( FermatNo ` n ) = prod_ n e. ( 0 ... y ) ( FermatNo ` n ) )
9 8 oveq1d 
 |-  ( x = y -> ( prod_ n e. ( 0 ... x ) ( FermatNo ` n ) + 2 ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) )
10 6 9 eqeq12d 
 |-  ( x = y -> ( ( FermatNo ` ( x + 1 ) ) = ( prod_ n e. ( 0 ... x ) ( FermatNo ` n ) + 2 ) <-> ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) ) )
11 fvoveq1 
 |-  ( x = ( y + 1 ) -> ( FermatNo ` ( x + 1 ) ) = ( FermatNo ` ( ( y + 1 ) + 1 ) ) )
12 oveq2 
 |-  ( x = ( y + 1 ) -> ( 0 ... x ) = ( 0 ... ( y + 1 ) ) )
13 12 prodeq1d 
 |-  ( x = ( y + 1 ) -> prod_ n e. ( 0 ... x ) ( FermatNo ` n ) = prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) )
14 13 oveq1d 
 |-  ( x = ( y + 1 ) -> ( prod_ n e. ( 0 ... x ) ( FermatNo ` n ) + 2 ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + 2 ) )
15 11 14 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( FermatNo ` ( x + 1 ) ) = ( prod_ n e. ( 0 ... x ) ( FermatNo ` n ) + 2 ) <-> ( FermatNo ` ( ( y + 1 ) + 1 ) ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + 2 ) ) )
16 fvoveq1 
 |-  ( x = N -> ( FermatNo ` ( x + 1 ) ) = ( FermatNo ` ( N + 1 ) ) )
17 oveq2 
 |-  ( x = N -> ( 0 ... x ) = ( 0 ... N ) )
18 prodeq1 
 |-  ( ( 0 ... x ) = ( 0 ... N ) -> prod_ n e. ( 0 ... x ) ( FermatNo ` n ) = prod_ n e. ( 0 ... N ) ( FermatNo ` n ) )
19 18 oveq1d 
 |-  ( ( 0 ... x ) = ( 0 ... N ) -> ( prod_ n e. ( 0 ... x ) ( FermatNo ` n ) + 2 ) = ( prod_ n e. ( 0 ... N ) ( FermatNo ` n ) + 2 ) )
20 17 19 syl 
 |-  ( x = N -> ( prod_ n e. ( 0 ... x ) ( FermatNo ` n ) + 2 ) = ( prod_ n e. ( 0 ... N ) ( FermatNo ` n ) + 2 ) )
21 16 20 eqeq12d 
 |-  ( x = N -> ( ( FermatNo ` ( x + 1 ) ) = ( prod_ n e. ( 0 ... x ) ( FermatNo ` n ) + 2 ) <-> ( FermatNo ` ( N + 1 ) ) = ( prod_ n e. ( 0 ... N ) ( FermatNo ` n ) + 2 ) ) )
22 fmtno0 
 |-  ( FermatNo ` 0 ) = 3
23 22 oveq1i 
 |-  ( ( FermatNo ` 0 ) + 2 ) = ( 3 + 2 )
24 3p2e5 
 |-  ( 3 + 2 ) = 5
25 23 24 eqtri 
 |-  ( ( FermatNo ` 0 ) + 2 ) = 5
26 fz0sn 
 |-  ( 0 ... 0 ) = { 0 }
27 26 prodeq1i 
 |-  prod_ n e. ( 0 ... 0 ) ( FermatNo ` n ) = prod_ n e. { 0 } ( FermatNo ` n )
28 0z 
 |-  0 e. ZZ
29 0nn0 
 |-  0 e. NN0
30 fmtnonn 
 |-  ( 0 e. NN0 -> ( FermatNo ` 0 ) e. NN )
31 30 nncnd 
 |-  ( 0 e. NN0 -> ( FermatNo ` 0 ) e. CC )
32 29 31 ax-mp 
 |-  ( FermatNo ` 0 ) e. CC
33 fveq2 
 |-  ( n = 0 -> ( FermatNo ` n ) = ( FermatNo ` 0 ) )
34 33 prodsn 
 |-  ( ( 0 e. ZZ /\ ( FermatNo ` 0 ) e. CC ) -> prod_ n e. { 0 } ( FermatNo ` n ) = ( FermatNo ` 0 ) )
35 28 32 34 mp2an 
 |-  prod_ n e. { 0 } ( FermatNo ` n ) = ( FermatNo ` 0 )
36 27 35 eqtri 
 |-  prod_ n e. ( 0 ... 0 ) ( FermatNo ` n ) = ( FermatNo ` 0 )
37 36 oveq1i 
 |-  ( prod_ n e. ( 0 ... 0 ) ( FermatNo ` n ) + 2 ) = ( ( FermatNo ` 0 ) + 2 )
38 0p1e1 
 |-  ( 0 + 1 ) = 1
39 38 fveq2i 
 |-  ( FermatNo ` ( 0 + 1 ) ) = ( FermatNo ` 1 )
40 fmtno1 
 |-  ( FermatNo ` 1 ) = 5
41 39 40 eqtri 
 |-  ( FermatNo ` ( 0 + 1 ) ) = 5
42 25 37 41 3eqtr4ri 
 |-  ( FermatNo ` ( 0 + 1 ) ) = ( prod_ n e. ( 0 ... 0 ) ( FermatNo ` n ) + 2 )
43 fmtnorec2lem 
 |-  ( y e. NN0 -> ( ( FermatNo ` ( y + 1 ) ) = ( prod_ n e. ( 0 ... y ) ( FermatNo ` n ) + 2 ) -> ( FermatNo ` ( ( y + 1 ) + 1 ) ) = ( prod_ n e. ( 0 ... ( y + 1 ) ) ( FermatNo ` n ) + 2 ) ) )
44 5 10 15 21 42 43 nn0ind 
 |-  ( N e. NN0 -> ( FermatNo ` ( N + 1 ) ) = ( prod_ n e. ( 0 ... N ) ( FermatNo ` n ) + 2 ) )