Step | Hyp | Ref
| Expression |
1 | | monoords.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ (𝑀...𝑁)) |
2 | 1 | ancli 552 |
. . 3
⊢ (𝜑 → (𝜑 ∧ 𝐼 ∈ (𝑀...𝑁))) |
3 | | eleq1 2820 |
. . . . . 6
⊢ (𝑘 = 𝐼 → (𝑘 ∈ (𝑀...𝑁) ↔ 𝐼 ∈ (𝑀...𝑁))) |
4 | 3 | anbi2d 632 |
. . . . 5
⊢ (𝑘 = 𝐼 → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝐼 ∈ (𝑀...𝑁)))) |
5 | | fveq2 6674 |
. . . . . 6
⊢ (𝑘 = 𝐼 → (𝐹‘𝑘) = (𝐹‘𝐼)) |
6 | 5 | eleq1d 2817 |
. . . . 5
⊢ (𝑘 = 𝐼 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝐼) ∈ ℝ)) |
7 | 4, 6 | imbi12d 348 |
. . . 4
⊢ (𝑘 = 𝐼 → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ 𝐼 ∈ (𝑀...𝑁)) → (𝐹‘𝐼) ∈ ℝ))) |
8 | | monoords.fk |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) |
9 | 7, 8 | vtoclg 3470 |
. . 3
⊢ (𝐼 ∈ (𝑀...𝑁) → ((𝜑 ∧ 𝐼 ∈ (𝑀...𝑁)) → (𝐹‘𝐼) ∈ ℝ)) |
10 | 1, 2, 9 | sylc 65 |
. 2
⊢ (𝜑 → (𝐹‘𝐼) ∈ ℝ) |
11 | | elfzel1 12997 |
. . . . . . 7
⊢ (𝐼 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ) |
12 | 1, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
13 | 1 | elfzelzd 12999 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℤ) |
14 | | elfzle1 13001 |
. . . . . . 7
⊢ (𝐼 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐼) |
15 | 1, 14 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀 ≤ 𝐼) |
16 | | eluz2 12330 |
. . . . . 6
⊢ (𝐼 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼)) |
17 | 12, 13, 15, 16 | syl3anbrc 1344 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ (ℤ≥‘𝑀)) |
18 | | elfzuz2 13003 |
. . . . . . 7
⊢ (𝐼 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝑀)) |
19 | 1, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
20 | | eluzelz 12334 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
22 | 13 | zred 12168 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℝ) |
23 | | monoords.j |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁)) |
24 | 23 | elfzelzd 12999 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ ℤ) |
25 | 24 | zred 12168 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ ℝ) |
26 | 21 | zred 12168 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℝ) |
27 | | monoords.iltj |
. . . . . 6
⊢ (𝜑 → 𝐼 < 𝐽) |
28 | | elfzle2 13002 |
. . . . . . 7
⊢ (𝐽 ∈ (𝑀...𝑁) → 𝐽 ≤ 𝑁) |
29 | 23, 28 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐽 ≤ 𝑁) |
30 | 22, 25, 26, 27, 29 | ltletrd 10878 |
. . . . 5
⊢ (𝜑 → 𝐼 < 𝑁) |
31 | | elfzo2 13132 |
. . . . 5
⊢ (𝐼 ∈ (𝑀..^𝑁) ↔ (𝐼 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝐼 < 𝑁)) |
32 | 17, 21, 30, 31 | syl3anbrc 1344 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ (𝑀..^𝑁)) |
33 | | fzofzp1 13225 |
. . . 4
⊢ (𝐼 ∈ (𝑀..^𝑁) → (𝐼 + 1) ∈ (𝑀...𝑁)) |
34 | 32, 33 | syl 17 |
. . 3
⊢ (𝜑 → (𝐼 + 1) ∈ (𝑀...𝑁)) |
35 | 34 | ancli 552 |
. . 3
⊢ (𝜑 → (𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁))) |
36 | | eleq1 2820 |
. . . . . 6
⊢ (𝑘 = (𝐼 + 1) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝐼 + 1) ∈ (𝑀...𝑁))) |
37 | 36 | anbi2d 632 |
. . . . 5
⊢ (𝑘 = (𝐼 + 1) → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁)))) |
38 | | fveq2 6674 |
. . . . . 6
⊢ (𝑘 = (𝐼 + 1) → (𝐹‘𝑘) = (𝐹‘(𝐼 + 1))) |
39 | 38 | eleq1d 2817 |
. . . . 5
⊢ (𝑘 = (𝐼 + 1) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(𝐼 + 1)) ∈ ℝ)) |
40 | 37, 39 | imbi12d 348 |
. . . 4
⊢ (𝑘 = (𝐼 + 1) → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝐼 + 1)) ∈ ℝ))) |
41 | 40, 8 | vtoclg 3470 |
. . 3
⊢ ((𝐼 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝐼 + 1)) ∈ ℝ)) |
42 | 34, 35, 41 | sylc 65 |
. 2
⊢ (𝜑 → (𝐹‘(𝐼 + 1)) ∈ ℝ) |
43 | 23 | ancli 552 |
. . 3
⊢ (𝜑 → (𝜑 ∧ 𝐽 ∈ (𝑀...𝑁))) |
44 | | eleq1 2820 |
. . . . . 6
⊢ (𝑘 = 𝐽 → (𝑘 ∈ (𝑀...𝑁) ↔ 𝐽 ∈ (𝑀...𝑁))) |
45 | 44 | anbi2d 632 |
. . . . 5
⊢ (𝑘 = 𝐽 → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)))) |
46 | | fveq2 6674 |
. . . . . 6
⊢ (𝑘 = 𝐽 → (𝐹‘𝑘) = (𝐹‘𝐽)) |
47 | 46 | eleq1d 2817 |
. . . . 5
⊢ (𝑘 = 𝐽 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝐽) ∈ ℝ)) |
48 | 45, 47 | imbi12d 348 |
. . . 4
⊢ (𝑘 = 𝐽 → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝐹‘𝐽) ∈ ℝ))) |
49 | 48, 8 | vtoclg 3470 |
. . 3
⊢ (𝐽 ∈ (𝑀...𝑁) → ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝐹‘𝐽) ∈ ℝ)) |
50 | 23, 43, 49 | sylc 65 |
. 2
⊢ (𝜑 → (𝐹‘𝐽) ∈ ℝ) |
51 | 32 | ancli 552 |
. . 3
⊢ (𝜑 → (𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁))) |
52 | | eleq1 2820 |
. . . . . 6
⊢ (𝑘 = 𝐼 → (𝑘 ∈ (𝑀..^𝑁) ↔ 𝐼 ∈ (𝑀..^𝑁))) |
53 | 52 | anbi2d 632 |
. . . . 5
⊢ (𝑘 = 𝐼 → ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁)))) |
54 | | fvoveq1 7193 |
. . . . . 6
⊢ (𝑘 = 𝐼 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝐼 + 1))) |
55 | 5, 54 | breq12d 5043 |
. . . . 5
⊢ (𝑘 = 𝐼 → ((𝐹‘𝑘) < (𝐹‘(𝑘 + 1)) ↔ (𝐹‘𝐼) < (𝐹‘(𝐼 + 1)))) |
56 | 53, 55 | imbi12d 348 |
. . . 4
⊢ (𝑘 = 𝐼 → (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) ↔ ((𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁)) → (𝐹‘𝐼) < (𝐹‘(𝐼 + 1))))) |
57 | | monoords.flt |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) |
58 | 56, 57 | vtoclg 3470 |
. . 3
⊢ (𝐼 ∈ (𝑀..^𝑁) → ((𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁)) → (𝐹‘𝐼) < (𝐹‘(𝐼 + 1)))) |
59 | 32, 51, 58 | sylc 65 |
. 2
⊢ (𝜑 → (𝐹‘𝐼) < (𝐹‘(𝐼 + 1))) |
60 | 13 | peano2zd 12171 |
. . . 4
⊢ (𝜑 → (𝐼 + 1) ∈ ℤ) |
61 | | zltp1le 12113 |
. . . . . 6
⊢ ((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (𝐼 < 𝐽 ↔ (𝐼 + 1) ≤ 𝐽)) |
62 | 13, 24, 61 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝐼 < 𝐽 ↔ (𝐼 + 1) ≤ 𝐽)) |
63 | 27, 62 | mpbid 235 |
. . . 4
⊢ (𝜑 → (𝐼 + 1) ≤ 𝐽) |
64 | | eluz2 12330 |
. . . 4
⊢ (𝐽 ∈
(ℤ≥‘(𝐼 + 1)) ↔ ((𝐼 + 1) ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐼 + 1) ≤ 𝐽)) |
65 | 60, 24, 63, 64 | syl3anbrc 1344 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘(𝐼 + 1))) |
66 | 12 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ∈ ℤ) |
67 | 21 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑁 ∈ ℤ) |
68 | | elfzelz 12998 |
. . . . . 6
⊢ (𝑘 ∈ ((𝐼 + 1)...𝐽) → 𝑘 ∈ ℤ) |
69 | 68 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ∈ ℤ) |
70 | 66 | zred 12168 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ∈ ℝ) |
71 | 69 | zred 12168 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ∈ ℝ) |
72 | 60 | zred 12168 |
. . . . . . . 8
⊢ (𝜑 → (𝐼 + 1) ∈ ℝ) |
73 | 72 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → (𝐼 + 1) ∈ ℝ) |
74 | 22 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐼 ∈ ℝ) |
75 | 15 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ≤ 𝐼) |
76 | 74 | ltp1d 11648 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐼 < (𝐼 + 1)) |
77 | 70, 74, 73, 75, 76 | lelttrd 10876 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 < (𝐼 + 1)) |
78 | | elfzle1 13001 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝐼 + 1)...𝐽) → (𝐼 + 1) ≤ 𝑘) |
79 | 78 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → (𝐼 + 1) ≤ 𝑘) |
80 | 70, 73, 71, 77, 79 | ltletrd 10878 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 < 𝑘) |
81 | 70, 71, 80 | ltled 10866 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ≤ 𝑘) |
82 | 25 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐽 ∈ ℝ) |
83 | 67 | zred 12168 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑁 ∈ ℝ) |
84 | | elfzle2 13002 |
. . . . . . 7
⊢ (𝑘 ∈ ((𝐼 + 1)...𝐽) → 𝑘 ≤ 𝐽) |
85 | 84 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ≤ 𝐽) |
86 | 29 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐽 ≤ 𝑁) |
87 | 71, 82, 83, 85, 86 | letrd 10875 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ≤ 𝑁) |
88 | 66, 67, 69, 81, 87 | elfzd 12989 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ∈ (𝑀...𝑁)) |
89 | 88, 8 | syldan 594 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → (𝐹‘𝑘) ∈ ℝ) |
90 | 12 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 ∈ ℤ) |
91 | 21 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑁 ∈ ℤ) |
92 | | elfzelz 12998 |
. . . . . . 7
⊢ (𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1)) → 𝑘 ∈ ℤ) |
93 | 92 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ ℤ) |
94 | 90 | zred 12168 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 ∈ ℝ) |
95 | 93 | zred 12168 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ ℝ) |
96 | 72 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐼 + 1) ∈ ℝ) |
97 | 12 | zred 12168 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) |
98 | 22 | ltp1d 11648 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 < (𝐼 + 1)) |
99 | 97, 22, 72, 15, 98 | lelttrd 10876 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 < (𝐼 + 1)) |
100 | 99 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 < (𝐼 + 1)) |
101 | | elfzle1 13001 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1)) → (𝐼 + 1) ≤ 𝑘) |
102 | 101 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐼 + 1) ≤ 𝑘) |
103 | 94, 96, 95, 100, 102 | ltletrd 10878 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 < 𝑘) |
104 | 94, 95, 103 | ltled 10866 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 ≤ 𝑘) |
105 | 91 | zred 12168 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑁 ∈ ℝ) |
106 | | peano2rem 11031 |
. . . . . . . . . 10
⊢ (𝐽 ∈ ℝ → (𝐽 − 1) ∈
ℝ) |
107 | 25, 106 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 − 1) ∈ ℝ) |
108 | 107 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) ∈ ℝ) |
109 | | elfzle2 13002 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1)) → 𝑘 ≤ (𝐽 − 1)) |
110 | 109 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ≤ (𝐽 − 1)) |
111 | 25 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝐽 ∈ ℝ) |
112 | 111 | ltm1d 11650 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) < 𝐽) |
113 | 29 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝐽 ≤ 𝑁) |
114 | 108, 111,
105, 112, 113 | ltletrd 10878 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) < 𝑁) |
115 | 95, 108, 105, 110, 114 | lelttrd 10876 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 < 𝑁) |
116 | 95, 105, 115 | ltled 10866 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ≤ 𝑁) |
117 | 90, 91, 93, 104, 116 | elfzd 12989 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ (𝑀...𝑁)) |
118 | 117, 8 | syldan 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘𝑘) ∈ ℝ) |
119 | | peano2zm 12106 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
120 | 91, 119 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝑁 − 1) ∈ ℤ) |
121 | 120 | zred 12168 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝑁 − 1) ∈ ℝ) |
122 | | 1red 10720 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ) |
123 | 25, 26, 122, 29 | lesub1dd 11334 |
. . . . . . . 8
⊢ (𝜑 → (𝐽 − 1) ≤ (𝑁 − 1)) |
124 | 123 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) ≤ (𝑁 − 1)) |
125 | 95, 108, 121, 110, 124 | letrd 10875 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ≤ (𝑁 − 1)) |
126 | 90, 120, 93, 104, 125 | elfzd 12989 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ (𝑀...(𝑁 − 1))) |
127 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝑘 ∈ (𝑀...(𝑁 − 1))) |
128 | | fzoval 13130 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
129 | 21, 128 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
130 | 129 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀...(𝑁 − 1)) = (𝑀..^𝑁)) |
131 | 130 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝑀...(𝑁 − 1)) = (𝑀..^𝑁)) |
132 | 127, 131 | eleqtrd 2835 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝑘 ∈ (𝑀..^𝑁)) |
133 | | fzofzp1 13225 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
134 | 132, 133 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
135 | | simpl 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝜑) |
136 | 135, 134 | jca 515 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁))) |
137 | | eleq1 2820 |
. . . . . . . . 9
⊢ (𝑗 = (𝑘 + 1) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑘 + 1) ∈ (𝑀...𝑁))) |
138 | 137 | anbi2d 632 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)))) |
139 | | fveq2 6674 |
. . . . . . . . 9
⊢ (𝑗 = (𝑘 + 1) → (𝐹‘𝑗) = (𝐹‘(𝑘 + 1))) |
140 | 139 | eleq1d 2817 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → ((𝐹‘𝑗) ∈ ℝ ↔ (𝐹‘(𝑘 + 1)) ∈ ℝ)) |
141 | 138, 140 | imbi12d 348 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ∈ ℝ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℝ))) |
142 | | eleq1 2820 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝑘 ∈ (𝑀...𝑁) ↔ 𝑗 ∈ (𝑀...𝑁))) |
143 | 142 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)))) |
144 | | fveq2 6674 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗)) |
145 | 144 | eleq1d 2817 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑗) ∈ ℝ)) |
146 | 143, 145 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ∈ ℝ))) |
147 | 146, 8 | chvarvv 2010 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ∈ ℝ) |
148 | 141, 147 | vtoclg 3470 |
. . . . . 6
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℝ)) |
149 | 134, 136,
148 | sylc 65 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ∈ ℝ) |
150 | 126, 149 | syldan 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘(𝑘 + 1)) ∈ ℝ) |
151 | 132, 57 | syldan 594 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) |
152 | 126, 151 | syldan 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) |
153 | 118, 150,
152 | ltled 10866 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) |
154 | 65, 89, 153 | monoord 13492 |
. 2
⊢ (𝜑 → (𝐹‘(𝐼 + 1)) ≤ (𝐹‘𝐽)) |
155 | 10, 42, 50, 59, 154 | ltletrd 10878 |
1
⊢ (𝜑 → (𝐹‘𝐼) < (𝐹‘𝐽)) |