Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (2 · 𝑥) = (2 ·
0)) |
2 | | 2t0e0 11060 |
. . . . . . . . . 10
⊢ (2
· 0) = 0 |
3 | 1, 2 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (2 · 𝑥) = 0) |
4 | 3 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑁 + (2 · 𝑥)) = (𝑁 + 0)) |
5 | 4 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = 0 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + 0))) |
6 | 5 | oveq2d 6565 |
. . . . . 6
⊢ (𝑥 = 0 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0)))) |
7 | 6 | breq1d 4593 |
. . . . 5
⊢ (𝑥 = 0 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) |
8 | 7 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 0 → (((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))) |
9 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → (2 · 𝑥) = (2 · 𝑛)) |
10 | 9 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝑛))) |
11 | 10 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) |
12 | 11 | oveq2d 6565 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))))) |
13 | 12 | breq1d 4593 |
. . . . 5
⊢ (𝑥 = 𝑛 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) |
14 | 13 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝑛 → (((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))) |
15 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → (2 · 𝑥) = (2 · (𝑛 + 1))) |
16 | 15 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · (𝑛 + 1)))) |
17 | 16 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) |
18 | 17 | oveq2d 6565 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))) |
19 | 18 | breq1d 4593 |
. . . . 5
⊢ (𝑥 = (𝑛 + 1) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) |
20 | 19 | imbi2d 329 |
. . . 4
⊢ (𝑥 = (𝑛 + 1) → (((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))) |
21 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑥 = 𝐾 → (2 · 𝑥) = (2 · 𝐾)) |
22 | 21 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑥 = 𝐾 → (𝑁 + (2 · 𝑥)) = (𝑁 + (2 · 𝐾))) |
23 | 22 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = 𝐾 → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥))) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) |
24 | 23 | oveq2d 6565 |
. . . . . 6
⊢ (𝑥 = 𝐾 → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))) |
25 | 24 | breq1d 4593 |
. . . . 5
⊢ (𝑥 = 𝐾 → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) |
26 | 25 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝐾 → (((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑥)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) ↔ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))) |
27 | | iseralt.1 |
. . . . . . . . . . . 12
⊢ 𝑍 =
(ℤ≥‘𝑀) |
28 | | uzssz 11583 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
29 | 27, 28 | eqsstri 3598 |
. . . . . . . . . . 11
⊢ 𝑍 ⊆
ℤ |
30 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ⊆ ℤ) |
31 | 30 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ ℤ) |
32 | 31 | zcnd 11359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ ℂ) |
33 | 32 | addid1d 10115 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (𝑁 + 0) = 𝑁) |
34 | 33 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘(𝑁 + 0)) = (seq𝑀( + , 𝐹)‘𝑁)) |
35 | 34 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) |
36 | | neg1rr 11002 |
. . . . . . . . 9
⊢ -1 ∈
ℝ |
37 | | neg1ne0 11003 |
. . . . . . . . 9
⊢ -1 ≠
0 |
38 | | reexpclz 12742 |
. . . . . . . . 9
⊢ ((-1
∈ ℝ ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) → (-1↑𝑁) ∈
ℝ) |
39 | 36, 37, 38 | mp3an12 1406 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ →
(-1↑𝑁) ∈
ℝ) |
40 | 31, 39 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (-1↑𝑁) ∈ ℝ) |
41 | | iseralt.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
42 | | iseralt.6 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘))) |
43 | 30 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ) |
44 | | reexpclz 12742 |
. . . . . . . . . . . . 13
⊢ ((-1
∈ ℝ ∧ -1 ≠ 0 ∧ 𝑘 ∈ ℤ) → (-1↑𝑘) ∈
ℝ) |
45 | 36, 37, 44 | mp3an12 1406 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℤ →
(-1↑𝑘) ∈
ℝ) |
46 | 43, 45 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (-1↑𝑘) ∈ ℝ) |
47 | | iseralt.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:𝑍⟶ℝ) |
48 | 47 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ) |
49 | 46, 48 | remulcld 9949 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((-1↑𝑘) · (𝐺‘𝑘)) ∈ ℝ) |
50 | 42, 49 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) |
51 | 27, 41, 50 | serfre 12692 |
. . . . . . . 8
⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ) |
52 | 51 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ) |
53 | 40, 52 | remulcld 9949 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ) |
54 | 53 | leidd 10473 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) |
55 | 35, 54 | eqbrtrd 4605 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 0))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) |
56 | 47 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝐺:𝑍⟶ℝ) |
57 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
58 | 57 | 2timesi 11024 |
. . . . . . . . . . . . . . 15
⊢ (2
· 1) = (1 + 1) |
59 | 58 | oveq2i 6560 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 + (2 · 𝑛)) + (2 · 1)) = ((𝑁 + (2 · 𝑛)) + (1 + 1)) |
60 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ 𝑍) |
61 | 60, 27 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → 𝑁 ∈ (ℤ≥‘𝑀)) |
62 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈
(ℤ≥‘𝑀)) |
63 | | eluzelz 11573 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈
ℤ) |
65 | 64 | zcnd 11359 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈
ℂ) |
66 | | 2cn 10968 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℂ |
67 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℂ) |
68 | 67 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℂ) |
69 | | mulcl 9899 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℂ ∧ 𝑛
∈ ℂ) → (2 · 𝑛) ∈ ℂ) |
70 | 66, 68, 69 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2
· 𝑛) ∈
ℂ) |
71 | 66, 57 | mulcli 9924 |
. . . . . . . . . . . . . . . 16
⊢ (2
· 1) ∈ ℂ |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2
· 1) ∈ ℂ) |
73 | 65, 70, 72 | addassd 9941 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (2 · 1)) = (𝑁 + ((2 · 𝑛) + (2 ·
1)))) |
74 | 59, 73 | syl5eqr 2658 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + (1 + 1)) = (𝑁 + ((2 · 𝑛) + (2 ·
1)))) |
75 | | 2nn0 11186 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℕ0 |
76 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
77 | | nn0mulcl 11206 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2
· 𝑛) ∈
ℕ0) |
78 | 75, 76, 77 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2
· 𝑛) ∈
ℕ0) |
79 | | uzaddcl 11620 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (2 · 𝑛) ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈
(ℤ≥‘𝑀)) |
80 | 62, 78, 79 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈
(ℤ≥‘𝑀)) |
81 | 28, 80 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈
ℤ) |
82 | 81 | zcnd 11359 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈
ℂ) |
83 | | 1cnd 9935 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 1 ∈
ℂ) |
84 | 82, 83, 83 | addassd 9941 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = ((𝑁 + (2 · 𝑛)) + (1 + 1))) |
85 | | 2cnd 10970 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈
ℂ) |
86 | 85, 68, 83 | adddid 9943 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2
· (𝑛 + 1)) = ((2
· 𝑛) + (2 ·
1))) |
87 | 86 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) = (𝑁 + ((2 · 𝑛) + (2 · 1)))) |
88 | 74, 84, 87 | 3eqtr4d 2654 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) = (𝑁 + (2 · (𝑛 + 1)))) |
89 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ0) |
90 | 89 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑛 + 1) ∈
ℕ0) |
91 | | nn0mulcl 11206 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ0 ∧ (𝑛 + 1) ∈ ℕ0) → (2
· (𝑛 + 1)) ∈
ℕ0) |
92 | 75, 90, 91 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2
· (𝑛 + 1)) ∈
ℕ0) |
93 | | uzaddcl 11620 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (2 · (𝑛 + 1)) ∈ ℕ0) →
(𝑁 + (2 · (𝑛 + 1))) ∈
(ℤ≥‘𝑀)) |
94 | 62, 92, 93 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈
(ℤ≥‘𝑀)) |
95 | 94, 27 | syl6eleqr 2699 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · (𝑛 + 1))) ∈ 𝑍) |
96 | 88, 95 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝑁 + (2 · 𝑛)) + 1) + 1) ∈ 𝑍) |
97 | 56, 96 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈
ℝ) |
98 | | peano2uz 11617 |
. . . . . . . . . . . . 13
⊢ ((𝑁 + (2 · 𝑛)) ∈
(ℤ≥‘𝑀) → ((𝑁 + (2 · 𝑛)) + 1) ∈
(ℤ≥‘𝑀)) |
99 | 80, 98 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈
(ℤ≥‘𝑀)) |
100 | 99, 27 | syl6eleqr 2699 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈ 𝑍) |
101 | 56, 100 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ) |
102 | 97, 101 | resubcld 10337 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ) |
103 | | 0red 9920 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 0 ∈
ℝ) |
104 | 40 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(-1↑𝑁) ∈
ℝ) |
105 | 51 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ) |
106 | 80, 27 | syl6eleqr 2699 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (2 · 𝑛)) ∈ 𝑍) |
107 | 105, 106 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℝ) |
108 | 104, 107 | remulcld 9949 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℝ) |
109 | | iseralt.4 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘)) |
110 | 109 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘)) |
111 | 110 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
∀𝑘 ∈ 𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘)) |
112 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝑘 + 1) = (((𝑁 + (2 · 𝑛)) + 1) + 1)) |
113 | 112 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺‘(𝑘 + 1)) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) |
114 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐺‘𝑘) = (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) |
115 | 113, 114 | breq12d 4596 |
. . . . . . . . . . . 12
⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘) ↔ (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) |
116 | 115 | rspcv 3278 |
. . . . . . . . . . 11
⊢ (((𝑁 + (2 · 𝑛)) + 1) ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) |
117 | 100, 111,
116 | sylc 63 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) |
118 | 97, 101 | suble0d 10497 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ≤ 0 ↔ (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ≤ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) |
119 | 117, 118 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ≤ 0) |
120 | 102, 103,
108, 119 | leadd2dd 10521 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0)) |
121 | | seqp1 12678 |
. . . . . . . . . . . . 13
⊢ (((𝑁 + (2 · 𝑛)) + 1) ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) |
122 | 99, 121 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) |
123 | | seqp1 12678 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 + (2 · 𝑛)) ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1)))) |
124 | 80, 123 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1)))) |
125 | 124 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) |
126 | 122, 125 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) |
127 | 88 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) |
128 | 107 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) ∈ ℂ) |
129 | 42 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘))) |
130 | 129 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘))) |
131 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (𝐹‘𝑘) = (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) |
132 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → (-1↑𝑘) = (-1↑((𝑁 + (2 · 𝑛)) + 1))) |
133 | 132, 114 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((-1↑𝑘) · (𝐺‘𝑘)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) |
134 | 131, 133 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = ((𝑁 + (2 · 𝑛)) + 1) → ((𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))) |
135 | 134 | rspcv 3278 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 + (2 · 𝑛)) + 1) ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))) |
136 | 100, 130,
135 | sylc 63 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑((𝑁 + (2 · 𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) |
137 | | neg1cn 11001 |
. . . . . . . . . . . . . . . . . . 19
⊢ -1 ∈
ℂ |
138 | 137 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈
ℂ) |
139 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ≠
0) |
140 | 138, 139,
81 | expp1zd 12879 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(-1↑((𝑁 + (2 ·
𝑛)) + 1)) =
((-1↑(𝑁 + (2 ·
𝑛))) ·
-1)) |
141 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -1 ∈
ℝ) |
142 | 141, 139,
81 | reexpclzd 12896 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(-1↑(𝑁 + (2 ·
𝑛))) ∈
ℝ) |
143 | 142 | recnd 9947 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(-1↑(𝑁 + (2 ·
𝑛))) ∈
ℂ) |
144 | | mulcom 9901 |
. . . . . . . . . . . . . . . . . 18
⊢
(((-1↑(𝑁 + (2
· 𝑛))) ∈
ℂ ∧ -1 ∈ ℂ) → ((-1↑(𝑁 + (2 · 𝑛))) · -1) = (-1 ·
(-1↑(𝑁 + (2 ·
𝑛))))) |
145 | 143, 137,
144 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑(𝑁 + (2 ·
𝑛))) · -1) = (-1
· (-1↑(𝑁 + (2
· 𝑛))))) |
146 | 143 | mulm1d 10361 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-1
· (-1↑(𝑁 + (2
· 𝑛)))) =
-(-1↑(𝑁 + (2 ·
𝑛)))) |
147 | 140, 145,
146 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(-1↑((𝑁 + (2 ·
𝑛)) + 1)) =
-(-1↑(𝑁 + (2 ·
𝑛)))) |
148 | 147 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑((𝑁 + (2 ·
𝑛)) + 1)) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (-(-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) |
149 | 101 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ) |
150 | | mulneg12 10347 |
. . . . . . . . . . . . . . . 16
⊢
(((-1↑(𝑁 + (2
· 𝑛))) ∈
ℂ ∧ (𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ) →
(-(-1↑(𝑁 + (2 ·
𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) |
151 | 143, 149,
150 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(-(-1↑(𝑁 + (2 ·
𝑛))) · (𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) |
152 | 136, 148,
151 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) |
153 | 101 | renegcld 10336 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ) |
154 | 142, 153 | remulcld 9949 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑(𝑁 + (2 ·
𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) ∈ ℝ) |
155 | 152, 154 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℝ) |
156 | 155 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ) |
157 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐹‘𝑘) = (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) |
158 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (-1↑𝑘) = (-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1))) |
159 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → (𝐺‘𝑘) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) |
160 | 158, 159 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((-1↑𝑘) · (𝐺‘𝑘)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) |
161 | 157, 160 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (((𝑁 + (2 · 𝑛)) + 1) + 1) → ((𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) ↔ (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) |
162 | 161 | rspcv 3278 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 + (2 · 𝑛)) + 1) + 1) ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) |
163 | 96, 130, 162 | sylc 63 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(((𝑁 + (2 · 𝑛)) + 1) + 1)) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) |
164 | 81 | peano2zd 11361 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + (2 · 𝑛)) + 1) ∈
ℤ) |
165 | 138, 139,
164 | expp1zd 12879 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(-1↑(((𝑁 + (2 ·
𝑛)) + 1) + 1)) =
((-1↑((𝑁 + (2 ·
𝑛)) + 1)) ·
-1)) |
166 | 147 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑((𝑁 + (2 ·
𝑛)) + 1)) · -1) =
(-(-1↑(𝑁 + (2 ·
𝑛))) ·
-1)) |
167 | | mul2neg 10348 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((-1↑(𝑁 + (2
· 𝑛))) ∈
ℂ ∧ 1 ∈ ℂ) → (-(-1↑(𝑁 + (2 · 𝑛))) · -1) = ((-1↑(𝑁 + (2 · 𝑛))) ·
1)) |
168 | 143, 57, 167 | sylancl 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(-(-1↑(𝑁 + (2 ·
𝑛))) · -1) =
((-1↑(𝑁 + (2 ·
𝑛))) ·
1)) |
169 | 143 | mulid1d 9936 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑(𝑁 + (2 ·
𝑛))) · 1) =
(-1↑(𝑁 + (2 ·
𝑛)))) |
170 | 168, 169 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(-(-1↑(𝑁 + (2 ·
𝑛))) · -1) =
(-1↑(𝑁 + (2 ·
𝑛)))) |
171 | 165, 166,
170 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(-1↑(((𝑁 + (2 ·
𝑛)) + 1) + 1)) =
(-1↑(𝑁 + (2 ·
𝑛)))) |
172 | 171 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑(((𝑁 + (2
· 𝑛)) + 1) + 1))
· (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) =
((-1↑(𝑁 + (2 ·
𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) |
173 | 163, 172 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) = ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) |
174 | 142, 97 | remulcld 9949 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑(𝑁 + (2 ·
𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈
ℝ) |
175 | 173, 174 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈
ℝ) |
176 | 175 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈
ℂ) |
177 | 128, 156,
176 | addassd 9941 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) |
178 | 126, 127,
177 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) |
179 | 178 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))) |
180 | 104 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(-1↑𝑁) ∈
ℂ) |
181 | 155, 175 | readdcld 9948 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈
ℝ) |
182 | 181 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) ∈
ℂ) |
183 | 180, 128,
182 | adddid 9943 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))) + ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))))) |
184 | 180, 156,
176 | adddid 9943 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (((-1↑𝑁) · (𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) |
185 | 152 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
(𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))) |
186 | 153 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ) |
187 | 180, 143,
186 | mulassd 9942 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(((-1↑𝑁) ·
(-1↑(𝑁 + (2 ·
𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))))) |
188 | 185, 187 | eqtr4d 2647 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
(𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = (((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) |
189 | 85, 65, 68 | adddid 9943 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2
· (𝑁 + 𝑛)) = ((2 · 𝑁) + (2 · 𝑛))) |
190 | 65 | 2timesd 11152 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (2
· 𝑁) = (𝑁 + 𝑁)) |
191 | 190 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((2
· 𝑁) + (2 ·
𝑛)) = ((𝑁 + 𝑁) + (2 · 𝑛))) |
192 | 65, 65, 70 | addassd 9941 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝑁 + 𝑁) + (2 · 𝑛)) = (𝑁 + (𝑁 + (2 · 𝑛)))) |
193 | 189, 191,
192 | 3eqtrrd 2649 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + (𝑁 + (2 · 𝑛))) = (2 · (𝑁 + 𝑛))) |
194 | 193 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = (-1↑(2 ·
(𝑁 + 𝑛)))) |
195 | | expaddz 12766 |
. . . . . . . . . . . . . . . 16
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ (𝑁 + (2 · 𝑛)) ∈ ℤ)) → (-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛))))) |
196 | 138, 139,
64, 81, 195 | syl22anc 1319 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(-1↑(𝑁 + (𝑁 + (2 · 𝑛)))) = ((-1↑𝑁) · (-1↑(𝑁 + (2 · 𝑛))))) |
197 | | 2z 11286 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℤ |
198 | 197 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → 2 ∈
ℤ) |
199 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) |
200 | | zaddcl 11294 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑁 + 𝑛) ∈ ℤ) |
201 | 31, 199, 200 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝑁 + 𝑛) ∈ ℤ) |
202 | | expmulz 12768 |
. . . . . . . . . . . . . . . . 17
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ (𝑁 + 𝑛) ∈ ℤ)) → (-1↑(2
· (𝑁 + 𝑛))) = ((-1↑2)↑(𝑁 + 𝑛))) |
203 | 138, 139,
198, 201, 202 | syl22anc 1319 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(-1↑(2 · (𝑁 +
𝑛))) =
((-1↑2)↑(𝑁 +
𝑛))) |
204 | | neg1sqe1 12821 |
. . . . . . . . . . . . . . . . . 18
⊢
(-1↑2) = 1 |
205 | 204 | oveq1i 6559 |
. . . . . . . . . . . . . . . . 17
⊢
((-1↑2)↑(𝑁
+ 𝑛)) = (1↑(𝑁 + 𝑛)) |
206 | | 1exp 12751 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 + 𝑛) ∈ ℤ → (1↑(𝑁 + 𝑛)) = 1) |
207 | 201, 206 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(1↑(𝑁 + 𝑛)) = 1) |
208 | 205, 207 | syl5eq 2656 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑2)↑(𝑁 +
𝑛)) = 1) |
209 | 203, 208 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(-1↑(2 · (𝑁 +
𝑛))) = 1) |
210 | 194, 196,
209 | 3eqtr3d 2652 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
(-1↑(𝑁 + (2 ·
𝑛)))) = 1) |
211 | 210 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(((-1↑𝑁) ·
(-1↑(𝑁 + (2 ·
𝑛)))) · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = (1 · -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) |
212 | 186 | mulid2d 9937 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (1
· -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) |
213 | 188, 211,
212 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
(𝐹‘((𝑁 + (2 · 𝑛)) + 1))) = -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) |
214 | 173 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
(𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) |
215 | 97 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) ∈
ℂ) |
216 | 180, 143,
215 | mulassd 9942 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(((-1↑𝑁) ·
(-1↑(𝑁 + (2 ·
𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((-1↑𝑁) · ((-1↑(𝑁 + (2 · 𝑛))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) |
217 | 214, 216 | eqtr4d 2647 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
(𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) =
(((-1↑𝑁) ·
(-1↑(𝑁 + (2 ·
𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) |
218 | 210 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(((-1↑𝑁) ·
(-1↑(𝑁 + (2 ·
𝑛)))) · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (1 · (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) |
219 | 215 | mulid2d 9937 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (1
· (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) |
220 | 217, 218,
219 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
(𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) |
221 | 213, 220 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(((-1↑𝑁) ·
(𝐹‘((𝑁 + (2 · 𝑛)) + 1))) + ((-1↑𝑁) · (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) |
222 | 149 | negcld 10258 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) ∈ ℂ) |
223 | 222, 215 | addcomd 10117 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) |
224 | 215, 149 | negsubd 10277 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) + -(𝐺‘((𝑁 + (2 · 𝑛)) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) |
225 | 223, 224 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (-(𝐺‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) |
226 | 184, 221,
225 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1)))) = ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) |
227 | 226 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((-1↑𝑁) · ((𝐹‘((𝑁 + (2 · 𝑛)) + 1)) + (𝐹‘(((𝑁 + (2 · 𝑛)) + 1) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1))))) |
228 | 179, 183,
227 | 3eqtrrd 2649 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + ((𝐺‘(((𝑁 + (2 · 𝑛)) + 1) + 1)) − (𝐺‘((𝑁 + (2 · 𝑛)) + 1)))) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))))) |
229 | 108 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℂ) |
230 | 229 | addid1d 10115 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) + 0) = ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))))) |
231 | 120, 228,
230 | 3brtr3d 4614 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛))))) |
232 | 105, 95 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1)))) ∈ ℝ) |
233 | 104, 232 | remulcld 9949 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ∈ ℝ) |
234 | 53 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ) |
235 | | letr 10010 |
. . . . . . . 8
⊢
((((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ∈ ℝ ∧
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∈ ℝ ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ) → ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) |
236 | 233, 108,
234, 235 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
((((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) |
237 | 231, 236 | mpand 707 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑁 ∈ 𝑍) ∧ 𝑛 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) |
238 | 237 | expcom 450 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
→ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))) |
239 | 238 | a2d 29 |
. . . 4
⊢ (𝑛 ∈ ℕ0
→ (((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝑛)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) → ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · (𝑛 + 1))))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))) |
240 | 8, 14, 20, 26, 55, 239 | nn0ind 11348 |
. . 3
⊢ (𝐾 ∈ ℕ0
→ ((𝜑 ∧ 𝑁 ∈ 𝑍) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) |
241 | 240 | com12 32 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍) → (𝐾 ∈ ℕ0 →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) |
242 | 241 | 3impia 1253 |
1
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) |