Step | Hyp | Ref
| Expression |
1 | | hoidmv1lelem3.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
2 | | hoidmv1lelem3.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 1, 2 | resubcld 10337 |
. 2
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
4 | | nnex 10903 |
. . . . . . 7
⊢ ℕ
∈ V |
5 | 4 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℕ ∈
V) |
6 | | icossicc 12131 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
7 | | 0xr 9965 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 0 ∈
ℝ*) |
9 | | pnfxr 9971 |
. . . . . . . . . 10
⊢ +∞
∈ ℝ* |
10 | 9 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → +∞ ∈
ℝ*) |
11 | | hoidmv1lelem3.c |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶:ℕ⟶ℝ) |
12 | 11 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ) |
13 | | hoidmv1lelem3.d |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷:ℕ⟶ℝ) |
14 | 13 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ) |
15 | 1 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐵 ∈ ℝ) |
16 | 14, 15 | ifcld 4081 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) ∈ ℝ) |
17 | | volicore 39471 |
. . . . . . . . . . 11
⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) ∈ ℝ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) ∈ ℝ) |
18 | 12, 16, 17 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) ∈ ℝ) |
19 | 18 | rexrd 9968 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) ∈
ℝ*) |
20 | 16 | rexrd 9968 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) ∈
ℝ*) |
21 | | icombl 23139 |
. . . . . . . . . . 11
⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) ∈ ℝ*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) ∈ dom vol) |
22 | 12, 20, 21 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) ∈ dom vol) |
23 | | volge0 38853 |
. . . . . . . . . 10
⊢ (((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) ∈ dom vol → 0 ≤
(vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 0 ≤
(vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))) |
25 | 18 | ltpnfd 11831 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) < +∞) |
26 | 8, 10, 19, 24, 25 | elicod 12095 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) ∈ (0[,)+∞)) |
27 | 6, 26 | sseldi 3566 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) ∈ (0[,]+∞)) |
28 | | eqid 2610 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ ↦
(vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))) |
29 | 27, 28 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))):ℕ⟶(0[,]+∞)) |
30 | 5, 29 | sge0xrcl 39278 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) ∈
ℝ*) |
31 | 9 | a1i 11 |
. . . . 5
⊢ (𝜑 → +∞ ∈
ℝ*) |
32 | | hoidmv1lelem3.r |
. . . . . . 7
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ) |
33 | 32 | rexrd 9968 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈
ℝ*) |
34 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑗𝜑 |
35 | | volf 23104 |
. . . . . . . . 9
⊢ vol:dom
vol⟶(0[,]+∞) |
36 | 35 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → vol:dom
vol⟶(0[,]+∞)) |
37 | 14 | rexrd 9968 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈
ℝ*) |
38 | | icombl 23139 |
. . . . . . . . 9
⊢ (((𝐶‘𝑗) ∈ ℝ ∧ (𝐷‘𝑗) ∈ ℝ*) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol) |
39 | 12, 37, 38 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol) |
40 | 36, 39 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∈ (0[,]+∞)) |
41 | 12 | rexrd 9968 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈
ℝ*) |
42 | 12 | leidd 10473 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ≤ (𝐶‘𝑗)) |
43 | | min1 11894 |
. . . . . . . . . 10
⊢ (((𝐷‘𝑗) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) ≤ (𝐷‘𝑗)) |
44 | 14, 15, 43 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) ≤ (𝐷‘𝑗)) |
45 | | icossico 12114 |
. . . . . . . . 9
⊢ ((((𝐶‘𝑗) ∈ ℝ* ∧ (𝐷‘𝑗) ∈ ℝ*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) ≤ (𝐷‘𝑗))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
46 | 41, 37, 42, 44, 45 | syl22anc 1319 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
47 | | volss 23108 |
. . . . . . . 8
⊢ ((((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
48 | 22, 39, 46, 47 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
49 | 34, 5, 27, 40, 48 | sge0lempt 39303 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))))) |
50 | 32 | ltpnfd 11831 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) < +∞) |
51 | 30, 33, 31, 49, 50 | xrlelttrd 11867 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) < +∞) |
52 | 30, 31, 51 | xrltned 38514 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) ≠ +∞) |
53 | 52 | neneqd 2787 |
. . 3
⊢ (𝜑 → ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) = +∞) |
54 | 5, 29 | sge0repnf 39279 |
. . 3
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) ∈ ℝ ↔ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) = +∞)) |
55 | 53, 54 | mpbird 246 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) ∈ ℝ) |
56 | 1 | rexrd 9968 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
57 | 2, 1 | iccssred 38574 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
58 | | hoidmv1lelem3.u |
. . . . . . . . . . 11
⊢ 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} |
59 | | ssrab2 3650 |
. . . . . . . . . . 11
⊢ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ⊆ (𝐴[,]𝐵) |
60 | 58, 59 | eqsstri 3598 |
. . . . . . . . . 10
⊢ 𝑈 ⊆ (𝐴[,]𝐵) |
61 | | hoidmv1lelem3.l |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 < 𝐵) |
62 | | hoidmv1lelem3.s |
. . . . . . . . . . . 12
⊢ 𝑆 = sup(𝑈, ℝ, < ) |
63 | 2, 1, 61, 11, 13, 32, 58, 62 | hoidmv1lelem1 39481 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 ∈ 𝑈 ∧ 𝐴 ∈ 𝑈 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥)) |
64 | 63 | simp1d 1066 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ 𝑈) |
65 | 60, 64 | sseldi 3566 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ (𝐴[,]𝐵)) |
66 | 57, 65 | sseldd 3569 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℝ) |
67 | 66 | rexrd 9968 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈
ℝ*) |
68 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → 𝜑) |
69 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → ¬ 𝐵 ≤ 𝑆) |
70 | 68, 66 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → 𝑆 ∈ ℝ) |
71 | 68, 1 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → 𝐵 ∈ ℝ) |
72 | 70, 71 | ltnled 10063 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → (𝑆 < 𝐵 ↔ ¬ 𝐵 ≤ 𝑆)) |
73 | 69, 72 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → 𝑆 < 𝐵) |
74 | | hoidmv1lelem3.x |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴[,)𝐵) ⊆ ∪ 𝑗 ∈ ℕ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
75 | 74 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → (𝐴[,)𝐵) ⊆ ∪ 𝑗 ∈ ℕ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
76 | 2 | rexrd 9968 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
77 | 76 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝐴 ∈
ℝ*) |
78 | 56 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝐵 ∈
ℝ*) |
79 | 67 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝑆 ∈
ℝ*) |
80 | 60, 57 | syl5ss 3579 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑈 ⊆ ℝ) |
81 | | ne0i 3880 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ∈ 𝑈 → 𝑈 ≠ ∅) |
82 | 64, 81 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑈 ≠ ∅) |
83 | 63 | simp3d 1068 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) |
84 | 63 | simp2d 1067 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
85 | | suprub 10863 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) ∧ 𝐴 ∈ 𝑈) → 𝐴 ≤ sup(𝑈, ℝ, < )) |
86 | 80, 82, 83, 84, 85 | syl31anc 1321 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ≤ sup(𝑈, ℝ, < )) |
87 | 86, 62 | syl6breqr 4625 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ≤ 𝑆) |
88 | 87 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝐴 ≤ 𝑆) |
89 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝑆 < 𝐵) |
90 | 77, 78, 79, 88, 89 | elicod 12095 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝑆 ∈ (𝐴[,)𝐵)) |
91 | 75, 90 | sseldd 3569 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝑆 ∈ ∪
𝑗 ∈ ℕ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
92 | | eliun 4460 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ ∪ 𝑗 ∈ ℕ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ↔ ∃𝑗 ∈ ℕ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
93 | 91, 92 | sylib 207 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → ∃𝑗 ∈ ℕ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
94 | 2 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝐴 ∈ ℝ) |
95 | 94 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝐴 ∈ ℝ) |
96 | 1 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝐵 ∈ ℝ) |
97 | 96 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝐵 ∈ ℝ) |
98 | 11 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝐶:ℕ⟶ℝ) |
99 | 98 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝐶:ℕ⟶ℝ) |
100 | 13 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝐷:ℕ⟶ℝ) |
101 | 100 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝐷:ℕ⟶ℝ) |
102 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑗 → (𝐶‘𝑖) = (𝐶‘𝑗)) |
103 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑗 → (𝐷‘𝑖) = (𝐷‘𝑗)) |
104 | 102, 103 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑗 → ((𝐶‘𝑖)[,)(𝐷‘𝑖)) = ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
105 | 104 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑗 → (vol‘((𝐶‘𝑖)[,)(𝐷‘𝑖))) = (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
106 | 105 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℕ ↦
(vol‘((𝐶‘𝑖)[,)(𝐷‘𝑖)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
107 | 106 | fveq2i 6106 |
. . . . . . . . . . . . . . . 16
⊢
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)(𝐷‘𝑖))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) |
108 | 107, 32 | syl5eqel 2692 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)(𝐷‘𝑖))))) ∈ ℝ) |
109 | 108 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < 𝐵) →
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)(𝐷‘𝑖))))) ∈ ℝ) |
110 | 109 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) →
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)(𝐷‘𝑖))))) ∈ ℝ) |
111 | 103 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = 𝑗 → ((𝐷‘𝑖) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝑧)) |
112 | 111, 103 | ifbieq1d 4059 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = 𝑗 → if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧) = if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) |
113 | 102, 112 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑗 → ((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) |
114 | 113 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑗 → (vol‘((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) |
115 | 114 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ℕ ↦
(vol‘((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) |
116 | 115 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ ℕ ↦
(vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧)))) |
117 | 116 | fveq2i 6106 |
. . . . . . . . . . . . . . . . 17
⊢
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) =
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧))))) |
118 | 117 | breq2i 4591 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝑧 − 𝐴) ≤
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧)))))) |
119 | 118 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝐴[,]𝐵) → ((𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝑧 − 𝐴) ≤
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧))))))) |
120 | 119 | rabbiia 3161 |
. . . . . . . . . . . . . 14
⊢ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧)))))} |
121 | 58, 120 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧)))))} |
122 | 64 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝑆 ∈ 𝑈) |
123 | 122 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝑆 ∈ 𝑈) |
124 | 88 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝐴 ≤ 𝑆) |
125 | 89 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝑆 < 𝐵) |
126 | | simp2 1055 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝑗 ∈ ℕ) |
127 | | simp3 1056 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
128 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) = if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) |
129 | 95, 97, 99, 101, 110, 121, 123, 124, 125, 126, 127, 128 | hoidmv1lelem2 39482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |
130 | 129 | 3exp 1256 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → (𝑗 ∈ ℕ → (𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢))) |
131 | 130 | rexlimdv 3012 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → (∃𝑗 ∈ ℕ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢)) |
132 | 93, 131 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |
133 | 68, 73, 132 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |
134 | 57 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝐴[,]𝐵) ⊆ ℝ) |
135 | 60, 134 | syl5ss 3579 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑈 ⊆ ℝ) |
136 | 82 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑈 ≠ ∅) |
137 | 2, 1 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
138 | 137 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
139 | 60 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑈 ⊆ (𝐴[,]𝐵)) |
140 | 64 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑆 ∈ 𝑈) |
141 | | iccsupr 12137 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑈 ⊆ (𝐴[,]𝐵) ∧ 𝑆 ∈ 𝑈) → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥)) |
142 | 138, 139,
140, 141 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥)) |
143 | 142 | simp3d 1068 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) |
144 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝑈) |
145 | | suprub 10863 |
. . . . . . . . . . . . . 14
⊢ (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) ∧ 𝑢 ∈ 𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < )) |
146 | 135, 136,
143, 144, 145 | syl31anc 1321 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < )) |
147 | 146, 62 | syl6breqr 4625 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ≤ 𝑆) |
148 | 147 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑢 ∈ 𝑈 𝑢 ≤ 𝑆) |
149 | 60 | sseli 3564 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ 𝑈 → 𝑢 ∈ (𝐴[,]𝐵)) |
150 | 149 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ (𝐴[,]𝐵)) |
151 | 134, 150 | sseldd 3569 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ ℝ) |
152 | 66 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑆 ∈ ℝ) |
153 | 151, 152 | lenltd 10062 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 ≤ 𝑆 ↔ ¬ 𝑆 < 𝑢)) |
154 | 153 | ralbidva 2968 |
. . . . . . . . . . 11
⊢ (𝜑 → (∀𝑢 ∈ 𝑈 𝑢 ≤ 𝑆 ↔ ∀𝑢 ∈ 𝑈 ¬ 𝑆 < 𝑢)) |
155 | 148, 154 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ¬ 𝑆 < 𝑢) |
156 | | ralnex 2975 |
. . . . . . . . . 10
⊢
(∀𝑢 ∈
𝑈 ¬ 𝑆 < 𝑢 ↔ ¬ ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |
157 | 155, 156 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → ¬ ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |
158 | 157 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → ¬ ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |
159 | 133, 158 | condan 831 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ≤ 𝑆) |
160 | | iccleub 12100 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑆
∈ (𝐴[,]𝐵)) → 𝑆 ≤ 𝐵) |
161 | 76, 56, 65, 160 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ≤ 𝐵) |
162 | 56, 67, 159, 161 | xrletrid 11862 |
. . . . . 6
⊢ (𝜑 → 𝐵 = 𝑆) |
163 | 162, 64 | eqeltrd 2688 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑈) |
164 | 163, 58 | syl6eleq 2698 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))}) |
165 | | oveq1 6556 |
. . . . . 6
⊢ (𝑧 = 𝐵 → (𝑧 − 𝐴) = (𝐵 − 𝐴)) |
166 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐵 → ((𝐷‘𝑗) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝐵)) |
167 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐵 → 𝑧 = 𝐵) |
168 | 166, 167 | ifbieq2d 4061 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐵 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) |
169 | 168 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑧 = 𝐵 → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) |
170 | 169 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑧 = 𝐵 → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))) |
171 | 170 | mpteq2dv 4673 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) |
172 | 171 | fveq2d 6107 |
. . . . . 6
⊢ (𝑧 = 𝐵 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))))) |
173 | 165, 172 | breq12d 4596 |
. . . . 5
⊢ (𝑧 = 𝐵 → ((𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝐵 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))))) |
174 | 173 | elrab 3331 |
. . . 4
⊢ (𝐵 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝐵 ∈ (𝐴[,]𝐵) ∧ (𝐵 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))))) |
175 | 164, 174 | sylib 207 |
. . 3
⊢ (𝜑 → (𝐵 ∈ (𝐴[,]𝐵) ∧ (𝐵 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))))) |
176 | 175 | simprd 478 |
. 2
⊢ (𝜑 → (𝐵 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))))) |
177 | 3, 55, 32, 176, 49 | letrd 10073 |
1
⊢ (𝜑 → (𝐵 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))))) |