Step | Hyp | Ref
| Expression |
1 | | smonoord.1 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) |
2 | | eluzfz2 12220 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑁 ∈ ((𝑀 + 1)...𝑁)) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → 𝑁 ∈ ((𝑀 + 1)...𝑁)) |
4 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = (𝑀 + 1) → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...𝑁))) |
5 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = (𝑀 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑀 + 1))) |
6 | 5 | breq2d 4595 |
. . . . . 6
⊢ (𝑥 = (𝑀 + 1) → ((𝐹‘𝑀) < (𝐹‘𝑥) ↔ (𝐹‘𝑀) < (𝐹‘(𝑀 + 1)))) |
7 | 4, 6 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = (𝑀 + 1) → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥)) ↔ ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑀 + 1))))) |
8 | 7 | imbi2d 329 |
. . . 4
⊢ (𝑥 = (𝑀 + 1) → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥))) ↔ (𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑀 + 1)))))) |
9 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ 𝑛 ∈ ((𝑀 + 1)...𝑁))) |
10 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝐹‘𝑥) = (𝐹‘𝑛)) |
11 | 10 | breq2d 4595 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((𝐹‘𝑀) < (𝐹‘𝑥) ↔ (𝐹‘𝑀) < (𝐹‘𝑛))) |
12 | 9, 11 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥)) ↔ (𝑛 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛)))) |
13 | 12 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥))) ↔ (𝜑 → (𝑛 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛))))) |
14 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) |
15 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑛 + 1))) |
16 | 15 | breq2d 4595 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑀) < (𝐹‘𝑥) ↔ (𝐹‘𝑀) < (𝐹‘(𝑛 + 1)))) |
17 | 14, 16 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = (𝑛 + 1) → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥)) ↔ ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1))))) |
18 | 17 | imbi2d 329 |
. . . 4
⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥))) ↔ (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1)))))) |
19 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ 𝑁 ∈ ((𝑀 + 1)...𝑁))) |
20 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝐹‘𝑥) = (𝐹‘𝑁)) |
21 | 20 | breq2d 4595 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((𝐹‘𝑀) < (𝐹‘𝑥) ↔ (𝐹‘𝑀) < (𝐹‘𝑁))) |
22 | 19, 21 | imbi12d 333 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥)) ↔ (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑁)))) |
23 | 22 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥))) ↔ (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑁))))) |
24 | | smonoord.0 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
25 | | eluzp1m1 11587 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
26 | 24, 1, 25 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
27 | | eluzfz1 12219 |
. . . . . . . 8
⊢ ((𝑁 − 1) ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...(𝑁 − 1))) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (𝑀...(𝑁 − 1))) |
29 | | smonoord.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) |
30 | 29 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...(𝑁 − 1))(𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) |
31 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → (𝐹‘𝑘) = (𝐹‘𝑀)) |
32 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑀 → (𝑘 + 1) = (𝑀 + 1)) |
33 | 32 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑀 + 1))) |
34 | 31, 33 | breq12d 4596 |
. . . . . . . 8
⊢ (𝑘 = 𝑀 → ((𝐹‘𝑘) < (𝐹‘(𝑘 + 1)) ↔ (𝐹‘𝑀) < (𝐹‘(𝑀 + 1)))) |
35 | 34 | rspcv 3278 |
. . . . . . 7
⊢ (𝑀 ∈ (𝑀...(𝑁 − 1)) → (∀𝑘 ∈ (𝑀...(𝑁 − 1))(𝐹‘𝑘) < (𝐹‘(𝑘 + 1)) → (𝐹‘𝑀) < (𝐹‘(𝑀 + 1)))) |
36 | 28, 30, 35 | sylc 63 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑀) < (𝐹‘(𝑀 + 1))) |
37 | 36 | a1d 25 |
. . . . 5
⊢ (𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑀 + 1)))) |
38 | 37 | a1i 11 |
. . . 4
⊢ ((𝑀 + 1) ∈ ℤ →
(𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑀 + 1))))) |
39 | | peano2fzr 12225 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → 𝑛 ∈ ((𝑀 + 1)...𝑁)) |
40 | 39 | adantll 746 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → 𝑛 ∈ ((𝑀 + 1)...𝑁)) |
41 | 40 | ex 449 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → 𝑛 ∈ ((𝑀 + 1)...𝑁))) |
42 | 41 | imim1d 80 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛)) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛)))) |
43 | | peano2uzr 11619 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℤ ∧ 𝑛 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑛 ∈ (ℤ≥‘𝑀)) |
44 | 43 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℤ → (𝑛 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑛 ∈ (ℤ≥‘𝑀))) |
45 | 24, 44 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) → 𝑛 ∈ (ℤ≥‘𝑀))) |
46 | 45 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘(𝑀 + 1)) → (𝜑 → 𝑛 ∈ (ℤ≥‘𝑀))) |
47 | 46 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → (𝜑 → 𝑛 ∈ (ℤ≥‘𝑀))) |
48 | 47 | impcom 445 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (ℤ≥‘𝑀)) |
49 | | eluzelz 11573 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑛 ∈ ℤ) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → 𝑛 ∈ ℤ) |
51 | 50 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ ℤ) |
52 | | elfzuz3 12210 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → 𝑁 ∈ (ℤ≥‘(𝑛 + 1))) |
53 | 52 | ad2antll 761 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑁 ∈ (ℤ≥‘(𝑛 + 1))) |
54 | | eluzp1m1 11587 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑛)) |
55 | 51, 53, 54 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝑁 − 1) ∈
(ℤ≥‘𝑛)) |
56 | | elfzuzb 12207 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (𝑀...(𝑁 − 1)) ↔ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑛))) |
57 | 48, 55, 56 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (𝑀...(𝑁 − 1))) |
58 | 30 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ∀𝑘 ∈ (𝑀...(𝑁 − 1))(𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) |
59 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
60 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → (𝑘 + 1) = (𝑛 + 1)) |
61 | 60 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑛 + 1))) |
62 | 59, 61 | breq12d 4596 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) < (𝐹‘(𝑘 + 1)) ↔ (𝐹‘𝑛) < (𝐹‘(𝑛 + 1)))) |
63 | 62 | rspcv 3278 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (𝑀...(𝑁 − 1)) → (∀𝑘 ∈ (𝑀...(𝑁 − 1))(𝐹‘𝑘) < (𝐹‘(𝑘 + 1)) → (𝐹‘𝑛) < (𝐹‘(𝑛 + 1)))) |
64 | 57, 58, 63 | sylc 63 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝐹‘𝑛) < (𝐹‘(𝑛 + 1))) |
65 | | zre 11258 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
66 | 65 | lep1d 10834 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℤ → 𝑀 ≤ (𝑀 + 1)) |
67 | 24, 66 | jccir 560 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1))) |
68 | | eluzuzle 11572 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1)) → (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → 𝑁 ∈ (ℤ≥‘𝑀))) |
69 | 67, 1, 68 | sylc 63 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
70 | | eluzfz1 12219 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
72 | | smonoord.2 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) |
73 | 72 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ) |
74 | 31 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑀 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑀) ∈ ℝ)) |
75 | 74 | rspcv 3278 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ → (𝐹‘𝑀) ∈ ℝ)) |
76 | 71, 73, 75 | sylc 63 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ) |
77 | 76 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝐹‘𝑀) ∈ ℝ) |
78 | | fzp1ss 12262 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
79 | 24, 78 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
80 | 79 | sseld 3567 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝑛 + 1) ∈ (𝑀...𝑁))) |
81 | 80 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝜑 → (𝑛 + 1) ∈ (𝑀...𝑁))) |
82 | 81 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → (𝜑 → (𝑛 + 1) ∈ (𝑀...𝑁))) |
83 | 82 | impcom 445 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝑛 + 1) ∈ (𝑀...𝑁)) |
84 | | peano2fzr 12225 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ (𝑀...𝑁)) |
85 | 48, 83, 84 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (𝑀...𝑁)) |
86 | 73 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ) |
87 | 59 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑛) ∈ ℝ)) |
88 | 87 | rspcv 3278 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ → (𝐹‘𝑛) ∈ ℝ)) |
89 | 85, 86, 88 | sylc 63 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝐹‘𝑛) ∈ ℝ) |
90 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) |
91 | 90 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(𝑛 + 1)) ∈ ℝ)) |
92 | 91 | rspcv 3278 |
. . . . . . . . . . . 12
⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ → (𝐹‘(𝑛 + 1)) ∈ ℝ)) |
93 | 83, 86, 92 | sylc 63 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝐹‘(𝑛 + 1)) ∈ ℝ) |
94 | | lttr 9993 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑀) ∈ ℝ ∧ (𝐹‘𝑛) ∈ ℝ ∧ (𝐹‘(𝑛 + 1)) ∈ ℝ) → (((𝐹‘𝑀) < (𝐹‘𝑛) ∧ (𝐹‘𝑛) < (𝐹‘(𝑛 + 1))) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1)))) |
95 | 77, 89, 93, 94 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (((𝐹‘𝑀) < (𝐹‘𝑛) ∧ (𝐹‘𝑛) < (𝐹‘(𝑛 + 1))) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1)))) |
96 | 64, 95 | mpan2d 706 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((𝐹‘𝑀) < (𝐹‘𝑛) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1)))) |
97 | 96 | expr 641 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → ((𝐹‘𝑀) < (𝐹‘𝑛) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1))))) |
98 | 97 | a2d 29 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → (((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛)) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1))))) |
99 | 42, 98 | syld 46 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛)) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1))))) |
100 | 99 | expcom 450 |
. . . . 5
⊢ (𝑛 ∈
(ℤ≥‘(𝑀 + 1)) → (𝜑 → ((𝑛 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛)) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1)))))) |
101 | 100 | a2d 29 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘(𝑀 + 1)) → ((𝜑 → (𝑛 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛))) → (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1)))))) |
102 | 8, 13, 18, 23, 38, 101 | uzind4 11622 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑁)))) |
103 | 1, 102 | mpcom 37 |
. 2
⊢ (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑁))) |
104 | 3, 103 | mpd 15 |
1
⊢ (𝜑 → (𝐹‘𝑀) < (𝐹‘𝑁)) |