Step | Hyp | Ref
| Expression |
1 | | serige0.1 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | vex 2604 |
. . . . . 6
⊢ 𝑘 ∈ V |
3 | | serile.3 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℝ) |
4 | | serige0.2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℝ) |
5 | 3, 4 | resubcld 7485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝐺‘𝑘) − (𝐹‘𝑘)) ∈ ℝ) |
6 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → (𝐺‘𝑥) = (𝐺‘𝑘)) |
7 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → (𝐹‘𝑥) = (𝐹‘𝑘)) |
8 | 6, 7 | oveq12d 5550 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → ((𝐺‘𝑥) − (𝐹‘𝑥)) = ((𝐺‘𝑘) − (𝐹‘𝑘))) |
9 | | eqid 2081 |
. . . . . . 7
⊢ (𝑥 ∈ V ↦ ((𝐺‘𝑥) − (𝐹‘𝑥))) = (𝑥 ∈ V ↦ ((𝐺‘𝑥) − (𝐹‘𝑥))) |
10 | 8, 9 | fvmptg 5269 |
. . . . . 6
⊢ ((𝑘 ∈ V ∧ ((𝐺‘𝑘) − (𝐹‘𝑘)) ∈ ℝ) → ((𝑥 ∈ V ↦ ((𝐺‘𝑥) − (𝐹‘𝑥)))‘𝑘) = ((𝐺‘𝑘) − (𝐹‘𝑘))) |
11 | 2, 5, 10 | sylancr 405 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑥 ∈ V ↦ ((𝐺‘𝑥) − (𝐹‘𝑥)))‘𝑘) = ((𝐺‘𝑘) − (𝐹‘𝑘))) |
12 | 11, 5 | eqeltrd 2155 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑥 ∈ V ↦ ((𝐺‘𝑥) − (𝐹‘𝑥)))‘𝑘) ∈ ℝ) |
13 | | serile.4 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ≤ (𝐺‘𝑘)) |
14 | 3, 4 | subge0d 7635 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (0 ≤ ((𝐺‘𝑘) − (𝐹‘𝑘)) ↔ (𝐹‘𝑘) ≤ (𝐺‘𝑘))) |
15 | 13, 14 | mpbird 165 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 0 ≤ ((𝐺‘𝑘) − (𝐹‘𝑘))) |
16 | 15, 11 | breqtrrd 3811 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 0 ≤ ((𝑥 ∈ V ↦ ((𝐺‘𝑥) − (𝐹‘𝑥)))‘𝑘)) |
17 | 1, 12, 16 | serige0 9473 |
. . 3
⊢ (𝜑 → 0 ≤ (seq𝑀( + , (𝑥 ∈ V ↦ ((𝐺‘𝑥) − (𝐹‘𝑥))), ℂ)‘𝑁)) |
18 | 3 | recnd 7147 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐺‘𝑘) ∈ ℂ) |
19 | 4 | recnd 7147 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
20 | 1, 18, 19, 11 | isersub 9464 |
. . 3
⊢ (𝜑 → (seq𝑀( + , (𝑥 ∈ V ↦ ((𝐺‘𝑥) − (𝐹‘𝑥))), ℂ)‘𝑁) = ((seq𝑀( + , 𝐺, ℂ)‘𝑁) − (seq𝑀( + , 𝐹, ℂ)‘𝑁))) |
21 | 17, 20 | breqtrd 3809 |
. 2
⊢ (𝜑 → 0 ≤ ((seq𝑀( + , 𝐺, ℂ)‘𝑁) − (seq𝑀( + , 𝐹, ℂ)‘𝑁))) |
22 | | eluzel2 8624 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
23 | 1, 22 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
24 | | cnex 7097 |
. . . . . . 7
⊢ ℂ
∈ V |
25 | 24 | a1i 9 |
. . . . . 6
⊢ (𝜑 → ℂ ∈
V) |
26 | | ax-resscn 7068 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
27 | 26 | a1i 9 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℂ) |
28 | | readdcl 7099 |
. . . . . . 7
⊢ ((𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑘 + 𝑥) ∈ ℝ) |
29 | 28 | adantl 271 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ)) → (𝑘 + 𝑥) ∈ ℝ) |
30 | | addcl 7098 |
. . . . . . 7
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 + 𝑥) ∈ ℂ) |
31 | 30 | adantl 271 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 + 𝑥) ∈ ℂ) |
32 | 23, 25, 27, 3, 29, 31 | iseqss 9446 |
. . . . 5
⊢ (𝜑 → seq𝑀( + , 𝐺, ℝ) = seq𝑀( + , 𝐺, ℂ)) |
33 | 32 | fveq1d 5200 |
. . . 4
⊢ (𝜑 → (seq𝑀( + , 𝐺, ℝ)‘𝑁) = (seq𝑀( + , 𝐺, ℂ)‘𝑁)) |
34 | | reex 7107 |
. . . . . 6
⊢ ℝ
∈ V |
35 | 34 | a1i 9 |
. . . . 5
⊢ (𝜑 → ℝ ∈
V) |
36 | 1, 35, 3, 29 | iseqcl 9443 |
. . . 4
⊢ (𝜑 → (seq𝑀( + , 𝐺, ℝ)‘𝑁) ∈ ℝ) |
37 | 33, 36 | eqeltrrd 2156 |
. . 3
⊢ (𝜑 → (seq𝑀( + , 𝐺, ℂ)‘𝑁) ∈ ℝ) |
38 | 23, 25, 27, 4, 29, 31 | iseqss 9446 |
. . . . 5
⊢ (𝜑 → seq𝑀( + , 𝐹, ℝ) = seq𝑀( + , 𝐹, ℂ)) |
39 | 38 | fveq1d 5200 |
. . . 4
⊢ (𝜑 → (seq𝑀( + , 𝐹, ℝ)‘𝑁) = (seq𝑀( + , 𝐹, ℂ)‘𝑁)) |
40 | 1, 35, 4, 29 | iseqcl 9443 |
. . . 4
⊢ (𝜑 → (seq𝑀( + , 𝐹, ℝ)‘𝑁) ∈ ℝ) |
41 | 39, 40 | eqeltrrd 2156 |
. . 3
⊢ (𝜑 → (seq𝑀( + , 𝐹, ℂ)‘𝑁) ∈ ℝ) |
42 | 37, 41 | subge0d 7635 |
. 2
⊢ (𝜑 → (0 ≤ ((seq𝑀( + , 𝐺, ℂ)‘𝑁) − (seq𝑀( + , 𝐹, ℂ)‘𝑁)) ↔ (seq𝑀( + , 𝐹, ℂ)‘𝑁) ≤ (seq𝑀( + , 𝐺, ℂ)‘𝑁))) |
43 | 21, 42 | mpbid 145 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹, ℂ)‘𝑁) ≤ (seq𝑀( + , 𝐺, ℂ)‘𝑁)) |