Step | Hyp | Ref
| Expression |
1 | | hoidmv1lelem3.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
2 | | hoidmv1lelem3.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 1, 2 | resubcld 10659 |
. 2
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
4 | | nnex 11227 |
. . . . . . 7
⊢ ℕ
∈ V |
5 | 4 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℕ ∈
V) |
6 | | icossicc 12465 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
7 | | 0xr 10287 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 0 ∈
ℝ*) |
9 | | pnfxr 10293 |
. . . . . . . . . 10
⊢ +∞
∈ ℝ* |
10 | 9 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → +∞ ∈
ℝ*) |
11 | | hoidmv1lelem3.c |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶:ℕ⟶ℝ) |
12 | 11 | ffvelrnda 6502 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ) |
13 | | hoidmv1lelem3.d |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷:ℕ⟶ℝ) |
14 | 13 | ffvelrnda 6502 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ) |
15 | 1 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐵 ∈ ℝ) |
16 | 14, 15 | ifcld 4268 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) ∈ ℝ) |
17 | | volicore 41309 |
. . . . . . . . . . 11
⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) ∈ ℝ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) ∈ ℝ) |
18 | 12, 16, 17 | syl2anc 565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) ∈ ℝ) |
19 | 18 | rexrd 10290 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) ∈
ℝ*) |
20 | 16 | rexrd 10290 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) ∈
ℝ*) |
21 | | icombl 23551 |
. . . . . . . . . . 11
⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) ∈ ℝ*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) ∈ dom vol) |
22 | 12, 20, 21 | syl2anc 565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) ∈ dom vol) |
23 | | volge0 40688 |
. . . . . . . . . 10
⊢ (((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) ∈ dom vol → 0 ≤
(vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 0 ≤
(vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))) |
25 | 18 | ltpnfd 12159 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) < +∞) |
26 | 8, 10, 19, 24, 25 | elicod 12428 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) ∈ (0[,)+∞)) |
27 | 6, 26 | sseldi 3748 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) ∈ (0[,]+∞)) |
28 | | eqid 2770 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ ↦
(vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))) |
29 | 27, 28 | fmptd 6527 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))):ℕ⟶(0[,]+∞)) |
30 | 5, 29 | sge0xrcl 41113 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) ∈
ℝ*) |
31 | 9 | a1i 11 |
. . . . 5
⊢ (𝜑 → +∞ ∈
ℝ*) |
32 | | hoidmv1lelem3.r |
. . . . . . 7
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ) |
33 | 32 | rexrd 10290 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈
ℝ*) |
34 | | nfv 1994 |
. . . . . . 7
⊢
Ⅎ𝑗𝜑 |
35 | | volf 23516 |
. . . . . . . . 9
⊢ vol:dom
vol⟶(0[,]+∞) |
36 | 35 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → vol:dom
vol⟶(0[,]+∞)) |
37 | 14 | rexrd 10290 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈
ℝ*) |
38 | | icombl 23551 |
. . . . . . . . 9
⊢ (((𝐶‘𝑗) ∈ ℝ ∧ (𝐷‘𝑗) ∈ ℝ*) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol) |
39 | 12, 37, 38 | syl2anc 565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol) |
40 | 36, 39 | ffvelrnd 6503 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∈ (0[,]+∞)) |
41 | 12 | rexrd 10290 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈
ℝ*) |
42 | 12 | leidd 10795 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ≤ (𝐶‘𝑗)) |
43 | | min1 12224 |
. . . . . . . . . 10
⊢ (((𝐷‘𝑗) ∈ ℝ ∧ 𝐵 ∈ ℝ) → if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) ≤ (𝐷‘𝑗)) |
44 | 14, 15, 43 | syl2anc 565 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) ≤ (𝐷‘𝑗)) |
45 | | icossico 12447 |
. . . . . . . . 9
⊢ ((((𝐶‘𝑗) ∈ ℝ* ∧ (𝐷‘𝑗) ∈ ℝ*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) ≤ (𝐷‘𝑗))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
46 | 41, 37, 42, 44, 45 | syl22anc 1476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
47 | | volss 23520 |
. . . . . . . 8
⊢ ((((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
48 | 22, 39, 46, 47 | syl3anc 1475 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
49 | 34, 5, 27, 40, 48 | sge0lempt 41138 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))))) |
50 | 32 | ltpnfd 12159 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) < +∞) |
51 | 30, 33, 31, 49, 50 | xrlelttrd 12195 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) < +∞) |
52 | 30, 31, 51 | xrltned 40083 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) ≠ +∞) |
53 | 52 | neneqd 2947 |
. . 3
⊢ (𝜑 → ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) = +∞) |
54 | 5, 29 | sge0repnf 41114 |
. . 3
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) ∈ ℝ ↔ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) = +∞)) |
55 | 53, 54 | mpbird 247 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) ∈ ℝ) |
56 | 1 | rexrd 10290 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
57 | 2, 1 | iccssred 40242 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
58 | | hoidmv1lelem3.u |
. . . . . . . . . . 11
⊢ 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} |
59 | | ssrab2 3834 |
. . . . . . . . . . 11
⊢ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ⊆ (𝐴[,]𝐵) |
60 | 58, 59 | eqsstri 3782 |
. . . . . . . . . 10
⊢ 𝑈 ⊆ (𝐴[,]𝐵) |
61 | | hoidmv1lelem3.l |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 < 𝐵) |
62 | | hoidmv1lelem3.s |
. . . . . . . . . . . 12
⊢ 𝑆 = sup(𝑈, ℝ, < ) |
63 | 2, 1, 61, 11, 13, 32, 58, 62 | hoidmv1lelem1 41319 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 ∈ 𝑈 ∧ 𝐴 ∈ 𝑈 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥)) |
64 | 63 | simp1d 1135 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ 𝑈) |
65 | 60, 64 | sseldi 3748 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ (𝐴[,]𝐵)) |
66 | 57, 65 | sseldd 3751 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℝ) |
67 | 66 | rexrd 10290 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈
ℝ*) |
68 | | simpl 468 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → 𝜑) |
69 | | simpr 471 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → ¬ 𝐵 ≤ 𝑆) |
70 | 68, 66 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → 𝑆 ∈ ℝ) |
71 | 68, 1 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → 𝐵 ∈ ℝ) |
72 | 70, 71 | ltnled 10385 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → (𝑆 < 𝐵 ↔ ¬ 𝐵 ≤ 𝑆)) |
73 | 69, 72 | mpbird 247 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → 𝑆 < 𝐵) |
74 | | hoidmv1lelem3.x |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴[,)𝐵) ⊆ ∪ 𝑗 ∈ ℕ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
75 | 74 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → (𝐴[,)𝐵) ⊆ ∪ 𝑗 ∈ ℕ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
76 | 2 | rexrd 10290 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
77 | 76 | adantr 466 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝐴 ∈
ℝ*) |
78 | 56 | adantr 466 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝐵 ∈
ℝ*) |
79 | 67 | adantr 466 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝑆 ∈
ℝ*) |
80 | 60, 57 | syl5ss 3761 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑈 ⊆ ℝ) |
81 | | ne0i 4067 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ∈ 𝑈 → 𝑈 ≠ ∅) |
82 | 64, 81 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑈 ≠ ∅) |
83 | 63 | simp3d 1137 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) |
84 | 63 | simp2d 1136 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
85 | | suprub 11185 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) ∧ 𝐴 ∈ 𝑈) → 𝐴 ≤ sup(𝑈, ℝ, < )) |
86 | 80, 82, 83, 84, 85 | syl31anc 1478 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ≤ sup(𝑈, ℝ, < )) |
87 | 86, 62 | syl6breqr 4826 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ≤ 𝑆) |
88 | 87 | adantr 466 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝐴 ≤ 𝑆) |
89 | | simpr 471 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝑆 < 𝐵) |
90 | 77, 78, 79, 88, 89 | elicod 12428 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝑆 ∈ (𝐴[,)𝐵)) |
91 | 75, 90 | sseldd 3751 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝑆 ∈ ∪
𝑗 ∈ ℕ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
92 | | eliun 4656 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ ∪ 𝑗 ∈ ℕ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ↔ ∃𝑗 ∈ ℕ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
93 | 91, 92 | sylib 208 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → ∃𝑗 ∈ ℕ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
94 | 2 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝐴 ∈ ℝ) |
95 | 94 | 3ad2ant1 1126 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝐴 ∈ ℝ) |
96 | 1 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝐵 ∈ ℝ) |
97 | 96 | 3ad2ant1 1126 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝐵 ∈ ℝ) |
98 | 11 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝐶:ℕ⟶ℝ) |
99 | 98 | 3ad2ant1 1126 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝐶:ℕ⟶ℝ) |
100 | 13 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝐷:ℕ⟶ℝ) |
101 | 100 | 3ad2ant1 1126 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝐷:ℕ⟶ℝ) |
102 | | fveq2 6332 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑗 → (𝐶‘𝑖) = (𝐶‘𝑗)) |
103 | | fveq2 6332 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑗 → (𝐷‘𝑖) = (𝐷‘𝑗)) |
104 | 102, 103 | oveq12d 6810 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑗 → ((𝐶‘𝑖)[,)(𝐷‘𝑖)) = ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
105 | 104 | fveq2d 6336 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑗 → (vol‘((𝐶‘𝑖)[,)(𝐷‘𝑖))) = (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
106 | 105 | cbvmptv 4882 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℕ ↦
(vol‘((𝐶‘𝑖)[,)(𝐷‘𝑖)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))) |
107 | 106 | fveq2i 6335 |
. . . . . . . . . . . . . . . 16
⊢
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)(𝐷‘𝑖))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) |
108 | 107, 32 | syl5eqel 2853 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)(𝐷‘𝑖))))) ∈ ℝ) |
109 | 108 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < 𝐵) →
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)(𝐷‘𝑖))))) ∈ ℝ) |
110 | 109 | 3ad2ant1 1126 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) →
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)(𝐷‘𝑖))))) ∈ ℝ) |
111 | 103 | breq1d 4794 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = 𝑗 → ((𝐷‘𝑖) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝑧)) |
112 | 111, 103 | ifbieq1d 4246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑗 → if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧) = if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) |
113 | 102, 112 | oveq12d 6810 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑗 → ((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) |
114 | 113 | fveq2d 6336 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑗 → (vol‘((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) |
115 | 114 | cbvmptv 4882 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ℕ ↦
(vol‘((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) |
116 | 115 | eqcomi 2779 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ ℕ ↦
(vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧)))) |
117 | 116 | fveq2i 6335 |
. . . . . . . . . . . . . . . 16
⊢
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) =
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧))))) |
118 | 117 | breq2i 4792 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝑧 − 𝐴) ≤
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧)))))) |
119 | 118 | rabbii 3334 |
. . . . . . . . . . . . . 14
⊢ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧)))))} |
120 | 58, 119 | eqtri 2792 |
. . . . . . . . . . . . 13
⊢ 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑖 ∈ ℕ ↦ (vol‘((𝐶‘𝑖)[,)if((𝐷‘𝑖) ≤ 𝑧, (𝐷‘𝑖), 𝑧)))))} |
121 | 64 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → 𝑆 ∈ 𝑈) |
122 | 121 | 3ad2ant1 1126 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝑆 ∈ 𝑈) |
123 | 88 | 3ad2ant1 1126 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝐴 ≤ 𝑆) |
124 | 89 | 3ad2ant1 1126 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝑆 < 𝐵) |
125 | | simp2 1130 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝑗 ∈ ℕ) |
126 | | simp3 1131 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
127 | | eqid 2770 |
. . . . . . . . . . . . 13
⊢ if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) = if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵) |
128 | 95, 97, 99, 101, 110, 120, 122, 123, 124, 125, 126, 127 | hoidmv1lelem2 41320 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑆 < 𝐵) ∧ 𝑗 ∈ ℕ ∧ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |
129 | 128 | 3exp 1111 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → (𝑗 ∈ ℕ → (𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢))) |
130 | 129 | rexlimdv 3177 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → (∃𝑗 ∈ ℕ 𝑆 ∈ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢)) |
131 | 93, 130 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 < 𝐵) → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |
132 | 68, 73, 131 | syl2anc 565 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |
133 | 57 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝐴[,]𝐵) ⊆ ℝ) |
134 | 60, 133 | syl5ss 3761 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑈 ⊆ ℝ) |
135 | 82 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑈 ≠ ∅) |
136 | 2, 1 | jca 495 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
137 | 136 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
138 | 60 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑈 ⊆ (𝐴[,]𝐵)) |
139 | 64 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑆 ∈ 𝑈) |
140 | | iccsupr 12471 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑈 ⊆ (𝐴[,]𝐵) ∧ 𝑆 ∈ 𝑈) → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥)) |
141 | 137, 138,
139, 140 | syl3anc 1475 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥)) |
142 | 141 | simp3d 1137 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) |
143 | | simpr 471 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝑈) |
144 | | suprub 11185 |
. . . . . . . . . . . . . 14
⊢ (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) ∧ 𝑢 ∈ 𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < )) |
145 | 134, 135,
142, 143, 144 | syl31anc 1478 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ≤ sup(𝑈, ℝ, < )) |
146 | 145, 62 | syl6breqr 4826 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ≤ 𝑆) |
147 | 146 | ralrimiva 3114 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑢 ∈ 𝑈 𝑢 ≤ 𝑆) |
148 | 60 | sseli 3746 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ 𝑈 → 𝑢 ∈ (𝐴[,]𝐵)) |
149 | 148 | adantl 467 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ (𝐴[,]𝐵)) |
150 | 133, 149 | sseldd 3751 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ ℝ) |
151 | 66 | adantr 466 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑆 ∈ ℝ) |
152 | 150, 151 | lenltd 10384 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 ≤ 𝑆 ↔ ¬ 𝑆 < 𝑢)) |
153 | 152 | ralbidva 3133 |
. . . . . . . . . . 11
⊢ (𝜑 → (∀𝑢 ∈ 𝑈 𝑢 ≤ 𝑆 ↔ ∀𝑢 ∈ 𝑈 ¬ 𝑆 < 𝑢)) |
154 | 147, 153 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑢 ∈ 𝑈 ¬ 𝑆 < 𝑢) |
155 | | ralnex 3140 |
. . . . . . . . . 10
⊢
(∀𝑢 ∈
𝑈 ¬ 𝑆 < 𝑢 ↔ ¬ ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |
156 | 154, 155 | sylib 208 |
. . . . . . . . 9
⊢ (𝜑 → ¬ ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |
157 | 156 | adantr 466 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐵 ≤ 𝑆) → ¬ ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |
158 | 132, 157 | condan 801 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ≤ 𝑆) |
159 | | iccleub 12433 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑆
∈ (𝐴[,]𝐵)) → 𝑆 ≤ 𝐵) |
160 | 76, 56, 65, 159 | syl3anc 1475 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ≤ 𝐵) |
161 | 56, 67, 158, 160 | xrletrid 12190 |
. . . . . 6
⊢ (𝜑 → 𝐵 = 𝑆) |
162 | 161, 64 | eqeltrd 2849 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑈) |
163 | 162, 58 | syl6eleq 2859 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))}) |
164 | | oveq1 6799 |
. . . . . 6
⊢ (𝑧 = 𝐵 → (𝑧 − 𝐴) = (𝐵 − 𝐴)) |
165 | | breq2 4788 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐵 → ((𝐷‘𝑗) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝐵)) |
166 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐵 → 𝑧 = 𝐵) |
167 | 165, 166 | ifbieq2d 4248 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐵 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)) |
168 | 167 | oveq2d 6808 |
. . . . . . . . 9
⊢ (𝑧 = 𝐵 → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))) |
169 | 168 | fveq2d 6336 |
. . . . . . . 8
⊢ (𝑧 = 𝐵 → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))) |
170 | 169 | mpteq2dv 4877 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))) |
171 | 170 | fveq2d 6336 |
. . . . . 6
⊢ (𝑧 = 𝐵 →
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))))) |
172 | 164, 171 | breq12d 4797 |
. . . . 5
⊢ (𝑧 = 𝐵 → ((𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝐵 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))))) |
173 | 172 | elrab 3513 |
. . . 4
⊢ (𝐵 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝐵 ∈ (𝐴[,]𝐵) ∧ (𝐵 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))))) |
174 | 163, 173 | sylib 208 |
. . 3
⊢ (𝜑 → (𝐵 ∈ (𝐴[,]𝐵) ∧ (𝐵 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵))))))) |
175 | 174 | simprd 477 |
. 2
⊢ (𝜑 → (𝐵 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐵, (𝐷‘𝑗), 𝐵)))))) |
176 | 3, 55, 32, 175, 49 | letrd 10395 |
1
⊢ (𝜑 → (𝐵 − 𝐴) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗)))))) |