Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . . 4
⊢ (𝑥 = 0 → (𝑥 + 1) = (0 + 1)) |
2 | 1 | fveq2d 6195 |
. . 3
⊢ (𝑥 = 0 →
(FermatNo‘(𝑥 + 1)) =
(FermatNo‘(0 + 1))) |
3 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = 0 → (0...𝑥) = (0...0)) |
4 | 3 | prodeq1d 14651 |
. . . 4
⊢ (𝑥 = 0 → ∏𝑛 ∈ (0...𝑥)(FermatNo‘𝑛) = ∏𝑛 ∈ (0...0)(FermatNo‘𝑛)) |
5 | 4 | oveq1d 6665 |
. . 3
⊢ (𝑥 = 0 → (∏𝑛 ∈ (0...𝑥)(FermatNo‘𝑛) + 2) = (∏𝑛 ∈ (0...0)(FermatNo‘𝑛) + 2)) |
6 | 2, 5 | eqeq12d 2637 |
. 2
⊢ (𝑥 = 0 →
((FermatNo‘(𝑥 + 1)) =
(∏𝑛 ∈ (0...𝑥)(FermatNo‘𝑛) + 2) ↔ (FermatNo‘(0
+ 1)) = (∏𝑛 ∈
(0...0)(FermatNo‘𝑛) +
2))) |
7 | | oveq1 6657 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑥 + 1) = (𝑦 + 1)) |
8 | 7 | fveq2d 6195 |
. . 3
⊢ (𝑥 = 𝑦 → (FermatNo‘(𝑥 + 1)) = (FermatNo‘(𝑦 + 1))) |
9 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = 𝑦 → (0...𝑥) = (0...𝑦)) |
10 | 9 | prodeq1d 14651 |
. . . 4
⊢ (𝑥 = 𝑦 → ∏𝑛 ∈ (0...𝑥)(FermatNo‘𝑛) = ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛)) |
11 | 10 | oveq1d 6665 |
. . 3
⊢ (𝑥 = 𝑦 → (∏𝑛 ∈ (0...𝑥)(FermatNo‘𝑛) + 2) = (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2)) |
12 | 8, 11 | eqeq12d 2637 |
. 2
⊢ (𝑥 = 𝑦 → ((FermatNo‘(𝑥 + 1)) = (∏𝑛 ∈ (0...𝑥)(FermatNo‘𝑛) + 2) ↔ (FermatNo‘(𝑦 + 1)) = (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2))) |
13 | | oveq1 6657 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝑥 + 1) = ((𝑦 + 1) + 1)) |
14 | 13 | fveq2d 6195 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → (FermatNo‘(𝑥 + 1)) = (FermatNo‘((𝑦 + 1) + 1))) |
15 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (0...𝑥) = (0...(𝑦 + 1))) |
16 | 15 | prodeq1d 14651 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → ∏𝑛 ∈ (0...𝑥)(FermatNo‘𝑛) = ∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛)) |
17 | 16 | oveq1d 6665 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → (∏𝑛 ∈ (0...𝑥)(FermatNo‘𝑛) + 2) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2)) |
18 | 14, 17 | eqeq12d 2637 |
. 2
⊢ (𝑥 = (𝑦 + 1) → ((FermatNo‘(𝑥 + 1)) = (∏𝑛 ∈ (0...𝑥)(FermatNo‘𝑛) + 2) ↔ (FermatNo‘((𝑦 + 1) + 1)) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2))) |
19 | | oveq1 6657 |
. . . 4
⊢ (𝑥 = 𝑁 → (𝑥 + 1) = (𝑁 + 1)) |
20 | 19 | fveq2d 6195 |
. . 3
⊢ (𝑥 = 𝑁 → (FermatNo‘(𝑥 + 1)) = (FermatNo‘(𝑁 + 1))) |
21 | | oveq2 6658 |
. . . 4
⊢ (𝑥 = 𝑁 → (0...𝑥) = (0...𝑁)) |
22 | | prodeq1 14639 |
. . . . 5
⊢
((0...𝑥) =
(0...𝑁) → ∏𝑛 ∈ (0...𝑥)(FermatNo‘𝑛) = ∏𝑛 ∈ (0...𝑁)(FermatNo‘𝑛)) |
23 | 22 | oveq1d 6665 |
. . . 4
⊢
((0...𝑥) =
(0...𝑁) →
(∏𝑛 ∈ (0...𝑥)(FermatNo‘𝑛) + 2) = (∏𝑛 ∈ (0...𝑁)(FermatNo‘𝑛) + 2)) |
24 | 21, 23 | syl 17 |
. . 3
⊢ (𝑥 = 𝑁 → (∏𝑛 ∈ (0...𝑥)(FermatNo‘𝑛) + 2) = (∏𝑛 ∈ (0...𝑁)(FermatNo‘𝑛) + 2)) |
25 | 20, 24 | eqeq12d 2637 |
. 2
⊢ (𝑥 = 𝑁 → ((FermatNo‘(𝑥 + 1)) = (∏𝑛 ∈ (0...𝑥)(FermatNo‘𝑛) + 2) ↔ (FermatNo‘(𝑁 + 1)) = (∏𝑛 ∈ (0...𝑁)(FermatNo‘𝑛) + 2))) |
26 | | fmtno0 41452 |
. . . . 5
⊢
(FermatNo‘0) = 3 |
27 | 26 | oveq1i 6660 |
. . . 4
⊢
((FermatNo‘0) + 2) = (3 + 2) |
28 | | 3p2e5 11160 |
. . . 4
⊢ (3 + 2) =
5 |
29 | 27, 28 | eqtri 2644 |
. . 3
⊢
((FermatNo‘0) + 2) = 5 |
30 | | fz0sn 12439 |
. . . . . 6
⊢ (0...0) =
{0} |
31 | 30 | prodeq1i 14648 |
. . . . 5
⊢
∏𝑛 ∈
(0...0)(FermatNo‘𝑛) =
∏𝑛 ∈ {0}
(FermatNo‘𝑛) |
32 | | 0z 11388 |
. . . . . 6
⊢ 0 ∈
ℤ |
33 | | 0nn0 11307 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
34 | | fmtnonn 41443 |
. . . . . . . 8
⊢ (0 ∈
ℕ0 → (FermatNo‘0) ∈ ℕ) |
35 | 34 | nncnd 11036 |
. . . . . . 7
⊢ (0 ∈
ℕ0 → (FermatNo‘0) ∈ ℂ) |
36 | 33, 35 | ax-mp 5 |
. . . . . 6
⊢
(FermatNo‘0) ∈ ℂ |
37 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑛 = 0 →
(FermatNo‘𝑛) =
(FermatNo‘0)) |
38 | 37 | prodsn 14692 |
. . . . . 6
⊢ ((0
∈ ℤ ∧ (FermatNo‘0) ∈ ℂ) → ∏𝑛 ∈ {0}
(FermatNo‘𝑛) =
(FermatNo‘0)) |
39 | 32, 36, 38 | mp2an 708 |
. . . . 5
⊢
∏𝑛 ∈ {0}
(FermatNo‘𝑛) =
(FermatNo‘0) |
40 | 31, 39 | eqtri 2644 |
. . . 4
⊢
∏𝑛 ∈
(0...0)(FermatNo‘𝑛) =
(FermatNo‘0) |
41 | 40 | oveq1i 6660 |
. . 3
⊢
(∏𝑛 ∈
(0...0)(FermatNo‘𝑛) +
2) = ((FermatNo‘0) + 2) |
42 | | 0p1e1 11132 |
. . . . 5
⊢ (0 + 1) =
1 |
43 | 42 | fveq2i 6194 |
. . . 4
⊢
(FermatNo‘(0 + 1)) = (FermatNo‘1) |
44 | | fmtno1 41453 |
. . . 4
⊢
(FermatNo‘1) = 5 |
45 | 43, 44 | eqtri 2644 |
. . 3
⊢
(FermatNo‘(0 + 1)) = 5 |
46 | 29, 41, 45 | 3eqtr4ri 2655 |
. 2
⊢
(FermatNo‘(0 + 1)) = (∏𝑛 ∈ (0...0)(FermatNo‘𝑛) + 2) |
47 | | fmtnorec2lem 41454 |
. 2
⊢ (𝑦 ∈ ℕ0
→ ((FermatNo‘(𝑦
+ 1)) = (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2) → (FermatNo‘((𝑦 + 1) + 1)) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2))) |
48 | 6, 12, 18, 25, 46, 47 | nn0ind 11472 |
1
⊢ (𝑁 ∈ ℕ0
→ (FermatNo‘(𝑁 +
1)) = (∏𝑛 ∈
(0...𝑁)(FermatNo‘𝑛) + 2)) |