Step | Hyp | Ref
| Expression |
1 | | itgspltprt.1 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
2 | 1 | peano2zd 11361 |
. . . . 5
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) |
3 | | itgspltprt.2 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) |
4 | | eluzelz 11573 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑁 ∈ ℤ) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
6 | 2, 5, 5 | 3jca 1235 |
. . . 4
⊢ (𝜑 → ((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
7 | | eluzle 11576 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑀 + 1) ≤ 𝑁) |
8 | 3, 7 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑀 + 1) ≤ 𝑁) |
9 | | eluzelre 11574 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → 𝑁 ∈ ℝ) |
10 | 3, 9 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℝ) |
11 | 10 | leidd 10473 |
. . . 4
⊢ (𝜑 → 𝑁 ≤ 𝑁) |
12 | 6, 8, 11 | jca32 556 |
. . 3
⊢ (𝜑 → (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑁 ∧ 𝑁 ≤ 𝑁))) |
13 | | elfz2 12204 |
. . 3
⊢ (𝑁 ∈ ((𝑀 + 1)...𝑁) ↔ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑀 + 1) ≤ 𝑁 ∧ 𝑁 ≤ 𝑁))) |
14 | 12, 13 | sylibr 223 |
. 2
⊢ (𝜑 → 𝑁 ∈ ((𝑀 + 1)...𝑁)) |
15 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑗 = (𝑀 + 1) → (𝑃‘𝑗) = (𝑃‘(𝑀 + 1))) |
16 | 15 | oveq2d 6565 |
. . . . . 6
⊢ (𝑗 = (𝑀 + 1) → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) |
17 | 16 | itgeq1d 38848 |
. . . . 5
⊢ (𝑗 = (𝑀 + 1) → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡) |
18 | | oveq2 6557 |
. . . . . 6
⊢ (𝑗 = (𝑀 + 1) → (𝑀..^𝑗) = (𝑀..^(𝑀 + 1))) |
19 | 18 | sumeq1d 14279 |
. . . . 5
⊢ (𝑗 = (𝑀 + 1) → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) |
20 | 17, 19 | eqeq12d 2625 |
. . . 4
⊢ (𝑗 = (𝑀 + 1) → (∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)) |
21 | 20 | imbi2d 329 |
. . 3
⊢ (𝑗 = (𝑀 + 1) → ((𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))) |
22 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑃‘𝑗) = (𝑃‘𝑘)) |
23 | 22 | oveq2d 6565 |
. . . . . 6
⊢ (𝑗 = 𝑘 → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘𝑘))) |
24 | 23 | itgeq1d 38848 |
. . . . 5
⊢ (𝑗 = 𝑘 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡) |
25 | | oveq2 6557 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (𝑀..^𝑗) = (𝑀..^𝑘)) |
26 | 25 | sumeq1d 14279 |
. . . . 5
⊢ (𝑗 = 𝑘 → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) |
27 | 24, 26 | eqeq12d 2625 |
. . . 4
⊢ (𝑗 = 𝑘 → (∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)) |
28 | 27 | imbi2d 329 |
. . 3
⊢ (𝑗 = 𝑘 → ((𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))) |
29 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → (𝑃‘𝑗) = (𝑃‘(𝑘 + 1))) |
30 | 29 | oveq2d 6565 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) |
31 | 30 | itgeq1d 38848 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) |
32 | | oveq2 6557 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (𝑀..^𝑗) = (𝑀..^(𝑘 + 1))) |
33 | 32 | sumeq1d 14279 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) |
34 | 31, 33 | eqeq12d 2625 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → (∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)) |
35 | 34 | imbi2d 329 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → ((𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))) |
36 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑗 = 𝑁 → (𝑃‘𝑗) = (𝑃‘𝑁)) |
37 | 36 | oveq2d 6565 |
. . . . . 6
⊢ (𝑗 = 𝑁 → ((𝑃‘𝑀)[,](𝑃‘𝑗)) = ((𝑃‘𝑀)[,](𝑃‘𝑁))) |
38 | 37 | itgeq1d 38848 |
. . . . 5
⊢ (𝑗 = 𝑁 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡) |
39 | | oveq2 6557 |
. . . . . 6
⊢ (𝑗 = 𝑁 → (𝑀..^𝑗) = (𝑀..^𝑁)) |
40 | 39 | sumeq1d 14279 |
. . . . 5
⊢ (𝑗 = 𝑁 → Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) |
41 | 38, 40 | eqeq12d 2625 |
. . . 4
⊢ (𝑗 = 𝑁 → (∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ↔ ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)) |
42 | 41 | imbi2d 329 |
. . 3
⊢ (𝑗 = 𝑁 → ((𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑗))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑗)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ↔ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))) |
43 | 1 | adantl 481 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → 𝑀 ∈ ℤ) |
44 | | fzval3 12404 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = (𝑀..^(𝑀 + 1))) |
45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → (𝑀...𝑀) = (𝑀..^(𝑀 + 1))) |
46 | 45 | eqcomd 2616 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀)) |
47 | 46 | sumeq1d 14279 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) |
48 | | itgspltprt.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃:(𝑀...𝑁)⟶ℝ) |
49 | 48 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑃:(𝑀...𝑁)⟶ℝ) |
50 | 1 | zred 11358 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℝ) |
51 | | 1red 9934 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈
ℝ) |
52 | 50, 51 | readdcld 9948 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀 + 1) ∈ ℝ) |
53 | 50 | ltp1d 10833 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
54 | 50, 52, 10, 53, 8 | ltletrd 10076 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 < 𝑁) |
55 | 50, 10, 54 | ltled 10064 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
56 | | eluz 11577 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) |
57 | 1, 5, 56 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) |
58 | 55, 57 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
59 | | eluzfz1 12219 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) |
61 | 60 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑀 ∈ (𝑀...𝑁)) |
62 | 49, 61 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘𝑀) ∈ ℝ) |
63 | | elfz1 12202 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (𝑀...𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑁))) |
64 | 1, 5, 63 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 ∈ (𝑀...𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑁))) |
65 | 5, 55, 11, 64 | mpbir3and 1238 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
66 | 48, 65 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃‘𝑁) ∈ ℝ) |
67 | 66 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘𝑁) ∈ ℝ) |
68 | 50 | lep1d 10834 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ≤ (𝑀 + 1)) |
69 | | elfz1 12202 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 + 1) ∈ (𝑀...𝑁) ↔ ((𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁))) |
70 | 1, 5, 69 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀 + 1) ∈ (𝑀...𝑁) ↔ ((𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁))) |
71 | 2, 68, 8, 70 | mpbir3and 1238 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀 + 1) ∈ (𝑀...𝑁)) |
72 | 48, 71 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃‘(𝑀 + 1)) ∈ ℝ) |
73 | 72 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ∈ ℝ) |
74 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) |
75 | | eliccre 38575 |
. . . . . . . . . . 11
⊢ (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ℝ) |
76 | 62, 73, 74, 75 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ℝ) |
77 | 48, 60 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃‘𝑀) ∈ ℝ) |
78 | 77 | rexrd 9968 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃‘𝑀) ∈
ℝ*) |
79 | 78 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘𝑀) ∈
ℝ*) |
80 | 73 | rexrd 9968 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ∈
ℝ*) |
81 | | iccgelb 12101 |
. . . . . . . . . . 11
⊢ (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ* ∧
𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘𝑀) ≤ 𝑡) |
82 | 79, 80, 74, 81 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘𝑀) ≤ 𝑡) |
83 | | iccleub 12100 |
. . . . . . . . . . . 12
⊢ (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑀 + 1)) ∈ ℝ* ∧
𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃‘(𝑀 + 1))) |
84 | 79, 80, 74, 83 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃‘(𝑀 + 1))) |
85 | 48 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ) |
86 | | elfzelz 12213 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ((𝑀 + 1)...𝑁) → 𝑖 ∈ ℤ) |
87 | 86 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ ℤ) |
88 | 50 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 ∈ ℝ) |
89 | 87 | zred 11358 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ ℝ) |
90 | 52 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 + 1) ∈ ℝ) |
91 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 < (𝑀 + 1)) |
92 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ((𝑀 + 1)...𝑁) → (𝑀 + 1) ≤ 𝑖) |
93 | 92 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 + 1) ≤ 𝑖) |
94 | 88, 90, 89, 91, 93 | ltletrd 10076 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 < 𝑖) |
95 | 88, 89, 94 | ltled 10064 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 ≤ 𝑖) |
96 | | elfzle2 12216 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ((𝑀 + 1)...𝑁) → 𝑖 ≤ 𝑁) |
97 | 96 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ≤ 𝑁) |
98 | 1, 5 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
99 | 98 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
100 | | elfz1 12202 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
102 | 87, 95, 97, 101 | mpbir3and 1238 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁)) |
103 | 85, 102 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑃‘𝑖) ∈ ℝ) |
104 | 48 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ) |
105 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ) |
106 | 105 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ) |
107 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ) |
108 | 106 | zred 11358 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ) |
109 | 52 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) ∈ ℝ) |
110 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < (𝑀 + 1)) |
111 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → (𝑀 + 1) ≤ 𝑖) |
112 | 111 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) ≤ 𝑖) |
113 | 107, 109,
108, 110, 112 | ltletrd 10076 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖) |
114 | 107, 108,
113 | ltled 10064 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 ≤ 𝑖) |
115 | 10 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ) |
116 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 1 ∈
ℝ) |
117 | 115, 116 | resubcld 10337 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ) |
118 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1)) |
119 | 118 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1)) |
120 | 115 | ltm1d 10835 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁) |
121 | 108, 117,
115, 119, 120 | lelttrd 10074 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁) |
122 | 108, 115,
121 | ltled 10064 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑁) |
123 | 98 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
124 | 123, 100 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
125 | 106, 114,
122, 124 | mpbir3and 1238 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁)) |
126 | 104, 125 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ∈ ℝ) |
127 | 106 | peano2zd 11361 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ) |
128 | 108, 116 | readdcld 9948 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ) |
129 | 107, 108,
116, 113 | ltadd1dd 10517 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑀 + 1) < (𝑖 + 1)) |
130 | 107, 109,
128, 110, 129 | lttrd 10077 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1)) |
131 | 107, 128,
130 | ltled 10064 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1)) |
132 | | zltp1le 11304 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) |
133 | 105, 5, 132 | syl2anr 494 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) |
134 | 121, 133 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁) |
135 | | elfz1 12202 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁))) |
136 | 123, 135 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁))) |
137 | 127, 131,
134, 136 | mpbir3and 1238 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁)) |
138 | 104, 137 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ) |
139 | | eluz 11577 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑖 ∈
(ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑖)) |
140 | 1, 105, 139 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑖 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑖)) |
141 | 114, 140 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀)) |
142 | 5 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ) |
143 | | elfzo2 12342 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀..^𝑁) ↔ (𝑖 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑖 < 𝑁)) |
144 | 141, 142,
121, 143 | syl3anbrc 1239 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁)) |
145 | | itgspltprt.4 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) |
146 | 144, 145 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) |
147 | 126, 138,
146 | ltled 10064 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1))) |
148 | 3, 103, 147 | monoord 12693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃‘(𝑀 + 1)) ≤ (𝑃‘𝑁)) |
149 | 148 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → (𝑃‘(𝑀 + 1)) ≤ (𝑃‘𝑁)) |
150 | 76, 73, 67, 84, 149 | letrd 10073 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ≤ (𝑃‘𝑁)) |
151 | 62, 67, 76, 82, 150 | eliccd 38573 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁))) |
152 | | itgspltprt.5 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁))) → 𝐴 ∈ ℂ) |
153 | 151, 152 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) → 𝐴 ∈ ℂ) |
154 | | id 22 |
. . . . . . . . . 10
⊢ (𝜑 → 𝜑) |
155 | | fzolb 12345 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (𝑀..^𝑁) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁)) |
156 | 1, 5, 54, 155 | syl3anbrc 1239 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ (𝑀..^𝑁)) |
157 | 154, 156 | jca 553 |
. . . . . . . . 9
⊢ (𝜑 → (𝜑 ∧ 𝑀 ∈ (𝑀..^𝑁))) |
158 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑀 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑀 ∈ (𝑀..^𝑁))) |
159 | 158 | anbi2d 736 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑀 → ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝑀 ∈ (𝑀..^𝑁)))) |
160 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑀 → (𝑃‘𝑖) = (𝑃‘𝑀)) |
161 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑀 → (𝑖 + 1) = (𝑀 + 1)) |
162 | 161 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑀 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑀 + 1))) |
163 | 160, 162 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑀 → ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))) |
164 | 163 | mpteq1d 4666 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑀 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴)) |
165 | 164 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑀 → ((𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1)) |
166 | 159, 165 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑀 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔
((𝜑 ∧ 𝑀 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1))) |
167 | | itgspltprt.6 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈
𝐿1) |
168 | 166, 167 | vtoclg 3239 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → ((𝜑 ∧ 𝑀 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1)) |
169 | 1, 157, 168 | sylc 63 |
. . . . . . . 8
⊢ (𝜑 → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1))) ↦ 𝐴) ∈
𝐿1) |
170 | 153, 169 | itgcl 23356 |
. . . . . . 7
⊢ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 ∈ ℂ) |
171 | 163 | itgeq1d 38848 |
. . . . . . . 8
⊢ (𝑖 = 𝑀 → ∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡) |
172 | 171 | fsum1 14320 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧
∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 ∈ ℂ) → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡) |
173 | 1, 170, 172 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡) |
174 | 173 | adantl 481 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → Σ𝑖 ∈ (𝑀...𝑀)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡) |
175 | 47, 174 | eqtr2d 2645 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘(𝑀 + 1)) ∧ 𝜑) → ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) |
176 | 175 | ex 449 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘(𝑀 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑀 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)) |
177 | | simp3 1056 |
. . . . 5
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → 𝜑) |
178 | | simp1 1054 |
. . . . 5
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → 𝑘 ∈ ((𝑀 + 1)..^𝑁)) |
179 | | simp2 1055 |
. . . . . 6
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)) |
180 | 177, 179 | mpd 15 |
. . . . 5
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) |
181 | 50 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℝ) |
182 | | elfzoelz 12339 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℤ) |
183 | 182 | zred 11358 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ ℝ) |
184 | 183 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℝ) |
185 | 52 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ∈ ℝ) |
186 | 53 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑀 + 1)) |
187 | | elfzole1 12347 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → (𝑀 + 1) ≤ 𝑘) |
188 | 187 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 + 1) ≤ 𝑘) |
189 | 181, 185,
184, 186, 188 | ltletrd 10076 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < 𝑘) |
190 | 181, 184,
189 | ltled 10064 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ 𝑘) |
191 | | eluz 11577 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈
(ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑘)) |
192 | 1, 182, 191 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑘)) |
193 | 190, 192 | mpbird 246 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
194 | | simplll 794 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝜑) |
195 | | eliccxr 38584 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) → 𝑡 ∈ ℝ*) |
196 | 195 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ*) |
197 | 194, 77 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑀) ∈ ℝ) |
198 | 194, 48 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑃:(𝑀...𝑁)⟶ℝ) |
199 | | elfzelz 12213 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℤ) |
200 | 199 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℤ) |
201 | | elfzle1 12215 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑀 ≤ 𝑖) |
202 | 201 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ≤ 𝑖) |
203 | 200 | zred 11358 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ) |
204 | 10 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℝ) |
205 | 184 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 ∈ ℝ) |
206 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑖 ≤ 𝑘) |
207 | 206 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ≤ 𝑘) |
208 | | elfzolt2 12348 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 < 𝑁) |
209 | 208 | ad2antlr 759 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑘 < 𝑁) |
210 | 203, 205,
204, 207, 209 | lelttrd 10074 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 < 𝑁) |
211 | 203, 204,
210 | ltled 10064 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ≤ 𝑁) |
212 | 98 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
213 | 212, 100 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
214 | 200, 202,
211, 213 | mpbir3and 1238 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀...𝑁)) |
215 | 214 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑖 ∈ (𝑀...𝑁)) |
216 | 198, 215 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑖) ∈ ℝ) |
217 | 200 | peano2zd 11361 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℤ) |
218 | 50 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ∈ ℝ) |
219 | 217 | zred 11358 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℝ) |
220 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ∈ ℝ) |
221 | 199 | zred 11358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ ℝ) |
222 | 221 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ ℝ) |
223 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 1 ∈ ℝ) |
224 | 222, 223 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ ℝ) |
225 | 201 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ≤ 𝑖) |
226 | 222 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 < (𝑖 + 1)) |
227 | 220, 222,
224, 225, 226 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 < (𝑖 + 1)) |
228 | 227 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 < (𝑖 + 1)) |
229 | 218, 219,
228 | ltled 10064 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑀 ≤ (𝑖 + 1)) |
230 | 5, 199 | anim12ci 589 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
231 | 230 | adantlr 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
232 | 231, 132 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) |
233 | 210, 232 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ≤ 𝑁) |
234 | 212, 135 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁))) |
235 | 217, 229,
233, 234 | mpbir3and 1238 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑖 + 1) ∈ (𝑀...𝑁)) |
236 | 235 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑖 + 1) ∈ (𝑀...𝑁)) |
237 | 198, 236 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ∈ ℝ) |
238 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) |
239 | | eliccre 38575 |
. . . . . . . . . . . . 13
⊢ (((𝑃‘𝑖) ∈ ℝ ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ) |
240 | 216, 237,
238, 239 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ℝ) |
241 | | elfzuz 12209 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ (ℤ≥‘𝑀)) |
242 | 241 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (ℤ≥‘𝑀)) |
243 | 48 | ad3antrrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑃:(𝑀...𝑁)⟶ℝ) |
244 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (𝑀...𝑖) → 𝑗 ∈ ℤ) |
245 | 244 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ ℤ) |
246 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (𝑀...𝑖) → 𝑀 ≤ 𝑗) |
247 | 246 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑀 ≤ 𝑗) |
248 | 245 | zred 11358 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ ℝ) |
249 | 204 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑁 ∈ ℝ) |
250 | 203 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑖 ∈ ℝ) |
251 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (𝑀...𝑖) → 𝑗 ≤ 𝑖) |
252 | 251 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ≤ 𝑖) |
253 | 210 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑖 < 𝑁) |
254 | 248, 250,
249, 252, 253 | lelttrd 10074 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 < 𝑁) |
255 | 248, 249,
254 | ltled 10064 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ≤ 𝑁) |
256 | 212 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
257 | | elfz1 12202 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))) |
258 | 256, 257 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))) |
259 | 245, 247,
255, 258 | mpbir3and 1238 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ (𝑀...𝑁)) |
260 | 243, 259 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝑃‘𝑗) ∈ ℝ) |
261 | 48 | ad3antrrr 762 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ) |
262 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ ℤ) |
263 | 262 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℤ) |
264 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑀 ≤ 𝑗) |
265 | 264 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ≤ 𝑗) |
266 | 263 | zred 11358 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℝ) |
267 | 204 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑁 ∈ ℝ) |
268 | 203 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑖 ∈ ℝ) |
269 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 1 ∈
ℝ) |
270 | 268, 269 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑖 − 1) ∈ ℝ) |
271 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ≤ (𝑖 − 1)) |
272 | 271 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ≤ (𝑖 − 1)) |
273 | 268 | ltm1d 10835 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑖 − 1) < 𝑖) |
274 | 266, 270,
268, 272, 273 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < 𝑖) |
275 | 210 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑖 < 𝑁) |
276 | 266, 268,
267, 274, 275 | lttrd 10077 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < 𝑁) |
277 | 266, 267,
276 | ltled 10064 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ≤ 𝑁) |
278 | 212 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
279 | 278, 257 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))) |
280 | 263, 265,
277, 279 | mpbir3and 1238 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (𝑀...𝑁)) |
281 | 261, 280 | ffvelrnd 6268 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃‘𝑗) ∈ ℝ) |
282 | 263 | peano2zd 11361 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℤ) |
283 | 181 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ∈ ℝ) |
284 | 266, 269 | readdcld 9948 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℝ) |
285 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ∈ ℝ) |
286 | 262 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ ℝ) |
287 | 286 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ ℝ) |
288 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 1 ∈
ℝ) |
289 | 287, 288 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ ℝ) |
290 | 264 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ≤ 𝑗) |
291 | 287 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 < (𝑗 + 1)) |
292 | 285, 287,
289, 290, 291 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 < (𝑗 + 1)) |
293 | 292 | ad4ant14 1285 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 < (𝑗 + 1)) |
294 | 283, 284,
293 | ltled 10064 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑀 ≤ (𝑗 + 1)) |
295 | | zltp1le 11304 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑗 < 𝑖 ↔ (𝑗 + 1) ≤ 𝑖)) |
296 | 262, 200,
295 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 < 𝑖 ↔ (𝑗 + 1) ≤ 𝑖)) |
297 | 274, 296 | mpbid 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ≤ 𝑖) |
298 | 284, 268,
267, 297, 275 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) < 𝑁) |
299 | 284, 267,
298 | ltled 10064 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ≤ 𝑁) |
300 | | elfz1 12202 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁))) |
301 | 278, 300 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁))) |
302 | 282, 294,
299, 301 | mpbir3and 1238 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑗 + 1) ∈ (𝑀...𝑁)) |
303 | 261, 302 | ffvelrnd 6268 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃‘(𝑗 + 1)) ∈ ℝ) |
304 | | simplll 794 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝜑) |
305 | | elfzuz 12209 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (𝑀...(𝑖 − 1)) → 𝑗 ∈ (ℤ≥‘𝑀)) |
306 | 305 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (ℤ≥‘𝑀)) |
307 | 304, 5 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑁 ∈ ℤ) |
308 | | elfzo2 12342 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (𝑀..^𝑁) ↔ (𝑗 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁)) |
309 | 306, 307,
276, 308 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → 𝑗 ∈ (𝑀..^𝑁)) |
310 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑗 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑗 ∈ (𝑀..^𝑁))) |
311 | 310 | anbi2d 736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)))) |
312 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑗 → (𝑃‘𝑖) = (𝑃‘𝑗)) |
313 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1)) |
314 | 313 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑗 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑗 + 1))) |
315 | 312, 314 | breq12d 4596 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑗 → ((𝑃‘𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃‘𝑗) < (𝑃‘(𝑗 + 1)))) |
316 | 311, 315 | imbi12d 333 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑃‘𝑗) < (𝑃‘(𝑗 + 1))))) |
317 | 316, 145 | chvarv 2251 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀..^𝑁)) → (𝑃‘𝑗) < (𝑃‘(𝑗 + 1))) |
318 | 304, 309,
317 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃‘𝑗) < (𝑃‘(𝑗 + 1))) |
319 | 281, 303,
318 | ltled 10064 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ (𝑀...(𝑖 − 1))) → (𝑃‘𝑗) ≤ (𝑃‘(𝑗 + 1))) |
320 | 242, 260,
319 | monoord 12693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃‘𝑀) ≤ (𝑃‘𝑖)) |
321 | 320 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑀) ≤ (𝑃‘𝑖)) |
322 | 216 | rexrd 9968 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑖) ∈
ℝ*) |
323 | 237 | rexrd 9968 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ∈
ℝ*) |
324 | | iccgelb 12101 |
. . . . . . . . . . . . 13
⊢ (((𝑃‘𝑖) ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑖) ≤ 𝑡) |
325 | 322, 323,
238, 324 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑖) ≤ 𝑡) |
326 | 197, 216,
240, 321, 325 | letrd 10073 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑀) ≤ 𝑡) |
327 | 194, 66 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘𝑁) ∈ ℝ) |
328 | | iccleub 12100 |
. . . . . . . . . . . . 13
⊢ (((𝑃‘𝑖) ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃‘(𝑖 + 1))) |
329 | 322, 323,
238, 328 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃‘(𝑖 + 1))) |
330 | 5 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ ℤ) |
331 | | eluz 11577 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑁)) |
332 | 217, 330,
331 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑁 ∈ (ℤ≥‘(𝑖 + 1)) ↔ (𝑖 + 1) ≤ 𝑁)) |
333 | 233, 332 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑁 ∈ (ℤ≥‘(𝑖 + 1))) |
334 | 333 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑁 ∈ (ℤ≥‘(𝑖 + 1))) |
335 | 48 | ad3antrrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ) |
336 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗 ∈ ℤ) |
337 | 336 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ ℤ) |
338 | | elfzel1 12212 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑀 ∈ ℤ) |
339 | 338 | zred 11358 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑀 ∈ ℝ) |
340 | 339 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 ∈ ℝ) |
341 | 336 | zred 11358 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗 ∈ ℝ) |
342 | 341 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ ℝ) |
343 | 221 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑖 ∈ ℝ) |
344 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 1 ∈ ℝ) |
345 | 343, 344 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑖 + 1) ∈ ℝ) |
346 | 201 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 ≤ 𝑖) |
347 | 343 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑖 < (𝑖 + 1)) |
348 | 340, 343,
345, 346, 347 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 < (𝑖 + 1)) |
349 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ ((𝑖 + 1)...𝑁) → (𝑖 + 1) ≤ 𝑗) |
350 | 349 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑖 + 1) ≤ 𝑗) |
351 | 340, 345,
342, 348, 350 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 < 𝑗) |
352 | 340, 342,
351 | ltled 10064 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 ≤ 𝑗) |
353 | 352 | adantll 746 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑀 ≤ 𝑗) |
354 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ((𝑖 + 1)...𝑁) → 𝑗 ≤ 𝑁) |
355 | 354 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ≤ 𝑁) |
356 | 212 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
357 | 356, 257 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))) |
358 | 337, 353,
355, 357 | mpbir3and 1238 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → 𝑗 ∈ (𝑀...𝑁)) |
359 | 335, 358 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑃‘𝑗) ∈ ℝ) |
360 | 359 | adantlr 747 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) ∧ 𝑗 ∈ ((𝑖 + 1)...𝑁)) → (𝑃‘𝑗) ∈ ℝ) |
361 | | simplll 794 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝜑) |
362 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑘)) |
363 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) |
364 | 48 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ) |
365 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → 𝑗 ∈ ℤ) |
366 | 365 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℤ) |
367 | 50 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ) |
368 | 366 | zred 11358 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℝ) |
369 | 224 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ) |
370 | 227 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1)) |
371 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → (𝑖 + 1) ≤ 𝑗) |
372 | 371 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑗) |
373 | 367, 369,
368, 370, 372 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < 𝑗) |
374 | 367, 368,
373 | ltled 10064 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ≤ 𝑗) |
375 | 365 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℤ) |
376 | 375 | zred 11358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ ℝ) |
377 | 10 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ) |
378 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 1 ∈
ℝ) |
379 | 377, 378 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ) |
380 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1)) → 𝑗 ≤ (𝑁 − 1)) |
381 | 380 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ≤ (𝑁 − 1)) |
382 | 377 | ltm1d 10835 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁) |
383 | 376, 379,
377, 381, 382 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 < 𝑁) |
384 | 376, 377,
383 | ltled 10064 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ≤ 𝑁) |
385 | 384 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ≤ 𝑁) |
386 | 98 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
387 | 386, 257 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 ∈ (𝑀...𝑁) ↔ (𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))) |
388 | 366, 374,
385, 387 | mpbir3and 1238 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (𝑀...𝑁)) |
389 | 364, 388 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘𝑗) ∈ ℝ) |
390 | 366 | peano2zd 11361 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ ℤ) |
391 | 390 | zred 11358 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ ℝ) |
392 | 221 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ) |
393 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 1 ∈
ℝ) |
394 | 226 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 < (𝑖 + 1)) |
395 | 392, 369,
368, 394, 372 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 < 𝑗) |
396 | 392, 368,
395 | ltled 10064 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑗) |
397 | 392, 368,
393, 396 | leadd1dd 10520 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ (𝑗 + 1)) |
398 | 367, 369,
391, 370, 397 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 < (𝑗 + 1)) |
399 | 367, 391,
398 | ltled 10064 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑗 + 1)) |
400 | | zltp1le 11304 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 < 𝑁 ↔ (𝑗 + 1) ≤ 𝑁)) |
401 | 365, 5, 400 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 < 𝑁 ↔ (𝑗 + 1) ≤ 𝑁)) |
402 | 383, 401 | mpbid 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ≤ 𝑁) |
403 | 402 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ≤ 𝑁) |
404 | 386, 300 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → ((𝑗 + 1) ∈ (𝑀...𝑁) ↔ ((𝑗 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑗 + 1) ∧ (𝑗 + 1) ≤ 𝑁))) |
405 | 390, 399,
403, 404 | mpbir3and 1238 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 + 1) ∈ (𝑀...𝑁)) |
406 | 364, 405 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘(𝑗 + 1)) ∈ ℝ) |
407 | | simp1 1054 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝜑) |
408 | 1 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℤ) |
409 | | eluz 11577 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈
(ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑗)) |
410 | 408, 366,
409 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑗 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑗)) |
411 | 374, 410 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (ℤ≥‘𝑀)) |
412 | 5 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ) |
413 | 383 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 < 𝑁) |
414 | 411, 412,
413, 308 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → 𝑗 ∈ (𝑀..^𝑁)) |
415 | 407, 414,
317 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘𝑗) < (𝑃‘(𝑗 + 1))) |
416 | 389, 406,
415 | ltled 10064 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘𝑗) ≤ (𝑃‘(𝑗 + 1))) |
417 | 361, 362,
363, 416 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘𝑗) ≤ (𝑃‘(𝑗 + 1))) |
418 | 417 | adantlr 747 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) ∧ 𝑗 ∈ ((𝑖 + 1)...(𝑁 − 1))) → (𝑃‘𝑗) ≤ (𝑃‘(𝑗 + 1))) |
419 | 334, 360,
418 | monoord 12693 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑁)) |
420 | 240, 237,
327, 329, 419 | letrd 10073 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ≤ (𝑃‘𝑁)) |
421 | 66 | rexrd 9968 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃‘𝑁) ∈
ℝ*) |
422 | 78, 421 | jca 553 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑁) ∈
ℝ*)) |
423 | 194, 422 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → ((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑁) ∈
ℝ*)) |
424 | | elicc1 12090 |
. . . . . . . . . . . 12
⊢ (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑁) ∈ ℝ*) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘𝑁)))) |
425 | 423, 424 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘𝑁)))) |
426 | 196, 326,
420, 425 | mpbir3and 1238 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁))) |
427 | 194, 426,
152 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) ∧ 𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))) → 𝐴 ∈ ℂ) |
428 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝜑) |
429 | 242, 330,
210, 143 | syl3anbrc 1239 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ (𝑀..^𝑁)) |
430 | 428, 429,
167 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈
𝐿1) |
431 | 427, 430 | itgcl 23356 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → ∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 ∈ ℂ) |
432 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → (𝑃‘𝑖) = (𝑃‘𝑘)) |
433 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1)) |
434 | 433 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑘 + 1))) |
435 | 432, 434 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) = ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))) |
436 | 435 | itgeq1d 38848 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → ∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) |
437 | 193, 431,
436 | fzosump1 14325 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)) |
438 | 437 | 3adant3 1074 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)) |
439 | | oveq1 6556 |
. . . . . . . 8
⊢
(∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 → (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)) |
440 | 439 | eqcomd 2616 |
. . . . . . 7
⊢
(∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 → (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)) |
441 | 440 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)) |
442 | 77 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ∈ ℝ) |
443 | 48 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ) |
444 | 182 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ ℤ) |
445 | 444 | peano2zd 11361 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℤ) |
446 | 445 | zred 11358 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ ℝ) |
447 | 184 | ltp1d 10833 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < (𝑘 + 1)) |
448 | 181, 184,
446, 189, 447 | lttrd 10077 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 < (𝑘 + 1)) |
449 | 181, 446,
448 | ltled 10064 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ≤ (𝑘 + 1)) |
450 | 208 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 < 𝑁) |
451 | | zltp1le 11304 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁)) |
452 | 182, 5, 451 | syl2anr 494 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 < 𝑁 ↔ (𝑘 + 1) ≤ 𝑁)) |
453 | 450, 452 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ≤ 𝑁) |
454 | 98 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
455 | | elfz1 12202 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁))) |
456 | 454, 455 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑘 + 1) ∈ (𝑀...𝑁) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1) ∧ (𝑘 + 1) ≤ 𝑁))) |
457 | 445, 449,
453, 456 | mpbir3and 1238 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁)) |
458 | 443, 457 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈ ℝ) |
459 | 10 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℝ) |
460 | 184, 459,
450 | ltled 10064 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ≤ 𝑁) |
461 | | elfz1 12202 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
462 | 454, 461 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
463 | 444, 190,
460, 462 | mpbir3and 1238 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀...𝑁)) |
464 | 443, 463 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈ ℝ) |
465 | 464 | rexrd 9968 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈
ℝ*) |
466 | 48 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑃:(𝑀...𝑁)⟶ℝ) |
467 | 466, 214 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝑃‘𝑖) ∈ ℝ) |
468 | 48 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ) |
469 | | elfzelz 12213 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ ℤ) |
470 | 469 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℤ) |
471 | | elfzle1 12215 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑀 ≤ 𝑖) |
472 | 471 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ 𝑖) |
473 | 470 | zred 11358 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ ℝ) |
474 | 10 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℝ) |
475 | 184 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 ∈ ℝ) |
476 | | 1red 9934 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 1 ∈
ℝ) |
477 | 475, 476 | resubcld 10337 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) ∈ ℝ) |
478 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ≤ (𝑘 − 1)) |
479 | 478 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ (𝑘 − 1)) |
480 | 475 | ltm1d 10835 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑘 − 1) < 𝑘) |
481 | 473, 477,
475, 479, 480 | lelttrd 10074 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑘) |
482 | 450 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑘 < 𝑁) |
483 | 473, 475,
474, 481, 482 | lttrd 10077 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < 𝑁) |
484 | 473, 474,
483 | ltled 10064 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ≤ 𝑁) |
485 | 98 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
486 | 485, 100 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 ∈ (𝑀...𝑁) ↔ (𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
487 | 470, 472,
484, 486 | mpbir3and 1238 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀...𝑁)) |
488 | 468, 487 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) ∈ ℝ) |
489 | 470 | peano2zd 11361 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℤ) |
490 | 50 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ∈ ℝ) |
491 | 473, 476 | readdcld 9948 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ ℝ) |
492 | 473 | ltp1d 10833 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 < (𝑖 + 1)) |
493 | 490, 473,
491, 472, 492 | lelttrd 10074 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 < (𝑖 + 1)) |
494 | 490, 491,
493 | ltled 10064 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑀 ≤ (𝑖 + 1)) |
495 | | zltp1le 11304 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑖 < 𝑘 ↔ (𝑖 + 1) ≤ 𝑘)) |
496 | 469, 444,
495 | syl2anr 494 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 < 𝑘 ↔ (𝑖 + 1) ≤ 𝑘)) |
497 | 481, 496 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑘) |
498 | 491, 475,
474, 497, 482 | lelttrd 10074 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) < 𝑁) |
499 | 491, 474,
498 | ltled 10064 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ≤ 𝑁) |
500 | 485, 135 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁))) |
501 | 489, 494,
499, 500 | mpbir3and 1238 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁)) |
502 | 468, 501 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ) |
503 | | simpll 786 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝜑) |
504 | | elfzuz 12209 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀...(𝑘 − 1)) → 𝑖 ∈ (ℤ≥‘𝑀)) |
505 | 504 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀)) |
506 | 5 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑁 ∈ ℤ) |
507 | 505, 506,
483, 143 | syl3anbrc 1239 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → 𝑖 ∈ (𝑀..^𝑁)) |
508 | 503, 507,
145 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) |
509 | 488, 502,
508 | ltled 10064 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀...(𝑘 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1))) |
510 | 193, 467,
509 | monoord 12693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ≤ (𝑃‘𝑘)) |
511 | 5 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ ℤ) |
512 | | elfzo2 12342 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀..^𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝑘 < 𝑁)) |
513 | 193, 511,
450, 512 | syl3anbrc 1239 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (𝑀..^𝑁)) |
514 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑘 → (𝑖 ∈ (𝑀..^𝑁) ↔ 𝑘 ∈ (𝑀..^𝑁))) |
515 | 514 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)))) |
516 | 432, 434 | breq12d 4596 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → ((𝑃‘𝑖) < (𝑃‘(𝑖 + 1)) ↔ (𝑃‘𝑘) < (𝑃‘(𝑘 + 1)))) |
517 | 515, 516 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1))))) |
518 | 517, 145 | chvarv 2251 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1))) |
519 | 513, 518 | syldan 486 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) < (𝑃‘(𝑘 + 1))) |
520 | 464, 458,
519 | ltled 10064 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ≤ (𝑃‘(𝑘 + 1))) |
521 | 78 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑀) ∈
ℝ*) |
522 | 458 | rexrd 9968 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ∈
ℝ*) |
523 | | elicc1 12090 |
. . . . . . . . . . 11
⊢ (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ*) →
((𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↔ ((𝑃‘𝑘) ∈ ℝ* ∧ (𝑃‘𝑀) ≤ (𝑃‘𝑘) ∧ (𝑃‘𝑘) ≤ (𝑃‘(𝑘 + 1))))) |
524 | 521, 522,
523 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ((𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) ↔ ((𝑃‘𝑘) ∈ ℝ* ∧ (𝑃‘𝑀) ≤ (𝑃‘𝑘) ∧ (𝑃‘𝑘) ≤ (𝑃‘(𝑘 + 1))))) |
525 | 465, 510,
520, 524 | mpbir3and 1238 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) |
526 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝜑) |
527 | | eliccxr 38584 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1))) → 𝑡 ∈ ℝ*) |
528 | 527 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ*) |
529 | 78 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ∈
ℝ*) |
530 | 522 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈
ℝ*) |
531 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) |
532 | | iccgelb 12101 |
. . . . . . . . . . . 12
⊢ (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ≤ 𝑡) |
533 | 529, 530,
531, 532 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ≤ 𝑡) |
534 | 77 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑀) ∈ ℝ) |
535 | 458 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ∈ ℝ) |
536 | | eliccre 38575 |
. . . . . . . . . . . . 13
⊢ (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ) |
537 | 534, 535,
531, 536 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ℝ) |
538 | 66 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘𝑁) ∈ ℝ) |
539 | | iccleub 12100 |
. . . . . . . . . . . . 13
⊢ (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘(𝑘 + 1)) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1))) |
540 | 529, 530,
531, 539 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘(𝑘 + 1))) |
541 | | eluz2 11569 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘(𝑘 + 1)) ↔ ((𝑘 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑘 + 1) ≤ 𝑁)) |
542 | 445, 511,
453, 541 | syl3anbrc 1239 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ≥‘(𝑘 + 1))) |
543 | 48 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ) |
544 | 1 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℤ) |
545 | 5 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑁 ∈ ℤ) |
546 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℤ) |
547 | 546 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℤ) |
548 | 544, 545,
547 | 3jca 1235 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ)) |
549 | 50 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ∈ ℝ) |
550 | 547 | zred 11358 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ) |
551 | 184 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ) |
552 | 189 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑘) |
553 | 183 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 ∈ ℝ) |
554 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 1 ∈ ℝ) |
555 | 553, 554 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ∈ ℝ) |
556 | 546 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ∈ ℝ) |
557 | 556 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ ℝ) |
558 | 553 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < (𝑘 + 1)) |
559 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → (𝑘 + 1) ≤ 𝑖) |
560 | 559 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑘 + 1) ≤ 𝑖) |
561 | 553, 555,
557, 558, 560 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖) |
562 | 561 | adantll 746 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑘 < 𝑖) |
563 | 549, 551,
550, 552, 562 | lttrd 10077 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 < 𝑖) |
564 | 549, 550,
563 | ltled 10064 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑀 ≤ 𝑖) |
565 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ((𝑘 + 1)...𝑁) → 𝑖 ≤ 𝑁) |
566 | 565 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ≤ 𝑁) |
567 | 548, 564,
566 | jca32 556 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
568 | | elfz2 12204 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
569 | 567, 568 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → 𝑖 ∈ (𝑀...𝑁)) |
570 | 543, 569 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...𝑁)) → (𝑃‘𝑖) ∈ ℝ) |
571 | 48 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ) |
572 | 1 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℤ) |
573 | 5 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℤ) |
574 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℤ) |
575 | 574 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℤ) |
576 | 572, 573,
575 | 3jca 1235 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ)) |
577 | 50 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ∈ ℝ) |
578 | 575 | zred 11358 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ) |
579 | 184 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ) |
580 | 189 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑘) |
581 | 183 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 ∈ ℝ) |
582 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈
ℝ) |
583 | 581, 582 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ∈ ℝ) |
584 | 574 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ∈ ℝ) |
585 | 584 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ) |
586 | 581 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑘 + 1)) |
587 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → (𝑘 + 1) ≤ 𝑖) |
588 | 587 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑘 + 1) ≤ 𝑖) |
589 | 581, 583,
585, 586, 588 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖) |
590 | 589 | adantll 746 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < 𝑖) |
591 | 577, 579,
578, 580, 590 | lttrd 10077 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < 𝑖) |
592 | 577, 578,
591 | ltled 10064 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ 𝑖) |
593 | 584 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ ℝ) |
594 | 10 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑁 ∈ ℝ) |
595 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 1 ∈
ℝ) |
596 | 594, 595 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ) |
597 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1)) |
598 | 597 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1)) |
599 | 594 | ltm1d 10835 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑁 − 1) < 𝑁) |
600 | 593, 596,
594, 598, 599 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁) |
601 | 593, 594,
600 | ltled 10064 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑁) |
602 | 601 | adantlr 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ≤ 𝑁) |
603 | 576, 592,
602 | jca32 556 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
604 | 603, 568 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁)) |
605 | 571, 604 | ffvelrnd 6268 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ∈ ℝ) |
606 | 575 | peano2zd 11361 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ) |
607 | 572, 573,
606 | 3jca 1235 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ)) |
608 | 606 | zred 11358 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ) |
609 | 578 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < (𝑖 + 1)) |
610 | 579, 578,
608, 590, 609 | lttrd 10077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑘 < (𝑖 + 1)) |
611 | 577, 579,
608, 580, 610 | lttrd 10077 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 < (𝑖 + 1)) |
612 | 577, 608,
611 | ltled 10064 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1)) |
613 | 600 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 < 𝑁) |
614 | 574, 511,
132 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) |
615 | 613, 614 | mpbid 221 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁) |
616 | 607, 612,
615 | jca32 556 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁))) |
617 | | elfz2 12204 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 + 1) ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁))) |
618 | 616, 617 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁)) |
619 | 571, 618 | ffvelrnd 6268 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ) |
620 | | simpll 786 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝜑) |
621 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀 ≤ 𝑖)) |
622 | 572, 575,
592, 621 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀)) |
623 | 622, 573,
613, 143 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁)) |
624 | 620, 623,
145 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) |
625 | 605, 619,
624 | ltled 10064 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ ((𝑘 + 1)...(𝑁 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1))) |
626 | 542, 570,
625 | monoord 12693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘(𝑘 + 1)) ≤ (𝑃‘𝑁)) |
627 | 626 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑃‘(𝑘 + 1)) ≤ (𝑃‘𝑁)) |
628 | 537, 535,
538, 540, 627 | letrd 10073 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ≤ (𝑃‘𝑁)) |
629 | 422 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → ((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑁) ∈
ℝ*)) |
630 | 629, 424 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁)) ↔ (𝑡 ∈ ℝ* ∧ (𝑃‘𝑀) ≤ 𝑡 ∧ 𝑡 ≤ (𝑃‘𝑁)))) |
631 | 528, 533,
628, 630 | mpbir3and 1238 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁))) |
632 | 526, 631,
152 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))) → 𝐴 ∈ ℂ) |
633 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑡(𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) |
634 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑀 ∈ ℤ) |
635 | | elfzouz 12343 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑘 ∈ (ℤ≥‘(𝑀 + 1))) |
636 | 635 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑘 ∈ (ℤ≥‘(𝑀 + 1))) |
637 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝜑) |
638 | | elfzouz 12343 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ (ℤ≥‘𝑀)) |
639 | 638 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ (ℤ≥‘𝑀)) |
640 | 5 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑁 ∈ ℤ) |
641 | | elfzoelz 12339 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ ℤ) |
642 | 641 | zred 11358 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑀..^𝑘) → 𝑖 ∈ ℝ) |
643 | 642 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ ℝ) |
644 | 184 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑘 ∈ ℝ) |
645 | 10 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑁 ∈ ℝ) |
646 | | elfzolt2 12348 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑀..^𝑘) → 𝑖 < 𝑘) |
647 | 646 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 < 𝑘) |
648 | 450 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑘 < 𝑁) |
649 | 643, 644,
645, 647, 648 | lttrd 10077 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 < 𝑁) |
650 | 639, 640,
649, 143 | syl3anbrc 1239 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → 𝑖 ∈ (𝑀..^𝑁)) |
651 | 637, 650,
145 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) |
652 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝜑) |
653 | 77 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑀) ∈ ℝ) |
654 | 66 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑁) ∈ ℝ) |
655 | 464 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑘) ∈ ℝ) |
656 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) |
657 | | eliccre 38575 |
. . . . . . . . . . . . 13
⊢ (((𝑃‘𝑀) ∈ ℝ ∧ (𝑃‘𝑘) ∈ ℝ ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ∈ ℝ) |
658 | 653, 655,
656, 657 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ∈ ℝ) |
659 | 78 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑀) ∈
ℝ*) |
660 | 465 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑘) ∈
ℝ*) |
661 | | iccgelb 12101 |
. . . . . . . . . . . . 13
⊢ (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑘) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑀) ≤ 𝑡) |
662 | 659, 660,
656, 661 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑀) ≤ 𝑡) |
663 | | iccleub 12100 |
. . . . . . . . . . . . . 14
⊢ (((𝑃‘𝑀) ∈ ℝ* ∧ (𝑃‘𝑘) ∈ ℝ* ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ≤ (𝑃‘𝑘)) |
664 | 659, 660,
656, 663 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ≤ (𝑃‘𝑘)) |
665 | | elfzouz2 12353 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → 𝑁 ∈ (ℤ≥‘𝑘)) |
666 | 665 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → 𝑁 ∈ (ℤ≥‘𝑘)) |
667 | 48 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑃:(𝑀...𝑁)⟶ℝ) |
668 | 1 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 ∈ ℤ) |
669 | 5 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑁 ∈ ℤ) |
670 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (𝑘...𝑁) → 𝑖 ∈ ℤ) |
671 | 670 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ ℤ) |
672 | 668, 669,
671 | 3jca 1235 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ)) |
673 | 50 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 ∈ ℝ) |
674 | 671 | zred 11358 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ ℝ) |
675 | 184 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑘 ∈ ℝ) |
676 | 189 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 < 𝑘) |
677 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (𝑘...𝑁) → 𝑘 ≤ 𝑖) |
678 | 677 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑘 ≤ 𝑖) |
679 | 673, 675,
674, 676, 678 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 < 𝑖) |
680 | 673, 674,
679 | ltled 10064 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑀 ≤ 𝑖) |
681 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (𝑘...𝑁) → 𝑖 ≤ 𝑁) |
682 | 681 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ≤ 𝑁) |
683 | 672, 680,
682 | jca32 556 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
684 | 683, 568 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → 𝑖 ∈ (𝑀...𝑁)) |
685 | 667, 684 | ffvelrnd 6268 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...𝑁)) → (𝑃‘𝑖) ∈ ℝ) |
686 | 48 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑃:(𝑀...𝑁)⟶ℝ) |
687 | 1 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ∈ ℤ) |
688 | 5 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑁 ∈ ℤ) |
689 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ∈ ℤ) |
690 | 689 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℤ) |
691 | 687, 688,
690 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ)) |
692 | 50 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ∈ ℝ) |
693 | 690 | zred 11358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℝ) |
694 | 184 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑘 ∈ ℝ) |
695 | 189 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < 𝑘) |
696 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑘 ≤ 𝑖) |
697 | 696 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑘 ≤ 𝑖) |
698 | 692, 694,
693, 695, 697 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < 𝑖) |
699 | 692, 693,
698 | ltled 10064 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ≤ 𝑖) |
700 | 689 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ∈ ℝ) |
701 | 700 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ ℝ) |
702 | 10 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑁 ∈ ℝ) |
703 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 1 ∈
ℝ) |
704 | 702, 703 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ) |
705 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ (𝑘...(𝑁 − 1)) → 𝑖 ≤ (𝑁 − 1)) |
706 | 705 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ≤ (𝑁 − 1)) |
707 | 702 | ltm1d 10835 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑁 − 1) < 𝑁) |
708 | 701, 704,
702, 706, 707 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < 𝑁) |
709 | 701, 702,
708 | ltled 10064 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ≤ 𝑁) |
710 | 709 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ≤ 𝑁) |
711 | 691, 699,
710 | jca32 556 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (𝑀 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
712 | 711, 568 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (𝑀...𝑁)) |
713 | 686, 712 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃‘𝑖) ∈ ℝ) |
714 | 690 | peano2zd 11361 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ ℤ) |
715 | 687, 688,
714 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ)) |
716 | 714 | zred 11358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ ℝ) |
717 | 693 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < (𝑖 + 1)) |
718 | 692, 693,
716, 699, 717 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 < (𝑖 + 1)) |
719 | 692, 716,
718 | ltled 10064 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑀 ≤ (𝑖 + 1)) |
720 | 689, 5, 132 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 < 𝑁 ↔ (𝑖 + 1) ≤ 𝑁)) |
721 | 708, 720 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁) |
722 | 721 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ≤ 𝑁) |
723 | 715, 719,
722 | jca32 556 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ 𝑁))) |
724 | 723, 617 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑖 + 1) ∈ (𝑀...𝑁)) |
725 | 686, 724 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃‘(𝑖 + 1)) ∈ ℝ) |
726 | | simpll 786 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝜑) |
727 | 687, 690,
699, 621 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (ℤ≥‘𝑀)) |
728 | 708 | adantlr 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 < 𝑁) |
729 | 727, 688,
728, 143 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → 𝑖 ∈ (𝑀..^𝑁)) |
730 | 726, 729,
145 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) |
731 | 713, 725,
730 | ltled 10064 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑘...(𝑁 − 1))) → (𝑃‘𝑖) ≤ (𝑃‘(𝑖 + 1))) |
732 | 666, 685,
731 | monoord 12693 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑃‘𝑘) ≤ (𝑃‘𝑁)) |
733 | 732 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → (𝑃‘𝑘) ≤ (𝑃‘𝑁)) |
734 | 658, 655,
654, 664, 733 | letrd 10073 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ≤ (𝑃‘𝑁)) |
735 | 653, 654,
658, 662, 734 | eliccd 38573 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑁))) |
736 | 652, 735,
152 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘))) → 𝐴 ∈ ℂ) |
737 | 637, 650,
167 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) ∧ 𝑖 ∈ (𝑀..^𝑘)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈
𝐿1) |
738 | 633, 634,
636, 467, 651, 736, 737 | iblspltprt 38865 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑀)[,](𝑃‘𝑘)) ↦ 𝐴) ∈
𝐿1) |
739 | 435 | mpteq1d 4666 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) = (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴)) |
740 | 739 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → ((𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1 ↔ (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1)) |
741 | 515, 740 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1))) ↦ 𝐴) ∈ 𝐿1) ↔
((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1))) |
742 | 741, 167 | chvarv 2251 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1) |
743 | 513, 742 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (𝑡 ∈ ((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1))) ↦ 𝐴) ∈
𝐿1) |
744 | 442, 458,
525, 632, 738, 743 | itgspliticc 23409 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡)) |
745 | 744 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁)) → (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) |
746 | 745 | 3adant3 1074 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 + ∫((𝑃‘𝑘)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) = ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡) |
747 | 438, 441,
746 | 3eqtrrd 2649 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) |
748 | 177, 178,
180, 747 | syl3anc 1318 |
. . . 4
⊢ ((𝑘 ∈ ((𝑀 + 1)..^𝑁) ∧ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) ∧ 𝜑) → ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) |
749 | 748 | 3exp 1256 |
. . 3
⊢ (𝑘 ∈ ((𝑀 + 1)..^𝑁) → ((𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑘))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑘)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) → (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘(𝑘 + 1)))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^(𝑘 + 1))∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡))) |
750 | 21, 28, 35, 42, 176, 749 | fzind2 12448 |
. 2
⊢ (𝑁 ∈ ((𝑀 + 1)...𝑁) → (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡)) |
751 | 14, 750 | mpcom 37 |
1
⊢ (𝜑 → ∫((𝑃‘𝑀)[,](𝑃‘𝑁))𝐴 d𝑡 = Σ𝑖 ∈ (𝑀..^𝑁)∫((𝑃‘𝑖)[,](𝑃‘(𝑖 + 1)))𝐴 d𝑡) |