Step | Hyp | Ref
| Expression |
1 | | monoords.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ (𝑀...𝑁)) |
2 | 1 | ancli 572 |
. . 3
⊢ (𝜑 → (𝜑 ∧ 𝐼 ∈ (𝑀...𝑁))) |
3 | | eleq1 2676 |
. . . . . 6
⊢ (𝑘 = 𝐼 → (𝑘 ∈ (𝑀...𝑁) ↔ 𝐼 ∈ (𝑀...𝑁))) |
4 | 3 | anbi2d 736 |
. . . . 5
⊢ (𝑘 = 𝐼 → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝐼 ∈ (𝑀...𝑁)))) |
5 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = 𝐼 → (𝐹‘𝑘) = (𝐹‘𝐼)) |
6 | 5 | eleq1d 2672 |
. . . . 5
⊢ (𝑘 = 𝐼 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝐼) ∈ ℝ)) |
7 | 4, 6 | imbi12d 333 |
. . . 4
⊢ (𝑘 = 𝐼 → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ 𝐼 ∈ (𝑀...𝑁)) → (𝐹‘𝐼) ∈ ℝ))) |
8 | | monoords.fk |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) |
9 | 7, 8 | vtoclg 3239 |
. . 3
⊢ (𝐼 ∈ (𝑀...𝑁) → ((𝜑 ∧ 𝐼 ∈ (𝑀...𝑁)) → (𝐹‘𝐼) ∈ ℝ)) |
10 | 1, 2, 9 | sylc 63 |
. 2
⊢ (𝜑 → (𝐹‘𝐼) ∈ ℝ) |
11 | | elfzel1 12212 |
. . . . . . 7
⊢ (𝐼 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ) |
12 | 1, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
13 | | elfzelz 12213 |
. . . . . . 7
⊢ (𝐼 ∈ (𝑀...𝑁) → 𝐼 ∈ ℤ) |
14 | 1, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℤ) |
15 | | elfzle1 12215 |
. . . . . . 7
⊢ (𝐼 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐼) |
16 | 1, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀 ≤ 𝐼) |
17 | | eluz2 11569 |
. . . . . 6
⊢ (𝐼 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼)) |
18 | 12, 14, 16, 17 | syl3anbrc 1239 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ (ℤ≥‘𝑀)) |
19 | | elfzuz2 12217 |
. . . . . . 7
⊢ (𝐼 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝑀)) |
20 | 1, 19 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
21 | | eluzelz 11573 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
22 | 20, 21 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
23 | 14 | zred 11358 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℝ) |
24 | | monoords.j |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁)) |
25 | | elfzelz 12213 |
. . . . . . . 8
⊢ (𝐽 ∈ (𝑀...𝑁) → 𝐽 ∈ ℤ) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ ℤ) |
27 | 26 | zred 11358 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ ℝ) |
28 | 22 | zred 11358 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℝ) |
29 | | monoords.iltj |
. . . . . 6
⊢ (𝜑 → 𝐼 < 𝐽) |
30 | | elfzle2 12216 |
. . . . . . 7
⊢ (𝐽 ∈ (𝑀...𝑁) → 𝐽 ≤ 𝑁) |
31 | 24, 30 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐽 ≤ 𝑁) |
32 | 23, 27, 28, 29, 31 | ltletrd 10076 |
. . . . 5
⊢ (𝜑 → 𝐼 < 𝑁) |
33 | | elfzo2 12342 |
. . . . 5
⊢ (𝐼 ∈ (𝑀..^𝑁) ↔ (𝐼 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝐼 < 𝑁)) |
34 | 18, 22, 32, 33 | syl3anbrc 1239 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ (𝑀..^𝑁)) |
35 | | fzofzp1 12431 |
. . . 4
⊢ (𝐼 ∈ (𝑀..^𝑁) → (𝐼 + 1) ∈ (𝑀...𝑁)) |
36 | 34, 35 | syl 17 |
. . 3
⊢ (𝜑 → (𝐼 + 1) ∈ (𝑀...𝑁)) |
37 | 36 | ancli 572 |
. . 3
⊢ (𝜑 → (𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁))) |
38 | | eleq1 2676 |
. . . . . 6
⊢ (𝑘 = (𝐼 + 1) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝐼 + 1) ∈ (𝑀...𝑁))) |
39 | 38 | anbi2d 736 |
. . . . 5
⊢ (𝑘 = (𝐼 + 1) → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁)))) |
40 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = (𝐼 + 1) → (𝐹‘𝑘) = (𝐹‘(𝐼 + 1))) |
41 | 40 | eleq1d 2672 |
. . . . 5
⊢ (𝑘 = (𝐼 + 1) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(𝐼 + 1)) ∈ ℝ)) |
42 | 39, 41 | imbi12d 333 |
. . . 4
⊢ (𝑘 = (𝐼 + 1) → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝐼 + 1)) ∈ ℝ))) |
43 | 42, 8 | vtoclg 3239 |
. . 3
⊢ ((𝐼 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝐼 + 1)) ∈ ℝ)) |
44 | 36, 37, 43 | sylc 63 |
. 2
⊢ (𝜑 → (𝐹‘(𝐼 + 1)) ∈ ℝ) |
45 | 24 | ancli 572 |
. . 3
⊢ (𝜑 → (𝜑 ∧ 𝐽 ∈ (𝑀...𝑁))) |
46 | | eleq1 2676 |
. . . . . 6
⊢ (𝑘 = 𝐽 → (𝑘 ∈ (𝑀...𝑁) ↔ 𝐽 ∈ (𝑀...𝑁))) |
47 | 46 | anbi2d 736 |
. . . . 5
⊢ (𝑘 = 𝐽 → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)))) |
48 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = 𝐽 → (𝐹‘𝑘) = (𝐹‘𝐽)) |
49 | 48 | eleq1d 2672 |
. . . . 5
⊢ (𝑘 = 𝐽 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝐽) ∈ ℝ)) |
50 | 47, 49 | imbi12d 333 |
. . . 4
⊢ (𝑘 = 𝐽 → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝐹‘𝐽) ∈ ℝ))) |
51 | 50, 8 | vtoclg 3239 |
. . 3
⊢ (𝐽 ∈ (𝑀...𝑁) → ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝐹‘𝐽) ∈ ℝ)) |
52 | 24, 45, 51 | sylc 63 |
. 2
⊢ (𝜑 → (𝐹‘𝐽) ∈ ℝ) |
53 | 34 | ancli 572 |
. . 3
⊢ (𝜑 → (𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁))) |
54 | | eleq1 2676 |
. . . . . 6
⊢ (𝑘 = 𝐼 → (𝑘 ∈ (𝑀..^𝑁) ↔ 𝐼 ∈ (𝑀..^𝑁))) |
55 | 54 | anbi2d 736 |
. . . . 5
⊢ (𝑘 = 𝐼 → ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁)))) |
56 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑘 = 𝐼 → (𝑘 + 1) = (𝐼 + 1)) |
57 | 56 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 𝐼 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝐼 + 1))) |
58 | 5, 57 | breq12d 4596 |
. . . . 5
⊢ (𝑘 = 𝐼 → ((𝐹‘𝑘) < (𝐹‘(𝑘 + 1)) ↔ (𝐹‘𝐼) < (𝐹‘(𝐼 + 1)))) |
59 | 55, 58 | imbi12d 333 |
. . . 4
⊢ (𝑘 = 𝐼 → (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) ↔ ((𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁)) → (𝐹‘𝐼) < (𝐹‘(𝐼 + 1))))) |
60 | | monoords.flt |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) |
61 | 59, 60 | vtoclg 3239 |
. . 3
⊢ (𝐼 ∈ (𝑀..^𝑁) → ((𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁)) → (𝐹‘𝐼) < (𝐹‘(𝐼 + 1)))) |
62 | 34, 53, 61 | sylc 63 |
. 2
⊢ (𝜑 → (𝐹‘𝐼) < (𝐹‘(𝐼 + 1))) |
63 | 14 | peano2zd 11361 |
. . . 4
⊢ (𝜑 → (𝐼 + 1) ∈ ℤ) |
64 | | zltp1le 11304 |
. . . . . 6
⊢ ((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (𝐼 < 𝐽 ↔ (𝐼 + 1) ≤ 𝐽)) |
65 | 14, 26, 64 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐼 < 𝐽 ↔ (𝐼 + 1) ≤ 𝐽)) |
66 | 29, 65 | mpbid 221 |
. . . 4
⊢ (𝜑 → (𝐼 + 1) ≤ 𝐽) |
67 | | eluz2 11569 |
. . . 4
⊢ (𝐽 ∈
(ℤ≥‘(𝐼 + 1)) ↔ ((𝐼 + 1) ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐼 + 1) ≤ 𝐽)) |
68 | 63, 26, 66, 67 | syl3anbrc 1239 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘(𝐼 + 1))) |
69 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ∈ ℤ) |
70 | 22 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑁 ∈ ℤ) |
71 | | elfzelz 12213 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝐼 + 1)...𝐽) → 𝑘 ∈ ℤ) |
72 | 71 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ∈ ℤ) |
73 | 69, 70, 72 | 3jca 1235 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ)) |
74 | 69 | zred 11358 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ∈ ℝ) |
75 | 72 | zred 11358 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ∈ ℝ) |
76 | 63 | zred 11358 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 + 1) ∈ ℝ) |
77 | 76 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → (𝐼 + 1) ∈ ℝ) |
78 | 23 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐼 ∈ ℝ) |
79 | 16 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ≤ 𝐼) |
80 | 78 | ltp1d 10833 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐼 < (𝐼 + 1)) |
81 | 74, 78, 77, 79, 80 | lelttrd 10074 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 < (𝐼 + 1)) |
82 | | elfzle1 12215 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝐼 + 1)...𝐽) → (𝐼 + 1) ≤ 𝑘) |
83 | 82 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → (𝐼 + 1) ≤ 𝑘) |
84 | 74, 77, 75, 81, 83 | ltletrd 10076 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 < 𝑘) |
85 | 74, 75, 84 | ltled 10064 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ≤ 𝑘) |
86 | 27 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐽 ∈ ℝ) |
87 | 70 | zred 11358 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑁 ∈ ℝ) |
88 | | elfzle2 12216 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝐼 + 1)...𝐽) → 𝑘 ≤ 𝐽) |
89 | 88 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ≤ 𝐽) |
90 | 31 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐽 ≤ 𝑁) |
91 | 75, 86, 87, 89, 90 | letrd 10073 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ≤ 𝑁) |
92 | 73, 85, 91 | jca32 556 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
93 | | elfz2 12204 |
. . . . 5
⊢ (𝑘 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
94 | 92, 93 | sylibr 223 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ∈ (𝑀...𝑁)) |
95 | 94, 8 | syldan 486 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → (𝐹‘𝑘) ∈ ℝ) |
96 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 ∈ ℤ) |
97 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑁 ∈ ℤ) |
98 | | elfzelz 12213 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1)) → 𝑘 ∈ ℤ) |
99 | 98 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ ℤ) |
100 | 96, 97, 99 | 3jca 1235 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ)) |
101 | 96 | zred 11358 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 ∈ ℝ) |
102 | 99 | zred 11358 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ ℝ) |
103 | 76 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐼 + 1) ∈ ℝ) |
104 | 12 | zred 11358 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
105 | 23 | ltp1d 10833 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 < (𝐼 + 1)) |
106 | 104, 23, 76, 16, 105 | lelttrd 10074 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 < (𝐼 + 1)) |
107 | 106 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 < (𝐼 + 1)) |
108 | | elfzle1 12215 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1)) → (𝐼 + 1) ≤ 𝑘) |
109 | 108 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐼 + 1) ≤ 𝑘) |
110 | 101, 103,
102, 107, 109 | ltletrd 10076 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 < 𝑘) |
111 | 101, 102,
110 | ltled 10064 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 ≤ 𝑘) |
112 | 97 | zred 11358 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑁 ∈ ℝ) |
113 | | peano2rem 10227 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ ℝ → (𝐽 − 1) ∈
ℝ) |
114 | 27, 113 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐽 − 1) ∈ ℝ) |
115 | 114 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) ∈ ℝ) |
116 | | elfzle2 12216 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1)) → 𝑘 ≤ (𝐽 − 1)) |
117 | 116 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ≤ (𝐽 − 1)) |
118 | 27 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝐽 ∈ ℝ) |
119 | 118 | ltm1d 10835 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) < 𝐽) |
120 | 31 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝐽 ≤ 𝑁) |
121 | 115, 118,
112, 119, 120 | ltletrd 10076 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) < 𝑁) |
122 | 102, 115,
112, 117, 121 | lelttrd 10074 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 < 𝑁) |
123 | 102, 112,
122 | ltled 10064 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ≤ 𝑁) |
124 | 100, 111,
123 | jca32 556 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
125 | 124, 93 | sylibr 223 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ (𝑀...𝑁)) |
126 | 125, 8 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘𝑘) ∈ ℝ) |
127 | | peano2zm 11297 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
128 | 97, 127 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝑁 − 1) ∈ ℤ) |
129 | 96, 128, 99 | 3jca 1235 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧ 𝑘 ∈
ℤ)) |
130 | 128 | zred 11358 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝑁 − 1) ∈ ℝ) |
131 | | 1red 9934 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
132 | 27, 28, 131, 31 | lesub1dd 10522 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 − 1) ≤ (𝑁 − 1)) |
133 | 132 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) ≤ (𝑁 − 1)) |
134 | 102, 115,
130, 117, 133 | letrd 10073 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ≤ (𝑁 − 1)) |
135 | 129, 111,
134 | jca32 556 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ (𝑁 − 1)))) |
136 | | elfz2 12204 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...(𝑁 − 1)) ↔ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ (𝑁 − 1)))) |
137 | 135, 136 | sylibr 223 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ (𝑀...(𝑁 − 1))) |
138 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝑘 ∈ (𝑀...(𝑁 − 1))) |
139 | | fzoval 12340 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
140 | 22, 139 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
141 | 140 | eqcomd 2616 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀...(𝑁 − 1)) = (𝑀..^𝑁)) |
142 | 141 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝑀...(𝑁 − 1)) = (𝑀..^𝑁)) |
143 | 138, 142 | eleqtrd 2690 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝑘 ∈ (𝑀..^𝑁)) |
144 | | fzofzp1 12431 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
145 | 143, 144 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
146 | | simpl 472 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝜑) |
147 | 146, 145 | jca 553 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁))) |
148 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑗 = (𝑘 + 1) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑘 + 1) ∈ (𝑀...𝑁))) |
149 | 148 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)))) |
150 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑗 = (𝑘 + 1) → (𝐹‘𝑗) = (𝐹‘(𝑘 + 1))) |
151 | 150 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → ((𝐹‘𝑗) ∈ ℝ ↔ (𝐹‘(𝑘 + 1)) ∈ ℝ)) |
152 | 149, 151 | imbi12d 333 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ∈ ℝ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℝ))) |
153 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝑘 ∈ (𝑀...𝑁) ↔ 𝑗 ∈ (𝑀...𝑁))) |
154 | 153 | anbi2d 736 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)))) |
155 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗)) |
156 | 155 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑗) ∈ ℝ)) |
157 | 154, 156 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ∈ ℝ))) |
158 | 157, 8 | chvarv 2251 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ∈ ℝ) |
159 | 152, 158 | vtoclg 3239 |
. . . . . 6
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℝ)) |
160 | 145, 147,
159 | sylc 63 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ∈ ℝ) |
161 | 137, 160 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘(𝑘 + 1)) ∈ ℝ) |
162 | 143, 60 | syldan 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) |
163 | 137, 162 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) |
164 | 126, 161,
163 | ltled 10064 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) |
165 | 68, 95, 164 | monoord 12693 |
. 2
⊢ (𝜑 → (𝐹‘(𝐼 + 1)) ≤ (𝐹‘𝐽)) |
166 | 10, 44, 52, 62, 165 | ltletrd 10076 |
1
⊢ (𝜑 → (𝐹‘𝐼) < (𝐹‘𝐽)) |