| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | iblspltprt.2 | . . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 2 | 1 | peano2zd 12727 | . . 3
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) | 
| 3 |  | iblspltprt.3 | . . . 4
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) | 
| 4 |  | eluzelz 12889 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑁 ∈ ℤ) | 
| 5 | 3, 4 | syl 17 | . . 3
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 6 |  | eluzle 12892 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑀 + 1) ≤ 𝑁) | 
| 7 | 3, 6 | syl 17 | . . 3
⊢ (𝜑 → (𝑀 + 1) ≤ 𝑁) | 
| 8 | 5 | zred 12724 | . . . 4
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 9 | 8 | leidd 11830 | . . 3
⊢ (𝜑 → 𝑁 ≤ 𝑁) | 
| 10 | 2, 5, 5, 7, 9 | elfzd 13556 | . 2
⊢ (𝜑 → 𝑁 ∈ ((𝑀 + 1)...𝑁)) | 
| 11 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑗 = (𝑀 + 1) → (𝑃‘𝑗) = (𝑃‘(𝑀 + 1))) | 
| 12 | 11 | oveq2d 7448 | . . . . . 6
⊢ (𝑗 = (𝑀 + 1) → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) | 
| 13 | 12 | mpteq1d 5236 | . . . . 5
⊢ (𝑗 = (𝑀 + 1) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴)) | 
| 14 | 13 | eleq1d 2825 | . . . 4
⊢ (𝑗 = (𝑀 + 1) → ((𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1)) | 
| 15 | 14 | imbi2d 340 | . . 3
⊢ (𝑗 = (𝑀 + 1) → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1) ↔
(𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1))) | 
| 16 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑃‘𝑗) = (𝑃‘𝑘)) | 
| 17 | 16 | oveq2d 7448 | . . . . . 6
⊢ (𝑗 = 𝑘 → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘𝑘))) | 
| 18 | 17 | mpteq1d 5236 | . . . . 5
⊢ (𝑗 = 𝑘 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴)) | 
| 19 | 18 | eleq1d 2825 | . . . 4
⊢ (𝑗 = 𝑘 → ((𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈
𝐿1)) | 
| 20 | 19 | imbi2d 340 | . . 3
⊢ (𝑗 = 𝑘 → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1) ↔
(𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈
𝐿1))) | 
| 21 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (𝑃‘𝑗) = (𝑃‘(𝑘 + 1))) | 
| 22 | 21 | oveq2d 7448 | . . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) | 
| 23 | 22 | mpteq1d 5236 | . . . . 5
⊢ (𝑗 = (𝑘 + 1) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴)) | 
| 24 | 23 | eleq1d 2825 | . . . 4
⊢ (𝑗 = (𝑘 + 1) → ((𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1)) | 
| 25 | 24 | imbi2d 340 | . . 3
⊢ (𝑗 = (𝑘 + 1) → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1) ↔
(𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1))) | 
| 26 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑗 = 𝑁 → (𝑃‘𝑗) = (𝑃‘𝑁)) | 
| 27 | 26 | oveq2d 7448 | . . . . . 6
⊢ (𝑗 = 𝑁 → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘𝑁))) | 
| 28 | 27 | mpteq1d 5236 | . . . . 5
⊢ (𝑗 = 𝑁 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴)) | 
| 29 | 28 | eleq1d 2825 | . . . 4
⊢ (𝑗 = 𝑁 → ((𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴) ∈
𝐿1)) | 
| 30 | 29 | imbi2d 340 | . . 3
⊢ (𝑗 = 𝑁 → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1) ↔
(𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴) ∈
𝐿1))) | 
| 31 |  | uzid 12894 | . . . . . . 7
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) | 
| 32 | 1, 31 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) | 
| 33 | 1 | zred 12724 | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 34 |  | 1red 11263 | . . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) | 
| 35 | 33, 34 | readdcld 11291 | . . . . . . 7
⊢ (𝜑 → (𝑀 + 1) ∈ ℝ) | 
| 36 | 33 | ltp1d 12199 | . . . . . . 7
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) | 
| 37 | 33, 35, 8, 36, 7 | ltletrd 11422 | . . . . . 6
⊢ (𝜑 → 𝑀 < 𝑁) | 
| 38 |  | elfzo2 13703 | . . . . . 6
⊢ (𝑀 ∈ (𝑀..^𝑁) ↔ (𝑀 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁)) | 
| 39 | 32, 5, 37, 38 | syl3anbrc 1343 | . . . . 5
⊢ (𝜑 → 𝑀 ∈ (𝑀..^𝑁)) | 
| 40 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑖 = 𝑀 → (𝑃‘𝑖) = (𝑃‘𝑀)) | 
| 41 |  | fvoveq1 7455 | . . . . . . . . . 10
⊢ (𝑖 = 𝑀 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑀 + 1))) | 
| 42 | 40, 41 | oveq12d 7450 | . . . . . . . . 9
⊢ (𝑖 = 𝑀 → ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) | 
| 43 | 42 | mpteq1d 5236 | . . . . . . . 8
⊢ (𝑖 = 𝑀 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴)) | 
| 44 | 43 | eleq1d 2825 | . . . . . . 7
⊢ (𝑖 = 𝑀 → ((𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1)) | 
| 45 | 44 | imbi2d 340 | . . . . . 6
⊢ (𝑖 = 𝑀 → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔
(𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1))) | 
| 46 |  | iblspltprt.7 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈
𝐿1) | 
| 47 | 46 | expcom 413 | . . . . . 6
⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈
𝐿1)) | 
| 48 | 45, 47 | vtoclga 3576 | . . . . 5
⊢ (𝑀 ∈ (𝑀..^𝑁) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1)) | 
| 49 | 39, 48 | mpcom 38 | . . . 4
⊢ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1) | 
| 50 | 49 | a1i 11 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1)) | 
| 51 |  | nfv 1913 | . . . . . 6
⊢
Ⅎ𝑡 𝑘 ∈ ((𝑀 + 1)..^𝑁) | 
| 52 |  | iblspltprt.1 | . . . . . . 7
⊢
Ⅎ𝑡𝜑 | 
| 53 |  | nfmpt1 5249 | . . . . . . . 8
⊢
Ⅎ𝑡(𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) | 
| 54 | 53 | nfel1 2921 | . . . . . . 7
⊢
Ⅎ𝑡(𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈
𝐿1 | 
| 55 | 52, 54 | nfim 1895 | . . . . . 6
⊢
Ⅎ𝑡(𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈
𝐿1) | 
| 56 | 51, 55, 52 | nf3an 1900 | . . . . 5
⊢
Ⅎ𝑡(𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) | 
| 57 |  | simp3 1138 | . . . . . 6
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → 𝜑) | 
| 58 |  | simp1 1136 | . . . . . 6
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → 𝑘 ∈ ((𝑀 + 1)..^𝑁)) | 
| 59 | 33 | leidd 11830 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ≤ 𝑀) | 
| 60 | 33, 8, 37 | ltled 11410 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ≤ 𝑁) | 
| 61 | 1, 5, 1, 59, 60 | elfzd 13556 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) | 
| 62 | 61 | ancli 548 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝜑 ∧ 𝑀 ∈ (𝑀...𝑁))) | 
| 63 |  | eleq1 2828 | . . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑀 → (𝑖 ∈ (𝑀...𝑁) ↔ 𝑀 ∈ (𝑀...𝑁))) | 
| 64 | 63 | anbi2d 630 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑀 → ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑀 ∈ (𝑀...𝑁)))) | 
| 65 | 40 | eleq1d 2825 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑀 → ((𝑃‘𝑖) ∈ ℝ ↔ (𝑃‘𝑀) ∈ ℝ)) | 
| 66 | 64, 65 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑀 → (((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ 𝑀 ∈ (𝑀...𝑁)) → (𝑃‘𝑀) ∈ ℝ))) | 
| 67 |  | iblspltprt.4 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ) | 
| 68 | 66, 67 | vtoclg 3553 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ (𝑀...𝑁) → ((𝜑 ∧ 𝑀 ∈ (𝑀...𝑁)) → (𝑃‘𝑀) ∈ ℝ)) | 
| 69 | 61, 62, 68 | sylc 65 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑃‘𝑀) ∈ ℝ) | 
| 70 | 69 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ∈ ℝ) | 
| 71 | 70 | rexrd 11312 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ∈
ℝ*) | 
| 72 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝜑) | 
| 73 |  | elfzoelz 13700 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℤ) | 
| 74 | 73 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℤ) | 
| 75 | 33 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℝ) | 
| 76 | 74 | zred 12724 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℝ) | 
| 77 | 35 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ∈ ℝ) | 
| 78 | 36 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑀 + 1)) | 
| 79 |  | elfzole1 13708 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑀 + 1) ≤ 𝑘) | 
| 80 | 79 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ≤ 𝑘) | 
| 81 | 75, 77, 76, 78, 80 | ltletrd 11422 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < 𝑘) | 
| 82 | 75, 76, 81 | ltled 11410 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ 𝑘) | 
| 83 | 8 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℝ) | 
| 84 |  | elfzolt2 13709 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 < 𝑁) | 
| 85 | 84 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < 𝑁) | 
| 86 | 76, 83, 85 | ltled 11410 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ≤ 𝑁) | 
| 87 | 1, 5 | jca 511 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) | 
| 88 | 87 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) | 
| 89 |  | elfz1 13553 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) | 
| 90 | 88, 89 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) | 
| 91 | 74, 82, 86, 90 | mpbir3and 1342 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀...𝑁)) | 
| 92 |  | eleq1 2828 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (𝑖 ∈ (𝑀...𝑁) ↔ 𝑘 ∈ (𝑀...𝑁))) | 
| 93 | 92 | anbi2d 630 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)))) | 
| 94 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (𝑃‘𝑖) = (𝑃‘𝑘)) | 
| 95 | 94 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → ((𝑃‘𝑖) ∈ ℝ ↔ (𝑃‘𝑘) ∈ ℝ)) | 
| 96 | 93, 95 | imbi12d 344 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑃‘𝑘) ∈ ℝ))) | 
| 97 | 96, 67 | chvarvv 1997 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑃‘𝑘) ∈ ℝ) | 
| 98 | 72, 91, 97 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈ ℝ) | 
| 99 | 98 | rexrd 11312 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈
ℝ*) | 
| 100 | 74 | peano2zd 12727 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℤ) | 
| 101 | 100 | zred 12724 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℝ) | 
| 102 |  | 1red 11263 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 1 ∈ ℝ) | 
| 103 | 75, 76, 102, 81 | ltadd1dd 11875 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) < (𝑘 + 1)) | 
| 104 | 75, 77, 101, 78, 103 | lttrd 11423 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑘 + 1)) | 
| 105 | 75, 101, 104 | ltled 11410 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ (𝑘 + 1)) | 
| 106 |  | zltp1le 12669 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁)) | 
| 107 | 73, 5, 106 | syl2anr 597 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁)) | 
| 108 | 85, 107 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ≤ 𝑁) | 
| 109 |  | elfz1 13553 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁))) | 
| 110 | 88, 109 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁))) | 
| 111 | 100, 105,
108, 110 | mpbir3and 1342 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁)) | 
| 112 | 72, 111 | jca 511 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁))) | 
| 113 |  | eleq1 2828 | . . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑘 + 1) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑘 + 1) ∈ (𝑀...𝑁))) | 
| 114 | 113 | anbi2d 630 | . . . . . . . . . . . . 13
⊢ (𝑖 = (𝑘 + 1) → ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)))) | 
| 115 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑘 + 1) → (𝑃‘𝑖) = (𝑃‘(𝑘 + 1))) | 
| 116 | 115 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑖 = (𝑘 + 1) → ((𝑃‘𝑖) ∈ ℝ ↔ (𝑃‘(𝑘 + 1)) ∈ ℝ)) | 
| 117 | 114, 116 | imbi12d 344 | . . . . . . . . . . . 12
⊢ (𝑖 = (𝑘 + 1) → (((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ))) | 
| 118 | 117, 67 | vtoclg 3553 | . . . . . . . . . . 11
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ)) | 
| 119 | 111, 112,
118 | sylc 65 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ) | 
| 120 | 119 | rexrd 11312 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈
ℝ*) | 
| 121 |  | eluz 12893 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈
(ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑘)) | 
| 122 | 1, 73, 121 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑘)) | 
| 123 | 82, 122 | mpbird 257 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ≥‘𝑀)) | 
| 124 |  | simpll 766 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝜑) | 
| 125 |  | elfzelz 13565 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℤ) | 
| 126 | 125 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℤ) | 
| 127 |  | elfzle1 13568 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑀 ≤ 𝑖) | 
| 128 | 127 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ≤ 𝑖) | 
| 129 | 126 | zred 12724 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ) | 
| 130 | 124, 8 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℝ) | 
| 131 | 76 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 ∈ ℝ) | 
| 132 |  | elfzle2 13569 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑖 ≤ 𝑘) | 
| 133 | 132 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ≤ 𝑘) | 
| 134 | 85 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 < 𝑁) | 
| 135 | 129, 131,
130, 133, 134 | lelttrd 11420 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 < 𝑁) | 
| 136 | 129, 130,
135 | ltled 11410 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ≤ 𝑁) | 
| 137 |  | elfz1 13553 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) | 
| 138 | 124, 87, 137 | 3syl 18 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) | 
| 139 | 126, 128,
136, 138 | mpbir3and 1342 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀...𝑁)) | 
| 140 | 124, 139,
67 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃‘𝑖) ∈ ℝ) | 
| 141 |  | simpll 766 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝜑) | 
| 142 |  | elfzelz 13565 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ ℤ) | 
| 143 | 142 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℤ) | 
| 144 |  | elfzle1 13568 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ≤ 𝑖) | 
| 145 | 144 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ 𝑖) | 
| 146 | 143 | zred 12724 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℝ) | 
| 147 | 141, 8 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℝ) | 
| 148 | 76 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 ∈ ℝ) | 
| 149 |  | 1red 11263 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 1 ∈
ℝ) | 
| 150 | 148, 149 | resubcld 11692 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) ∈ ℝ) | 
| 151 |  | elfzle2 13569 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ≤ (𝑘 − 1)) | 
| 152 | 151 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ (𝑘 − 1)) | 
| 153 | 73 | zred 12724 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℝ) | 
| 154 |  | 1red 11263 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 1 ∈ ℝ) | 
| 155 | 153, 154 | resubcld 11692 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 − 1) ∈ ℝ) | 
| 156 |  | elfzoel2 13699 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ ℤ) | 
| 157 | 156 | zred 12724 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ ℝ) | 
| 158 | 153 | ltm1d 12201 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 − 1) < 𝑘) | 
| 159 | 155, 153,
157, 158, 84 | lttrd 11423 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 − 1) < 𝑁) | 
| 160 | 159 | ad2antlr 727 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) < 𝑁) | 
| 161 | 146, 150,
147, 152, 160 | lelttrd 11420 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑁) | 
| 162 | 146, 147,
161 | ltled 11410 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ 𝑁) | 
| 163 | 141, 87, 137 | 3syl 18 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) | 
| 164 | 143, 145,
162, 163 | mpbir3and 1342 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀...𝑁)) | 
| 165 | 141, 164,
67 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) ∈ ℝ) | 
| 166 | 143 | peano2zd 12727 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℤ) | 
| 167 |  | elfzel1 13564 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ∈ ℤ) | 
| 168 | 167 | zred 12724 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ∈ ℝ) | 
| 169 | 142 | zred 12724 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ ℝ) | 
| 170 |  | 1red 11263 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 1 ∈
ℝ) | 
| 171 | 169, 170 | readdcld 11291 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → (𝑖 + 1) ∈ ℝ) | 
| 172 | 169 | ltp1d 12199 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 < (𝑖 + 1)) | 
| 173 | 168, 169,
171, 144, 172 | lelttrd 11420 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 < (𝑖 + 1)) | 
| 174 | 168, 171,
173 | ltled 11410 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ≤ (𝑖 + 1)) | 
| 175 | 174 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ (𝑖 + 1)) | 
| 176 | 141, 3, 4 | 3syl 18 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℤ) | 
| 177 |  | zltp1le 12669 | . . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) | 
| 178 | 143, 176,
177 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) | 
| 179 | 161, 178 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑁) | 
| 180 |  | elfz1 13553 | . . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁))) | 
| 181 | 141, 87, 180 | 3syl 18 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁))) | 
| 182 | 166, 175,
179, 181 | mpbir3and 1342 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁)) | 
| 183 | 141, 182 | jca 511 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁))) | 
| 184 |  | eleq1 2828 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑖 + 1) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑖 + 1) ∈ (𝑀...𝑁))) | 
| 185 | 184 | anbi2d 630 | . . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑖 + 1) → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁)))) | 
| 186 |  | fveq2 6905 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑖 + 1) → (𝑃‘𝑘) = (𝑃‘(𝑖 + 1))) | 
| 187 | 186 | eleq1d 2825 | . . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑖 + 1) → ((𝑃‘𝑘) ∈ ℝ ↔ (𝑃‘(𝑖 + 1)) ∈ ℝ)) | 
| 188 | 185, 187 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑘 = (𝑖 + 1) → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑃‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑖 + 1)) ∈ ℝ))) | 
| 189 | 188, 97 | vtoclg 3553 | . . . . . . . . . . . 12
⊢ ((𝑖 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑖 + 1)) ∈ ℝ)) | 
| 190 | 182, 183,
189 | sylc 65 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ) | 
| 191 |  | elfzuz 13561 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ (ℤ≥‘𝑀)) | 
| 192 | 191 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀)) | 
| 193 |  | elfzo2 13703 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ (𝑀..^𝑁) ↔ (𝑖 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑖 < 𝑁)) | 
| 194 | 192, 176,
161, 193 | syl3anbrc 1343 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀..^𝑁)) | 
| 195 |  | iblspltprt.5 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) | 
| 196 | 141, 194,
195 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) | 
| 197 | 165, 190,
196 | ltled 11410 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1))) | 
| 198 | 123, 140,
197 | monoord 14074 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ≤ (𝑃‘𝑘)) | 
| 199 | 156 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℤ) | 
| 200 |  | elfzo2 13703 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀..^𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑘 < 𝑁)) | 
| 201 | 123, 199,
85, 200 | syl3anbrc 1343 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀..^𝑁)) | 
| 202 |  | eleq1 2828 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑘 ∈ (𝑀..^𝑁))) | 
| 203 | 202 | anbi2d 630 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)))) | 
| 204 |  | fvoveq1 7455 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑘 + 1))) | 
| 205 | 94, 204 | breq12d 5155 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → ((𝑃‘𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃‘𝑘) < (𝑃‘(𝑘 + 1)))) | 
| 206 | 203, 205 | imbi12d 344 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1))))) | 
| 207 | 206, 195 | chvarvv 1997 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1))) | 
| 208 | 72, 201, 207 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1))) | 
| 209 | 98, 119, 208 | ltled 11410 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ≤ (𝑃‘(𝑘 + 1))) | 
| 210 |  | iccintsng 45541 | . . . . . . . . 9
⊢ ((((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑘) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*) ∧
((𝑃‘𝑀) ≤ (𝑃‘𝑘) ∧ (𝑃‘𝑘) ≤ (𝑃‘(𝑘 + 1)))) → (((𝑃‘𝑀)[,](𝑃‘𝑘)) ∩ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))) = {(𝑃‘𝑘)}) | 
| 211 | 71, 99, 120, 198, 209, 210 | syl32anc 1379 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (((𝑃‘𝑀)[,](𝑃‘𝑘)) ∩ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))) = {(𝑃‘𝑘)}) | 
| 212 | 211 | fveq2d 6909 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (vol*‘(((𝑃‘𝑀)[,](𝑃‘𝑘)) ∩ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))) = (vol*‘{(𝑃‘𝑘)})) | 
| 213 |  | ovolsn 25531 | . . . . . . . 8
⊢ ((𝑃‘𝑘) ∈ ℝ → (vol*‘{(𝑃‘𝑘)}) = 0) | 
| 214 | 98, 213 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (vol*‘{(𝑃‘𝑘)}) = 0) | 
| 215 | 212, 214 | eqtrd 2776 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (vol*‘(((𝑃‘𝑀)[,](𝑃‘𝑘)) ∩ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))) = 0) | 
| 216 | 57, 58, 215 | syl2anc 584 | . . . . 5
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (vol*‘(((𝑃‘𝑀)[,](𝑃‘𝑘)) ∩ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))) = 0) | 
| 217 | 70, 119, 98, 198, 209 | eliccd 45522 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) | 
| 218 | 70, 119, 217 | 3jca 1128 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ (𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))))) | 
| 219 | 57, 58, 218 | syl2anc 584 | . . . . . 6
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → ((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ (𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))))) | 
| 220 |  | iccsplit 13526 | . . . . . 6
⊢ (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ (𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) = (((𝑃‘𝑀)[,](𝑃‘𝑘)) ∪ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))) | 
| 221 | 219, 220 | syl 17 | . . . . 5
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) = (((𝑃‘𝑀)[,](𝑃‘𝑘)) ∪ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))) | 
| 222 |  | simpl3 1193 | . . . . . 6
⊢ (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝜑) | 
| 223 |  | simpl1 1191 | . . . . . 6
⊢ (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑘 ∈ ((𝑀 + 1)..^𝑁)) | 
| 224 |  | simpr 484 | . . . . . 6
⊢ (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) | 
| 225 |  | simp1 1136 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝜑) | 
| 226 |  | eliccxr 13476 | . . . . . . . . 9
⊢ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) → 𝑡 ∈ ℝ*) | 
| 227 | 226 | 3ad2ant3 1135 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ*) | 
| 228 | 69 | rexrd 11312 | . . . . . . . . . 10
⊢ (𝜑 → (𝑃‘𝑀) ∈
ℝ*) | 
| 229 | 228 | 3ad2ant1 1133 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ∈
ℝ*) | 
| 230 | 120 | 3adant3 1132 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈
ℝ*) | 
| 231 |  | simp3 1138 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) | 
| 232 |  | iccgelb 13444 | . . . . . . . . 9
⊢ (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ≤ 𝑡) | 
| 233 | 229, 230,
231, 232 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ≤ 𝑡) | 
| 234 | 70, 119 | jca 511 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ)) | 
| 235 | 234 | 3adant3 1132 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → ((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ)) | 
| 236 |  | iccssre 13470 | . . . . . . . . . . 11
⊢ (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ) → ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ⊆ ℝ) | 
| 237 | 236 | sseld 3981 | . . . . . . . . . 10
⊢ (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) → 𝑡 ∈ ℝ)) | 
| 238 | 235, 231,
237 | sylc 65 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ) | 
| 239 | 119 | 3adant3 1132 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ) | 
| 240 | 1, 5, 5, 60, 9 | elfzd 13556 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) | 
| 241 | 240 | ancli 548 | . . . . . . . . . . 11
⊢ (𝜑 → (𝜑 ∧ 𝑁 ∈ (𝑀...𝑁))) | 
| 242 |  | eleq1 2828 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑁 → (𝑖 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁))) | 
| 243 | 242 | anbi2d 630 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑁 → ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑁 ∈ (𝑀...𝑁)))) | 
| 244 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑁 → (𝑃‘𝑖) = (𝑃‘𝑁)) | 
| 245 | 244 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑁 → ((𝑃‘𝑖) ∈ ℝ ↔ (𝑃‘𝑁) ∈ ℝ)) | 
| 246 | 243, 245 | imbi12d 344 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝑁 → (((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ 𝑁 ∈ (𝑀...𝑁)) → (𝑃‘𝑁) ∈ ℝ))) | 
| 247 | 246, 67 | vtoclg 3553 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → ((𝜑 ∧ 𝑁 ∈ (𝑀...𝑁)) → (𝑃‘𝑁) ∈ ℝ)) | 
| 248 | 5, 241, 247 | sylc 65 | . . . . . . . . . 10
⊢ (𝜑 → (𝑃‘𝑁) ∈ ℝ) | 
| 249 | 248 | 3ad2ant1 1133 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑁) ∈ ℝ) | 
| 250 |  | elicc1 13432 | . . . . . . . . . . . 12
⊢ (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*) →
(𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘(𝑘 + 1))))) | 
| 251 | 229, 230,
250 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘(𝑘 + 1))))) | 
| 252 | 231, 251 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘(𝑘 + 1)))) | 
| 253 | 252 | simp3d 1144 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1))) | 
| 254 |  | elfzop1le2 13713 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 + 1) ≤ 𝑁) | 
| 255 | 73 | peano2zd 12727 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 + 1) ∈ ℤ) | 
| 256 |  | eluz 12893 | . . . . . . . . . . . . . 14
⊢ (((𝑘 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘(𝑘 + 1)) ↔ (𝑘 + 1) ≤ 𝑁)) | 
| 257 | 255, 156,
256 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑁 ∈ (ℤ≥‘(𝑘 + 1)) ↔ (𝑘 + 1) ≤ 𝑁)) | 
| 258 | 254, 257 | mpbird 257 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ (ℤ≥‘(𝑘 + 1))) | 
| 259 | 258 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ≥‘(𝑘 + 1))) | 
| 260 |  | simpll 766 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝜑) | 
| 261 |  | elfzelz 13565 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℤ) | 
| 262 | 261 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℤ) | 
| 263 | 260, 33 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℝ) | 
| 264 | 262 | zred 12724 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ) | 
| 265 | 76 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ) | 
| 266 | 81 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑘) | 
| 267 | 153 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ) | 
| 268 |  | 1red 11263 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 1 ∈ ℝ) | 
| 269 | 267, 268 | readdcld 11291 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ∈ ℝ) | 
| 270 | 261 | zred 12724 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℝ) | 
| 271 | 270 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ) | 
| 272 | 267 | ltp1d 12199 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < (𝑘 + 1)) | 
| 273 |  | elfzle1 13568 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → (𝑘 + 1) ≤ 𝑖) | 
| 274 | 273 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ≤ 𝑖) | 
| 275 | 267, 269,
271, 272, 274 | ltletrd 11422 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖) | 
| 276 | 275 | adantll 714 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖) | 
| 277 | 263, 265,
264, 266, 276 | lttrd 11423 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑖) | 
| 278 | 263, 264,
277 | ltled 11410 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ≤ 𝑖) | 
| 279 |  | elfzle2 13569 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ≤ 𝑁) | 
| 280 | 279 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ≤ 𝑁) | 
| 281 | 260, 87, 137 | 3syl 18 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) | 
| 282 | 262, 278,
280, 281 | mpbir3and 1342 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁)) | 
| 283 | 260, 282,
67 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑃‘𝑖) ∈ ℝ) | 
| 284 |  | simpll 766 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝜑) | 
| 285 |  | elfzelz 13565 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ) | 
| 286 | 285 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ) | 
| 287 | 284, 33 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ) | 
| 288 | 286 | zred 12724 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ) | 
| 289 | 76 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ) | 
| 290 | 81 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑘) | 
| 291 | 153 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ) | 
| 292 |  | 1red 11263 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈
ℝ) | 
| 293 | 291, 292 | readdcld 11291 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ∈ ℝ) | 
| 294 | 285 | zred 12724 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℝ) | 
| 295 | 294 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ) | 
| 296 | 291 | ltp1d 12199 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑘 + 1)) | 
| 297 |  | elfzle1 13568 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → (𝑘 + 1) ≤ 𝑖) | 
| 298 | 297 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ≤ 𝑖) | 
| 299 | 291, 293,
295, 296, 298 | ltletrd 11422 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖) | 
| 300 | 299 | adantll 714 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖) | 
| 301 | 287, 289,
288, 290, 300 | lttrd 11423 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖) | 
| 302 | 287, 288,
301 | ltled 11410 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ 𝑖) | 
| 303 | 294 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ) | 
| 304 | 8 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ) | 
| 305 |  | 1red 11263 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈
ℝ) | 
| 306 | 304, 305 | resubcld 11692 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ) | 
| 307 |  | elfzle2 13569 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1)) | 
| 308 | 307 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1)) | 
| 309 | 304 | ltm1d 12201 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁) | 
| 310 | 303, 306,
304, 308, 309 | lelttrd 11420 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁) | 
| 311 | 303, 304,
310 | ltled 11410 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑁) | 
| 312 | 311 | adantlr 715 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑁) | 
| 313 | 284, 87, 137 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) | 
| 314 | 286, 302,
312, 313 | mpbir3and 1342 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁)) | 
| 315 | 284, 314,
67 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ∈ ℝ) | 
| 316 | 286 | peano2zd 12727 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ) | 
| 317 | 316 | zred 12724 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ) | 
| 318 | 295, 292 | readdcld 11291 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ) | 
| 319 | 291, 295,
299 | ltled 11410 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ≤ 𝑖) | 
| 320 | 291, 295,
292, 319 | leadd1dd 11878 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ≤ (𝑖 + 1)) | 
| 321 | 291, 293,
318, 296, 320 | ltletrd 11422 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑖 + 1)) | 
| 322 | 321 | adantll 714 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑖 + 1)) | 
| 323 | 287, 289,
317, 290, 322 | lttrd 11423 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1)) | 
| 324 | 287, 317,
323 | ltled 11410 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1)) | 
| 325 | 285, 5, 177 | syl2anr 597 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) | 
| 326 | 310, 325 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁) | 
| 327 | 326 | adantlr 715 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁) | 
| 328 | 284, 87, 180 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁))) | 
| 329 | 316, 324,
327, 328 | mpbir3and 1342 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁)) | 
| 330 | 284, 329 | jca 511 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁))) | 
| 331 | 329, 330,
189 | sylc 65 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ) | 
| 332 | 284, 1 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℤ) | 
| 333 |  | eluz 12893 | . . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈
(ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑖)) | 
| 334 | 332, 286,
333 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑖)) | 
| 335 | 302, 334 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀)) | 
| 336 | 284, 3, 4 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ) | 
| 337 | 310 | adantlr 715 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁) | 
| 338 | 335, 336,
337, 193 | syl3anbrc 1343 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁)) | 
| 339 | 284, 338,
195 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) | 
| 340 | 315, 331,
339 | ltled 11410 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1))) | 
| 341 | 259, 283,
340 | monoord 14074 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ≤ (𝑃‘𝑁)) | 
| 342 | 341 | 3adant3 1132 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ≤ (𝑃‘𝑁)) | 
| 343 | 238, 239,
249, 253, 342 | letrd 11419 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘𝑁)) | 
| 344 | 249 | rexrd 11312 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑁) ∈
ℝ*) | 
| 345 |  | elicc1 13432 | . . . . . . . . 9
⊢ (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑁) ∈ ℝ*) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘𝑁)))) | 
| 346 | 229, 344,
345 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘𝑁)))) | 
| 347 | 227, 233,
343, 346 | mpbir3and 1342 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁))) | 
| 348 |  | iblspltprt.6 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁))) → 𝐴 ∈ ℂ) | 
| 349 | 225, 347,
348 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝐴 ∈ ℂ) | 
| 350 | 222, 223,
224, 349 | syl3anc 1372 | . . . . 5
⊢ (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝐴 ∈ ℂ) | 
| 351 |  | simp2 1137 | . . . . . 6
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈
𝐿1)) | 
| 352 | 57, 351 | mpd 15 | . . . . 5
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈
𝐿1) | 
| 353 | 57, 58 | jca 511 | . . . . . 6
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁))) | 
| 354 | 72, 201 | jca 511 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁))) | 
| 355 | 94, 204 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑖 = 𝑘 → ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))) | 
| 356 | 355 | mpteq1d 5236 | . . . . . . . . 9
⊢ (𝑖 = 𝑘 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴)) | 
| 357 | 356 | eleq1d 2825 | . . . . . . . 8
⊢ (𝑖 = 𝑘 → ((𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1)) | 
| 358 | 203, 357 | imbi12d 344 | . . . . . . 7
⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔
((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1))) | 
| 359 | 358, 46 | chvarvv 1997 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1) | 
| 360 | 353, 354,
359 | 3syl 18 | . . . . 5
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1) | 
| 361 | 56, 216, 221, 350, 352, 360 | iblsplitf 45990 | . . . 4
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1) | 
| 362 | 361 | 3exp 1119 | . . 3
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) →
(𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1))) | 
| 363 | 15, 20, 25, 30, 50, 362 | fzind2 13825 | . 2
⊢ (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴) ∈
𝐿1)) | 
| 364 | 10, 363 | mpcom 38 | 1
⊢ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴) ∈
𝐿1) |