Step | Hyp | Ref
| Expression |
1 | | monoord2.1 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | monoord2.2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) |
3 | 2 | renegcld 8299 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → -(𝐹‘𝑘) ∈ ℝ) |
4 | | eqid 2170 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘)) = (𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘)) |
5 | 3, 4 | fmptd 5650 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘)):(𝑀...𝑁)⟶ℝ) |
6 | 5 | ffvelrnda 5631 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑛) ∈ ℝ) |
7 | | monoord2.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
8 | 7 | ralrimiva 2543 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...(𝑁 − 1))(𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
9 | | oveq1 5860 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑛 → (𝑘 + 1) = (𝑛 + 1)) |
10 | 9 | fveq2d 5500 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑛 + 1))) |
11 | | fveq2 5496 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
12 | 10, 11 | breq12d 4002 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → ((𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘) ↔ (𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛))) |
13 | 12 | cbvralv 2696 |
. . . . . . . 8
⊢
(∀𝑘 ∈
(𝑀...(𝑁 − 1))(𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘) ↔ ∀𝑛 ∈ (𝑀...(𝑁 − 1))(𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛)) |
14 | 8, 13 | sylib 121 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ (𝑀...(𝑁 − 1))(𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛)) |
15 | 14 | r19.21bi 2558 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛)) |
16 | | fveq2 5496 |
. . . . . . . . 9
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) |
17 | 16 | eleq1d 2239 |
. . . . . . . 8
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(𝑛 + 1)) ∈ ℝ)) |
18 | 2 | ralrimiva 2543 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ) |
19 | 18 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ) |
20 | | fzp1elp1 10031 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝑀...(𝑁 − 1)) → (𝑛 + 1) ∈ (𝑀...((𝑁 − 1) + 1))) |
21 | 20 | adantl 275 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝑛 + 1) ∈ (𝑀...((𝑁 − 1) + 1))) |
22 | | eluzelz 9496 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
23 | 1, 22 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℤ) |
24 | 23 | zcnd 9335 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
25 | | ax-1cn 7867 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
26 | | npcan 8128 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
27 | 24, 25, 26 | sylancl 411 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
28 | 27 | oveq2d 5869 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀...((𝑁 − 1) + 1)) = (𝑀...𝑁)) |
29 | 28 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝑀...((𝑁 − 1) + 1)) = (𝑀...𝑁)) |
30 | 21, 29 | eleqtrd 2249 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝑛 + 1) ∈ (𝑀...𝑁)) |
31 | 17, 19, 30 | rspcdva 2839 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑛 + 1)) ∈ ℝ) |
32 | 11 | eleq1d 2239 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑛) ∈ ℝ)) |
33 | | fzssp1 10023 |
. . . . . . . . . 10
⊢ (𝑀...(𝑁 − 1)) ⊆ (𝑀...((𝑁 − 1) + 1)) |
34 | 33, 28 | sseqtrid 3197 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀...(𝑁 − 1)) ⊆ (𝑀...𝑁)) |
35 | 34 | sselda 3147 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → 𝑛 ∈ (𝑀...𝑁)) |
36 | 32, 19, 35 | rspcdva 2839 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑛) ∈ ℝ) |
37 | 31, 36 | lenegd 8443 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ((𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛) ↔ -(𝐹‘𝑛) ≤ -(𝐹‘(𝑛 + 1)))) |
38 | 15, 37 | mpbid 146 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → -(𝐹‘𝑛) ≤ -(𝐹‘(𝑛 + 1))) |
39 | 36 | renegcld 8299 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → -(𝐹‘𝑛) ∈ ℝ) |
40 | 11 | negeqd 8114 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → -(𝐹‘𝑘) = -(𝐹‘𝑛)) |
41 | 40, 4 | fvmptg 5572 |
. . . . . 6
⊢ ((𝑛 ∈ (𝑀...𝑁) ∧ -(𝐹‘𝑛) ∈ ℝ) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑛) = -(𝐹‘𝑛)) |
42 | 35, 39, 41 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑛) = -(𝐹‘𝑛)) |
43 | 31 | renegcld 8299 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → -(𝐹‘(𝑛 + 1)) ∈ ℝ) |
44 | 16 | negeqd 8114 |
. . . . . . 7
⊢ (𝑘 = (𝑛 + 1) → -(𝐹‘𝑘) = -(𝐹‘(𝑛 + 1))) |
45 | 44, 4 | fvmptg 5572 |
. . . . . 6
⊢ (((𝑛 + 1) ∈ (𝑀...𝑁) ∧ -(𝐹‘(𝑛 + 1)) ∈ ℝ) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘(𝑛 + 1)) = -(𝐹‘(𝑛 + 1))) |
46 | 30, 43, 45 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘(𝑛 + 1)) = -(𝐹‘(𝑛 + 1))) |
47 | 38, 42, 46 | 3brtr4d 4021 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑛) ≤ ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘(𝑛 + 1))) |
48 | 1, 6, 47 | monoord 10432 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑀) ≤ ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑁)) |
49 | | eluzfz1 9987 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
50 | 1, 49 | syl 14 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
51 | | fveq2 5496 |
. . . . . . 7
⊢ (𝑘 = 𝑀 → (𝐹‘𝑘) = (𝐹‘𝑀)) |
52 | 51 | eleq1d 2239 |
. . . . . 6
⊢ (𝑘 = 𝑀 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑀) ∈ ℝ)) |
53 | 52, 18, 50 | rspcdva 2839 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ) |
54 | 53 | renegcld 8299 |
. . . 4
⊢ (𝜑 → -(𝐹‘𝑀) ∈ ℝ) |
55 | 51 | negeqd 8114 |
. . . . 5
⊢ (𝑘 = 𝑀 → -(𝐹‘𝑘) = -(𝐹‘𝑀)) |
56 | 55, 4 | fvmptg 5572 |
. . . 4
⊢ ((𝑀 ∈ (𝑀...𝑁) ∧ -(𝐹‘𝑀) ∈ ℝ) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑀) = -(𝐹‘𝑀)) |
57 | 50, 54, 56 | syl2anc 409 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑀) = -(𝐹‘𝑀)) |
58 | | eluzfz2 9988 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
59 | 1, 58 | syl 14 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
60 | | fveq2 5496 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (𝐹‘𝑘) = (𝐹‘𝑁)) |
61 | 60 | eleq1d 2239 |
. . . . . 6
⊢ (𝑘 = 𝑁 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑁) ∈ ℝ)) |
62 | 61, 18, 59 | rspcdva 2839 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ) |
63 | 62 | renegcld 8299 |
. . . 4
⊢ (𝜑 → -(𝐹‘𝑁) ∈ ℝ) |
64 | 60 | negeqd 8114 |
. . . . 5
⊢ (𝑘 = 𝑁 → -(𝐹‘𝑘) = -(𝐹‘𝑁)) |
65 | 64, 4 | fvmptg 5572 |
. . . 4
⊢ ((𝑁 ∈ (𝑀...𝑁) ∧ -(𝐹‘𝑁) ∈ ℝ) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑁) = -(𝐹‘𝑁)) |
66 | 59, 63, 65 | syl2anc 409 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑁) = -(𝐹‘𝑁)) |
67 | 48, 57, 66 | 3brtr3d 4020 |
. 2
⊢ (𝜑 → -(𝐹‘𝑀) ≤ -(𝐹‘𝑁)) |
68 | 62, 53 | lenegd 8443 |
. 2
⊢ (𝜑 → ((𝐹‘𝑁) ≤ (𝐹‘𝑀) ↔ -(𝐹‘𝑀) ≤ -(𝐹‘𝑁))) |
69 | 67, 68 | mpbird 166 |
1
⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀)) |