| Step | Hyp | Ref
| Expression |
| 1 | | monoordxrv.1 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
| 2 | | eluzfz2 13572 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
| 3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
| 4 | | eleq1 2829 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑀 ∈ (𝑀...𝑁))) |
| 5 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → (𝐹‘𝑥) = (𝐹‘𝑀)) |
| 6 | 5 | breq2d 5155 |
. . . . . 6
⊢ (𝑥 = 𝑀 → ((𝐹‘𝑀) ≤ (𝐹‘𝑥) ↔ (𝐹‘𝑀) ≤ (𝐹‘𝑀))) |
| 7 | 4, 6 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 𝑀 → ((𝑥 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑥)) ↔ (𝑀 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑀)))) |
| 8 | 7 | imbi2d 340 |
. . . 4
⊢ (𝑥 = 𝑀 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑥))) ↔ (𝜑 → (𝑀 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑀))))) |
| 9 | | eleq1 2829 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑛 ∈ (𝑀...𝑁))) |
| 10 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝐹‘𝑥) = (𝐹‘𝑛)) |
| 11 | 10 | breq2d 5155 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((𝐹‘𝑀) ≤ (𝐹‘𝑥) ↔ (𝐹‘𝑀) ≤ (𝐹‘𝑛))) |
| 12 | 9, 11 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑥)) ↔ (𝑛 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑛)))) |
| 13 | 12 | imbi2d 340 |
. . . 4
⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑥))) ↔ (𝜑 → (𝑛 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑛))))) |
| 14 | | eleq1 2829 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → (𝑥 ∈ (𝑀...𝑁) ↔ (𝑛 + 1) ∈ (𝑀...𝑁))) |
| 15 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑛 + 1))) |
| 16 | 15 | breq2d 5155 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑀) ≤ (𝐹‘𝑥) ↔ (𝐹‘𝑀) ≤ (𝐹‘(𝑛 + 1)))) |
| 17 | 14, 16 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = (𝑛 + 1) → ((𝑥 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑥)) ↔ ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘(𝑛 + 1))))) |
| 18 | 17 | imbi2d 340 |
. . . 4
⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑥))) ↔ (𝜑 → ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘(𝑛 + 1)))))) |
| 19 | | eleq1 2829 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (𝑥 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁))) |
| 20 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝐹‘𝑥) = (𝐹‘𝑁)) |
| 21 | 20 | breq2d 5155 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((𝐹‘𝑀) ≤ (𝐹‘𝑥) ↔ (𝐹‘𝑀) ≤ (𝐹‘𝑁))) |
| 22 | 19, 21 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((𝑥 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑥)) ↔ (𝑁 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑁)))) |
| 23 | 22 | imbi2d 340 |
. . . 4
⊢ (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑁))))) |
| 24 | | eluzfz1 13571 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
| 25 | 1, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
| 26 | | monoordxrv.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈
ℝ*) |
| 27 | 26 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈
ℝ*) |
| 28 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑀 → (𝐹‘𝑘) = (𝐹‘𝑀)) |
| 29 | 28 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → ((𝐹‘𝑘) ∈ ℝ* ↔ (𝐹‘𝑀) ∈
ℝ*)) |
| 30 | 29 | rspcv 3618 |
. . . . . . . 8
⊢ (𝑀 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ* → (𝐹‘𝑀) ∈
ℝ*)) |
| 31 | 25, 27, 30 | sylc 65 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝑀) ∈
ℝ*) |
| 32 | 31 | xrleidd 13194 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑀) ≤ (𝐹‘𝑀)) |
| 33 | 32 | a1d 25 |
. . . . 5
⊢ (𝜑 → (𝑀 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑀))) |
| 34 | 33 | a1i 11 |
. . . 4
⊢ (𝑀 ∈ ℤ → (𝜑 → (𝑀 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑀)))) |
| 35 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑛 ∈ (ℤ≥‘𝑀)) |
| 36 | | simprr 773 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝑛 + 1) ∈ (𝑀...𝑁)) |
| 37 | | peano2fzr 13577 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ (𝑀...𝑁)) |
| 38 | 35, 36, 37 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑛 ∈ (𝑀...𝑁)) |
| 39 | 38 | expr 456 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → 𝑛 ∈ (𝑀...𝑁))) |
| 40 | 39 | imim1d 82 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → ((𝑛 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑛)) → ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑛)))) |
| 41 | | eluzelz 12888 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → 𝑛 ∈ ℤ) |
| 42 | 35, 41 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑛 ∈ ℤ) |
| 43 | | elfzuz3 13561 |
. . . . . . . . . 10
⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘(𝑛 + 1))) |
| 44 | 36, 43 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑁 ∈ (ℤ≥‘(𝑛 + 1))) |
| 45 | | eluzp1m1 12904 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑛)) |
| 46 | 42, 44, 45 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝑁 − 1) ∈
(ℤ≥‘𝑛)) |
| 47 | | elfzuzb 13558 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝑀...(𝑁 − 1)) ↔ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑛))) |
| 48 | 35, 46, 47 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → 𝑛 ∈ (𝑀...(𝑁 − 1))) |
| 49 | | monoordxrv.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) |
| 50 | 49 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...(𝑁 − 1))(𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) |
| 51 | 50 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ∀𝑘 ∈ (𝑀...(𝑁 − 1))(𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) |
| 52 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
| 53 | | fvoveq1 7454 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑛 + 1))) |
| 54 | 52, 53 | breq12d 5156 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)) ↔ (𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1)))) |
| 55 | 54 | rspcv 3618 |
. . . . . . 7
⊢ (𝑛 ∈ (𝑀...(𝑁 − 1)) → (∀𝑘 ∈ (𝑀...(𝑁 − 1))(𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1)) → (𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1)))) |
| 56 | 48, 51, 55 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1))) |
| 57 | 31 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐹‘𝑀) ∈
ℝ*) |
| 58 | 27 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈
ℝ*) |
| 59 | 52 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) ∈ ℝ* ↔ (𝐹‘𝑛) ∈
ℝ*)) |
| 60 | 59 | rspcv 3618 |
. . . . . . . 8
⊢ (𝑛 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ* → (𝐹‘𝑛) ∈
ℝ*)) |
| 61 | 38, 58, 60 | sylc 65 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐹‘𝑛) ∈
ℝ*) |
| 62 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) |
| 63 | 62 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ∈ ℝ* ↔ (𝐹‘(𝑛 + 1)) ∈
ℝ*)) |
| 64 | 63 | rspcv 3618 |
. . . . . . . 8
⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ* → (𝐹‘(𝑛 + 1)) ∈
ℝ*)) |
| 65 | 36, 58, 64 | sylc 65 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (𝐹‘(𝑛 + 1)) ∈
ℝ*) |
| 66 | | xrletr 13200 |
. . . . . . 7
⊢ (((𝐹‘𝑀) ∈ ℝ* ∧ (𝐹‘𝑛) ∈ ℝ* ∧ (𝐹‘(𝑛 + 1)) ∈ ℝ*) →
(((𝐹‘𝑀) ≤ (𝐹‘𝑛) ∧ (𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1))) → (𝐹‘𝑀) ≤ (𝐹‘(𝑛 + 1)))) |
| 67 | 57, 61, 65, 66 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → (((𝐹‘𝑀) ≤ (𝐹‘𝑛) ∧ (𝐹‘𝑛) ≤ (𝐹‘(𝑛 + 1))) → (𝐹‘𝑀) ≤ (𝐹‘(𝑛 + 1)))) |
| 68 | 56, 67 | mpan2d 694 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁))) → ((𝐹‘𝑀) ≤ (𝐹‘𝑛) → (𝐹‘𝑀) ≤ (𝐹‘(𝑛 + 1)))) |
| 69 | 40, 68 | animpimp2impd 847 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → ((𝜑 → (𝑛 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑛))) → (𝜑 → ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘(𝑛 + 1)))))) |
| 70 | 8, 13, 18, 23, 34, 69 | uzind4 12948 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝜑 → (𝑁 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑁)))) |
| 71 | 1, 70 | mpcom 38 |
. 2
⊢ (𝜑 → (𝑁 ∈ (𝑀...𝑁) → (𝐹‘𝑀) ≤ (𝐹‘𝑁))) |
| 72 | 3, 71 | mpd 15 |
1
⊢ (𝜑 → (𝐹‘𝑀) ≤ (𝐹‘𝑁)) |