Step | Hyp | Ref
| Expression |
1 | | smonoord.1 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) |
2 | | eluzfz2 12349 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑁 ∈ ((𝑀 + 1)...𝑁)) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → 𝑁 ∈ ((𝑀 + 1)...𝑁)) |
4 | | eleq1 2689 |
. . . . . 6
⊢ (𝑥 = (𝑀 + 1) → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...𝑁))) |
5 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = (𝑀 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑀 + 1))) |
6 | 5 | breq2d 4665 |
. . . . . 6
⊢ (𝑥 = (𝑀 + 1) → ((𝐹‘𝑀) < (𝐹‘𝑥) ↔ (𝐹‘𝑀) < (𝐹‘(𝑀 + 1)))) |
7 | 4, 6 | imbi12d 334 |
. . . . 5
⊢ (𝑥 = (𝑀 + 1) → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥)) ↔ ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑀 + 1))))) |
8 | 7 | imbi2d 330 |
. . . 4
⊢ (𝑥 = (𝑀 + 1) → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥))) ↔ (𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑀 + 1)))))) |
9 | | eleq1 2689 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ 𝑛 ∈ ((𝑀 + 1)...𝑁))) |
10 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝐹‘𝑥) = (𝐹‘𝑛)) |
11 | 10 | breq2d 4665 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((𝐹‘𝑀) < (𝐹‘𝑥) ↔ (𝐹‘𝑀) < (𝐹‘𝑛))) |
12 | 9, 11 | imbi12d 334 |
. . . . 5
⊢ (𝑥 = 𝑛 → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥)) ↔ (𝑛 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛)))) |
13 | 12 | imbi2d 330 |
. . . 4
⊢ (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥))) ↔ (𝜑 → (𝑛 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛))))) |
14 | | eleq1 2689 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) |
15 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑛 + 1))) |
16 | 15 | breq2d 4665 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((𝐹‘𝑀) < (𝐹‘𝑥) ↔ (𝐹‘𝑀) < (𝐹‘(𝑛 + 1)))) |
17 | 14, 16 | imbi12d 334 |
. . . . 5
⊢ (𝑥 = (𝑛 + 1) → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥)) ↔ ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1))))) |
18 | 17 | imbi2d 330 |
. . . 4
⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥))) ↔ (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1)))))) |
19 | | eleq1 2689 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ 𝑁 ∈ ((𝑀 + 1)...𝑁))) |
20 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝐹‘𝑥) = (𝐹‘𝑁)) |
21 | 20 | breq2d 4665 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((𝐹‘𝑀) < (𝐹‘𝑥) ↔ (𝐹‘𝑀) < (𝐹‘𝑁))) |
22 | 19, 21 | imbi12d 334 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥)) ↔ (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑁)))) |
23 | 22 | imbi2d 330 |
. . . 4
⊢ (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑥))) ↔ (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑁))))) |
24 | | smonoord.0 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
25 | | eluzp1m1 11711 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
26 | 24, 1, 25 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
27 | | eluzfz1 12348 |
. . . . . . . 8
⊢ ((𝑁 − 1) ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...(𝑁 − 1))) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (𝑀...(𝑁 − 1))) |
29 | | smonoord.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) |
30 | 29 | ralrimiva 2966 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...(𝑁 − 1))(𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) |
31 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → (𝐹‘𝑘) = (𝐹‘𝑀)) |
32 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑀 → (𝑘 + 1) = (𝑀 + 1)) |
33 | 32 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑀 + 1))) |
34 | 31, 33 | breq12d 4666 |
. . . . . . . 8
⊢ (𝑘 = 𝑀 → ((𝐹‘𝑘) < (𝐹‘(𝑘 + 1)) ↔ (𝐹‘𝑀) < (𝐹‘(𝑀 + 1)))) |
35 | 34 | rspcv 3305 |
. . . . . . 7
⊢ (𝑀 ∈ (𝑀...(𝑁 − 1)) → (∀𝑘 ∈ (𝑀...(𝑁 − 1))(𝐹‘𝑘) < (𝐹‘(𝑘 + 1)) → (𝐹‘𝑀) < (𝐹‘(𝑀 + 1)))) |
36 | 28, 30, 35 | sylc 65 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑀) < (𝐹‘(𝑀 + 1))) |
37 | 36 | a1d 25 |
. . . . 5
⊢ (𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑀 + 1)))) |
38 | 37 | a1i 11 |
. . . 4
⊢ ((𝑀 + 1) ∈ ℤ →
(𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑀 + 1))))) |
39 | | peano2fzr 12354 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → 𝑛 ∈ ((𝑀 + 1)...𝑁)) |
40 | 39 | adantll 750 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → 𝑛 ∈ ((𝑀 + 1)...𝑁)) |
41 | 40 | ex 450 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → 𝑛 ∈ ((𝑀 + 1)...𝑁))) |
42 | 41 | imim1d 82 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛)) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛)))) |
43 | | peano2uzr 11743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ 𝑛 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑛 ∈ (ℤ≥‘𝑀)) |
44 | 43 | ex 450 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℤ → (𝑛 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑛 ∈ (ℤ≥‘𝑀))) |
45 | 44, 24 | syl11 33 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘(𝑀 + 1)) → (𝜑 → 𝑛 ∈ (ℤ≥‘𝑀))) |
46 | 45 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → (𝜑 → 𝑛 ∈ (ℤ≥‘𝑀))) |
47 | 46 | impcom 446 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (ℤ≥‘𝑀)) |
48 | | eluzelz 11697 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑛 ∈ ℤ) |
49 | 48 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → 𝑛 ∈ ℤ) |
50 | 49 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ ℤ) |
51 | | elfzuz3 12339 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → 𝑁 ∈ (ℤ≥‘(𝑛 + 1))) |
52 | 51 | ad2antll 765 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑁 ∈ (ℤ≥‘(𝑛 + 1))) |
53 | | eluzp1m1 11711 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑛 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑛)) |
54 | 50, 52, 53 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝑁 − 1) ∈
(ℤ≥‘𝑛)) |
55 | | elfzuzb 12336 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (𝑀...(𝑁 − 1)) ↔ (𝑛 ∈ (ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑛))) |
56 | 47, 54, 55 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (𝑀...(𝑁 − 1))) |
57 | 30 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ∀𝑘 ∈ (𝑀...(𝑁 − 1))(𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) |
58 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
59 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → (𝑘 + 1) = (𝑛 + 1)) |
60 | 59 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝑛 + 1))) |
61 | 58, 60 | breq12d 4666 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) < (𝐹‘(𝑘 + 1)) ↔ (𝐹‘𝑛) < (𝐹‘(𝑛 + 1)))) |
62 | 61 | rspcv 3305 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (𝑀...(𝑁 − 1)) → (∀𝑘 ∈ (𝑀...(𝑁 − 1))(𝐹‘𝑘) < (𝐹‘(𝑘 + 1)) → (𝐹‘𝑛) < (𝐹‘(𝑛 + 1)))) |
63 | 56, 57, 62 | sylc 65 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝐹‘𝑛) < (𝐹‘(𝑛 + 1))) |
64 | | zre 11381 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
65 | 64 | lep1d 10955 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℤ → 𝑀 ≤ (𝑀 + 1)) |
66 | 24, 65 | jccir 562 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1))) |
67 | | eluzuzle 11696 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1)) → (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → 𝑁 ∈ (ℤ≥‘𝑀))) |
68 | 66, 1, 67 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
69 | | eluzfz1 12348 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
71 | | smonoord.2 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) |
72 | 71 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ) |
73 | 31 | eleq1d 2686 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑀 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑀) ∈ ℝ)) |
74 | 73 | rspcv 3305 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ → (𝐹‘𝑀) ∈ ℝ)) |
75 | 70, 72, 74 | sylc 65 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝑀) ∈ ℝ) |
76 | 75 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝐹‘𝑀) ∈ ℝ) |
77 | | fzp1ss 12392 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
78 | 24, 77 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁)) |
79 | 78 | sseld 3602 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝑛 + 1) ∈ (𝑀...𝑁))) |
80 | 79 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝜑 → (𝑛 + 1) ∈ (𝑀...𝑁))) |
81 | 80 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈
(ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → (𝜑 → (𝑛 + 1) ∈ (𝑀...𝑁))) |
82 | 81 | impcom 446 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝑛 + 1) ∈ (𝑀...𝑁)) |
83 | | peano2fzr 12354 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘𝑀) ∧ (𝑛 + 1) ∈ (𝑀...𝑁)) → 𝑛 ∈ (𝑀...𝑁)) |
84 | 47, 82, 83 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (𝑀...𝑁)) |
85 | 72 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ) |
86 | 58 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑛) ∈ ℝ)) |
87 | 86 | rspcv 3305 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ → (𝐹‘𝑛) ∈ ℝ)) |
88 | 84, 85, 87 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝐹‘𝑛) ∈ ℝ) |
89 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) |
90 | 89 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(𝑛 + 1)) ∈ ℝ)) |
91 | 90 | rspcv 3305 |
. . . . . . . . . . . 12
⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) ∈ ℝ → (𝐹‘(𝑛 + 1)) ∈ ℝ)) |
92 | 82, 85, 91 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝐹‘(𝑛 + 1)) ∈ ℝ) |
93 | | lttr 10114 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑀) ∈ ℝ ∧ (𝐹‘𝑛) ∈ ℝ ∧ (𝐹‘(𝑛 + 1)) ∈ ℝ) → (((𝐹‘𝑀) < (𝐹‘𝑛) ∧ (𝐹‘𝑛) < (𝐹‘(𝑛 + 1))) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1)))) |
94 | 76, 88, 92, 93 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (((𝐹‘𝑀) < (𝐹‘𝑛) ∧ (𝐹‘𝑛) < (𝐹‘(𝑛 + 1))) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1)))) |
95 | 63, 94 | mpan2d 710 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (ℤ≥‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((𝐹‘𝑀) < (𝐹‘𝑛) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1)))) |
96 | 95 | expr 643 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → ((𝐹‘𝑀) < (𝐹‘𝑛) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1))))) |
97 | 96 | a2d 29 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → (((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛)) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1))))) |
98 | 42, 97 | syld 47 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑛 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛)) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1))))) |
99 | 98 | expcom 451 |
. . . . 5
⊢ (𝑛 ∈
(ℤ≥‘(𝑀 + 1)) → (𝜑 → ((𝑛 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛)) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1)))))) |
100 | 99 | a2d 29 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘(𝑀 + 1)) → ((𝜑 → (𝑛 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑛))) → (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘(𝑛 + 1)))))) |
101 | 8, 13, 18, 23, 38, 100 | uzind4 11746 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑁)))) |
102 | 1, 101 | mpcom 38 |
. 2
⊢ (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝐹‘𝑀) < (𝐹‘𝑁))) |
103 | 3, 102 | mpd 15 |
1
⊢ (𝜑 → (𝐹‘𝑀) < (𝐹‘𝑁)) |