| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | monoords.i | . . 3
⊢ (𝜑 → 𝐼 ∈ (𝑀...𝑁)) | 
| 2 | 1 | ancli 548 | . . 3
⊢ (𝜑 → (𝜑 ∧ 𝐼 ∈ (𝑀...𝑁))) | 
| 3 |  | eleq1 2828 | . . . . . 6
⊢ (𝑘 = 𝐼 → (𝑘 ∈ (𝑀...𝑁) ↔ 𝐼 ∈ (𝑀...𝑁))) | 
| 4 | 3 | anbi2d 630 | . . . . 5
⊢ (𝑘 = 𝐼 → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝐼 ∈ (𝑀...𝑁)))) | 
| 5 |  | fveq2 6905 | . . . . . 6
⊢ (𝑘 = 𝐼 → (𝐹‘𝑘) = (𝐹‘𝐼)) | 
| 6 | 5 | eleq1d 2825 | . . . . 5
⊢ (𝑘 = 𝐼 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝐼) ∈ ℝ)) | 
| 7 | 4, 6 | imbi12d 344 | . . . 4
⊢ (𝑘 = 𝐼 → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ 𝐼 ∈ (𝑀...𝑁)) → (𝐹‘𝐼) ∈ ℝ))) | 
| 8 |  | monoords.fk | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) | 
| 9 | 7, 8 | vtoclg 3553 | . . 3
⊢ (𝐼 ∈ (𝑀...𝑁) → ((𝜑 ∧ 𝐼 ∈ (𝑀...𝑁)) → (𝐹‘𝐼) ∈ ℝ)) | 
| 10 | 1, 2, 9 | sylc 65 | . 2
⊢ (𝜑 → (𝐹‘𝐼) ∈ ℝ) | 
| 11 |  | elfzel1 13564 | . . . . . . 7
⊢ (𝐼 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ) | 
| 12 | 1, 11 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 13 | 1 | elfzelzd 13566 | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℤ) | 
| 14 |  | elfzle1 13568 | . . . . . . 7
⊢ (𝐼 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐼) | 
| 15 | 1, 14 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑀 ≤ 𝐼) | 
| 16 |  | eluz2 12885 | . . . . . 6
⊢ (𝐼 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼)) | 
| 17 | 12, 13, 15, 16 | syl3anbrc 1343 | . . . . 5
⊢ (𝜑 → 𝐼 ∈ (ℤ≥‘𝑀)) | 
| 18 |  | elfzuz2 13570 | . . . . . . 7
⊢ (𝐼 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 19 | 1, 18 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 20 |  | eluzelz 12889 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) | 
| 21 | 19, 20 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 22 | 13 | zred 12724 | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℝ) | 
| 23 |  | monoords.j | . . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (𝑀...𝑁)) | 
| 24 | 23 | elfzelzd 13566 | . . . . . . 7
⊢ (𝜑 → 𝐽 ∈ ℤ) | 
| 25 | 24 | zred 12724 | . . . . . 6
⊢ (𝜑 → 𝐽 ∈ ℝ) | 
| 26 | 21 | zred 12724 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 27 |  | monoords.iltj | . . . . . 6
⊢ (𝜑 → 𝐼 < 𝐽) | 
| 28 |  | elfzle2 13569 | . . . . . . 7
⊢ (𝐽 ∈ (𝑀...𝑁) → 𝐽 ≤ 𝑁) | 
| 29 | 23, 28 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐽 ≤ 𝑁) | 
| 30 | 22, 25, 26, 27, 29 | ltletrd 11422 | . . . . 5
⊢ (𝜑 → 𝐼 < 𝑁) | 
| 31 |  | elfzo2 13703 | . . . . 5
⊢ (𝐼 ∈ (𝑀..^𝑁) ↔ (𝐼 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝐼 < 𝑁)) | 
| 32 | 17, 21, 30, 31 | syl3anbrc 1343 | . . . 4
⊢ (𝜑 → 𝐼 ∈ (𝑀..^𝑁)) | 
| 33 |  | fzofzp1 13804 | . . . 4
⊢ (𝐼 ∈ (𝑀..^𝑁) → (𝐼 + 1) ∈ (𝑀...𝑁)) | 
| 34 | 32, 33 | syl 17 | . . 3
⊢ (𝜑 → (𝐼 + 1) ∈ (𝑀...𝑁)) | 
| 35 | 34 | ancli 548 | . . 3
⊢ (𝜑 → (𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁))) | 
| 36 |  | eleq1 2828 | . . . . . 6
⊢ (𝑘 = (𝐼 + 1) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝐼 + 1) ∈ (𝑀...𝑁))) | 
| 37 | 36 | anbi2d 630 | . . . . 5
⊢ (𝑘 = (𝐼 + 1) → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁)))) | 
| 38 |  | fveq2 6905 | . . . . . 6
⊢ (𝑘 = (𝐼 + 1) → (𝐹‘𝑘) = (𝐹‘(𝐼 + 1))) | 
| 39 | 38 | eleq1d 2825 | . . . . 5
⊢ (𝑘 = (𝐼 + 1) → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘(𝐼 + 1)) ∈ ℝ)) | 
| 40 | 37, 39 | imbi12d 344 | . . . 4
⊢ (𝑘 = (𝐼 + 1) → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝐼 + 1)) ∈ ℝ))) | 
| 41 | 40, 8 | vtoclg 3553 | . . 3
⊢ ((𝐼 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝐼 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝐼 + 1)) ∈ ℝ)) | 
| 42 | 34, 35, 41 | sylc 65 | . 2
⊢ (𝜑 → (𝐹‘(𝐼 + 1)) ∈ ℝ) | 
| 43 | 23 | ancli 548 | . . 3
⊢ (𝜑 → (𝜑 ∧ 𝐽 ∈ (𝑀...𝑁))) | 
| 44 |  | eleq1 2828 | . . . . . 6
⊢ (𝑘 = 𝐽 → (𝑘 ∈ (𝑀...𝑁) ↔ 𝐽 ∈ (𝑀...𝑁))) | 
| 45 | 44 | anbi2d 630 | . . . . 5
⊢ (𝑘 = 𝐽 → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)))) | 
| 46 |  | fveq2 6905 | . . . . . 6
⊢ (𝑘 = 𝐽 → (𝐹‘𝑘) = (𝐹‘𝐽)) | 
| 47 | 46 | eleq1d 2825 | . . . . 5
⊢ (𝑘 = 𝐽 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝐽) ∈ ℝ)) | 
| 48 | 45, 47 | imbi12d 344 | . . . 4
⊢ (𝑘 = 𝐽 → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝐹‘𝐽) ∈ ℝ))) | 
| 49 | 48, 8 | vtoclg 3553 | . . 3
⊢ (𝐽 ∈ (𝑀...𝑁) → ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝐹‘𝐽) ∈ ℝ)) | 
| 50 | 23, 43, 49 | sylc 65 | . 2
⊢ (𝜑 → (𝐹‘𝐽) ∈ ℝ) | 
| 51 | 32 | ancli 548 | . . 3
⊢ (𝜑 → (𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁))) | 
| 52 |  | eleq1 2828 | . . . . . 6
⊢ (𝑘 = 𝐼 → (𝑘 ∈ (𝑀..^𝑁) ↔ 𝐼 ∈ (𝑀..^𝑁))) | 
| 53 | 52 | anbi2d 630 | . . . . 5
⊢ (𝑘 = 𝐼 → ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁)))) | 
| 54 |  | fvoveq1 7455 | . . . . . 6
⊢ (𝑘 = 𝐼 → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝐼 + 1))) | 
| 55 | 5, 54 | breq12d 5155 | . . . . 5
⊢ (𝑘 = 𝐼 → ((𝐹‘𝑘) < (𝐹‘(𝑘 + 1)) ↔ (𝐹‘𝐼) < (𝐹‘(𝐼 + 1)))) | 
| 56 | 53, 55 | imbi12d 344 | . . . 4
⊢ (𝑘 = 𝐼 → (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) ↔ ((𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁)) → (𝐹‘𝐼) < (𝐹‘(𝐼 + 1))))) | 
| 57 |  | monoords.flt | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) | 
| 58 | 56, 57 | vtoclg 3553 | . . 3
⊢ (𝐼 ∈ (𝑀..^𝑁) → ((𝜑 ∧ 𝐼 ∈ (𝑀..^𝑁)) → (𝐹‘𝐼) < (𝐹‘(𝐼 + 1)))) | 
| 59 | 32, 51, 58 | sylc 65 | . 2
⊢ (𝜑 → (𝐹‘𝐼) < (𝐹‘(𝐼 + 1))) | 
| 60 | 13 | peano2zd 12727 | . . . 4
⊢ (𝜑 → (𝐼 + 1) ∈ ℤ) | 
| 61 |  | zltp1le 12669 | . . . . . 6
⊢ ((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (𝐼 < 𝐽 ↔ (𝐼 + 1) ≤ 𝐽)) | 
| 62 | 13, 24, 61 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝐼 < 𝐽 ↔ (𝐼 + 1) ≤ 𝐽)) | 
| 63 | 27, 62 | mpbid 232 | . . . 4
⊢ (𝜑 → (𝐼 + 1) ≤ 𝐽) | 
| 64 |  | eluz2 12885 | . . . 4
⊢ (𝐽 ∈
(ℤ≥‘(𝐼 + 1)) ↔ ((𝐼 + 1) ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐼 + 1) ≤ 𝐽)) | 
| 65 | 60, 24, 63, 64 | syl3anbrc 1343 | . . 3
⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘(𝐼 + 1))) | 
| 66 | 12 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ∈ ℤ) | 
| 67 | 21 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑁 ∈ ℤ) | 
| 68 |  | elfzelz 13565 | . . . . . 6
⊢ (𝑘 ∈ ((𝐼 + 1)...𝐽) → 𝑘 ∈ ℤ) | 
| 69 | 68 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ∈ ℤ) | 
| 70 | 66 | zred 12724 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ∈ ℝ) | 
| 71 | 69 | zred 12724 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ∈ ℝ) | 
| 72 | 60 | zred 12724 | . . . . . . . 8
⊢ (𝜑 → (𝐼 + 1) ∈ ℝ) | 
| 73 | 72 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → (𝐼 + 1) ∈ ℝ) | 
| 74 | 22 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐼 ∈ ℝ) | 
| 75 | 15 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ≤ 𝐼) | 
| 76 | 74 | ltp1d 12199 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐼 < (𝐼 + 1)) | 
| 77 | 70, 74, 73, 75, 76 | lelttrd 11420 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 < (𝐼 + 1)) | 
| 78 |  | elfzle1 13568 | . . . . . . . 8
⊢ (𝑘 ∈ ((𝐼 + 1)...𝐽) → (𝐼 + 1) ≤ 𝑘) | 
| 79 | 78 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → (𝐼 + 1) ≤ 𝑘) | 
| 80 | 70, 73, 71, 77, 79 | ltletrd 11422 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 < 𝑘) | 
| 81 | 70, 71, 80 | ltled 11410 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑀 ≤ 𝑘) | 
| 82 | 25 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐽 ∈ ℝ) | 
| 83 | 67 | zred 12724 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑁 ∈ ℝ) | 
| 84 |  | elfzle2 13569 | . . . . . . 7
⊢ (𝑘 ∈ ((𝐼 + 1)...𝐽) → 𝑘 ≤ 𝐽) | 
| 85 | 84 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ≤ 𝐽) | 
| 86 | 29 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝐽 ≤ 𝑁) | 
| 87 | 71, 82, 83, 85, 86 | letrd 11419 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ≤ 𝑁) | 
| 88 | 66, 67, 69, 81, 87 | elfzd 13556 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → 𝑘 ∈ (𝑀...𝑁)) | 
| 89 | 88, 8 | syldan 591 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...𝐽)) → (𝐹‘𝑘) ∈ ℝ) | 
| 90 | 12 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 ∈ ℤ) | 
| 91 | 21 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑁 ∈ ℤ) | 
| 92 |  | elfzelz 13565 | . . . . . . 7
⊢ (𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1)) → 𝑘 ∈ ℤ) | 
| 93 | 92 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ ℤ) | 
| 94 | 90 | zred 12724 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 ∈ ℝ) | 
| 95 | 93 | zred 12724 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ ℝ) | 
| 96 | 72 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐼 + 1) ∈ ℝ) | 
| 97 | 12 | zred 12724 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 98 | 22 | ltp1d 12199 | . . . . . . . . . 10
⊢ (𝜑 → 𝐼 < (𝐼 + 1)) | 
| 99 | 97, 22, 72, 15, 98 | lelttrd 11420 | . . . . . . . . 9
⊢ (𝜑 → 𝑀 < (𝐼 + 1)) | 
| 100 | 99 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 < (𝐼 + 1)) | 
| 101 |  | elfzle1 13568 | . . . . . . . . 9
⊢ (𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1)) → (𝐼 + 1) ≤ 𝑘) | 
| 102 | 101 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐼 + 1) ≤ 𝑘) | 
| 103 | 94, 96, 95, 100, 102 | ltletrd 11422 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 < 𝑘) | 
| 104 | 94, 95, 103 | ltled 11410 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑀 ≤ 𝑘) | 
| 105 | 91 | zred 12724 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑁 ∈ ℝ) | 
| 106 |  | peano2rem 11577 | . . . . . . . . . 10
⊢ (𝐽 ∈ ℝ → (𝐽 − 1) ∈
ℝ) | 
| 107 | 25, 106 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝐽 − 1) ∈ ℝ) | 
| 108 | 107 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) ∈ ℝ) | 
| 109 |  | elfzle2 13569 | . . . . . . . . 9
⊢ (𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1)) → 𝑘 ≤ (𝐽 − 1)) | 
| 110 | 109 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ≤ (𝐽 − 1)) | 
| 111 | 25 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝐽 ∈ ℝ) | 
| 112 | 111 | ltm1d 12201 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) < 𝐽) | 
| 113 | 29 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝐽 ≤ 𝑁) | 
| 114 | 108, 111,
105, 112, 113 | ltletrd 11422 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) < 𝑁) | 
| 115 | 95, 108, 105, 110, 114 | lelttrd 11420 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 < 𝑁) | 
| 116 | 95, 105, 115 | ltled 11410 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ≤ 𝑁) | 
| 117 | 90, 91, 93, 104, 116 | elfzd 13556 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ (𝑀...𝑁)) | 
| 118 | 117, 8 | syldan 591 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘𝑘) ∈ ℝ) | 
| 119 |  | peano2zm 12662 | . . . . . . 7
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) | 
| 120 | 91, 119 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝑁 − 1) ∈ ℤ) | 
| 121 | 120 | zred 12724 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝑁 − 1) ∈ ℝ) | 
| 122 |  | 1red 11263 | . . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ) | 
| 123 | 25, 26, 122, 29 | lesub1dd 11880 | . . . . . . . 8
⊢ (𝜑 → (𝐽 − 1) ≤ (𝑁 − 1)) | 
| 124 | 123 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐽 − 1) ≤ (𝑁 − 1)) | 
| 125 | 95, 108, 121, 110, 124 | letrd 11419 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ≤ (𝑁 − 1)) | 
| 126 | 90, 120, 93, 104, 125 | elfzd 13556 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → 𝑘 ∈ (𝑀...(𝑁 − 1))) | 
| 127 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝑘 ∈ (𝑀...(𝑁 − 1))) | 
| 128 |  | fzoval 13701 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) | 
| 129 | 21, 128 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) | 
| 130 | 129 | eqcomd 2742 | . . . . . . . . 9
⊢ (𝜑 → (𝑀...(𝑁 − 1)) = (𝑀..^𝑁)) | 
| 131 | 130 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝑀...(𝑁 − 1)) = (𝑀..^𝑁)) | 
| 132 | 127, 131 | eleqtrd 2842 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝑘 ∈ (𝑀..^𝑁)) | 
| 133 |  | fzofzp1 13804 | . . . . . . 7
⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁)) | 
| 134 | 132, 133 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝑘 + 1) ∈ (𝑀...𝑁)) | 
| 135 |  | simpl 482 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝜑) | 
| 136 | 135, 134 | jca 511 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁))) | 
| 137 |  | eleq1 2828 | . . . . . . . . 9
⊢ (𝑗 = (𝑘 + 1) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑘 + 1) ∈ (𝑀...𝑁))) | 
| 138 | 137 | anbi2d 630 | . . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)))) | 
| 139 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑗 = (𝑘 + 1) → (𝐹‘𝑗) = (𝐹‘(𝑘 + 1))) | 
| 140 | 139 | eleq1d 2825 | . . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → ((𝐹‘𝑗) ∈ ℝ ↔ (𝐹‘(𝑘 + 1)) ∈ ℝ)) | 
| 141 | 138, 140 | imbi12d 344 | . . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ∈ ℝ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℝ))) | 
| 142 |  | eleq1 2828 | . . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝑘 ∈ (𝑀...𝑁) ↔ 𝑗 ∈ (𝑀...𝑁))) | 
| 143 | 142 | anbi2d 630 | . . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)))) | 
| 144 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗)) | 
| 145 | 144 | eleq1d 2825 | . . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) ∈ ℝ ↔ (𝐹‘𝑗) ∈ ℝ)) | 
| 146 | 143, 145 | imbi12d 344 | . . . . . . . 8
⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ∈ ℝ))) | 
| 147 | 146, 8 | chvarvv 1997 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ∈ ℝ) | 
| 148 | 141, 147 | vtoclg 3553 | . . . . . 6
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℝ)) | 
| 149 | 134, 136,
148 | sylc 65 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘(𝑘 + 1)) ∈ ℝ) | 
| 150 | 126, 149 | syldan 591 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘(𝑘 + 1)) ∈ ℝ) | 
| 151 | 132, 57 | syldan 591 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) | 
| 152 | 126, 151 | syldan 591 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) | 
| 153 | 118, 150,
152 | ltled 11410 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐼 + 1)...(𝐽 − 1))) → (𝐹‘𝑘) ≤ (𝐹‘(𝑘 + 1))) | 
| 154 | 65, 89, 153 | monoord 14074 | . 2
⊢ (𝜑 → (𝐹‘(𝐼 + 1)) ≤ (𝐹‘𝐽)) | 
| 155 | 10, 42, 50, 59, 154 | ltletrd 11422 | 1
⊢ (𝜑 → (𝐹‘𝐼) < (𝐹‘𝐽)) |