Proof of Theorem fmtnorec2lem
| Step | Hyp | Ref
| Expression |
| 1 | | peano2nn0 12566 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ (𝑦 + 1) ∈
ℕ0) |
| 2 | | peano2nn0 12566 |
. . . . . 6
⊢ ((𝑦 + 1) ∈ ℕ0
→ ((𝑦 + 1) + 1) ∈
ℕ0) |
| 3 | | fmtno 47516 |
. . . . . 6
⊢ (((𝑦 + 1) + 1) ∈
ℕ0 → (FermatNo‘((𝑦 + 1) + 1)) = ((2↑(2↑((𝑦 + 1) + 1))) +
1)) |
| 4 | 1, 2, 3 | 3syl 18 |
. . . . 5
⊢ (𝑦 ∈ ℕ0
→ (FermatNo‘((𝑦
+ 1) + 1)) = ((2↑(2↑((𝑦 + 1) + 1))) + 1)) |
| 5 | | 2cnd 12344 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ 2 ∈ ℂ) |
| 6 | 5, 1 | expp1d 14187 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ (2↑((𝑦 + 1) +
1)) = ((2↑(𝑦 + 1))
· 2)) |
| 7 | 6 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ (2↑(2↑((𝑦
+ 1) + 1))) = (2↑((2↑(𝑦 + 1)) · 2))) |
| 8 | | 2nn0 12543 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 |
| 9 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ 2 ∈ ℕ0) |
| 10 | 9, 1 | nn0expcld 14285 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (2↑(𝑦 + 1))
∈ ℕ0) |
| 11 | 9, 10 | nn0expcld 14285 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ (2↑(2↑(𝑦 +
1))) ∈ ℕ0) |
| 12 | 11 | nn0cnd 12589 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ (2↑(2↑(𝑦 +
1))) ∈ ℂ) |
| 13 | 12 | sqvald 14183 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ ((2↑(2↑(𝑦
+ 1)))↑2) = ((2↑(2↑(𝑦 + 1))) · (2↑(2↑(𝑦 + 1))))) |
| 14 | 5, 9, 10 | expmuld 14189 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ (2↑((2↑(𝑦
+ 1)) · 2)) = ((2↑(2↑(𝑦 + 1)))↑2)) |
| 15 | | fmtnom1nn 47519 |
. . . . . . . . . 10
⊢ ((𝑦 + 1) ∈ ℕ0
→ ((FermatNo‘(𝑦
+ 1)) − 1) = (2↑(2↑(𝑦 + 1)))) |
| 16 | 1, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ ((FermatNo‘(𝑦
+ 1)) − 1) = (2↑(2↑(𝑦 + 1)))) |
| 17 | 16, 16 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ (((FermatNo‘(𝑦
+ 1)) − 1) · ((FermatNo‘(𝑦 + 1)) − 1)) = ((2↑(2↑(𝑦 + 1))) ·
(2↑(2↑(𝑦 +
1))))) |
| 18 | 13, 14, 17 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ (2↑((2↑(𝑦
+ 1)) · 2)) = (((FermatNo‘(𝑦 + 1)) − 1) ·
((FermatNo‘(𝑦 + 1))
− 1))) |
| 19 | 7, 18 | eqtrd 2777 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ (2↑(2↑((𝑦
+ 1) + 1))) = (((FermatNo‘(𝑦 + 1)) − 1) ·
((FermatNo‘(𝑦 + 1))
− 1))) |
| 20 | 19 | oveq1d 7446 |
. . . . 5
⊢ (𝑦 ∈ ℕ0
→ ((2↑(2↑((𝑦
+ 1) + 1))) + 1) = ((((FermatNo‘(𝑦 + 1)) − 1) ·
((FermatNo‘(𝑦 + 1))
− 1)) + 1)) |
| 21 | 4, 20 | eqtrd 2777 |
. . . 4
⊢ (𝑦 ∈ ℕ0
→ (FermatNo‘((𝑦
+ 1) + 1)) = ((((FermatNo‘(𝑦 + 1)) − 1) ·
((FermatNo‘(𝑦 + 1))
− 1)) + 1)) |
| 22 | 21 | adantr 480 |
. . 3
⊢ ((𝑦 ∈ ℕ0
∧ (FermatNo‘(𝑦 +
1)) = (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2)) → (FermatNo‘((𝑦 + 1) + 1)) =
((((FermatNo‘(𝑦 + 1))
− 1) · ((FermatNo‘(𝑦 + 1)) − 1)) + 1)) |
| 23 | | oveq1 7438 |
. . . . . 6
⊢
((FermatNo‘(𝑦
+ 1)) = (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2) → ((FermatNo‘(𝑦 + 1)) − 1) =
((∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2) − 1)) |
| 24 | 23 | oveq1d 7446 |
. . . . 5
⊢
((FermatNo‘(𝑦
+ 1)) = (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2) → (((FermatNo‘(𝑦 + 1)) − 1) ·
((FermatNo‘(𝑦 + 1))
− 1)) = (((∏𝑛
∈ (0...𝑦)(FermatNo‘𝑛) + 2) − 1) ·
((FermatNo‘(𝑦 + 1))
− 1))) |
| 25 | 24 | oveq1d 7446 |
. . . 4
⊢
((FermatNo‘(𝑦
+ 1)) = (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2) → ((((FermatNo‘(𝑦 + 1)) − 1) ·
((FermatNo‘(𝑦 + 1))
− 1)) + 1) = ((((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) − 1) ·
((FermatNo‘(𝑦 + 1))
− 1)) + 1)) |
| 26 | 25 | adantl 481 |
. . 3
⊢ ((𝑦 ∈ ℕ0
∧ (FermatNo‘(𝑦 +
1)) = (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2)) → ((((FermatNo‘(𝑦 + 1)) − 1) ·
((FermatNo‘(𝑦 + 1))
− 1)) + 1) = ((((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) − 1) ·
((FermatNo‘(𝑦 + 1))
− 1)) + 1)) |
| 27 | | fzfid 14014 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (0...𝑦) ∈
Fin) |
| 28 | | elfznn0 13660 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (0...𝑦) → 𝑛 ∈ ℕ0) |
| 29 | | fmtnonn 47518 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ0
→ (FermatNo‘𝑛)
∈ ℕ) |
| 30 | 29 | nncnd 12282 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
→ (FermatNo‘𝑛)
∈ ℂ) |
| 31 | 28, 30 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (0...𝑦) → (FermatNo‘𝑛) ∈ ℂ) |
| 32 | 31 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ 𝑛 ∈ (0...𝑦)) → (FermatNo‘𝑛) ∈
ℂ) |
| 33 | 27, 32 | fprodcl 15988 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ ∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) ∈ ℂ) |
| 34 | | 1cnd 11256 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ 1 ∈ ℂ) |
| 35 | 33, 5, 34 | addsubassd 11640 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ ((∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2) − 1) = (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + (2 − 1))) |
| 36 | | 2m1e1 12392 |
. . . . . . . . . 10
⊢ (2
− 1) = 1 |
| 37 | 36 | oveq2i 7442 |
. . . . . . . . 9
⊢
(∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + (2 − 1)) = (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 1) |
| 38 | 35, 37 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ ((∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2) − 1) = (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 1)) |
| 39 | 38 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ (((∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2) − 1) ·
((FermatNo‘(𝑦 + 1))
− 1)) = ((∏𝑛
∈ (0...𝑦)(FermatNo‘𝑛) + 1) · ((FermatNo‘(𝑦 + 1)) −
1))) |
| 40 | | fmtnonn 47518 |
. . . . . . . . . . 11
⊢ ((𝑦 + 1) ∈ ℕ0
→ (FermatNo‘(𝑦 +
1)) ∈ ℕ) |
| 41 | 1, 40 | syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ (FermatNo‘(𝑦 +
1)) ∈ ℕ) |
| 42 | 41 | nncnd 12282 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ (FermatNo‘(𝑦 +
1)) ∈ ℂ) |
| 43 | 42, 34 | subcld 11620 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ ((FermatNo‘(𝑦
+ 1)) − 1) ∈ ℂ) |
| 44 | 33, 42 | muls1d 11723 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) · ((FermatNo‘(𝑦 + 1)) − 1)) =
((∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) − ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛))) |
| 45 | 43 | mullidd 11279 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ (1 · ((FermatNo‘(𝑦 + 1)) − 1)) = ((FermatNo‘(𝑦 + 1)) −
1)) |
| 46 | 44, 45 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ ((∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) · ((FermatNo‘(𝑦 + 1)) − 1)) + (1 ·
((FermatNo‘(𝑦 + 1))
− 1))) = (((∏𝑛
∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) − ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛)) + ((FermatNo‘(𝑦 + 1)) − 1))) |
| 47 | 33, 43, 34, 46 | joinlmuladdmuld 11288 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ ((∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 1) · ((FermatNo‘(𝑦 + 1)) − 1)) =
(((∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) − ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛)) + ((FermatNo‘(𝑦 + 1)) − 1))) |
| 48 | 39, 47 | eqtrd 2777 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ (((∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2) − 1) ·
((FermatNo‘(𝑦 + 1))
− 1)) = (((∏𝑛
∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) − ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛)) + ((FermatNo‘(𝑦 + 1)) − 1))) |
| 49 | 48 | adantr 480 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0
∧ (FermatNo‘(𝑦 +
1)) = (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2)) → (((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) − 1) ·
((FermatNo‘(𝑦 + 1))
− 1)) = (((∏𝑛
∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) − ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛)) + ((FermatNo‘(𝑦 + 1)) − 1))) |
| 50 | 49 | oveq1d 7446 |
. . . 4
⊢ ((𝑦 ∈ ℕ0
∧ (FermatNo‘(𝑦 +
1)) = (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2)) → ((((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) − 1) ·
((FermatNo‘(𝑦 + 1))
− 1)) + 1) = ((((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) − ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛)) + ((FermatNo‘(𝑦 + 1)) − 1)) + 1)) |
| 51 | | eqcom 2744 |
. . . . . . 7
⊢
((FermatNo‘(𝑦
+ 1)) = (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2) ↔ (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) = (FermatNo‘(𝑦 + 1))) |
| 52 | 42, 5, 33 | subadd2d 11639 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ (((FermatNo‘(𝑦
+ 1)) − 2) = ∏𝑛
∈ (0...𝑦)(FermatNo‘𝑛) ↔ (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) = (FermatNo‘(𝑦 + 1)))) |
| 53 | 51, 52 | bitr4id 290 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ ((FermatNo‘(𝑦
+ 1)) = (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2) ↔ ((FermatNo‘(𝑦 + 1)) − 2) = ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛))) |
| 54 | | oveq2 7439 |
. . . . . . . . . . 11
⊢
(∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) = ((FermatNo‘(𝑦 + 1)) − 2) → ((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) − ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛)) = ((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) −
((FermatNo‘(𝑦 + 1))
− 2))) |
| 55 | 54 | oveq1d 7446 |
. . . . . . . . . 10
⊢
(∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) = ((FermatNo‘(𝑦 + 1)) − 2) → (((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) − ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛)) + ((FermatNo‘(𝑦 + 1)) − 1)) = (((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) −
((FermatNo‘(𝑦 + 1))
− 2)) + ((FermatNo‘(𝑦 + 1)) − 1))) |
| 56 | 55 | oveq1d 7446 |
. . . . . . . . 9
⊢
(∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) = ((FermatNo‘(𝑦 + 1)) − 2) → ((((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) − ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛)) + ((FermatNo‘(𝑦 + 1)) − 1)) + 1) = ((((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) −
((FermatNo‘(𝑦 + 1))
− 2)) + ((FermatNo‘(𝑦 + 1)) − 1)) + 1)) |
| 57 | 56 | eqcoms 2745 |
. . . . . . . 8
⊢
(((FermatNo‘(𝑦
+ 1)) − 2) = ∏𝑛
∈ (0...𝑦)(FermatNo‘𝑛) → ((((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) − ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛)) + ((FermatNo‘(𝑦 + 1)) − 1)) + 1) = ((((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) −
((FermatNo‘(𝑦 + 1))
− 2)) + ((FermatNo‘(𝑦 + 1)) − 1)) + 1)) |
| 58 | 33, 42 | mulcld 11281 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) ∈
ℂ) |
| 59 | 42, 5 | subcld 11620 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ ((FermatNo‘(𝑦
+ 1)) − 2) ∈ ℂ) |
| 60 | 58, 59 | subcld 11620 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ ((∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) −
((FermatNo‘(𝑦 + 1))
− 2)) ∈ ℂ) |
| 61 | 60, 43, 34 | addassd 11283 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ ((((∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) −
((FermatNo‘(𝑦 + 1))
− 2)) + ((FermatNo‘(𝑦 + 1)) − 1)) + 1) = (((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) −
((FermatNo‘(𝑦 + 1))
− 2)) + (((FermatNo‘(𝑦 + 1)) − 1) + 1))) |
| 62 | | elnn0uz 12923 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ0
↔ 𝑦 ∈
(ℤ≥‘0)) |
| 63 | 62 | biimpi 216 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
(ℤ≥‘0)) |
| 64 | | elfznn0 13660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (0...(𝑦 + 1)) → 𝑛 ∈ ℕ0) |
| 65 | 64, 30 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (0...(𝑦 + 1)) → (FermatNo‘𝑛) ∈
ℂ) |
| 66 | 65 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ0
∧ 𝑛 ∈ (0...(𝑦 + 1))) →
(FermatNo‘𝑛) ∈
ℂ) |
| 67 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑦 + 1) → (FermatNo‘𝑛) = (FermatNo‘(𝑦 + 1))) |
| 68 | 63, 66, 67 | fprodp1 16005 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ0
→ ∏𝑛 ∈
(0...(𝑦 +
1))(FermatNo‘𝑛) =
(∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) ·
(FermatNo‘(𝑦 +
1)))) |
| 69 | 68 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ0
→ (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) = ∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛)) |
| 70 | 69 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ ((∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) −
((FermatNo‘(𝑦 + 1))
− 2)) = (∏𝑛
∈ (0...(𝑦 +
1))(FermatNo‘𝑛)
− ((FermatNo‘(𝑦
+ 1)) − 2))) |
| 71 | | npcan1 11688 |
. . . . . . . . . . . 12
⊢
((FermatNo‘(𝑦
+ 1)) ∈ ℂ → (((FermatNo‘(𝑦 + 1)) − 1) + 1) =
(FermatNo‘(𝑦 +
1))) |
| 72 | 42, 71 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ (((FermatNo‘(𝑦
+ 1)) − 1) + 1) = (FermatNo‘(𝑦 + 1))) |
| 73 | 70, 72 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ (((∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) −
((FermatNo‘(𝑦 + 1))
− 2)) + (((FermatNo‘(𝑦 + 1)) − 1) + 1)) = ((∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) − ((FermatNo‘(𝑦 + 1)) − 2)) +
(FermatNo‘(𝑦 +
1)))) |
| 74 | | fzfid 14014 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ0
→ (0...(𝑦 + 1)) ∈
Fin) |
| 75 | 74, 66 | fprodcl 15988 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ ∏𝑛 ∈
(0...(𝑦 +
1))(FermatNo‘𝑛)
∈ ℂ) |
| 76 | 75, 59, 42 | subadd23d 11642 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ ((∏𝑛 ∈
(0...(𝑦 +
1))(FermatNo‘𝑛)
− ((FermatNo‘(𝑦
+ 1)) − 2)) + (FermatNo‘(𝑦 + 1))) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + ((FermatNo‘(𝑦 + 1)) − ((FermatNo‘(𝑦 + 1)) −
2)))) |
| 77 | 73, 76 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ (((∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) −
((FermatNo‘(𝑦 + 1))
− 2)) + (((FermatNo‘(𝑦 + 1)) − 1) + 1)) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + ((FermatNo‘(𝑦 + 1)) − ((FermatNo‘(𝑦 + 1)) −
2)))) |
| 78 | 42, 5 | nncand 11625 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ ((FermatNo‘(𝑦
+ 1)) − ((FermatNo‘(𝑦 + 1)) − 2)) = 2) |
| 79 | 78 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ0
→ (∏𝑛 ∈
(0...(𝑦 +
1))(FermatNo‘𝑛) +
((FermatNo‘(𝑦 + 1))
− ((FermatNo‘(𝑦
+ 1)) − 2))) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2)) |
| 80 | 61, 77, 79 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ0
→ ((((∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) −
((FermatNo‘(𝑦 + 1))
− 2)) + ((FermatNo‘(𝑦 + 1)) − 1)) + 1) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2)) |
| 81 | 57, 80 | sylan9eqr 2799 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((FermatNo‘(𝑦 +
1)) − 2) = ∏𝑛
∈ (0...𝑦)(FermatNo‘𝑛)) → ((((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) − ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛)) + ((FermatNo‘(𝑦 + 1)) − 1)) + 1) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2)) |
| 82 | 81 | ex 412 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ (((FermatNo‘(𝑦
+ 1)) − 2) = ∏𝑛
∈ (0...𝑦)(FermatNo‘𝑛) → ((((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) − ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛)) + ((FermatNo‘(𝑦 + 1)) − 1)) + 1) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2))) |
| 83 | 53, 82 | sylbid 240 |
. . . . 5
⊢ (𝑦 ∈ ℕ0
→ ((FermatNo‘(𝑦
+ 1)) = (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2) → ((((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) − ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛)) + ((FermatNo‘(𝑦 + 1)) − 1)) + 1) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2))) |
| 84 | 83 | imp 406 |
. . . 4
⊢ ((𝑦 ∈ ℕ0
∧ (FermatNo‘(𝑦 +
1)) = (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2)) → ((((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) · (FermatNo‘(𝑦 + 1))) − ∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛)) + ((FermatNo‘(𝑦 + 1)) − 1)) + 1) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2)) |
| 85 | 50, 84 | eqtrd 2777 |
. . 3
⊢ ((𝑦 ∈ ℕ0
∧ (FermatNo‘(𝑦 +
1)) = (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2)) → ((((∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) − 1) ·
((FermatNo‘(𝑦 + 1))
− 1)) + 1) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2)) |
| 86 | 22, 26, 85 | 3eqtrd 2781 |
. 2
⊢ ((𝑦 ∈ ℕ0
∧ (FermatNo‘(𝑦 +
1)) = (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2)) → (FermatNo‘((𝑦 + 1) + 1)) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2)) |
| 87 | 86 | ex 412 |
1
⊢ (𝑦 ∈ ℕ0
→ ((FermatNo‘(𝑦
+ 1)) = (∏𝑛 ∈
(0...𝑦)(FermatNo‘𝑛) + 2) → (FermatNo‘((𝑦 + 1) + 1)) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2))) |