Step | Hyp | Ref
| Expression |
1 | | iblspltprt.3 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) |
2 | | eluzelz 12061 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑁 ∈ ℤ) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℤ) |
4 | | eluzle 12064 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑀 + 1) ≤ 𝑁) |
5 | 1, 4 | syl 17 |
. . 3
⊢ (𝜑 → (𝑀 + 1) ≤ 𝑁) |
6 | 3 | zred 11893 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℝ) |
7 | 6 | leidd 10999 |
. . 3
⊢ (𝜑 → 𝑁 ≤ 𝑁) |
8 | | iblspltprt.2 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
9 | 8 | peano2zd 11896 |
. . . 4
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) |
10 | | elfz1 12706 |
. . . 4
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁 ∧ 𝑁 ≤ 𝑁))) |
11 | 9, 3, 10 | syl2anc 576 |
. . 3
⊢ (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁 ∧ 𝑁 ≤ 𝑁))) |
12 | 3, 5, 7, 11 | mpbir3and 1322 |
. 2
⊢ (𝜑 → 𝑁 ∈ ((𝑀 + 1)...𝑁)) |
13 | | fveq2 6493 |
. . . . . . 7
⊢ (𝑗 = (𝑀 + 1) → (𝑃‘𝑗) = (𝑃‘(𝑀 + 1))) |
14 | 13 | oveq2d 6986 |
. . . . . 6
⊢ (𝑗 = (𝑀 + 1) → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) |
15 | 14 | mpteq1d 5010 |
. . . . 5
⊢ (𝑗 = (𝑀 + 1) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴)) |
16 | 15 | eleq1d 2844 |
. . . 4
⊢ (𝑗 = (𝑀 + 1) → ((𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1)) |
17 | 16 | imbi2d 333 |
. . 3
⊢ (𝑗 = (𝑀 + 1) → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1) ↔
(𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1))) |
18 | | fveq2 6493 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑃‘𝑗) = (𝑃‘𝑘)) |
19 | 18 | oveq2d 6986 |
. . . . . 6
⊢ (𝑗 = 𝑘 → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘𝑘))) |
20 | 19 | mpteq1d 5010 |
. . . . 5
⊢ (𝑗 = 𝑘 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴)) |
21 | 20 | eleq1d 2844 |
. . . 4
⊢ (𝑗 = 𝑘 → ((𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈
𝐿1)) |
22 | 21 | imbi2d 333 |
. . 3
⊢ (𝑗 = 𝑘 → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1) ↔
(𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈
𝐿1))) |
23 | | fveq2 6493 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (𝑃‘𝑗) = (𝑃‘(𝑘 + 1))) |
24 | 23 | oveq2d 6986 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) |
25 | 24 | mpteq1d 5010 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴)) |
26 | 25 | eleq1d 2844 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → ((𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1)) |
27 | 26 | imbi2d 333 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1) ↔
(𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1))) |
28 | | fveq2 6493 |
. . . . . . 7
⊢ (𝑗 = 𝑁 → (𝑃‘𝑗) = (𝑃‘𝑁)) |
29 | 28 | oveq2d 6986 |
. . . . . 6
⊢ (𝑗 = 𝑁 → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘𝑁))) |
30 | 29 | mpteq1d 5010 |
. . . . 5
⊢ (𝑗 = 𝑁 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴)) |
31 | 30 | eleq1d 2844 |
. . . 4
⊢ (𝑗 = 𝑁 → ((𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴) ∈
𝐿1)) |
32 | 31 | imbi2d 333 |
. . 3
⊢ (𝑗 = 𝑁 → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑗)) ↦ 𝐴) ∈ 𝐿1) ↔
(𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴) ∈
𝐿1))) |
33 | | uzid 12066 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
34 | 8, 33 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
35 | 8 | zred 11893 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℝ) |
36 | | 1red 10432 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
37 | 35, 36 | readdcld 10461 |
. . . . . . 7
⊢ (𝜑 → (𝑀 + 1) ∈ ℝ) |
38 | 35 | ltp1d 11363 |
. . . . . . 7
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
39 | 35, 37, 6, 38, 5 | ltletrd 10592 |
. . . . . 6
⊢ (𝜑 → 𝑀 < 𝑁) |
40 | | elfzo2 12850 |
. . . . . 6
⊢ (𝑀 ∈ (𝑀..^𝑁) ↔ (𝑀 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁)) |
41 | 34, 3, 39, 40 | syl3anbrc 1323 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ (𝑀..^𝑁)) |
42 | | fveq2 6493 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑀 → (𝑃‘𝑖) = (𝑃‘𝑀)) |
43 | | fvoveq1 6993 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑀 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑀 + 1))) |
44 | 42, 43 | oveq12d 6988 |
. . . . . . . . 9
⊢ (𝑖 = 𝑀 → ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) |
45 | 44 | mpteq1d 5010 |
. . . . . . . 8
⊢ (𝑖 = 𝑀 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴)) |
46 | 45 | eleq1d 2844 |
. . . . . . 7
⊢ (𝑖 = 𝑀 → ((𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1)) |
47 | 46 | imbi2d 333 |
. . . . . 6
⊢ (𝑖 = 𝑀 → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔
(𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1))) |
48 | | iblspltprt.7 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈
𝐿1) |
49 | 48 | expcom 406 |
. . . . . 6
⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈
𝐿1)) |
50 | 47, 49 | vtoclga 3487 |
. . . . 5
⊢ (𝑀 ∈ (𝑀..^𝑁) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1)) |
51 | 41, 50 | mpcom 38 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1) |
52 | 51 | a1i 11 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1)) |
53 | | nfv 1873 |
. . . . . 6
⊢
Ⅎ𝑡 𝑘 ∈ ((𝑀 + 1)..^𝑁) |
54 | | iblspltprt.1 |
. . . . . . 7
⊢
Ⅎ𝑡𝜑 |
55 | | nfmpt1 5019 |
. . . . . . . 8
⊢
Ⅎ𝑡(𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) |
56 | 55 | nfel1 2940 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈
𝐿1 |
57 | 54, 56 | nfim 1859 |
. . . . . 6
⊢
Ⅎ𝑡(𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈
𝐿1) |
58 | 53, 57, 54 | nf3an 1864 |
. . . . 5
⊢
Ⅎ𝑡(𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) |
59 | | simp3 1118 |
. . . . . 6
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → 𝜑) |
60 | | simp1 1116 |
. . . . . 6
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → 𝑘 ∈ ((𝑀 + 1)..^𝑁)) |
61 | 35 | leidd 10999 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ≤ 𝑀) |
62 | 35, 6, 39 | ltled 10580 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
63 | | elfz1 12706 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (𝑀...𝑁) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁))) |
64 | 8, 3, 63 | syl2anc 576 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀 ∈ (𝑀...𝑁) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁))) |
65 | 8, 61, 62, 64 | mpbir3and 1322 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
66 | 65 | ancli 541 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝜑 ∧ 𝑀 ∈ (𝑀...𝑁))) |
67 | | eleq1 2847 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑀 → (𝑖 ∈ (𝑀...𝑁) ↔ 𝑀 ∈ (𝑀...𝑁))) |
68 | 67 | anbi2d 619 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑀 → ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑀 ∈ (𝑀...𝑁)))) |
69 | 42 | eleq1d 2844 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑀 → ((𝑃‘𝑖) ∈ ℝ ↔ (𝑃‘𝑀) ∈ ℝ)) |
70 | 68, 69 | imbi12d 337 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑀 → (((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ 𝑀 ∈ (𝑀...𝑁)) → (𝑃‘𝑀) ∈ ℝ))) |
71 | | iblspltprt.4 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ) |
72 | 70, 71 | vtoclg 3480 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ (𝑀...𝑁) → ((𝜑 ∧ 𝑀 ∈ (𝑀...𝑁)) → (𝑃‘𝑀) ∈ ℝ)) |
73 | 65, 66, 72 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃‘𝑀) ∈ ℝ) |
74 | 73 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ∈ ℝ) |
75 | 74 | rexrd 10482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ∈
ℝ*) |
76 | | simpl 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝜑) |
77 | | elfzoelz 12847 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℤ) |
78 | 77 | adantl 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℤ) |
79 | 35 | adantr 473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℝ) |
80 | 78 | zred 11893 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℝ) |
81 | 37 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ∈ ℝ) |
82 | 38 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑀 + 1)) |
83 | | elfzole1 12855 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑀 + 1) ≤ 𝑘) |
84 | 83 | adantl 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ≤ 𝑘) |
85 | 79, 81, 80, 82, 84 | ltletrd 10592 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < 𝑘) |
86 | 79, 80, 85 | ltled 10580 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ 𝑘) |
87 | 6 | adantr 473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℝ) |
88 | | elfzolt2 12856 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 < 𝑁) |
89 | 88 | adantl 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < 𝑁) |
90 | 80, 87, 89 | ltled 10580 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ≤ 𝑁) |
91 | 8, 3 | jca 504 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
92 | 91 | adantr 473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
93 | | elfz1 12706 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
95 | 78, 86, 90, 94 | mpbir3and 1322 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀...𝑁)) |
96 | | eleq1 2847 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (𝑖 ∈ (𝑀...𝑁) ↔ 𝑘 ∈ (𝑀...𝑁))) |
97 | 96 | anbi2d 619 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)))) |
98 | | fveq2 6493 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (𝑃‘𝑖) = (𝑃‘𝑘)) |
99 | 98 | eleq1d 2844 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → ((𝑃‘𝑖) ∈ ℝ ↔ (𝑃‘𝑘) ∈ ℝ)) |
100 | 97, 99 | imbi12d 337 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑃‘𝑘) ∈ ℝ))) |
101 | 100, 71 | chvarv 2325 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑃‘𝑘) ∈ ℝ) |
102 | 76, 95, 101 | syl2anc 576 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈ ℝ) |
103 | 102 | rexrd 10482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈
ℝ*) |
104 | 78 | peano2zd 11896 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℤ) |
105 | 104 | zred 11893 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℝ) |
106 | | 1red 10432 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 1 ∈ ℝ) |
107 | 79, 80, 106, 85 | ltadd1dd 11044 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) < (𝑘 + 1)) |
108 | 79, 81, 105, 82, 107 | lttrd 10593 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑘 + 1)) |
109 | 79, 105, 108 | ltled 10580 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ (𝑘 + 1)) |
110 | | zltp1le 11838 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁)) |
111 | 77, 3, 110 | syl2anr 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁)) |
112 | 89, 111 | mpbid 224 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ≤ 𝑁) |
113 | | elfz1 12706 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁))) |
114 | 92, 113 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁))) |
115 | 104, 109,
112, 114 | mpbir3and 1322 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
116 | 76, 115 | jca 504 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁))) |
117 | | eleq1 2847 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑘 + 1) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑘 + 1) ∈ (𝑀...𝑁))) |
118 | 117 | anbi2d 619 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑘 + 1) → ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)))) |
119 | | fveq2 6493 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑘 + 1) → (𝑃‘𝑖) = (𝑃‘(𝑘 + 1))) |
120 | 119 | eleq1d 2844 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑘 + 1) → ((𝑃‘𝑖) ∈ ℝ ↔ (𝑃‘(𝑘 + 1)) ∈ ℝ)) |
121 | 118, 120 | imbi12d 337 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑘 + 1) → (((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ))) |
122 | 121, 71 | vtoclg 3480 |
. . . . . . . . . . 11
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ)) |
123 | 115, 116,
122 | sylc 65 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ) |
124 | 123 | rexrd 10482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈
ℝ*) |
125 | | eluz 12065 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈
(ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑘)) |
126 | 8, 77, 125 | syl2an 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑘)) |
127 | 86, 126 | mpbird 249 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
128 | | simpll 754 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝜑) |
129 | | elfzelz 12717 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℤ) |
130 | 129 | adantl 474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℤ) |
131 | | elfzle1 12719 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑀 ≤ 𝑖) |
132 | 131 | adantl 474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ≤ 𝑖) |
133 | 130 | zred 11893 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ) |
134 | 128, 6 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℝ) |
135 | 80 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 ∈ ℝ) |
136 | | elfzle2 12720 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑖 ≤ 𝑘) |
137 | 136 | adantl 474 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ≤ 𝑘) |
138 | 89 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 < 𝑁) |
139 | 133, 135,
134, 137, 138 | lelttrd 10590 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 < 𝑁) |
140 | 133, 134,
139 | ltled 10580 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ≤ 𝑁) |
141 | | elfz1 12706 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
142 | 128, 91, 141 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
143 | 130, 132,
140, 142 | mpbir3and 1322 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀...𝑁)) |
144 | 128, 143,
71 | syl2anc 576 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃‘𝑖) ∈ ℝ) |
145 | | simpll 754 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝜑) |
146 | | elfzelz 12717 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ ℤ) |
147 | 146 | adantl 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℤ) |
148 | | elfzle1 12719 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ≤ 𝑖) |
149 | 148 | adantl 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ 𝑖) |
150 | 147 | zred 11893 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℝ) |
151 | 145, 6 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℝ) |
152 | 80 | adantr 473 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 ∈ ℝ) |
153 | | 1red 10432 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 1 ∈
ℝ) |
154 | 152, 153 | resubcld 10861 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) ∈ ℝ) |
155 | | elfzle2 12720 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ≤ (𝑘 − 1)) |
156 | 155 | adantl 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ (𝑘 − 1)) |
157 | 77 | zred 11893 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℝ) |
158 | | 1red 10432 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 1 ∈ ℝ) |
159 | 157, 158 | resubcld 10861 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 − 1) ∈ ℝ) |
160 | | elfzoel2 12846 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ ℤ) |
161 | 160 | zred 11893 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ ℝ) |
162 | 157 | ltm1d 11365 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 − 1) < 𝑘) |
163 | 159, 157,
161, 162, 88 | lttrd 10593 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 − 1) < 𝑁) |
164 | 163 | ad2antlr 714 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) < 𝑁) |
165 | 150, 154,
151, 156, 164 | lelttrd 10590 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑁) |
166 | 150, 151,
165 | ltled 10580 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ 𝑁) |
167 | 145, 91, 141 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
168 | 147, 149,
166, 167 | mpbir3and 1322 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀...𝑁)) |
169 | 145, 168,
71 | syl2anc 576 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) ∈ ℝ) |
170 | 147 | peano2zd 11896 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℤ) |
171 | | elfzel1 12716 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ∈ ℤ) |
172 | 171 | zred 11893 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ∈ ℝ) |
173 | 146 | zred 11893 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ ℝ) |
174 | | 1red 10432 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 1 ∈
ℝ) |
175 | 173, 174 | readdcld 10461 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → (𝑖 + 1) ∈ ℝ) |
176 | 173 | ltp1d 11363 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 < (𝑖 + 1)) |
177 | 172, 173,
175, 148, 176 | lelttrd 10590 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 < (𝑖 + 1)) |
178 | 172, 175,
177 | ltled 10580 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ≤ (𝑖 + 1)) |
179 | 178 | adantl 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ (𝑖 + 1)) |
180 | 145, 1, 2 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℤ) |
181 | | zltp1le 11838 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) |
182 | 147, 180,
181 | syl2anc 576 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) |
183 | 165, 182 | mpbid 224 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑁) |
184 | | elfz1 12706 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁))) |
185 | 145, 91, 184 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁))) |
186 | 170, 179,
183, 185 | mpbir3and 1322 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁)) |
187 | 145, 186 | jca 504 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁))) |
188 | | eleq1 2847 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑖 + 1) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑖 + 1) ∈ (𝑀...𝑁))) |
189 | 188 | anbi2d 619 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑖 + 1) → ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁)))) |
190 | | fveq2 6493 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑖 + 1) → (𝑃‘𝑘) = (𝑃‘(𝑖 + 1))) |
191 | 190 | eleq1d 2844 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑖 + 1) → ((𝑃‘𝑘) ∈ ℝ ↔ (𝑃‘(𝑖 + 1)) ∈ ℝ)) |
192 | 189, 191 | imbi12d 337 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑖 + 1) → (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑃‘𝑘) ∈ ℝ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑖 + 1)) ∈ ℝ))) |
193 | 192, 101 | vtoclg 3480 |
. . . . . . . . . . . 12
⊢ ((𝑖 + 1) ∈ (𝑀...𝑁) → ((𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁)) → (𝑃‘(𝑖 + 1)) ∈ ℝ)) |
194 | 186, 187,
193 | sylc 65 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ) |
195 | | elfzuz 12713 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ (ℤ≥‘𝑀)) |
196 | 195 | adantl 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀)) |
197 | | elfzo2 12850 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (𝑀..^𝑁) ↔ (𝑖 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑖 < 𝑁)) |
198 | 196, 180,
165, 197 | syl3anbrc 1323 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀..^𝑁)) |
199 | | iblspltprt.5 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) |
200 | 145, 198,
199 | syl2anc 576 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) |
201 | 169, 194,
200 | ltled 10580 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1))) |
202 | 127, 144,
201 | monoord 13208 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ≤ (𝑃‘𝑘)) |
203 | 160 | adantl 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℤ) |
204 | | elfzo2 12850 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀..^𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑘 < 𝑁)) |
205 | 127, 203,
89, 204 | syl3anbrc 1323 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀..^𝑁)) |
206 | | eleq1 2847 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑘 ∈ (𝑀..^𝑁))) |
207 | 206 | anbi2d 619 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)))) |
208 | | fvoveq1 6993 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑘 + 1))) |
209 | 98, 208 | breq12d 4936 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → ((𝑃‘𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃‘𝑘) < (𝑃‘(𝑘 + 1)))) |
210 | 207, 209 | imbi12d 337 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1))))) |
211 | 210, 199 | chvarv 2325 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1))) |
212 | 76, 205, 211 | syl2anc 576 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1))) |
213 | 102, 123,
212 | ltled 10580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ≤ (𝑃‘(𝑘 + 1))) |
214 | | iccintsng 41176 |
. . . . . . . . 9
⊢ ((((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑘) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*) ∧
((𝑃‘𝑀) ≤ (𝑃‘𝑘) ∧ (𝑃‘𝑘) ≤ (𝑃‘(𝑘 + 1)))) → (((𝑃‘𝑀)[,](𝑃‘𝑘)) ∩ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))) = {(𝑃‘𝑘)}) |
215 | 75, 103, 124, 202, 213, 214 | syl32anc 1358 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (((𝑃‘𝑀)[,](𝑃‘𝑘)) ∩ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))) = {(𝑃‘𝑘)}) |
216 | 215 | fveq2d 6497 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (vol*‘(((𝑃‘𝑀)[,](𝑃‘𝑘)) ∩ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))) = (vol*‘{(𝑃‘𝑘)})) |
217 | | ovolsn 23789 |
. . . . . . . 8
⊢ ((𝑃‘𝑘) ∈ ℝ → (vol*‘{(𝑃‘𝑘)}) = 0) |
218 | 102, 217 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (vol*‘{(𝑃‘𝑘)}) = 0) |
219 | 216, 218 | eqtrd 2808 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (vol*‘(((𝑃‘𝑀)[,](𝑃‘𝑘)) ∩ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))) = 0) |
220 | 59, 60, 219 | syl2anc 576 |
. . . . 5
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (vol*‘(((𝑃‘𝑀)[,](𝑃‘𝑘)) ∩ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))) = 0) |
221 | 74, 123, 102, 202, 213 | eliccd 41156 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) |
222 | 74, 123, 221 | 3jca 1108 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ (𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))))) |
223 | 59, 60, 222 | syl2anc 576 |
. . . . . 6
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → ((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ (𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))))) |
224 | | iccsplit 12680 |
. . . . . 6
⊢ (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ (𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) = (((𝑃‘𝑀)[,](𝑃‘𝑘)) ∪ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))) |
225 | 223, 224 | syl 17 |
. . . . 5
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) = (((𝑃‘𝑀)[,](𝑃‘𝑘)) ∪ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))))) |
226 | | simpl3 1173 |
. . . . . 6
⊢ (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝜑) |
227 | | simpl1 1171 |
. . . . . 6
⊢ (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑘 ∈ ((𝑀 + 1)..^𝑁)) |
228 | | simpr 477 |
. . . . . 6
⊢ (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) |
229 | | simp1 1116 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝜑) |
230 | | eliccxr 12632 |
. . . . . . . . 9
⊢ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) → 𝑡 ∈ ℝ*) |
231 | 230 | 3ad2ant3 1115 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ*) |
232 | 73 | rexrd 10482 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃‘𝑀) ∈
ℝ*) |
233 | 232 | 3ad2ant1 1113 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ∈
ℝ*) |
234 | 124 | 3adant3 1112 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈
ℝ*) |
235 | | simp3 1118 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) |
236 | | iccgelb 12602 |
. . . . . . . . 9
⊢ (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ≤ 𝑡) |
237 | 233, 234,
235, 236 | syl3anc 1351 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ≤ 𝑡) |
238 | 74, 123 | jca 504 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ)) |
239 | 238 | 3adant3 1112 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → ((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ)) |
240 | | iccssre 12627 |
. . . . . . . . . . 11
⊢ (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ) → ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ⊆ ℝ) |
241 | 240 | sseld 3853 |
. . . . . . . . . 10
⊢ (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) → 𝑡 ∈ ℝ)) |
242 | 239, 235,
241 | sylc 65 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ) |
243 | 123 | 3adant3 1112 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ) |
244 | | elfz1 12706 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (𝑀...𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑁))) |
245 | 8, 3, 244 | syl2anc 576 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 ∈ (𝑀...𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑁))) |
246 | 3, 62, 7, 245 | mpbir3and 1322 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
247 | 246 | ancli 541 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝜑 ∧ 𝑁 ∈ (𝑀...𝑁))) |
248 | | eleq1 2847 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑁 → (𝑖 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁))) |
249 | 248 | anbi2d 619 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑁 → ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) ↔ (𝜑 ∧ 𝑁 ∈ (𝑀...𝑁)))) |
250 | | fveq2 6493 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑁 → (𝑃‘𝑖) = (𝑃‘𝑁)) |
251 | 250 | eleq1d 2844 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑁 → ((𝑃‘𝑖) ∈ ℝ ↔ (𝑃‘𝑁) ∈ ℝ)) |
252 | 249, 251 | imbi12d 337 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑁 → (((𝜑 ∧ 𝑖 ∈ (𝑀...𝑁)) → (𝑃‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ 𝑁 ∈ (𝑀...𝑁)) → (𝑃‘𝑁) ∈ ℝ))) |
253 | 252, 71 | vtoclg 3480 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → ((𝜑 ∧ 𝑁 ∈ (𝑀...𝑁)) → (𝑃‘𝑁) ∈ ℝ)) |
254 | 3, 247, 253 | sylc 65 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃‘𝑁) ∈ ℝ) |
255 | 254 | 3ad2ant1 1113 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑁) ∈ ℝ) |
256 | | elicc1 12591 |
. . . . . . . . . . . 12
⊢ (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*) →
(𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘(𝑘 + 1))))) |
257 | 233, 234,
256 | syl2anc 576 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘(𝑘 + 1))))) |
258 | 235, 257 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘(𝑘 + 1)))) |
259 | 258 | simp3d 1124 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1))) |
260 | | elfzop1le2 40931 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 + 1) ≤ 𝑁) |
261 | 77 | peano2zd 11896 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑘 + 1) ∈ ℤ) |
262 | | eluz 12065 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘(𝑘 + 1)) ↔ (𝑘 + 1) ≤ 𝑁)) |
263 | 261, 160,
262 | syl2anc 576 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑁 ∈ (ℤ≥‘(𝑘 + 1)) ↔ (𝑘 + 1) ≤ 𝑁)) |
264 | 260, 263 | mpbird 249 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ (ℤ≥‘(𝑘 + 1))) |
265 | 264 | adantl 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ≥‘(𝑘 + 1))) |
266 | | simpll 754 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝜑) |
267 | | elfzelz 12717 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℤ) |
268 | 267 | adantl 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℤ) |
269 | 266, 35 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℝ) |
270 | 268 | zred 11893 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ) |
271 | 80 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ) |
272 | 85 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑘) |
273 | 157 | adantr 473 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ) |
274 | | 1red 10432 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 1 ∈ ℝ) |
275 | 273, 274 | readdcld 10461 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ∈ ℝ) |
276 | 267 | zred 11893 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℝ) |
277 | 276 | adantl 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ) |
278 | 273 | ltp1d 11363 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < (𝑘 + 1)) |
279 | | elfzle1 12719 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → (𝑘 + 1) ≤ 𝑖) |
280 | 279 | adantl 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ≤ 𝑖) |
281 | 273, 275,
277, 278, 280 | ltletrd 10592 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖) |
282 | 281 | adantll 701 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖) |
283 | 269, 271,
270, 272, 282 | lttrd 10593 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑖) |
284 | 269, 270,
283 | ltled 10580 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ≤ 𝑖) |
285 | | elfzle2 12720 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ≤ 𝑁) |
286 | 285 | adantl 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ≤ 𝑁) |
287 | 266, 91, 141 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
288 | 268, 284,
286, 287 | mpbir3and 1322 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁)) |
289 | 266, 288,
71 | syl2anc 576 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑃‘𝑖) ∈ ℝ) |
290 | | simpll 754 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝜑) |
291 | | elfzelz 12717 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ) |
292 | 291 | adantl 474 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ) |
293 | 290, 35 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ) |
294 | 292 | zred 11893 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ) |
295 | 80 | adantr 473 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ) |
296 | 85 | adantr 473 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑘) |
297 | 157 | adantr 473 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ) |
298 | | 1red 10432 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈
ℝ) |
299 | 297, 298 | readdcld 10461 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ∈ ℝ) |
300 | 291 | zred 11893 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℝ) |
301 | 300 | adantl 474 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ) |
302 | 297 | ltp1d 11363 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑘 + 1)) |
303 | | elfzle1 12719 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → (𝑘 + 1) ≤ 𝑖) |
304 | 303 | adantl 474 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ≤ 𝑖) |
305 | 297, 299,
301, 302, 304 | ltletrd 10592 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖) |
306 | 305 | adantll 701 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖) |
307 | 293, 295,
294, 296, 306 | lttrd 10593 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖) |
308 | 293, 294,
307 | ltled 10580 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ 𝑖) |
309 | 300 | adantl 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ) |
310 | 6 | adantr 473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ) |
311 | | 1red 10432 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈
ℝ) |
312 | 310, 311 | resubcld 10861 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ) |
313 | | elfzle2 12720 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1)) |
314 | 313 | adantl 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1)) |
315 | 310 | ltm1d 11365 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁) |
316 | 309, 312,
310, 314, 315 | lelttrd 10590 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁) |
317 | 309, 310,
316 | ltled 10580 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑁) |
318 | 317 | adantlr 702 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑁) |
319 | 290, 91, 141 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
320 | 292, 308,
318, 319 | mpbir3and 1322 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁)) |
321 | 290, 320,
71 | syl2anc 576 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ∈ ℝ) |
322 | 292 | peano2zd 11896 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ) |
323 | 322 | zred 11893 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ) |
324 | 301, 298 | readdcld 10461 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ) |
325 | 297, 301,
305 | ltled 10580 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ≤ 𝑖) |
326 | 297, 301,
298, 325 | leadd1dd 11047 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ≤ (𝑖 + 1)) |
327 | 297, 299,
324, 302, 326 | ltletrd 10592 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑖 + 1)) |
328 | 327 | adantll 701 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑖 + 1)) |
329 | 293, 295,
323, 296, 328 | lttrd 10593 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1)) |
330 | 293, 323,
329 | ltled 10580 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1)) |
331 | 291, 3, 181 | syl2anr 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) |
332 | 316, 331 | mpbid 224 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁) |
333 | 332 | adantlr 702 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁) |
334 | 290, 91, 184 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁))) |
335 | 322, 330,
333, 334 | mpbir3and 1322 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁)) |
336 | 290, 335 | jca 504 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝜑 ∧ (𝑖 + 1) ∈ (𝑀...𝑁))) |
337 | 335, 336,
193 | sylc 65 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ) |
338 | 290, 8 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℤ) |
339 | | eluz 12065 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈
(ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑖)) |
340 | 338, 292,
339 | syl2anc 576 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑖)) |
341 | 308, 340 | mpbird 249 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀)) |
342 | 290, 1, 2 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ) |
343 | 316 | adantlr 702 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁) |
344 | 341, 342,
343, 197 | syl3anbrc 1323 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁)) |
345 | 290, 344,
199 | syl2anc 576 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) |
346 | 321, 337,
345 | ltled 10580 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1))) |
347 | 265, 289,
346 | monoord 13208 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ≤ (𝑃‘𝑁)) |
348 | 347 | 3adant3 1112 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ≤ (𝑃‘𝑁)) |
349 | 242, 243,
255, 259, 348 | letrd 10589 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘𝑁)) |
350 | 255 | rexrd 10482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑁) ∈
ℝ*) |
351 | | elicc1 12591 |
. . . . . . . . 9
⊢ (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑁) ∈ ℝ*) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘𝑁)))) |
352 | 233, 350,
351 | syl2anc 576 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘𝑁)))) |
353 | 231, 237,
349, 352 | mpbir3and 1322 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁))) |
354 | | iblspltprt.6 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁))) → 𝐴 ∈ ℂ) |
355 | 229, 353,
354 | syl2anc 576 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝐴 ∈ ℂ) |
356 | 226, 227,
228, 355 | syl3anc 1351 |
. . . . 5
⊢ (((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝐴 ∈ ℂ) |
357 | | simp2 1117 |
. . . . . 6
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈
𝐿1)) |
358 | 59, 357 | mpd 15 |
. . . . 5
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈
𝐿1) |
359 | 59, 60 | jca 504 |
. . . . . 6
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁))) |
360 | 76, 205 | jca 504 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁))) |
361 | 98, 208 | oveq12d 6988 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))) |
362 | 361 | mpteq1d 5010 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴)) |
363 | 362 | eleq1d 2844 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → ((𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1)) |
364 | 207, 363 | imbi12d 337 |
. . . . . . 7
⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔
((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1))) |
365 | 364, 48 | chvarv 2325 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1) |
366 | 359, 360,
365 | 3syl 18 |
. . . . 5
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1) |
367 | 58, 220, 225, 356, 358, 366 | iblsplitf 41631 |
. . . 4
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) ∧ 𝜑) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1) |
368 | 367 | 3exp 1099 |
. . 3
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → ((𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈ 𝐿1) →
(𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1))) |
369 | 17, 22, 27, 32, 52, 368 | fzind2 12963 |
. 2
⊢ (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴) ∈
𝐿1)) |
370 | 12, 369 | mpcom 38 |
1
⊢ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↦ 𝐴) ∈
𝐿1) |