Step | Hyp | Ref
| Expression |
1 | | monoord2.1 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | monoord2.2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) |
3 | 2 | renegcld 7484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → -(𝐹‘𝑘) ∈ ℝ) |
4 | | eqid 2081 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘)) = (𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘)) |
5 | 3, 4 | fmptd 5343 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘)):(𝑀...𝑁)⟶ℝ) |
6 | 5 | ffvelrnda 5323 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑛) ∈ ℝ) |
7 | | monoord2.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
8 | 7 | ralrimiva 2434 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...(𝑁 − 1))(𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) |
9 | | oveq1 5539 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑛 → (𝑘 + 1) = (𝑛 + 1)) |
10 | 9 | fveq2d 5202 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑛 + 1))) |
11 | | fveq2 5198 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
12 | 10, 11 | breq12d 3798 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → ((𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘) ↔ (𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛))) |
13 | 12 | cbvralv 2577 |
. . . . . . . 8
⊢
(∀𝑘 ∈
(𝑀...(𝑁 − 1))(𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘) ↔ ∀𝑛 ∈ (𝑀...(𝑁 − 1))(𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛)) |
14 | 8, 13 | sylib 120 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ (𝑀...(𝑁 − 1))(𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛)) |
15 | 14 | r19.21bi 2449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛)) |
16 | | fzp1elp1 9092 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (𝑀...(𝑁 − 1)) → (𝑛 + 1) ∈ (𝑀...((𝑁 − 1) + 1))) |
17 | 16 | adantl 271 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝑛 + 1) ∈ (𝑀...((𝑁 − 1) + 1))) |
18 | | eluzelz 8628 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
19 | 1, 18 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℤ) |
20 | 19 | zcnd 8470 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
21 | | ax-1cn 7069 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
22 | | npcan 7317 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
23 | 20, 21, 22 | sylancl 404 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
24 | 23 | oveq2d 5548 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀...((𝑁 − 1) + 1)) = (𝑀...𝑁)) |
25 | 24 | adantr 270 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝑀...((𝑁 − 1) + 1)) = (𝑀...𝑁)) |
26 | 17, 25 | eleqtrd 2157 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝑛 + 1) ∈ (𝑀...𝑁)) |
27 | 2 | ralrimiva 2434 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ) |
28 | 27 | adantr 270 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ) |
29 | | fveq2 5198 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) |
30 | 29 | eleq1d 2147 |
. . . . . . . . 9
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(𝑛 + 1)) ∈ ℝ)) |
31 | 30 | rspcv 2697 |
. . . . . . . 8
⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ → (𝐹‘(𝑛 + 1)) ∈ ℝ)) |
32 | 26, 28, 31 | sylc 61 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑛 + 1)) ∈ ℝ) |
33 | | fzssp1 9085 |
. . . . . . . . . 10
⊢ (𝑀...(𝑁 − 1)) ⊆ (𝑀...((𝑁 − 1) + 1)) |
34 | 33, 24 | syl5sseq 3047 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀...(𝑁 − 1)) ⊆ (𝑀...𝑁)) |
35 | 34 | sselda 2999 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → 𝑛 ∈ (𝑀...𝑁)) |
36 | 11 | eleq1d 2147 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑛) ∈ ℝ)) |
37 | 36 | rspcv 2697 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ → (𝐹‘𝑛) ∈ ℝ)) |
38 | 35, 28, 37 | sylc 61 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑛) ∈ ℝ) |
39 | 32, 38 | lenegd 7624 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ((𝐹‘(𝑛 + 1)) ≤ (𝐹‘𝑛) ↔ -(𝐹‘𝑛) ≤ -(𝐹‘(𝑛 + 1)))) |
40 | 15, 39 | mpbid 145 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → -(𝐹‘𝑛) ≤ -(𝐹‘(𝑛 + 1))) |
41 | 38 | renegcld 7484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → -(𝐹‘𝑛) ∈ ℝ) |
42 | 11 | negeqd 7303 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → -(𝐹‘𝑘) = -(𝐹‘𝑛)) |
43 | 42, 4 | fvmptg 5269 |
. . . . . 6
⊢ ((𝑛 ∈ (𝑀...𝑁) ∧ -(𝐹‘𝑛) ∈ ℝ) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑛) = -(𝐹‘𝑛)) |
44 | 35, 41, 43 | syl2anc 403 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑛) = -(𝐹‘𝑛)) |
45 | 32 | renegcld 7484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → -(𝐹‘(𝑛 + 1)) ∈ ℝ) |
46 | 29 | negeqd 7303 |
. . . . . . 7
⊢ (𝑘 = (𝑛 + 1) → -(𝐹‘𝑘) = -(𝐹‘(𝑛 + 1))) |
47 | 46, 4 | fvmptg 5269 |
. . . . . 6
⊢ (((𝑛 + 1) ∈ (𝑀...𝑁) ∧ -(𝐹‘(𝑛 + 1)) ∈ ℝ) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘(𝑛 + 1)) = -(𝐹‘(𝑛 + 1))) |
48 | 26, 45, 47 | syl2anc 403 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘(𝑛 + 1)) = -(𝐹‘(𝑛 + 1))) |
49 | 40, 44, 48 | 3brtr4d 3815 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...(𝑁 − 1))) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑛) ≤ ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘(𝑛 + 1))) |
50 | 1, 6, 49 | monoord 9455 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑀) ≤ ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑁)) |
51 | | eluzfz1 9050 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
52 | 1, 51 | syl 14 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
53 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑘 = 𝑀 → (𝐹‘𝑘) = (𝐹‘𝑀)) |
54 | 53 | eleq1d 2147 |
. . . . . . 7
⊢ (𝑘 = 𝑀 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑀) ∈ ℝ)) |
55 | 54 | rspcv 2697 |
. . . . . 6
⊢ (𝑀 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ → (𝐹‘𝑀) ∈ ℝ)) |
56 | 52, 27, 55 | sylc 61 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ) |
57 | 56 | renegcld 7484 |
. . . 4
⊢ (𝜑 → -(𝐹‘𝑀) ∈ ℝ) |
58 | 53 | negeqd 7303 |
. . . . 5
⊢ (𝑘 = 𝑀 → -(𝐹‘𝑘) = -(𝐹‘𝑀)) |
59 | 58, 4 | fvmptg 5269 |
. . . 4
⊢ ((𝑀 ∈ (𝑀...𝑁) ∧ -(𝐹‘𝑀) ∈ ℝ) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑀) = -(𝐹‘𝑀)) |
60 | 52, 57, 59 | syl2anc 403 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑀) = -(𝐹‘𝑀)) |
61 | | eluzfz2 9051 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
62 | 1, 61 | syl 14 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
63 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → (𝐹‘𝑘) = (𝐹‘𝑁)) |
64 | 63 | eleq1d 2147 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑁) ∈ ℝ)) |
65 | 64 | rspcv 2697 |
. . . . . 6
⊢ (𝑁 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ → (𝐹‘𝑁) ∈ ℝ)) |
66 | 62, 27, 65 | sylc 61 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑁) ∈ ℝ) |
67 | 66 | renegcld 7484 |
. . . 4
⊢ (𝜑 → -(𝐹‘𝑁) ∈ ℝ) |
68 | 63 | negeqd 7303 |
. . . . 5
⊢ (𝑘 = 𝑁 → -(𝐹‘𝑘) = -(𝐹‘𝑁)) |
69 | 68, 4 | fvmptg 5269 |
. . . 4
⊢ ((𝑁 ∈ (𝑀...𝑁) ∧ -(𝐹‘𝑁) ∈ ℝ) → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑁) = -(𝐹‘𝑁)) |
70 | 62, 67, 69 | syl2anc 403 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ↦ -(𝐹‘𝑘))‘𝑁) = -(𝐹‘𝑁)) |
71 | 50, 60, 70 | 3brtr3d 3814 |
. 2
⊢ (𝜑 → -(𝐹‘𝑀) ≤ -(𝐹‘𝑁)) |
72 | 66, 56 | lenegd 7624 |
. 2
⊢ (𝜑 → ((𝐹‘𝑁) ≤ (𝐹‘𝑀) ↔ -(𝐹‘𝑀) ≤ -(𝐹‘𝑁))) |
73 | 71, 72 | mpbird 165 |
1
⊢ (𝜑 → (𝐹‘𝑁) ≤ (𝐹‘𝑀)) |