Metamath Proof Explorer


Theorem ovollb2lem

Description: Lemma for ovollb2 . (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypotheses ovollb2.1 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
ovollb2.2 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ⟩ )
ovollb2.3 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
ovollb2.4 ( 𝜑𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
ovollb2.5 ( 𝜑𝐴 ran ( [,] ∘ 𝐹 ) )
ovollb2.6 ( 𝜑𝐵 ∈ ℝ+ )
ovollb2.7 ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ )
Assertion ovollb2lem ( 𝜑 → ( vol* ‘ 𝐴 ) ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ovollb2.1 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
2 ovollb2.2 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ⟩ )
3 ovollb2.3 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
4 ovollb2.4 ( 𝜑𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
5 ovollb2.5 ( 𝜑𝐴 ran ( [,] ∘ 𝐹 ) )
6 ovollb2.6 ( 𝜑𝐵 ∈ ℝ+ )
7 ovollb2.7 ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ )
8 ovolficcss ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ran ( [,] ∘ 𝐹 ) ⊆ ℝ )
9 4 8 syl ( 𝜑 ran ( [,] ∘ 𝐹 ) ⊆ ℝ )
10 5 9 sstrd ( 𝜑𝐴 ⊆ ℝ )
11 ovolcl ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) ∈ ℝ* )
12 10 11 syl ( 𝜑 → ( vol* ‘ 𝐴 ) ∈ ℝ* )
13 ovolfcl ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
14 4 13 sylan ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
15 14 simp1d ( ( 𝜑𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ )
16 6 rphalfcld ( 𝜑 → ( 𝐵 / 2 ) ∈ ℝ+ )
17 16 adantr ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐵 / 2 ) ∈ ℝ+ )
18 2nn 2 ∈ ℕ
19 nnnn0 ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
20 19 adantl ( ( 𝜑𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
21 nnexpcl ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
22 18 20 21 sylancr ( ( 𝜑𝑛 ∈ ℕ ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
23 22 nnrpd ( ( 𝜑𝑛 ∈ ℕ ) → ( 2 ↑ 𝑛 ) ∈ ℝ+ )
24 17 23 rpdivcld ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ+ )
25 24 rpred ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
26 15 25 resubcld ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
27 14 simp2d ( ( 𝜑𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ )
28 27 25 readdcld ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐹𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
29 15 24 ltsubrpd ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) < ( 1st ‘ ( 𝐹𝑛 ) ) )
30 14 simp3d ( ( 𝜑𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) )
31 27 24 ltaddrpd ( ( 𝜑𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐹𝑛 ) ) < ( ( 2nd ‘ ( 𝐹𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) )
32 15 27 28 30 31 lelttrd ( ( 𝜑𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐹𝑛 ) ) < ( ( 2nd ‘ ( 𝐹𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) )
33 26 15 28 29 32 lttrd ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) < ( ( 2nd ‘ ( 𝐹𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) )
34 26 28 33 ltled ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ≤ ( ( 2nd ‘ ( 𝐹𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) )
35 df-br ( ( ( 1st ‘ ( 𝐹𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ≤ ( ( 2nd ‘ ( 𝐹𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ↔ ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ⟩ ∈ ≤ )
36 34 35 sylib ( ( 𝜑𝑛 ∈ ℕ ) → ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ⟩ ∈ ≤ )
37 26 28 opelxpd ( ( 𝜑𝑛 ∈ ℕ ) → ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ⟩ ∈ ( ℝ × ℝ ) )
38 36 37 elind ( ( 𝜑𝑛 ∈ ℕ ) → ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
39 38 2 fmptd ( 𝜑𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
40 eqid ( ( abs ∘ − ) ∘ 𝐺 ) = ( ( abs ∘ − ) ∘ 𝐺 )
41 40 3 ovolsf ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) )
42 39 41 syl ( 𝜑𝑇 : ℕ ⟶ ( 0 [,) +∞ ) )
43 42 frnd ( 𝜑 → ran 𝑇 ⊆ ( 0 [,) +∞ ) )
44 icossxr ( 0 [,) +∞ ) ⊆ ℝ*
45 43 44 sstrdi ( 𝜑 → ran 𝑇 ⊆ ℝ* )
46 supxrcl ( ran 𝑇 ⊆ ℝ* → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ* )
47 45 46 syl ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ* )
48 6 rpred ( 𝜑𝐵 ∈ ℝ )
49 7 48 readdcld ( 𝜑 → ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) ∈ ℝ )
50 49 rexrd ( 𝜑 → ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) ∈ ℝ* )
51 2fveq3 ( 𝑛 = 𝑚 → ( 1st ‘ ( 𝐹𝑛 ) ) = ( 1st ‘ ( 𝐹𝑚 ) ) )
52 oveq2 ( 𝑛 = 𝑚 → ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑚 ) )
53 52 oveq2d ( 𝑛 = 𝑚 → ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) = ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) )
54 51 53 oveq12d ( 𝑛 = 𝑚 → ( ( 1st ‘ ( 𝐹𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) = ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) )
55 2fveq3 ( 𝑛 = 𝑚 → ( 2nd ‘ ( 𝐹𝑛 ) ) = ( 2nd ‘ ( 𝐹𝑚 ) ) )
56 55 53 oveq12d ( 𝑛 = 𝑚 → ( ( 2nd ‘ ( 𝐹𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) = ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) )
57 54 56 opeq12d ( 𝑛 = 𝑚 → ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ⟩ = ⟨ ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ )
58 opex ⟨ ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ ∈ V
59 57 2 58 fvmpt ( 𝑚 ∈ ℕ → ( 𝐺𝑚 ) = ⟨ ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ )
60 59 adantl ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝐺𝑚 ) = ⟨ ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ )
61 60 fveq2d ( ( 𝜑𝑚 ∈ ℕ ) → ( 1st ‘ ( 𝐺𝑚 ) ) = ( 1st ‘ ⟨ ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ ) )
62 ovex ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ∈ V
63 ovex ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ∈ V
64 62 63 op1st ( 1st ‘ ⟨ ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ ) = ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) )
65 61 64 eqtrdi ( ( 𝜑𝑚 ∈ ℕ ) → ( 1st ‘ ( 𝐺𝑚 ) ) = ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) )
66 ovolfcl ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑚 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹𝑚 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹𝑚 ) ) ≤ ( 2nd ‘ ( 𝐹𝑚 ) ) ) )
67 4 66 sylan ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑚 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹𝑚 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹𝑚 ) ) ≤ ( 2nd ‘ ( 𝐹𝑚 ) ) ) )
68 67 simp1d ( ( 𝜑𝑚 ∈ ℕ ) → ( 1st ‘ ( 𝐹𝑚 ) ) ∈ ℝ )
69 16 adantr ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝐵 / 2 ) ∈ ℝ+ )
70 nnnn0 ( 𝑚 ∈ ℕ → 𝑚 ∈ ℕ0 )
71 70 adantl ( ( 𝜑𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ0 )
72 nnexpcl ( ( 2 ∈ ℕ ∧ 𝑚 ∈ ℕ0 ) → ( 2 ↑ 𝑚 ) ∈ ℕ )
73 18 71 72 sylancr ( ( 𝜑𝑚 ∈ ℕ ) → ( 2 ↑ 𝑚 ) ∈ ℕ )
74 73 nnrpd ( ( 𝜑𝑚 ∈ ℕ ) → ( 2 ↑ 𝑚 ) ∈ ℝ+ )
75 69 74 rpdivcld ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ∈ ℝ+ )
76 68 75 ltsubrpd ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) < ( 1st ‘ ( 𝐹𝑚 ) ) )
77 65 76 eqbrtrd ( ( 𝜑𝑚 ∈ ℕ ) → ( 1st ‘ ( 𝐺𝑚 ) ) < ( 1st ‘ ( 𝐹𝑚 ) ) )
78 77 adantlr ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 1st ‘ ( 𝐺𝑚 ) ) < ( 1st ‘ ( 𝐹𝑚 ) ) )
79 ovolfcl ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺𝑚 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺𝑚 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺𝑚 ) ) ≤ ( 2nd ‘ ( 𝐺𝑚 ) ) ) )
80 39 79 sylan ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺𝑚 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺𝑚 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐺𝑚 ) ) ≤ ( 2nd ‘ ( 𝐺𝑚 ) ) ) )
81 80 simp1d ( ( 𝜑𝑚 ∈ ℕ ) → ( 1st ‘ ( 𝐺𝑚 ) ) ∈ ℝ )
82 81 adantlr ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 1st ‘ ( 𝐺𝑚 ) ) ∈ ℝ )
83 68 adantlr ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 1st ‘ ( 𝐹𝑚 ) ) ∈ ℝ )
84 10 sselda ( ( 𝜑𝑧𝐴 ) → 𝑧 ∈ ℝ )
85 84 adantr ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑚 ∈ ℕ ) → 𝑧 ∈ ℝ )
86 ltletr ( ( ( 1st ‘ ( 𝐺𝑚 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹𝑚 ) ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( ( 1st ‘ ( 𝐺𝑚 ) ) < ( 1st ‘ ( 𝐹𝑚 ) ) ∧ ( 1st ‘ ( 𝐹𝑚 ) ) ≤ 𝑧 ) → ( 1st ‘ ( 𝐺𝑚 ) ) < 𝑧 ) )
87 82 83 85 86 syl3anc ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 1st ‘ ( 𝐺𝑚 ) ) < ( 1st ‘ ( 𝐹𝑚 ) ) ∧ ( 1st ‘ ( 𝐹𝑚 ) ) ≤ 𝑧 ) → ( 1st ‘ ( 𝐺𝑚 ) ) < 𝑧 ) )
88 78 87 mpand ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑚 ) ) ≤ 𝑧 → ( 1st ‘ ( 𝐺𝑚 ) ) < 𝑧 ) )
89 67 simp2d ( ( 𝜑𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝐹𝑚 ) ) ∈ ℝ )
90 89 75 ltaddrpd ( ( 𝜑𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝐹𝑚 ) ) < ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) )
91 60 fveq2d ( ( 𝜑𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝐺𝑚 ) ) = ( 2nd ‘ ⟨ ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ ) )
92 62 63 op2nd ( 2nd ‘ ⟨ ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ ) = ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) )
93 91 92 eqtrdi ( ( 𝜑𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝐺𝑚 ) ) = ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) )
94 90 93 breqtrrd ( ( 𝜑𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝐹𝑚 ) ) < ( 2nd ‘ ( 𝐺𝑚 ) ) )
95 94 adantlr ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝐹𝑚 ) ) < ( 2nd ‘ ( 𝐺𝑚 ) ) )
96 89 adantlr ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝐹𝑚 ) ) ∈ ℝ )
97 80 simp2d ( ( 𝜑𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝐺𝑚 ) ) ∈ ℝ )
98 97 adantlr ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝐺𝑚 ) ) ∈ ℝ )
99 lelttr ( ( 𝑧 ∈ ℝ ∧ ( 2nd ‘ ( 𝐹𝑚 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐺𝑚 ) ) ∈ ℝ ) → ( ( 𝑧 ≤ ( 2nd ‘ ( 𝐹𝑚 ) ) ∧ ( 2nd ‘ ( 𝐹𝑚 ) ) < ( 2nd ‘ ( 𝐺𝑚 ) ) ) → 𝑧 < ( 2nd ‘ ( 𝐺𝑚 ) ) ) )
100 85 96 98 99 syl3anc ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑧 ≤ ( 2nd ‘ ( 𝐹𝑚 ) ) ∧ ( 2nd ‘ ( 𝐹𝑚 ) ) < ( 2nd ‘ ( 𝐺𝑚 ) ) ) → 𝑧 < ( 2nd ‘ ( 𝐺𝑚 ) ) ) )
101 95 100 mpan2d ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑧 ≤ ( 2nd ‘ ( 𝐹𝑚 ) ) → 𝑧 < ( 2nd ‘ ( 𝐺𝑚 ) ) ) )
102 88 101 anim12d ( ( ( 𝜑𝑧𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 1st ‘ ( 𝐹𝑚 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑚 ) ) ) → ( ( 1st ‘ ( 𝐺𝑚 ) ) < 𝑧𝑧 < ( 2nd ‘ ( 𝐺𝑚 ) ) ) ) )
103 102 reximdva ( ( 𝜑𝑧𝐴 ) → ( ∃ 𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑚 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑚 ) ) ) → ∃ 𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐺𝑚 ) ) < 𝑧𝑧 < ( 2nd ‘ ( 𝐺𝑚 ) ) ) ) )
104 103 ralimdva ( 𝜑 → ( ∀ 𝑧𝐴𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑚 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑚 ) ) ) → ∀ 𝑧𝐴𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐺𝑚 ) ) < 𝑧𝑧 < ( 2nd ‘ ( 𝐺𝑚 ) ) ) ) )
105 ovolficc ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ran ( [,] ∘ 𝐹 ) ↔ ∀ 𝑧𝐴𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑚 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑚 ) ) ) ) )
106 10 4 105 syl2anc ( 𝜑 → ( 𝐴 ran ( [,] ∘ 𝐹 ) ↔ ∀ 𝑧𝐴𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑚 ) ) ≤ 𝑧𝑧 ≤ ( 2nd ‘ ( 𝐹𝑚 ) ) ) ) )
107 ovolfioo ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ran ( (,) ∘ 𝐺 ) ↔ ∀ 𝑧𝐴𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐺𝑚 ) ) < 𝑧𝑧 < ( 2nd ‘ ( 𝐺𝑚 ) ) ) ) )
108 10 39 107 syl2anc ( 𝜑 → ( 𝐴 ran ( (,) ∘ 𝐺 ) ↔ ∀ 𝑧𝐴𝑚 ∈ ℕ ( ( 1st ‘ ( 𝐺𝑚 ) ) < 𝑧𝑧 < ( 2nd ‘ ( 𝐺𝑚 ) ) ) ) )
109 104 106 108 3imtr4d ( 𝜑 → ( 𝐴 ran ( [,] ∘ 𝐹 ) → 𝐴 ran ( (,) ∘ 𝐺 ) ) )
110 5 109 mpd ( 𝜑𝐴 ran ( (,) ∘ 𝐺 ) )
111 3 ovollb ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ran ( (,) ∘ 𝐺 ) ) → ( vol* ‘ 𝐴 ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
112 39 110 111 syl2anc ( 𝜑 → ( vol* ‘ 𝐴 ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
113 3 fveq1i ( 𝑇𝑘 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑘 )
114 fzfid ( ( 𝜑𝑘 ∈ ℕ ) → ( 1 ... 𝑘 ) ∈ Fin )
115 rge0ssre ( 0 [,) +∞ ) ⊆ ℝ
116 eqid ( ( abs ∘ − ) ∘ 𝐹 ) = ( ( abs ∘ − ) ∘ 𝐹 )
117 116 ovolfsf ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ( 0 [,) +∞ ) )
118 4 117 syl ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ( 0 [,) +∞ ) )
119 118 adantr ( ( 𝜑𝑘 ∈ ℕ ) → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ( 0 [,) +∞ ) )
120 elfznn ( 𝑚 ∈ ( 1 ... 𝑘 ) → 𝑚 ∈ ℕ )
121 ffvelrn ( ( ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ( 0 [,) +∞ ) ∧ 𝑚 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) ∈ ( 0 [,) +∞ ) )
122 119 120 121 syl2an ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) ∈ ( 0 [,) +∞ ) )
123 115 122 sselid ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) ∈ ℝ )
124 123 recnd ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) ∈ ℂ )
125 6 adantr ( ( 𝜑𝑚 ∈ ℕ ) → 𝐵 ∈ ℝ+ )
126 125 74 rpdivcld ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝐵 / ( 2 ↑ 𝑚 ) ) ∈ ℝ+ )
127 126 rpcnd ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝐵 / ( 2 ↑ 𝑚 ) ) ∈ ℂ )
128 120 127 sylan2 ( ( 𝜑𝑚 ∈ ( 1 ... 𝑘 ) ) → ( 𝐵 / ( 2 ↑ 𝑚 ) ) ∈ ℂ )
129 128 adantlr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( 𝐵 / ( 2 ↑ 𝑚 ) ) ∈ ℂ )
130 114 124 129 fsumadd ( ( 𝜑𝑘 ∈ ℕ ) → Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) + Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) )
131 40 ovolfsval ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑚 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑚 ) = ( ( 2nd ‘ ( 𝐺𝑚 ) ) − ( 1st ‘ ( 𝐺𝑚 ) ) ) )
132 39 131 sylan ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑚 ) = ( ( 2nd ‘ ( 𝐺𝑚 ) ) − ( 1st ‘ ( 𝐺𝑚 ) ) ) )
133 89 recnd ( ( 𝜑𝑚 ∈ ℕ ) → ( 2nd ‘ ( 𝐹𝑚 ) ) ∈ ℂ )
134 75 rpcnd ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ∈ ℂ )
135 68 recnd ( ( 𝜑𝑚 ∈ ℕ ) → ( 1st ‘ ( 𝐹𝑚 ) ) ∈ ℂ )
136 135 134 subcld ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ∈ ℂ )
137 133 134 136 addsubassd ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) − ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ) = ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) − ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ) ) )
138 93 65 oveq12d ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐺𝑚 ) ) − ( 1st ‘ ( 𝐺𝑚 ) ) ) = ( ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) − ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ) )
139 133 135 127 subadd23d ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( 2nd ‘ ( 𝐹𝑚 ) ) − ( 1st ‘ ( 𝐹𝑚 ) ) ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) = ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / ( 2 ↑ 𝑚 ) ) − ( 1st ‘ ( 𝐹𝑚 ) ) ) ) )
140 116 ovolfsval ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑚 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) = ( ( 2nd ‘ ( 𝐹𝑚 ) ) − ( 1st ‘ ( 𝐹𝑚 ) ) ) )
141 4 140 sylan ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) = ( ( 2nd ‘ ( 𝐹𝑚 ) ) − ( 1st ‘ ( 𝐹𝑚 ) ) ) )
142 141 oveq1d ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) = ( ( ( 2nd ‘ ( 𝐹𝑚 ) ) − ( 1st ‘ ( 𝐹𝑚 ) ) ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) )
143 134 135 134 subsub3d ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) − ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ) = ( ( ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) − ( 1st ‘ ( 𝐹𝑚 ) ) ) )
144 69 rpcnd ( ( 𝜑𝑚 ∈ ℕ ) → ( 𝐵 / 2 ) ∈ ℂ )
145 73 nncnd ( ( 𝜑𝑚 ∈ ℕ ) → ( 2 ↑ 𝑚 ) ∈ ℂ )
146 73 nnne0d ( ( 𝜑𝑚 ∈ ℕ ) → ( 2 ↑ 𝑚 ) ≠ 0 )
147 144 144 145 146 divdird ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( 𝐵 / 2 ) + ( 𝐵 / 2 ) ) / ( 2 ↑ 𝑚 ) ) = ( ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) )
148 125 rpcnd ( ( 𝜑𝑚 ∈ ℕ ) → 𝐵 ∈ ℂ )
149 148 2halvesd ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝐵 / 2 ) + ( 𝐵 / 2 ) ) = 𝐵 )
150 149 oveq1d ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( 𝐵 / 2 ) + ( 𝐵 / 2 ) ) / ( 2 ↑ 𝑚 ) ) = ( 𝐵 / ( 2 ↑ 𝑚 ) ) )
151 147 150 eqtr3d ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) = ( 𝐵 / ( 2 ↑ 𝑚 ) ) )
152 151 oveq1d ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) − ( 1st ‘ ( 𝐹𝑚 ) ) ) = ( ( 𝐵 / ( 2 ↑ 𝑚 ) ) − ( 1st ‘ ( 𝐹𝑚 ) ) ) )
153 143 152 eqtrd ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) − ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ) = ( ( 𝐵 / ( 2 ↑ 𝑚 ) ) − ( 1st ‘ ( 𝐹𝑚 ) ) ) )
154 153 oveq2d ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) − ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ) ) = ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( 𝐵 / ( 2 ↑ 𝑚 ) ) − ( 1st ‘ ( 𝐹𝑚 ) ) ) ) )
155 139 142 154 3eqtr4d ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) = ( ( 2nd ‘ ( 𝐹𝑚 ) ) + ( ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) − ( ( 1st ‘ ( 𝐹𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ) ) )
156 137 138 155 3eqtr4d ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐺𝑚 ) ) − ( 1st ‘ ( 𝐺𝑚 ) ) ) = ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) )
157 132 156 eqtrd ( ( 𝜑𝑚 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑚 ) = ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) )
158 120 157 sylan2 ( ( 𝜑𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑚 ) = ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) )
159 158 adantlr ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑚 ) = ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) )
160 simpr ( ( 𝜑𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
161 nnuz ℕ = ( ℤ ‘ 1 )
162 160 161 eleqtrdi ( ( 𝜑𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ ‘ 1 ) )
163 124 129 addcld ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) ∈ ℂ )
164 159 162 163 fsumser ( ( 𝜑𝑘 ∈ ℕ ) → Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑘 ) )
165 eqidd ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑚 ∈ ( 1 ... 𝑘 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) = ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) )
166 165 162 124 fsumser ( ( 𝜑𝑘 ∈ ℕ ) → Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑘 ) )
167 1 fveq1i ( 𝑆𝑘 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑘 )
168 166 167 eqtr4di ( ( 𝜑𝑘 ∈ ℕ ) → Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) = ( 𝑆𝑘 ) )
169 6 adantr ( ( 𝜑𝑘 ∈ ℕ ) → 𝐵 ∈ ℝ+ )
170 169 rpcnd ( ( 𝜑𝑘 ∈ ℕ ) → 𝐵 ∈ ℂ )
171 geo2sum ( ( 𝑘 ∈ ℕ ∧ 𝐵 ∈ ℂ ) → Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( 𝐵 / ( 2 ↑ 𝑚 ) ) = ( 𝐵 − ( 𝐵 / ( 2 ↑ 𝑘 ) ) ) )
172 160 170 171 syl2anc ( ( 𝜑𝑘 ∈ ℕ ) → Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( 𝐵 / ( 2 ↑ 𝑚 ) ) = ( 𝐵 − ( 𝐵 / ( 2 ↑ 𝑘 ) ) ) )
173 168 172 oveq12d ( ( 𝜑𝑘 ∈ ℕ ) → ( Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) + Σ 𝑚 ∈ ( 1 ... 𝑘 ) ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) = ( ( 𝑆𝑘 ) + ( 𝐵 − ( 𝐵 / ( 2 ↑ 𝑘 ) ) ) ) )
174 130 164 173 3eqtr3d ( ( 𝜑𝑘 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑘 ) = ( ( 𝑆𝑘 ) + ( 𝐵 − ( 𝐵 / ( 2 ↑ 𝑘 ) ) ) ) )
175 113 174 eqtrid ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑇𝑘 ) = ( ( 𝑆𝑘 ) + ( 𝐵 − ( 𝐵 / ( 2 ↑ 𝑘 ) ) ) ) )
176 116 1 ovolsf ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
177 4 176 syl ( 𝜑𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
178 177 ffvelrnda ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑆𝑘 ) ∈ ( 0 [,) +∞ ) )
179 115 178 sselid ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑆𝑘 ) ∈ ℝ )
180 169 rpred ( ( 𝜑𝑘 ∈ ℕ ) → 𝐵 ∈ ℝ )
181 nnnn0 ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
182 181 adantl ( ( 𝜑𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ0 )
183 nnexpcl ( ( 2 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ 𝑘 ) ∈ ℕ )
184 18 182 183 sylancr ( ( 𝜑𝑘 ∈ ℕ ) → ( 2 ↑ 𝑘 ) ∈ ℕ )
185 184 nnrpd ( ( 𝜑𝑘 ∈ ℕ ) → ( 2 ↑ 𝑘 ) ∈ ℝ+ )
186 169 185 rpdivcld ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐵 / ( 2 ↑ 𝑘 ) ) ∈ ℝ+ )
187 186 rpred ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐵 / ( 2 ↑ 𝑘 ) ) ∈ ℝ )
188 180 187 resubcld ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐵 − ( 𝐵 / ( 2 ↑ 𝑘 ) ) ) ∈ ℝ )
189 7 adantr ( ( 𝜑𝑘 ∈ ℕ ) → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ )
190 177 frnd ( 𝜑 → ran 𝑆 ⊆ ( 0 [,) +∞ ) )
191 190 44 sstrdi ( 𝜑 → ran 𝑆 ⊆ ℝ* )
192 191 adantr ( ( 𝜑𝑘 ∈ ℕ ) → ran 𝑆 ⊆ ℝ* )
193 177 ffnd ( 𝜑𝑆 Fn ℕ )
194 fnfvelrn ( ( 𝑆 Fn ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑆𝑘 ) ∈ ran 𝑆 )
195 193 194 sylan ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑆𝑘 ) ∈ ran 𝑆 )
196 supxrub ( ( ran 𝑆 ⊆ ℝ* ∧ ( 𝑆𝑘 ) ∈ ran 𝑆 ) → ( 𝑆𝑘 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
197 192 195 196 syl2anc ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑆𝑘 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
198 180 186 ltsubrpd ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐵 − ( 𝐵 / ( 2 ↑ 𝑘 ) ) ) < 𝐵 )
199 188 180 198 ltled ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐵 − ( 𝐵 / ( 2 ↑ 𝑘 ) ) ) ≤ 𝐵 )
200 179 188 189 180 197 199 le2addd ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝑆𝑘 ) + ( 𝐵 − ( 𝐵 / ( 2 ↑ 𝑘 ) ) ) ) ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) )
201 175 200 eqbrtrd ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑇𝑘 ) ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) )
202 201 ralrimiva ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝑇𝑘 ) ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) )
203 ffn ( 𝑇 : ℕ ⟶ ( 0 [,) +∞ ) → 𝑇 Fn ℕ )
204 breq1 ( 𝑦 = ( 𝑇𝑘 ) → ( 𝑦 ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) ↔ ( 𝑇𝑘 ) ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) ) )
205 204 ralrn ( 𝑇 Fn ℕ → ( ∀ 𝑦 ∈ ran 𝑇 𝑦 ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) ↔ ∀ 𝑘 ∈ ℕ ( 𝑇𝑘 ) ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) ) )
206 42 203 205 3syl ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝑇 𝑦 ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) ↔ ∀ 𝑘 ∈ ℕ ( 𝑇𝑘 ) ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) ) )
207 202 206 mpbird ( 𝜑 → ∀ 𝑦 ∈ ran 𝑇 𝑦 ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) )
208 supxrleub ( ( ran 𝑇 ⊆ ℝ* ∧ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) ∈ ℝ* ) → ( sup ( ran 𝑇 , ℝ* , < ) ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) ↔ ∀ 𝑦 ∈ ran 𝑇 𝑦 ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) ) )
209 45 50 208 syl2anc ( 𝜑 → ( sup ( ran 𝑇 , ℝ* , < ) ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) ↔ ∀ 𝑦 ∈ ran 𝑇 𝑦 ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) ) )
210 207 209 mpbird ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) )
211 12 47 50 112 210 xrletrd ( 𝜑 → ( vol* ‘ 𝐴 ) ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝐵 ) )