Step | Hyp | Ref
| Expression |
1 | | sermono.2 |
. 2
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾)) |
2 | | elfzuz 12209 |
. . . 4
⊢ (𝑘 ∈ (𝐾...𝑁) → 𝑘 ∈ (ℤ≥‘𝐾)) |
3 | | sermono.1 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) |
4 | | uztrn 11580 |
. . . 4
⊢ ((𝑘 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
5 | 2, 3, 4 | syl2anr 494 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
6 | | elfzuz3 12210 |
. . . . . . 7
⊢ (𝑘 ∈ (𝐾...𝑁) → 𝑁 ∈ (ℤ≥‘𝑘)) |
7 | 6 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) → 𝑁 ∈ (ℤ≥‘𝑘)) |
8 | | fzss2 12252 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑘) → (𝑀...𝑘) ⊆ (𝑀...𝑁)) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) → (𝑀...𝑘) ⊆ (𝑀...𝑁)) |
10 | 9 | sselda 3568 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) ∧ 𝑥 ∈ (𝑀...𝑘)) → 𝑥 ∈ (𝑀...𝑁)) |
11 | | sermono.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ ℝ) |
12 | 11 | adantlr 747 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ ℝ) |
13 | 10, 12 | syldan 486 |
. . 3
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) ∧ 𝑥 ∈ (𝑀...𝑘)) → (𝐹‘𝑥) ∈ ℝ) |
14 | | readdcl 9898 |
. . . 4
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ) |
15 | 14 | adantl 481 |
. . 3
⊢ (((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ) |
16 | 5, 13, 15 | seqcl 12683 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...𝑁)) → (seq𝑀( + , 𝐹)‘𝑘) ∈ ℝ) |
17 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑘 ∈ (𝐾...(𝑁 − 1))) |
18 | 3 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝐾 ∈ (ℤ≥‘𝑀)) |
19 | | eluzelz 11573 |
. . . . . . . . 9
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝐾 ∈ ℤ) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝐾 ∈ ℤ) |
21 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑁 ∈ (ℤ≥‘𝐾)) |
22 | | eluzelz 11573 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → 𝑁 ∈ ℤ) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑁 ∈ ℤ) |
24 | | peano2zm 11297 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
25 | 23, 24 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑁 − 1) ∈ ℤ) |
26 | | elfzelz 12213 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝐾...(𝑁 − 1)) → 𝑘 ∈ ℤ) |
27 | 26 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑘 ∈ ℤ) |
28 | | 1zzd 11285 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 1 ∈
ℤ) |
29 | | fzaddel 12246 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ)
∧ (𝑘 ∈ ℤ
∧ 1 ∈ ℤ)) → (𝑘 ∈ (𝐾...(𝑁 − 1)) ↔ (𝑘 + 1) ∈ ((𝐾 + 1)...((𝑁 − 1) + 1)))) |
30 | 20, 25, 27, 28, 29 | syl22anc 1319 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 ∈ (𝐾...(𝑁 − 1)) ↔ (𝑘 + 1) ∈ ((𝐾 + 1)...((𝑁 − 1) + 1)))) |
31 | 17, 30 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ ((𝐾 + 1)...((𝑁 − 1) + 1))) |
32 | | zcn 11259 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
33 | | ax-1cn 9873 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
34 | | npcan 10169 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
35 | 32, 33, 34 | sylancl 693 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → ((𝑁 − 1) + 1) = 𝑁) |
36 | 23, 35 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁) |
37 | 36 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → ((𝐾 + 1)...((𝑁 − 1) + 1)) = ((𝐾 + 1)...𝑁)) |
38 | 31, 37 | eleqtrd 2690 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ ((𝐾 + 1)...𝑁)) |
39 | | sermono.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → 0 ≤ (𝐹‘𝑥)) |
40 | 39 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ ((𝐾 + 1)...𝑁)0 ≤ (𝐹‘𝑥)) |
41 | 40 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → ∀𝑥 ∈ ((𝐾 + 1)...𝑁)0 ≤ (𝐹‘𝑥)) |
42 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑘 + 1))) |
43 | 42 | breq2d 4595 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → (0 ≤ (𝐹‘𝑥) ↔ 0 ≤ (𝐹‘(𝑘 + 1)))) |
44 | 43 | rspcv 3278 |
. . . . 5
⊢ ((𝑘 + 1) ∈ ((𝐾 + 1)...𝑁) → (∀𝑥 ∈ ((𝐾 + 1)...𝑁)0 ≤ (𝐹‘𝑥) → 0 ≤ (𝐹‘(𝑘 + 1)))) |
45 | 38, 41, 44 | sylc 63 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 0 ≤ (𝐹‘(𝑘 + 1))) |
46 | | fzelp1 12263 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝐾...(𝑁 − 1)) → 𝑘 ∈ (𝐾...((𝑁 − 1) + 1))) |
47 | 46 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑘 ∈ (𝐾...((𝑁 − 1) + 1))) |
48 | 36 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝐾...((𝑁 − 1) + 1)) = (𝐾...𝑁)) |
49 | 47, 48 | eleqtrd 2690 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑘 ∈ (𝐾...𝑁)) |
50 | 49, 16 | syldan 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (seq𝑀( + , 𝐹)‘𝑘) ∈ ℝ) |
51 | | fzss1 12251 |
. . . . . . . 8
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) |
52 | 18, 51 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝐾...𝑁) ⊆ (𝑀...𝑁)) |
53 | | fzp1elp1 12264 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝐾...(𝑁 − 1)) → (𝑘 + 1) ∈ (𝐾...((𝑁 − 1) + 1))) |
54 | 53 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ (𝐾...((𝑁 − 1) + 1))) |
55 | 54, 48 | eleqtrd 2690 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ (𝐾...𝑁)) |
56 | 52, 55 | sseldd 3569 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
57 | 11 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) ∈ ℝ) |
58 | 57 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → ∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) ∈ ℝ) |
59 | 42 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘(𝑘 + 1)) ∈ ℝ)) |
60 | 59 | rspcv 3278 |
. . . . . 6
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → (∀𝑥 ∈ (𝑀...𝑁)(𝐹‘𝑥) ∈ ℝ → (𝐹‘(𝑘 + 1)) ∈ ℝ)) |
61 | 56, 58, 60 | sylc 63 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ∈ ℝ) |
62 | 50, 61 | addge01d 10494 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (0 ≤ (𝐹‘(𝑘 + 1)) ↔ (seq𝑀( + , 𝐹)‘𝑘) ≤ ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1))))) |
63 | 45, 62 | mpbid 221 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (seq𝑀( + , 𝐹)‘𝑘) ≤ ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1)))) |
64 | 49, 5 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → 𝑘 ∈ (ℤ≥‘𝑀)) |
65 | | seqp1 12678 |
. . . 4
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1)))) |
66 | 64, 65 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (seq𝑀( + , 𝐹)‘(𝑘 + 1)) = ((seq𝑀( + , 𝐹)‘𝑘) + (𝐹‘(𝑘 + 1)))) |
67 | 63, 66 | breqtrrd 4611 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐾...(𝑁 − 1))) → (seq𝑀( + , 𝐹)‘𝑘) ≤ (seq𝑀( + , 𝐹)‘(𝑘 + 1))) |
68 | 1, 16, 67 | monoord 12693 |
1
⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) ≤ (seq𝑀( + , 𝐹)‘𝑁)) |