Step | Hyp | Ref
| Expression |
1 | | nnuz 9501 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 9218 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | cvgratnn.6 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
4 | 1, 2, 3 | serf 10409 |
. . . . . 6
⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ) |
5 | 4 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → seq1( + , 𝐹):ℕ⟶ℂ) |
6 | | cvgratnn.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
7 | 6 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → 𝑀 ∈ ℕ) |
8 | 5, 7 | ffvelrnd 5621 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → (seq1( + , 𝐹)‘𝑀) ∈ ℂ) |
9 | | eqid 2165 |
. . . . . . 7
⊢
(ℤ≥‘(𝑀 + 1)) =
(ℤ≥‘(𝑀 + 1)) |
10 | 6 | nnzd 9312 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
11 | 10 | peano2zd 9316 |
. . . . . . 7
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) |
12 | | fveq2 5486 |
. . . . . . . . 9
⊢ (𝑘 = 𝑥 → (𝐹‘𝑘) = (𝐹‘𝑥)) |
13 | 12 | eleq1d 2235 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘𝑥) ∈ ℂ)) |
14 | 3 | ralrimiva 2539 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℂ) |
15 | 14 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℂ) |
16 | 6 | peano2nnd 8872 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 + 1) ∈ ℕ) |
17 | | eluznn 9538 |
. . . . . . . . 9
⊢ (((𝑀 + 1) ∈ ℕ ∧ 𝑥 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑥 ∈ ℕ) |
18 | 16, 17 | sylan 281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈
ℕ) |
19 | 13, 15, 18 | rspcdva 2835 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ ℂ) |
20 | 9, 11, 19 | serf 10409 |
. . . . . 6
⊢ (𝜑 → seq(𝑀 + 1)( + , 𝐹):(ℤ≥‘(𝑀 +
1))⟶ℂ) |
21 | 20 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → seq(𝑀 + 1)( + , 𝐹):(ℤ≥‘(𝑀 +
1))⟶ℂ) |
22 | 11 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → (𝑀 + 1) ∈ ℤ) |
23 | | cvgratnn.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
24 | | eluzelz 9475 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
25 | 23, 24 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℤ) |
26 | 25 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → 𝑁 ∈ ℤ) |
27 | | zltp1le 9245 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) |
28 | 10, 25, 27 | syl2anc 409 |
. . . . . . 7
⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) |
29 | 28 | biimpa 294 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → (𝑀 + 1) ≤ 𝑁) |
30 | | eluz2 9472 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) ↔ ((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) |
31 | 22, 26, 29, 30 | syl3anbrc 1171 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) |
32 | 21, 31 | ffvelrnd 5621 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → (seq(𝑀 + 1)( + , 𝐹)‘𝑁) ∈ ℂ) |
33 | 8, 32 | pncan2d 8211 |
. . 3
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → (((seq1( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁)) − (seq1( + , 𝐹)‘𝑀)) = (seq(𝑀 + 1)( + , 𝐹)‘𝑁)) |
34 | | addcl 7878 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ) |
35 | 34 | adantl 275 |
. . . . 5
⊢ (((𝜑 ∧ 𝑀 < 𝑁) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ) |
36 | | addass 7883 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
37 | 36 | adantl 275 |
. . . . 5
⊢ (((𝜑 ∧ 𝑀 < 𝑁) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
38 | 6, 1 | eleqtrdi 2259 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
39 | 38 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → 𝑀 ∈
(ℤ≥‘1)) |
40 | 14 | ad2antrr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑀 < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘1))
→ ∀𝑘 ∈
ℕ (𝐹‘𝑘) ∈
ℂ) |
41 | | simpr 109 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑀 < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘1))
→ 𝑥 ∈
(ℤ≥‘1)) |
42 | 41, 1 | eleqtrrdi 2260 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑀 < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘1))
→ 𝑥 ∈
ℕ) |
43 | 13, 40, 42 | rspcdva 2835 |
. . . . 5
⊢ (((𝜑 ∧ 𝑀 < 𝑁) ∧ 𝑥 ∈ (ℤ≥‘1))
→ (𝐹‘𝑥) ∈
ℂ) |
44 | 35, 37, 31, 39, 43 | seq3split 10414 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → (seq1( + , 𝐹)‘𝑁) = ((seq1( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁))) |
45 | 44 | oveq1d 5857 |
. . 3
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → ((seq1( + , 𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀)) = (((seq1( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁)) − (seq1( + , 𝐹)‘𝑀))) |
46 | | eqidd 2166 |
. . . 4
⊢ (((𝜑 ∧ 𝑀 < 𝑁) ∧ 𝑖 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑖) = (𝐹‘𝑖)) |
47 | | fveq2 5486 |
. . . . . 6
⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖)) |
48 | 47 | eleq1d 2235 |
. . . . 5
⊢ (𝑘 = 𝑖 → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘𝑖) ∈ ℂ)) |
49 | 14 | ad2antrr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑀 < 𝑁) ∧ 𝑖 ∈ (ℤ≥‘(𝑀 + 1))) → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℂ) |
50 | 16 | ad2antrr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑀 < 𝑁) ∧ 𝑖 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑀 + 1) ∈
ℕ) |
51 | | simpr 109 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑀 < 𝑁) ∧ 𝑖 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑖 ∈
(ℤ≥‘(𝑀 + 1))) |
52 | | eluznn 9538 |
. . . . . 6
⊢ (((𝑀 + 1) ∈ ℕ ∧ 𝑖 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑖 ∈ ℕ) |
53 | 50, 51, 52 | syl2anc 409 |
. . . . 5
⊢ (((𝜑 ∧ 𝑀 < 𝑁) ∧ 𝑖 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑖 ∈
ℕ) |
54 | 48, 49, 53 | rspcdva 2835 |
. . . 4
⊢ (((𝜑 ∧ 𝑀 < 𝑁) ∧ 𝑖 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑖) ∈ ℂ) |
55 | 46, 31, 54 | fsum3ser 11338 |
. . 3
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐹‘𝑖) = (seq(𝑀 + 1)( + , 𝐹)‘𝑁)) |
56 | 33, 45, 55 | 3eqtr4d 2208 |
. 2
⊢ ((𝜑 ∧ 𝑀 < 𝑁) → ((seq1( + , 𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀)) = Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐹‘𝑖)) |
57 | | simpr 109 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → 𝑀 = 𝑁) |
58 | 6 | nnred 8870 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℝ) |
59 | 58 | ltp1d 8825 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
60 | 59 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → 𝑀 < (𝑀 + 1)) |
61 | 57, 60 | eqbrtrrd 4006 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → 𝑁 < (𝑀 + 1)) |
62 | 11 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → (𝑀 + 1) ∈ ℤ) |
63 | 25 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → 𝑁 ∈ ℤ) |
64 | | fzn 9977 |
. . . . . . 7
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑁) = ∅)) |
65 | 62, 63, 64 | syl2anc 409 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → (𝑁 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑁) = ∅)) |
66 | 61, 65 | mpbid 146 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → ((𝑀 + 1)...𝑁) = ∅) |
67 | 66 | sumeq1d 11307 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐹‘𝑖) = Σ𝑖 ∈ ∅ (𝐹‘𝑖)) |
68 | | sum0 11329 |
. . . 4
⊢
Σ𝑖 ∈
∅ (𝐹‘𝑖) = 0 |
69 | 67, 68 | eqtrdi 2215 |
. . 3
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐹‘𝑖) = 0) |
70 | 4, 6 | ffvelrnd 5621 |
. . . . 5
⊢ (𝜑 → (seq1( + , 𝐹)‘𝑀) ∈ ℂ) |
71 | 70 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → (seq1( + , 𝐹)‘𝑀) ∈ ℂ) |
72 | 71 | subidd 8197 |
. . 3
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → ((seq1( + , 𝐹)‘𝑀) − (seq1( + , 𝐹)‘𝑀)) = 0) |
73 | 57 | fveq2d 5490 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → (seq1( + , 𝐹)‘𝑀) = (seq1( + , 𝐹)‘𝑁)) |
74 | 73 | oveq1d 5857 |
. . 3
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → ((seq1( + , 𝐹)‘𝑀) − (seq1( + , 𝐹)‘𝑀)) = ((seq1( + , 𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀))) |
75 | 69, 72, 74 | 3eqtr2rd 2205 |
. 2
⊢ ((𝜑 ∧ 𝑀 = 𝑁) → ((seq1( + , 𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀)) = Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐹‘𝑖)) |
76 | | eluzle 9478 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
77 | 23, 76 | syl 14 |
. . 3
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
78 | | zleloe 9238 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝑀 < 𝑁 ∨ 𝑀 = 𝑁))) |
79 | 10, 25, 78 | syl2anc 409 |
. . 3
⊢ (𝜑 → (𝑀 ≤ 𝑁 ↔ (𝑀 < 𝑁 ∨ 𝑀 = 𝑁))) |
80 | 77, 79 | mpbid 146 |
. 2
⊢ (𝜑 → (𝑀 < 𝑁 ∨ 𝑀 = 𝑁)) |
81 | 56, 75, 80 | mpjaodan 788 |
1
⊢ (𝜑 → ((seq1( + , 𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀)) = Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐹‘𝑖)) |