Step | Hyp | Ref
| Expression |
1 | | monoords.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ (𝑀...𝑁)) |
2 | 1 | ancli 551 |
. . 3
⊢ (𝜑 → (𝜑 ∧ 𝐼 ∈ (𝑀...𝑁))) |
3 | | eleq1 2900 |
. . . . . 6
⊢ (𝑘 = 𝐼 → (𝑘 ∈ (𝑀...𝑁) ↔ 𝐼 ∈ (𝑀...𝑁))) |
4 | 3 | anbi2d 630 |
. . . . 5
⊢ (𝑘 = 𝐼 → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝐼 ∈ (𝑀...𝑁)))) |
5 | | fveq2 6665 |
. . . . . 6
⊢ (𝑘 = 𝐼 → (𝐹‘𝑘) = (𝐹‘𝐼)) |
6 | 5 | eleq1d 2897 |
. . . . 5
⊢ (𝑘 = 𝐼 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝐼) ∈ ℝ)) |
7 | 4, 6 | imbi12d 347 |
. . . 4
⊢ (𝑘 = 𝐼 → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ 𝐼 ∈ (𝑀...𝑁)) → (𝐹‘𝐼) ∈ ℝ))) |
8 | | monoords.fk |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) |
9 | 7, 8 | vtoclg 3568 |
. . 3
⊢ (𝐼 ∈ (𝑀...𝑁) → ((𝜑 ∧ 𝐼 ∈ (𝑀...𝑁)) → (𝐹‘𝐼) ∈ ℝ)) |
10 | 1, 2, 9 | sylc 65 |
. 2
⊢ (𝜑 → (𝐹‘𝐼) ∈ ℝ) |
11 | | elfzel1 12901 |
. . . . . . 7
⊢ (𝐼 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ) |
12 | 1, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
13 | | elfzelz 12902 |
. . . . . . 7
⊢ (𝐼 ∈ (𝑀...𝑁) → 𝐼 ∈ ℤ) |
14 | 1, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℤ) |
15 | | elfzle1 12904 |
. . . . . . 7
⊢ (𝐼 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐼) |
16 | 1, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀 ≤ 𝐼) |
17 | | eluz2 12243 |
. . . . . 6
⊢ (𝐼 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼)) |
18 | 12, 14, 16, 17 | syl3anbrc 1339 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ (ℤ≥‘𝑀)) |
19 | | elfzuz2 12906 |
. . . . . . 7
⊢ (𝐼 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝑀)) |
20 | 1, 19 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
21 | | eluzelz 12247 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
22 | 20, 21 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
23 | 14 | zred 12081 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℝ) |
24 | | monoords.j |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁)) |
25 | | elfzelz 12902 |
. . . . . . . 8
⊢ (𝐽 ∈ (𝑀...𝑁) → 𝐽 ∈ ℤ) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ ℤ) |
27 | 26 | zred 12081 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ ℝ) |
28 | 22 | zred 12081 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℝ) |
29 | | monoords.iltj |
. . . . . 6
⊢ (𝜑 → 𝐼 < 𝐽) |
30 | | elfzle2 12905 |
. . . . . . 7
⊢ (𝐽 ∈ (𝑀...𝑁) → 𝐽 ≤ 𝑁) |
31 | 24, 30 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐽 ≤ 𝑁) |
32 | 23, 27, 28, 29, 31 | ltletrd 10794 |
. . . . 5
⊢ (𝜑 → 𝐼 < 𝑁) |
33 | | elfzo2 13035 |
. . . . 5
⊢ (𝐼 ∈ (𝑀..^𝑁) ↔ (𝐼 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝐼 < 𝑁)) |
34 | 18, 22, 32, 33 | syl3anbrc 1339 |
. . . 4
⊢ (𝜑 → 𝐼 ∈ (𝑀..^𝑁)) |
35 | | fzofzp1 13128 |
. . . 4
⊢ (𝐼 ∈ (𝑀..^𝑁) → (𝐼 + 1) ∈ (𝑀...𝑁)) |
36 | 34, 35 | syl 17 |
. . 3
⊢ (𝜑 → (𝐼 + 1) ∈ (𝑀...𝑁)) |
37 | 36 | ancli 551 |
. . 3
⊢ (𝜑 → (𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁))) |
38 | | eleq1 2900 |
. . . . . 6
⊢ (𝑘 = (𝐼 + 1) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝐼 + 1) ∈ (𝑀...𝑁))) |
39 | 38 | anbi2d 630 |
. . . . 5
⊢ (𝑘 = (𝐼 + 1) → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁)))) |
40 | | fveq2 6665 |
. . . . . 6
⊢ (𝑘 = (𝐼 + 1) → (𝐹‘𝑘) = (𝐹‘(𝐼 + 1))) |
41 | 40 | eleq1d 2897 |
. . . . 5
⊢ (𝑘 = (𝐼 + 1) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(𝐼 + 1)) ∈ ℝ)) |
42 | 39, 41 | imbi12d 347 |
. . . 4
⊢ (𝑘 = (𝐼 + 1) → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝐼 + 1)) ∈ ℝ))) |
43 | 42, 8 | vtoclg 3568 |
. . 3
⊢ ((𝐼 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝐼 + 1)) ∈ ℝ)) |
44 | 36, 37, 43 | sylc 65 |
. 2
⊢ (𝜑 → (𝐹‘(𝐼 + 1)) ∈ ℝ) |
45 | 24 | ancli 551 |
. . 3
⊢ (𝜑 → (𝜑 ∧ 𝐽 ∈ (𝑀...𝑁))) |
46 | | eleq1 2900 |
. . . . . 6
⊢ (𝑘 = 𝐽 → (𝑘 ∈ (𝑀...𝑁) ↔ 𝐽 ∈ (𝑀...𝑁))) |
47 | 46 | anbi2d 630 |
. . . . 5
⊢ (𝑘 = 𝐽 → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)))) |
48 | | fveq2 6665 |
. . . . . 6
⊢ (𝑘 = 𝐽 → (𝐹‘𝑘) = (𝐹‘𝐽)) |
49 | 48 | eleq1d 2897 |
. . . . 5
⊢ (𝑘 = 𝐽 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝐽) ∈ ℝ)) |
50 | 47, 49 | imbi12d 347 |
. . . 4
⊢ (𝑘 = 𝐽 → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝐹‘𝐽) ∈ ℝ))) |
51 | 50, 8 | vtoclg 3568 |
. . 3
⊢ (𝐽 ∈ (𝑀...𝑁) → ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝐹‘𝐽) ∈ ℝ)) |
52 | 24, 45, 51 | sylc 65 |
. 2
⊢ (𝜑 → (𝐹‘𝐽) ∈ ℝ) |
53 | 34 | ancli 551 |
. . 3
⊢ (𝜑 → (𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁))) |
54 | | eleq1 2900 |
. . . . . 6
⊢ (𝑘 = 𝐼 → (𝑘 ∈ (𝑀..^𝑁) ↔ 𝐼 ∈ (𝑀..^𝑁))) |
55 | 54 | anbi2d 630 |
. . . . 5
⊢ (𝑘 = 𝐼 → ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁)))) |
56 | | fvoveq1 7173 |
. . . . . 6
⊢ (𝑘 = 𝐼 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝐼 + 1))) |
57 | 5, 56 | breq12d 5072 |
. . . . 5
⊢ (𝑘 = 𝐼 → ((𝐹‘𝑘) < (𝐹‘(𝑘 + 1)) ↔ (𝐹‘𝐼) < (𝐹‘(𝐼 + 1)))) |
58 | 55, 57 | imbi12d 347 |
. . . 4
⊢ (𝑘 = 𝐼 → (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) ↔ ((𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁)) → (𝐹‘𝐼) < (𝐹‘(𝐼 + 1))))) |
59 | | monoords.flt |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) |
60 | 58, 59 | vtoclg 3568 |
. . 3
⊢ (𝐼 ∈ (𝑀..^𝑁) → ((𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁)) → (𝐹‘𝐼) < (𝐹‘(𝐼 + 1)))) |
61 | 34, 53, 60 | sylc 65 |
. 2
⊢ (𝜑 → (𝐹‘𝐼) < (𝐹‘(𝐼 + 1))) |
62 | 14 | peano2zd 12084 |
. . . 4
⊢ (𝜑 → (𝐼 + 1) ∈ ℤ) |
63 | | zltp1le 12026 |
. . . . . 6
⊢ ((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (𝐼 < 𝐽 ↔ (𝐼 + 1) ≤ 𝐽)) |
64 | 14, 26, 63 | syl2anc 586 |
. . . . 5
⊢ (𝜑 → (𝐼 < 𝐽 ↔ (𝐼 + 1) ≤ 𝐽)) |
65 | 29, 64 | mpbid 234 |
. . . 4
⊢ (𝜑 → (𝐼 + 1) ≤ 𝐽) |
66 | | eluz2 12243 |
. . . 4
⊢ (𝐽 ∈
(ℤ≥‘(𝐼 + 1)) ↔ ((𝐼 + 1) ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐼 + 1) ≤ 𝐽)) |
67 | 62, 26, 65, 66 | syl3anbrc 1339 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘(𝐼 + 1))) |
68 | 12 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ∈ ℤ) |
69 | 22 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑁 ∈ ℤ) |
70 | | elfzelz 12902 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝐼 + 1)...𝐽) → 𝑘 ∈ ℤ) |
71 | 70 | adantl 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ∈ ℤ) |
72 | 68, 69, 71 | 3jca 1124 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ)) |
73 | 68 | zred 12081 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ∈ ℝ) |
74 | 71 | zred 12081 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ∈ ℝ) |
75 | 62 | zred 12081 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 + 1) ∈ ℝ) |
76 | 75 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → (𝐼 + 1) ∈ ℝ) |
77 | 23 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐼 ∈ ℝ) |
78 | 16 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ≤ 𝐼) |
79 | 77 | ltp1d 11564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐼 < (𝐼 + 1)) |
80 | 73, 77, 76, 78, 79 | lelttrd 10792 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 < (𝐼 + 1)) |
81 | | elfzle1 12904 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝐼 + 1)...𝐽) → (𝐼 + 1) ≤ 𝑘) |
82 | 81 | adantl 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → (𝐼 + 1) ≤ 𝑘) |
83 | 73, 76, 74, 80, 82 | ltletrd 10794 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 < 𝑘) |
84 | 73, 74, 83 | ltled 10782 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ≤ 𝑘) |
85 | 27 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐽 ∈ ℝ) |
86 | 69 | zred 12081 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑁 ∈ ℝ) |
87 | | elfzle2 12905 |
. . . . . . . 8
⊢ (𝑘 ∈ ((𝐼 + 1)...𝐽) → 𝑘 ≤ 𝐽) |
88 | 87 | adantl 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ≤ 𝐽) |
89 | 31 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐽 ≤ 𝑁) |
90 | 74, 85, 86, 88, 89 | letrd 10791 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ≤ 𝑁) |
91 | 72, 84, 90 | jca32 518 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
92 | | elfz2 12893 |
. . . . 5
⊢ (𝑘 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
93 | 91, 92 | sylibr 236 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ∈ (𝑀...𝑁)) |
94 | 93, 8 | syldan 593 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → (𝐹‘𝑘) ∈ ℝ) |
95 | 12 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 ∈ ℤ) |
96 | 22 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑁 ∈ ℤ) |
97 | | elfzelz 12902 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1)) → 𝑘 ∈ ℤ) |
98 | 97 | adantl 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ ℤ) |
99 | 95, 96, 98 | 3jca 1124 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ)) |
100 | 95 | zred 12081 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 ∈ ℝ) |
101 | 98 | zred 12081 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ ℝ) |
102 | 75 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐼 + 1) ∈ ℝ) |
103 | 12 | zred 12081 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
104 | 23 | ltp1d 11564 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 < (𝐼 + 1)) |
105 | 103, 23, 75, 16, 104 | lelttrd 10792 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 < (𝐼 + 1)) |
106 | 105 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 < (𝐼 + 1)) |
107 | | elfzle1 12904 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1)) → (𝐼 + 1) ≤ 𝑘) |
108 | 107 | adantl 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐼 + 1) ≤ 𝑘) |
109 | 100, 102,
101, 106, 108 | ltletrd 10794 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 < 𝑘) |
110 | 100, 101,
109 | ltled 10782 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 ≤ 𝑘) |
111 | 96 | zred 12081 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑁 ∈ ℝ) |
112 | | peano2rem 10947 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ ℝ → (𝐽 − 1) ∈
ℝ) |
113 | 27, 112 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐽 − 1) ∈ ℝ) |
114 | 113 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) ∈ ℝ) |
115 | | elfzle2 12905 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1)) → 𝑘 ≤ (𝐽 − 1)) |
116 | 115 | adantl 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ≤ (𝐽 − 1)) |
117 | 27 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝐽 ∈ ℝ) |
118 | 117 | ltm1d 11566 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) < 𝐽) |
119 | 31 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝐽 ≤ 𝑁) |
120 | 114, 117,
111, 118, 119 | ltletrd 10794 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) < 𝑁) |
121 | 101, 114,
111, 116, 120 | lelttrd 10792 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 < 𝑁) |
122 | 101, 111,
121 | ltled 10782 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ≤ 𝑁) |
123 | 99, 110, 122 | jca32 518 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
124 | 123, 92 | sylibr 236 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ (𝑀...𝑁)) |
125 | 124, 8 | syldan 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘𝑘) ∈ ℝ) |
126 | | peano2zm 12019 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
127 | 96, 126 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝑁 − 1) ∈ ℤ) |
128 | 95, 127, 98 | 3jca 1124 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧ 𝑘 ∈
ℤ)) |
129 | 127 | zred 12081 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝑁 − 1) ∈ ℝ) |
130 | | 1red 10636 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
131 | 27, 28, 130, 31 | lesub1dd 11250 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 − 1) ≤ (𝑁 − 1)) |
132 | 131 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) ≤ (𝑁 − 1)) |
133 | 101, 114,
129, 116, 132 | letrd 10791 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ≤ (𝑁 − 1)) |
134 | 128, 110,
133 | jca32 518 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ (𝑁 − 1)))) |
135 | | elfz2 12893 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...(𝑁 − 1)) ↔ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ (𝑁 − 1)))) |
136 | 134, 135 | sylibr 236 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ (𝑀...(𝑁 − 1))) |
137 | | simpr 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝑘 ∈ (𝑀...(𝑁 − 1))) |
138 | | fzoval 13033 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
139 | 22, 138 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
140 | 139 | eqcomd 2827 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀...(𝑁 − 1)) = (𝑀..^𝑁)) |
141 | 140 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝑀...(𝑁 − 1)) = (𝑀..^𝑁)) |
142 | 137, 141 | eleqtrd 2915 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝑘 ∈ (𝑀..^𝑁)) |
143 | | fzofzp1 13128 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
144 | 142, 143 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
145 | | simpl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝜑) |
146 | 145, 144 | jca 514 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁))) |
147 | | eleq1 2900 |
. . . . . . . . 9
⊢ (𝑗 = (𝑘 + 1) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑘 + 1) ∈ (𝑀...𝑁))) |
148 | 147 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)))) |
149 | | fveq2 6665 |
. . . . . . . . 9
⊢ (𝑗 = (𝑘 + 1) → (𝐹‘𝑗) = (𝐹‘(𝑘 + 1))) |
150 | 149 | eleq1d 2897 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → ((𝐹‘𝑗) ∈ ℝ ↔ (𝐹‘(𝑘 + 1)) ∈ ℝ)) |
151 | 148, 150 | imbi12d 347 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ∈ ℝ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℝ))) |
152 | | eleq1 2900 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝑘 ∈ (𝑀...𝑁) ↔ 𝑗 ∈ (𝑀...𝑁))) |
153 | 152 | anbi2d 630 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)))) |
154 | | fveq2 6665 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗)) |
155 | 154 | eleq1d 2897 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑗) ∈ ℝ)) |
156 | 153, 155 | imbi12d 347 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ∈ ℝ))) |
157 | 156, 8 | chvarvv 2001 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ∈ ℝ) |
158 | 151, 157 | vtoclg 3568 |
. . . . . 6
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℝ)) |
159 | 144, 146,
158 | sylc 65 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ∈ ℝ) |
160 | 136, 159 | syldan 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘(𝑘 + 1)) ∈ ℝ) |
161 | 142, 59 | syldan 593 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) |
162 | 136, 161 | syldan 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) |
163 | 125, 160,
162 | ltled 10782 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) |
164 | 67, 94, 163 | monoord 13394 |
. 2
⊢ (𝜑 → (𝐹‘(𝐼 + 1)) ≤ (𝐹‘𝐽)) |
165 | 10, 44, 52, 61, 164 | ltletrd 10794 |
1
⊢ (𝜑 → (𝐹‘𝐼) < (𝐹‘𝐽)) |