Step | Hyp | Ref
| Expression |
1 | | isermono.2 |
. 2
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾)) |
2 | | elfzuz 9041 |
. . . 4
⊢ (𝑘 ∈ (𝐾...𝑁) → 𝑘 ∈ (ℤ≥‘𝐾)) |
3 | | isermono.1 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) |
4 | | uztrn 8635 |
. . . 4
⊢ ((𝑘 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
5 | 2, 3, 4 | syl2anr 284 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
6 | | reex 7107 |
. . . 4
⊢ ℝ
∈ V |
7 | 6 | a1i 9 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) → ℝ ∈ V) |
8 | | isermono.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ ℝ) |
9 | 8 | adantlr 460 |
. . 3
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ ℝ) |
10 | | readdcl 7099 |
. . . 4
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ) |
11 | 10 | adantl 271 |
. . 3
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ) |
12 | 5, 7, 9, 11 | iseqcl 9443 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) → (seq𝑀( + , 𝐹, ℝ)‘𝑘) ∈ ℝ) |
13 | | simpr 108 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑘 ∈ (𝐾...(𝑁 − 1))) |
14 | 3 | adantr 270 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝐾 ∈ (ℤ≥‘𝑀)) |
15 | | eluzelz 8628 |
. . . . . . . . 9
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝐾 ∈ ℤ) |
16 | 14, 15 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝐾 ∈ ℤ) |
17 | 1 | adantr 270 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑁 ∈ (ℤ≥‘𝐾)) |
18 | | eluzelz 8628 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → 𝑁 ∈ ℤ) |
19 | 17, 18 | syl 14 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑁 ∈ ℤ) |
20 | | peano2zm 8389 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
21 | 19, 20 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑁 − 1) ∈ ℤ) |
22 | | elfzelz 9045 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝐾...(𝑁 − 1)) → 𝑘 ∈ ℤ) |
23 | 22 | adantl 271 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑘 ∈ ℤ) |
24 | | 1zzd 8378 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 1 ∈
ℤ) |
25 | | fzaddel 9077 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ)
∧ (𝑘 ∈ ℤ
∧ 1 ∈ ℤ)) → (𝑘 ∈ (𝐾...(𝑁 − 1)) ↔ (𝑘 + 1) ∈ ((𝐾 + 1)...((𝑁 − 1) + 1)))) |
26 | 16, 21, 23, 24, 25 | syl22anc 1170 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 ∈ (𝐾...(𝑁 − 1)) ↔ (𝑘 + 1) ∈ ((𝐾 + 1)...((𝑁 − 1) + 1)))) |
27 | 13, 26 | mpbid 145 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ ((𝐾 + 1)...((𝑁 − 1) + 1))) |
28 | | zcn 8356 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
29 | | ax-1cn 7069 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
30 | | npcan 7317 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
31 | 28, 29, 30 | sylancl 404 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → ((𝑁 − 1) + 1) = 𝑁) |
32 | 19, 31 | syl 14 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁) |
33 | 32 | oveq2d 5548 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → ((𝐾 + 1)...((𝑁 − 1) + 1)) = ((𝐾 + 1)...𝑁)) |
34 | 27, 33 | eleqtrd 2157 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ ((𝐾 + 1)...𝑁)) |
35 | | isermono.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝐹‘𝑥)) |
36 | 35 | ralrimiva 2434 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ ((𝐾 + 1)...𝑁)0 ≤ (𝐹‘𝑥)) |
37 | 36 | adantr 270 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → ∀𝑥 ∈ ((𝐾 + 1)...𝑁)0 ≤ (𝐹‘𝑥)) |
38 | | fveq2 5198 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑘 + 1))) |
39 | 38 | breq2d 3797 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → (0 ≤ (𝐹‘𝑥) ↔ 0 ≤ (𝐹‘(𝑘 + 1)))) |
40 | 39 | rspcv 2697 |
. . . . 5
⊢ ((𝑘 + 1) ∈ ((𝐾 + 1)...𝑁) → (∀𝑥 ∈ ((𝐾 + 1)...𝑁)0 ≤ (𝐹‘𝑥) → 0 ≤ (𝐹‘(𝑘 + 1)))) |
41 | 34, 37, 40 | sylc 61 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 0 ≤ (𝐹‘(𝑘 + 1))) |
42 | | fzelp1 9091 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝐾...(𝑁 − 1)) → 𝑘 ∈ (𝐾...((𝑁 − 1) + 1))) |
43 | 42 | adantl 271 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑘 ∈ (𝐾...((𝑁 − 1) + 1))) |
44 | 32 | oveq2d 5548 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝐾...((𝑁 − 1) + 1)) = (𝐾...𝑁)) |
45 | 43, 44 | eleqtrd 2157 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑘 ∈ (𝐾...𝑁)) |
46 | 45, 12 | syldan 276 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (seq𝑀( + , 𝐹, ℝ)‘𝑘) ∈ ℝ) |
47 | | fzss1 9081 |
. . . . . . . . 9
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) |
48 | 14, 47 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) |
49 | | fzp1elp1 9092 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝐾...(𝑁 − 1)) → (𝑘 + 1) ∈ (𝐾...((𝑁 − 1) + 1))) |
50 | 49 | adantl 271 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ (𝐾...((𝑁 − 1) + 1))) |
51 | 50, 44 | eleqtrd 2157 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ (𝐾...𝑁)) |
52 | 48, 51 | sseldd 3000 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
53 | | elfzuz 9041 |
. . . . . . 7
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → (𝑘 + 1) ∈
(ℤ≥‘𝑀)) |
54 | 52, 53 | syl 14 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈
(ℤ≥‘𝑀)) |
55 | 8 | ralrimiva 2434 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ ℝ) |
56 | 55 | adantr 270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → ∀𝑥 ∈
(ℤ≥‘𝑀)(𝐹‘𝑥) ∈ ℝ) |
57 | 38 | eleq1d 2147 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘(𝑘 + 1)) ∈ ℝ)) |
58 | 57 | rspcv 2697 |
. . . . . 6
⊢ ((𝑘 + 1) ∈
(ℤ≥‘𝑀) → (∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ ℝ → (𝐹‘(𝑘 + 1)) ∈ ℝ)) |
59 | 54, 56, 58 | sylc 61 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ∈ ℝ) |
60 | 46, 59 | addge01d 7633 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (0 ≤ (𝐹‘(𝑘 + 1)) ↔ (seq𝑀( + , 𝐹, ℝ)‘𝑘) ≤ ((seq𝑀( + , 𝐹, ℝ)‘𝑘) + (𝐹‘(𝑘 + 1))))) |
61 | 41, 60 | mpbid 145 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (seq𝑀( + , 𝐹, ℝ)‘𝑘) ≤ ((seq𝑀( + , 𝐹, ℝ)‘𝑘) + (𝐹‘(𝑘 + 1)))) |
62 | 45, 5 | syldan 276 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑘 ∈ (ℤ≥‘𝑀)) |
63 | 6 | a1i 9 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → ℝ ∈
V) |
64 | 8 | adantlr 460 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ ℝ) |
65 | 10 | adantl 271 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ) |
66 | 62, 63, 64, 65 | iseqp1 9445 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (seq𝑀( + , 𝐹, ℝ)‘(𝑘 + 1)) = ((seq𝑀( + , 𝐹, ℝ)‘𝑘) + (𝐹‘(𝑘 + 1)))) |
67 | 61, 66 | breqtrrd 3811 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (seq𝑀( + , 𝐹, ℝ)‘𝑘) ≤ (seq𝑀( + , 𝐹, ℝ)‘(𝑘 + 1))) |
68 | 1, 12, 67 | monoord 9455 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹, ℝ)‘𝐾) ≤ (seq𝑀( + , 𝐹, ℝ)‘𝑁)) |