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