Proof of Theorem ovolval5lem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nfv 1913 | . . 3
⊢
Ⅎ𝑛𝜑 | 
| 2 |  | nnex 12273 | . . . 4
⊢ ℕ
∈ V | 
| 3 | 2 | a1i 11 | . . 3
⊢ (𝜑 → ℕ ∈
V) | 
| 4 |  | volf 25565 | . . . . 5
⊢ vol:dom
vol⟶(0[,]+∞) | 
| 5 | 4 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → vol:dom
vol⟶(0[,]+∞)) | 
| 6 |  | ioombl 25601 | . . . . 5
⊢ ((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵) ∈ dom vol | 
| 7 | 6 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵) ∈ dom vol) | 
| 8 | 5, 7 | ffvelcdmd 7104 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ∈ (0[,]+∞)) | 
| 9 | 1, 3, 8 | sge0xrclmpt 46448 | . 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)))) ∈
ℝ*) | 
| 10 |  | 0xr 11309 | . . . . 5
⊢ 0 ∈
ℝ* | 
| 11 | 10 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ∈
ℝ*) | 
| 12 |  | pnfxr 11316 | . . . . 5
⊢ +∞
∈ ℝ* | 
| 13 | 12 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → +∞ ∈
ℝ*) | 
| 14 |  | ovolval5lem1.a | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℝ) | 
| 15 |  | ovolval5lem1.b | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℝ) | 
| 16 |  | volicore 46601 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(vol‘(𝐴[,)𝐵)) ∈
ℝ) | 
| 17 | 14, 15, 16 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐴[,)𝐵)) ∈ ℝ) | 
| 18 |  | ovolval5lem1.w | . . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈
ℝ+) | 
| 19 | 18 | rpred 13078 | . . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ ℝ) | 
| 20 | 19 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑊 ∈ ℝ) | 
| 21 |  | 2nn 12340 | . . . . . . . . . . 11
⊢ 2 ∈
ℕ | 
| 22 | 21 | a1i 11 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 2 ∈
ℕ) | 
| 23 |  | nnnn0 12535 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) | 
| 24 |  | nnexpcl 14116 | . . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) | 
| 25 | 22, 23, 24 | syl2anc 584 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℕ) | 
| 26 | 25 | nnred 12282 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℝ) | 
| 27 | 26 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈
ℝ) | 
| 28 | 25 | nnne0d 12317 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ≠
0) | 
| 29 | 28 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ≠ 0) | 
| 30 | 20, 27, 29 | redivcld 12096 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ) | 
| 31 | 17, 30 | readdcld 11291 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ) | 
| 32 | 31 | rexrd 11312 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈
ℝ*) | 
| 33 | 15 | rexrd 11312 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈
ℝ*) | 
| 34 |  | icombl 25600 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
→ (𝐴[,)𝐵) ∈ dom
vol) | 
| 35 | 14, 33, 34 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴[,)𝐵) ∈ dom vol) | 
| 36 |  | volge0 45981 | . . . . . 6
⊢ ((𝐴[,)𝐵) ∈ dom vol → 0 ≤
(vol‘(𝐴[,)𝐵))) | 
| 37 | 35, 36 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤
(vol‘(𝐴[,)𝐵))) | 
| 38 | 18 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑊 ∈
ℝ+) | 
| 39 | 25 | nnrpd 13076 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℝ+) | 
| 40 | 39 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈
ℝ+) | 
| 41 | 38, 40 | rpdivcld 13095 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈
ℝ+) | 
| 42 | 41 | rpge0d 13082 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (𝑊 / (2↑𝑛))) | 
| 43 | 17, 30, 37, 42 | addge0d 11840 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤
((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) | 
| 44 |  | rexr 11308 | . . . . . 6
⊢
(((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈
ℝ*) | 
| 45 | 12 | a1i 11 | . . . . . 6
⊢
(((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → +∞ ∈
ℝ*) | 
| 46 |  | ltpnf 13163 | . . . . . 6
⊢
(((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) < +∞) | 
| 47 | 44, 45, 46 | xrltled 13193 | . . . . 5
⊢
(((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ≤ +∞) | 
| 48 | 31, 47 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ≤ +∞) | 
| 49 | 11, 13, 32, 43, 48 | eliccxrd 45545 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ (0[,]+∞)) | 
| 50 | 1, 3, 49 | sge0xrclmpt 46448 | . 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) ∈
ℝ*) | 
| 51 | 5, 35 | ffvelcdmd 7104 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐴[,)𝐵)) ∈ (0[,]+∞)) | 
| 52 | 1, 3, 51 | sge0xrclmpt 46448 | . . 3
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) ∈
ℝ*) | 
| 53 | 19 | rexrd 11312 | . . 3
⊢ (𝜑 → 𝑊 ∈
ℝ*) | 
| 54 | 52, 53 | xaddcld 13344 | . 2
⊢ (𝜑 →
((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒 𝑊) ∈
ℝ*) | 
| 55 | 14, 30 | resubcld 11692 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 − (𝑊 / (2↑𝑛))) ∈ ℝ) | 
| 56 |  | volioore 46010 | . . . . . . . 8
⊢ (((𝐴 − (𝑊 / (2↑𝑛))) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0)) | 
| 57 | 55, 15, 56 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0)) | 
| 58 | 57 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0)) | 
| 59 |  | iftrue 4530 | . . . . . . 7
⊢ ((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵 → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = (𝐵 − (𝐴 − (𝑊 / (2↑𝑛))))) | 
| 60 | 59 | adantl 481 | . . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = (𝐵 − (𝐴 − (𝑊 / (2↑𝑛))))) | 
| 61 | 15 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℂ) | 
| 62 | 14 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℂ) | 
| 63 | 30 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℂ) | 
| 64 | 61, 62, 63 | subsubd 11649 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))) = ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛)))) | 
| 65 | 64 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))) = ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛)))) | 
| 66 | 58, 60, 65 | 3eqtrd 2780 | . . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛)))) | 
| 67 | 15, 14 | resubcld 11692 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 − 𝐴) ∈ ℝ) | 
| 68 | 14, 15 | sublevolico 46004 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 − 𝐴) ≤ (vol‘(𝐴[,)𝐵))) | 
| 69 | 67, 17, 30, 68 | leadd1dd 11878 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛))) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) | 
| 70 | 69 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛))) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) | 
| 71 | 66, 70 | eqbrtrd 5164 | . . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) | 
| 72 | 57 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0)) | 
| 73 |  | iffalse 4533 | . . . . . . 7
⊢ (¬
(𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵 → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = 0) | 
| 74 | 73 | adantl 481 | . . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = 0) | 
| 75 | 72, 74 | eqtrd 2776 | . . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = 0) | 
| 76 | 43 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → 0 ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) | 
| 77 | 75, 76 | eqbrtrd 5164 | . . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) | 
| 78 | 71, 77 | pm2.61dan 812 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) | 
| 79 | 1, 3, 8, 49, 78 | sge0lempt 46430 | . 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)))) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))))) | 
| 80 | 17, 30 | rexaddd 13277 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) +𝑒 (𝑊 / (2↑𝑛))) = ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) | 
| 81 | 80 | eqcomd 2742 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) = ((vol‘(𝐴[,)𝐵)) +𝑒 (𝑊 / (2↑𝑛)))) | 
| 82 | 81 | mpteq2dva 5241 | . . . . 5
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) = (𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) +𝑒 (𝑊 / (2↑𝑛))))) | 
| 83 | 82 | fveq2d 6909 | . . . 4
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) =
(Σ^‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) +𝑒 (𝑊 / (2↑𝑛)))))) | 
| 84 | 30 | rexrd 11312 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈
ℝ*) | 
| 85 |  | rexr 11308 | . . . . . . . 8
⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → (𝑊 / (2↑𝑛)) ∈
ℝ*) | 
| 86 | 12 | a1i 11 | . . . . . . . 8
⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → +∞ ∈
ℝ*) | 
| 87 |  | ltpnf 13163 | . . . . . . . 8
⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → (𝑊 / (2↑𝑛)) < +∞) | 
| 88 | 85, 86, 87 | xrltled 13193 | . . . . . . 7
⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → (𝑊 / (2↑𝑛)) ≤ +∞) | 
| 89 | 30, 88 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ≤ +∞) | 
| 90 | 11, 13, 84, 42, 89 | eliccxrd 45545 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ (0[,]+∞)) | 
| 91 | 1, 3, 51, 90 | sge0xadd 46455 | . . . 4
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) +𝑒 (𝑊 / (2↑𝑛))))) =
((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑊 / (2↑𝑛)))))) | 
| 92 | 10 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ*) | 
| 93 | 12 | a1i 11 | . . . . . . 7
⊢ (𝜑 → +∞ ∈
ℝ*) | 
| 94 | 18 | rpge0d 13082 | . . . . . . 7
⊢ (𝜑 → 0 ≤ 𝑊) | 
| 95 | 19 | ltpnfd 13164 | . . . . . . 7
⊢ (𝜑 → 𝑊 < +∞) | 
| 96 | 92, 93, 53, 94, 95 | elicod 13438 | . . . . . 6
⊢ (𝜑 → 𝑊 ∈ (0[,)+∞)) | 
| 97 | 96 | sge0ad2en 46451 | . . . . 5
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑊 / (2↑𝑛)))) = 𝑊) | 
| 98 | 97 | oveq2d 7448 | . . . 4
⊢ (𝜑 →
((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒
(Σ^‘(𝑛 ∈ ℕ ↦ (𝑊 / (2↑𝑛))))) =
((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒 𝑊)) | 
| 99 | 83, 91, 98 | 3eqtrd 2780 | . . 3
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) =
((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒 𝑊)) | 
| 100 | 50, 99 | xreqled 45346 | . 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) ≤
((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒 𝑊)) | 
| 101 | 9, 50, 54, 79, 100 | xrletrd 13205 | 1
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)))) ≤
((Σ^‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +𝑒 𝑊)) |