Metamath Proof Explorer

Theorem ovolval5lem1

Description: |- ( ph -> ( sum^( n e. NN |-> ( vol( ( A - ( W / ( 2 ^ n ) ) ) (,) B ) ) ) ) <_ ( ( sum^( n e. NN |-> ( vol( A [,) B ) ) ) ) +e W ) ) . (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovolval5lem1.a ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ℝ )
ovolval5lem1.b ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐵 ∈ ℝ )
ovolval5lem1.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ+ )
ovolval5lem1.c ⊢ 𝐶 = { 𝑛 ∈ ℕ ∣ 𝐴 < 𝐵 }
Assertion ovolval5lem1 ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ) ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ) ) +𝑒 𝑊 ) )

Proof

Step Hyp Ref Expression
1 ovolval5lem1.a ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ℝ )
2 ovolval5lem1.b ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐵 ∈ ℝ )
3 ovolval5lem1.w ⊢ ( 𝜑 → 𝑊 ∈ ℝ+ )
4 ovolval5lem1.c ⊢ 𝐶 = { 𝑛 ∈ ℕ ∣ 𝐴 < 𝐵 }
5 nfv ⊢ Ⅎ 𝑛 𝜑
6 nnex ⊢ ℕ ∈ V
7 6 a1i ⊢ ( 𝜑 → ℕ ∈ V )
8 volf ⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
9 8 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → vol : dom vol ⟶ ( 0 [,] +∞ ) )
10 ioombl ⊢ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ∈ dom vol
11 10 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ∈ dom vol )
12 9 11 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
13 5 7 12 sge0xrclmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ) ) ) ∈ ℝ* )
14 0xr ⊢ 0 ∈ ℝ*
15 14 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ∈ ℝ* )
16 pnfxr ⊢ +∞ ∈ ℝ*
17 16 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → +∞ ∈ ℝ* )
18 volicore ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ∈ ℝ )
19 1 2 18 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ∈ ℝ )
20 3 rpred ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑊 ∈ ℝ )
22 2nn ⊢ 2 ∈ ℕ
23 22 a1i ⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℕ )
24 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
25 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
26 23 24 25 syl2anc ⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℕ )
27 26 nnred ⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℝ )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 ↑ 𝑛 ) ∈ ℝ )
29 26 nnne0d ⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ≠ 0 )
30 29 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 ↑ 𝑛 ) ≠ 0 )
31 21 28 30 redivcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑊 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
32 19 31 readdcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
33 32 rexrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ* )
34 2 rexrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐵 ∈ ℝ* )
35 icombl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )
36 1 34 35 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 [,) 𝐵 ) ∈ dom vol )
37 volge0 ⊢ ( ( 𝐴 [,) 𝐵 ) ∈ dom vol → 0 ≤ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
38 36 37 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
39 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑊 ∈ ℝ+ )
40 26 nnrpd ⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℝ+ )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 ↑ 𝑛 ) ∈ ℝ+ )
42 39 41 rpdivcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑊 / ( 2 ↑ 𝑛 ) ) ∈ ℝ+ )
43 42 rpge0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( 𝑊 / ( 2 ↑ 𝑛 ) ) )
44 19 31 38 43 addge0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
45 rexr ⊢ ( ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ → ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ* )
46 16 a1i ⊢ ( ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ → +∞ ∈ ℝ* )
47 ltpnf ⊢ ( ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ → ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) < +∞ )
48 45 46 47 xrltled ⊢ ( ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ → ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ +∞ )
49 32 48 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ +∞ )
50 15 17 33 44 49 eliccxrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ∈ ( 0 [,] +∞ ) )
51 5 7 50 sge0xrclmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) ) ∈ ℝ* )
52 9 36 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
53 5 7 52 sge0xrclmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ) ) ∈ ℝ* )
54 20 rexrd ⊢ ( 𝜑 → 𝑊 ∈ ℝ* )
55 53 54 xaddcld ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ) ) +𝑒 𝑊 ) ∈ ℝ* )
56 1 31 resubcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
57 volioore ⊢ ( ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ) = if ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 , ( 𝐵 − ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) , 0 ) )
58 56 2 57 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ) = if ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 , ( 𝐵 − ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) , 0 ) )
59 58 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 ) → ( vol ‘ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ) = if ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 , ( 𝐵 − ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) , 0 ) )
60 iftrue ⊢ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 → if ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 , ( 𝐵 − ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) , 0 ) = ( 𝐵 − ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) )
61 60 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 ) → if ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 , ( 𝐵 − ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) , 0 ) = ( 𝐵 − ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) )
62 2 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐵 ∈ ℂ )
63 1 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ℂ )
64 31 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑊 / ( 2 ↑ 𝑛 ) ) ∈ ℂ )
65 62 63 64 subsubd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐵 − ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) = ( ( 𝐵 − 𝐴 ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
66 65 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 ) → ( 𝐵 − ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) = ( ( 𝐵 − 𝐴 ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
67 59 61 66 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 ) → ( vol ‘ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ) = ( ( 𝐵 − 𝐴 ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
68 2 1 resubcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
69 1 2 sublevolico ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐵 − 𝐴 ) ≤ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) )
70 68 19 31 69 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐵 − 𝐴 ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
71 70 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 ) → ( ( 𝐵 − 𝐴 ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
72 67 71 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 ) → ( vol ‘ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ) ≤ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
73 58 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 ) → ( vol ‘ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ) = if ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 , ( 𝐵 − ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) , 0 ) )
74 iffalse ⊢ ( ¬ ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 → if ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 , ( 𝐵 − ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) , 0 ) = 0 )
75 74 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 ) → if ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 , ( 𝐵 − ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) , 0 ) = 0 )
76 73 75 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 ) → ( vol ‘ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ) = 0 )
77 44 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 ) → 0 ≤ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
78 76 77 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ¬ ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ≤ 𝐵 ) → ( vol ‘ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ) ≤ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
79 72 78 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( vol ‘ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ) ≤ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
80 5 7 12 50 79 sge0lempt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ) ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) ) )
81 19 31 rexaddd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) +𝑒 ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) = ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
82 81 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) = ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) +𝑒 ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) )
83 82 mpteq2dva ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) +𝑒 ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) )
84 83 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) +𝑒 ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) ) )
85 31 rexrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑊 / ( 2 ↑ 𝑛 ) ) ∈ ℝ* )
86 rexr ⊢ ( ( 𝑊 / ( 2 ↑ 𝑛 ) ) ∈ ℝ → ( 𝑊 / ( 2 ↑ 𝑛 ) ) ∈ ℝ* )
87 16 a1i ⊢ ( ( 𝑊 / ( 2 ↑ 𝑛 ) ) ∈ ℝ → +∞ ∈ ℝ* )
88 ltpnf ⊢ ( ( 𝑊 / ( 2 ↑ 𝑛 ) ) ∈ ℝ → ( 𝑊 / ( 2 ↑ 𝑛 ) ) < +∞ )
89 86 87 88 xrltled ⊢ ( ( 𝑊 / ( 2 ↑ 𝑛 ) ) ∈ ℝ → ( 𝑊 / ( 2 ↑ 𝑛 ) ) ≤ +∞ )
90 31 89 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑊 / ( 2 ↑ 𝑛 ) ) ≤ +∞ )
91 15 17 85 43 90 eliccxrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑊 / ( 2 ↑ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
92 5 7 52 91 sge0xadd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) +𝑒 ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ) ) +𝑒 ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) ) )
93 14 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
94 16 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
95 3 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝑊 )
96 20 ltpnfd ⊢ ( 𝜑 → 𝑊 < +∞ )
97 93 94 54 95 96 elicod ⊢ ( 𝜑 → 𝑊 ∈ ( 0 [,) +∞ ) )
98 97 sge0ad2en ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) = 𝑊 )
99 98 oveq2d ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ) ) +𝑒 ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ) ) +𝑒 𝑊 ) )
100 84 92 99 3eqtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) ) = ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ) ) +𝑒 𝑊 ) )
101 51 100 xreqled ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( vol ‘ ( 𝐴 [,) 𝐵 ) ) + ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ) ) +𝑒 𝑊 ) )
102 13 51 55 80 101 xrletrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( ( 𝐴 − ( 𝑊 / ( 2 ↑ 𝑛 ) ) ) (,) 𝐵 ) ) ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐴 [,) 𝐵 ) ) ) ) +𝑒 𝑊 ) )