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 ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ ( 𝑁 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑁 ) ( FermatNo ‘ 𝑛 ) + 2 ) )

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢ ( 𝑥 = 0 → ( FermatNo ‘ ( 𝑥 + 1 ) ) = ( FermatNo ‘ ( 0 + 1 ) ) )
2 oveq2 ⊢ ( 𝑥 = 0 → ( 0 ... 𝑥 ) = ( 0 ... 0 ) )
3 2 prodeq1d ⊢ ( 𝑥 = 0 → ∏ 𝑛 ∈ ( 0 ... 𝑥 ) ( FermatNo ‘ 𝑛 ) = ∏ 𝑛 ∈ ( 0 ... 0 ) ( FermatNo ‘ 𝑛 ) )
4 3 oveq1d ⊢ ( 𝑥 = 0 → ( ∏ 𝑛 ∈ ( 0 ... 𝑥 ) ( FermatNo ‘ 𝑛 ) + 2 ) = ( ∏ 𝑛 ∈ ( 0 ... 0 ) ( FermatNo ‘ 𝑛 ) + 2 ) )
5 1 4 eqeq12d ⊢ ( 𝑥 = 0 → ( ( FermatNo ‘ ( 𝑥 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑥 ) ( FermatNo ‘ 𝑛 ) + 2 ) ↔ ( FermatNo ‘ ( 0 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 0 ) ( FermatNo ‘ 𝑛 ) + 2 ) ) )
6 fvoveq1 ⊢ ( 𝑥 = 𝑦 → ( FermatNo ‘ ( 𝑥 + 1 ) ) = ( FermatNo ‘ ( 𝑦 + 1 ) ) )
7 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 0 ... 𝑥 ) = ( 0 ... 𝑦 ) )
8 7 prodeq1d ⊢ ( 𝑥 = 𝑦 → ∏ 𝑛 ∈ ( 0 ... 𝑥 ) ( FermatNo ‘ 𝑛 ) = ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) )
9 8 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ∏ 𝑛 ∈ ( 0 ... 𝑥 ) ( FermatNo ‘ 𝑛 ) + 2 ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) )
10 6 9 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( FermatNo ‘ ( 𝑥 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑥 ) ( FermatNo ‘ 𝑛 ) + 2 ) ↔ ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) ) )
11 fvoveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( FermatNo ‘ ( 𝑥 + 1 ) ) = ( FermatNo ‘ ( ( 𝑦 + 1 ) + 1 ) ) )
12 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 0 ... 𝑥 ) = ( 0 ... ( 𝑦 + 1 ) ) )
13 12 prodeq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ∏ 𝑛 ∈ ( 0 ... 𝑥 ) ( FermatNo ‘ 𝑛 ) = ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) )
14 13 oveq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ∏ 𝑛 ∈ ( 0 ... 𝑥 ) ( FermatNo ‘ 𝑛 ) + 2 ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + 2 ) )
15 11 14 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( FermatNo ‘ ( 𝑥 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑥 ) ( FermatNo ‘ 𝑛 ) + 2 ) ↔ ( FermatNo ‘ ( ( 𝑦 + 1 ) + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + 2 ) ) )
16 fvoveq1 ⊢ ( 𝑥 = 𝑁 → ( FermatNo ‘ ( 𝑥 + 1 ) ) = ( FermatNo ‘ ( 𝑁 + 1 ) ) )
17 oveq2 ⊢ ( 𝑥 = 𝑁 → ( 0 ... 𝑥 ) = ( 0 ... 𝑁 ) )
18 prodeq1 ⊢ ( ( 0 ... 𝑥 ) = ( 0 ... 𝑁 ) → ∏ 𝑛 ∈ ( 0 ... 𝑥 ) ( FermatNo ‘ 𝑛 ) = ∏ 𝑛 ∈ ( 0 ... 𝑁 ) ( FermatNo ‘ 𝑛 ) )
19 18 oveq1d ⊢ ( ( 0 ... 𝑥 ) = ( 0 ... 𝑁 ) → ( ∏ 𝑛 ∈ ( 0 ... 𝑥 ) ( FermatNo ‘ 𝑛 ) + 2 ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑁 ) ( FermatNo ‘ 𝑛 ) + 2 ) )
20 17 19 syl ⊢ ( 𝑥 = 𝑁 → ( ∏ 𝑛 ∈ ( 0 ... 𝑥 ) ( FermatNo ‘ 𝑛 ) + 2 ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑁 ) ( FermatNo ‘ 𝑛 ) + 2 ) )
21 16 20 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( FermatNo ‘ ( 𝑥 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑥 ) ( FermatNo ‘ 𝑛 ) + 2 ) ↔ ( FermatNo ‘ ( 𝑁 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑁 ) ( FermatNo ‘ 𝑛 ) + 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 ⊢ ∏ 𝑛 ∈ ( 0 ... 0 ) ( FermatNo ‘ 𝑛 ) = ∏ 𝑛 ∈ { 0 } ( FermatNo ‘ 𝑛 )
28 0z ⊢ 0 ∈ ℤ
29 0nn0 ⊢ 0 ∈ ℕ0
30 fmtnonn ⊢ ( 0 ∈ ℕ0 → ( FermatNo ‘ 0 ) ∈ ℕ )
31 30 nncnd ⊢ ( 0 ∈ ℕ0 → ( FermatNo ‘ 0 ) ∈ ℂ )
32 29 31 ax-mp ⊢ ( FermatNo ‘ 0 ) ∈ ℂ
33 fveq2 ⊢ ( 𝑛 = 0 → ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 0 ) )
34 33 prodsn ⊢ ( ( 0 ∈ ℤ ∧ ( FermatNo ‘ 0 ) ∈ ℂ ) → ∏ 𝑛 ∈ { 0 } ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 0 ) )
35 28 32 34 mp2an ⊢ ∏ 𝑛 ∈ { 0 } ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 0 )
36 27 35 eqtri ⊢ ∏ 𝑛 ∈ ( 0 ... 0 ) ( FermatNo ‘ 𝑛 ) = ( FermatNo ‘ 0 )
37 36 oveq1i ⊢ ( ∏ 𝑛 ∈ ( 0 ... 0 ) ( FermatNo ‘ 𝑛 ) + 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 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 0 ) ( FermatNo ‘ 𝑛 ) + 2 )
43 fmtnorec2lem ⊢ ( 𝑦 ∈ ℕ0 → ( ( FermatNo ‘ ( 𝑦 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑦 ) ( FermatNo ‘ 𝑛 ) + 2 ) → ( FermatNo ‘ ( ( 𝑦 + 1 ) + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... ( 𝑦 + 1 ) ) ( FermatNo ‘ 𝑛 ) + 2 ) ) )
44 5 10 15 21 42 43 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ ( 𝑁 + 1 ) ) = ( ∏ 𝑛 ∈ ( 0 ... 𝑁 ) ( FermatNo ‘ 𝑛 ) + 2 ) )