Proof of Theorem ovolval5lem1
Step | Hyp | Ref
| Expression |
1 | | nfv 1917 |
. . 3
⊢
Ⅎ𝑛𝜑 |
2 | | nnex 12089 |
. . . 4
⊢ ℕ
∈ V |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → ℕ ∈
V) |
4 | | volf 24803 |
. . . . 5
⊢ vol:dom
vol⟶(0[,]+∞) |
5 | 4 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → vol:dom
vol⟶(0[,]+∞)) |
6 | | ioombl 24839 |
. . . . 5
⊢ ((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵) ∈ dom vol |
7 | 6 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵) ∈ dom vol) |
8 | 5, 7 | ffvelcdmd 7027 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ∈ (0[,]+∞)) |
9 | 1, 3, 8 | sge0xrclmpt 44355 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)))) ∈
ℝ*) |
10 | | 0xr 11132 |
. . . . 5
⊢ 0 ∈
ℝ* |
11 | 10 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ∈
ℝ*) |
12 | | pnfxr 11139 |
. . . . 5
⊢ +∞
∈ ℝ* |
13 | 12 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → +∞ ∈
ℝ*) |
14 | | ovolval5lem1.a |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℝ) |
15 | | ovolval5lem1.b |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℝ) |
16 | | volicore 44508 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(vol‘(𝐴[,)𝐵)) ∈
ℝ) |
17 | 14, 15, 16 | syl2anc 585 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐴[,)𝐵)) ∈ ℝ) |
18 | | ovolval5lem1.w |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈
ℝ+) |
19 | 18 | rpred 12882 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ ℝ) |
20 | 19 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑊 ∈ ℝ) |
21 | | 2nn 12156 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
22 | 21 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 2 ∈
ℕ) |
23 | | nnnn0 12350 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
24 | | nnexpcl 13905 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) |
25 | 22, 23, 24 | syl2anc 585 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℕ) |
26 | 25 | nnred 12098 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℝ) |
27 | 26 | adantl 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈
ℝ) |
28 | 25 | nnne0d 12133 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ≠
0) |
29 | 28 | adantl 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ≠ 0) |
30 | 20, 27, 29 | redivcld 11913 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ) |
31 | 17, 30 | readdcld 11114 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ) |
32 | 31 | rexrd 11135 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈
ℝ*) |
33 | 15 | rexrd 11135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈
ℝ*) |
34 | | icombl 24838 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
→ (𝐴[,)𝐵) ∈ dom
vol) |
35 | 14, 33, 34 | syl2anc 585 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴[,)𝐵) ∈ dom vol) |
36 | | volge0 43890 |
. . . . . 6
⊢ ((𝐴[,)𝐵) ∈ dom vol → 0 ≤
(vol‘(𝐴[,)𝐵))) |
37 | 35, 36 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤
(vol‘(𝐴[,)𝐵))) |
38 | 18 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑊 ∈
ℝ+) |
39 | 25 | nnrpd 12880 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℝ+) |
40 | 39 | adantl 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈
ℝ+) |
41 | 38, 40 | rpdivcld 12899 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈
ℝ+) |
42 | 41 | rpge0d 12886 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (𝑊 / (2↑𝑛))) |
43 | 17, 30, 37, 42 | addge0d 11661 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤
((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) |
44 | | rexr 11131 |
. . . . . 6
⊢
(((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈
ℝ*) |
45 | 12 | a1i 11 |
. . . . . 6
⊢
(((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → +∞ ∈
ℝ*) |
46 | | ltpnf 12966 |
. . . . . 6
⊢
(((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) < +∞) |
47 | 44, 45, 46 | xrltled 12994 |
. . . . 5
⊢
(((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ≤ +∞) |
48 | 31, 47 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ≤ +∞) |
49 | 11, 13, 32, 43, 48 | eliccxrd 43453 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ (0[,]+∞)) |
50 | 1, 3, 49 | sge0xrclmpt 44355 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) ∈
ℝ*) |
51 | 5, 35 | ffvelcdmd 7027 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐴[,)𝐵)) ∈ (0[,]+∞)) |
52 | 1, 3, 51 | sge0xrclmpt 44355 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) ∈
ℝ*) |
53 | 19 | rexrd 11135 |
. . 3
⊢ (𝜑 → 𝑊 ∈
ℝ*) |
54 | 52, 53 | xaddcld 13145 |
. 2
⊢ (𝜑 →
((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒 𝑊) ∈
ℝ*) |
55 | 14, 30 | resubcld 11513 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 − (𝑊 / (2↑𝑛))) ∈ ℝ) |
56 | | volioore 43919 |
. . . . . . . 8
⊢ (((𝐴 − (𝑊 / (2↑𝑛))) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0)) |
57 | 55, 15, 56 | syl2anc 585 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0)) |
58 | 57 | adantr 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0)) |
59 | | iftrue 4487 |
. . . . . . 7
⊢ ((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵 → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = (𝐵 − (𝐴 − (𝑊 / (2↑𝑛))))) |
60 | 59 | adantl 483 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = (𝐵 − (𝐴 − (𝑊 / (2↑𝑛))))) |
61 | 15 | recnd 11113 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℂ) |
62 | 14 | recnd 11113 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℂ) |
63 | 30 | recnd 11113 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℂ) |
64 | 61, 62, 63 | subsubd 11470 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))) = ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛)))) |
65 | 64 | adantr 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))) = ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛)))) |
66 | 58, 60, 65 | 3eqtrd 2781 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛)))) |
67 | 15, 14 | resubcld 11513 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 − 𝐴) ∈ ℝ) |
68 | 14, 15 | sublevolico 43913 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 − 𝐴) ≤ (vol‘(𝐴[,)𝐵))) |
69 | 67, 17, 30, 68 | leadd1dd 11699 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛))) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) |
70 | 69 | adantr 482 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛))) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) |
71 | 66, 70 | eqbrtrd 5122 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) |
72 | 57 | adantr 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0)) |
73 | | iffalse 4490 |
. . . . . . 7
⊢ (¬
(𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵 → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = 0) |
74 | 73 | adantl 483 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = 0) |
75 | 72, 74 | eqtrd 2777 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = 0) |
76 | 43 | adantr 482 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → 0 ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) |
77 | 75, 76 | eqbrtrd 5122 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) |
78 | 71, 77 | pm2.61dan 811 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) |
79 | 1, 3, 8, 49, 78 | sge0lempt 44337 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)))) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))))) |
80 | 17, 30 | rexaddd 13078 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) +𝑒 (𝑊 / (2↑𝑛))) = ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) |
81 | 80 | eqcomd 2743 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) = ((vol‘(𝐴[,)𝐵)) +𝑒 (𝑊 / (2↑𝑛)))) |
82 | 81 | mpteq2dva 5200 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) = (𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) +𝑒 (𝑊 / (2↑𝑛))))) |
83 | 82 | fveq2d 6838 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) =
(Σ^‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) +𝑒 (𝑊 / (2↑𝑛)))))) |
84 | 30 | rexrd 11135 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈
ℝ*) |
85 | | rexr 11131 |
. . . . . . . 8
⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → (𝑊 / (2↑𝑛)) ∈
ℝ*) |
86 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → +∞ ∈
ℝ*) |
87 | | ltpnf 12966 |
. . . . . . . 8
⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → (𝑊 / (2↑𝑛)) < +∞) |
88 | 85, 86, 87 | xrltled 12994 |
. . . . . . 7
⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → (𝑊 / (2↑𝑛)) ≤ +∞) |
89 | 30, 88 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ≤ +∞) |
90 | 11, 13, 84, 42, 89 | eliccxrd 43453 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ (0[,]+∞)) |
91 | 1, 3, 51, 90 | sge0xadd 44362 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) +𝑒 (𝑊 / (2↑𝑛))))) =
((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑊 / (2↑𝑛)))))) |
92 | 10 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ*) |
93 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → +∞ ∈
ℝ*) |
94 | 18 | rpge0d 12886 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝑊) |
95 | 19 | ltpnfd 12967 |
. . . . . . 7
⊢ (𝜑 → 𝑊 < +∞) |
96 | 92, 93, 53, 94, 95 | elicod 13239 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ (0[,)+∞)) |
97 | 96 | sge0ad2en 44358 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑊 / (2↑𝑛)))) = 𝑊) |
98 | 97 | oveq2d 7362 |
. . . 4
⊢ (𝜑 →
((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑊 / (2↑𝑛))))) =
((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒 𝑊)) |
99 | 83, 91, 98 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) =
((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒 𝑊)) |
100 | 50, 99 | xreqled 43256 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) ≤
((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒 𝑊)) |
101 | 9, 50, 54, 79, 100 | xrletrd 13006 |
1
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)))) ≤
((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒 𝑊)) |