ovollb2lem

	Ref	Expression
Hypotheses	ovollb2.1	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
	ovollb2.2	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐵 / 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	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐵 / 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	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
14	4 13	sylan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
15	14	simp1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
16	6	rphalfcld	⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℝ⁺ )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐵 / 2 ) ∈ ℝ⁺ )
18		2nn	⊢ 2 ∈ ℕ
19		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀ )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ₀ )
21		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ₀ ) → ( 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	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
27	14	simp2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
28	27 25	readdcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
29	15 24	ltsubrpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) < ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) )
30	14	simp3d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) )
31	27 24	ltaddrpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) )
32	15 27 28 30 31	lelttrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) )
33	26 15 28 29 32	lttrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) < ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) )
34	26 28 33	ltled	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ≤ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) )
35		df-br	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ≤ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ↔ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ⟩ ∈ ≤ )
36	34 35	sylib	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ⟩ ∈ ≤ )
37	26 28	opelxpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ⟩ ∈ ( ℝ × ℝ ) )
38	36 37	elind	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐵 / 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	⊢ ( 𝑛 = 𝑚 → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) = ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) )
52		oveq2	⊢ ( 𝑛 = 𝑚 → ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝑚 ) )
53	52	oveq2d	⊢ ( 𝑛 = 𝑚 → ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) = ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) )
54	51 53	oveq12d	⊢ ( 𝑛 = 𝑚 → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) )
55		2fveq3	⊢ ( 𝑛 = 𝑚 → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) )
56	55 53	oveq12d	⊢ ( 𝑛 = 𝑚 → ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) )
57	54 56	opeq12d	⊢ ( 𝑛 = 𝑚 → ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ⟩ = ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ )
58		opex	⊢ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ ∈ V
59	57 2 58	fvmpt	⊢ ( 𝑚 ∈ ℕ → ( 𝐺 ‘ 𝑚 ) = ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ )
60	59	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐺 ‘ 𝑚 ) = ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ )
61	60	fveq2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) = ( 1^st ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ ) )
62		ovex	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ∈ V
63		ovex	⊢ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ∈ V
64	62 63	op1st	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) )
65	61 64	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) )
66		ovolfcl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
67	4 66	sylan	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
68	67	simp1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ )
69	16	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐵 / 2 ) ∈ ℝ⁺ )
70		nnnn0	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℕ₀ )
71	70	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ₀ )
72		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑚 ∈ ℕ₀ ) → ( 2 ↑ 𝑚 ) ∈ ℕ )
73	18 71 72	sylancr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2 ↑ 𝑚 ) ∈ ℕ )
74	73	nnrpd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2 ↑ 𝑚 ) ∈ ℝ⁺ )
75	69 74	rpdivcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ∈ ℝ⁺ )
76	68 75	ltsubrpd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) < ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) )
77	65 76	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) < ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) )
78	77	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) < ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) )
79		ovolfcl	⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) )
80	39 79	sylan	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) )
81	80	simp1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) ∈ ℝ )
82	81	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) ∈ ℝ )
83	68	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ )
84	10	sselda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℝ )
85	84	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑚 ∈ ℕ ) → 𝑧 ∈ ℝ )
86		ltletr	⊢ ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) < ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ 𝑧 ) → ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ) )
87	82 83 85 86	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) < ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ 𝑧 ) → ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ) )
88	78 87	mpand	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ 𝑧 → ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ) )
89	67	simp2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ )
90	89 75	ltaddrpd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) < ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) )
91	60	fveq2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) = ( 2^nd ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ ) )
92	62 63	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) )
93	91 92	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) )
94	90 93	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) )
95	94	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) )
96	89	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ )
97	80	simp2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ∈ ℝ )
98	97	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ∈ ℝ )
99		lelttr	⊢ ( ( 𝑧 ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ∈ ℝ ) → ( ( 𝑧 ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) → 𝑧 < ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) )
100	85 96 98 99	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑧 ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) < ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) → 𝑧 < ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) )
101	95 100	mpan2d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( 𝑧 ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) → 𝑧 < ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) )
102	88 101	anim12d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) )
103	102	reximdva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) )
104	103	ralimdva	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) )
105		ovolficc	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
106	10 4 105	syl2anc	⊢ ( 𝜑 → ( 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ≤ 𝑧 ∧ 𝑧 ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
107		ovolfioo	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) )
108	10 39 107	syl2anc	⊢ ( 𝜑 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑚 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) < 𝑧 ∧ 𝑧 < ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) )
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 ∘ − ) ∘ 𝐺 ) ‘ 𝑚 ) = ( ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) − ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) ) )
132	39 131	sylan	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑚 ) = ( ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) − ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) ) )
133	89	recnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℂ )
134	75	rpcnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ∈ ℂ )
135	68	recnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℂ )
136	135 134	subcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ∈ ℂ )
137	133 134 136	addsubassd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) − ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) − ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ) ) )
138	93 65	oveq12d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) − ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) ) = ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) − ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ) )
139	133 135 127	subadd23d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / ( 2 ↑ 𝑚 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
140	116	ovolfsval	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑚 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
141	4 140	sylan	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
142	141	oveq1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) = ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) )
143	134 135 134	subsub3d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) − ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ) = ( ( ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) + ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
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 ↑ 𝑚 ) ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) = ( ( 𝐵 / ( 2 ↑ 𝑚 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
153	143 152	eqtrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) − ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ) = ( ( 𝐵 / ( 2 ↑ 𝑚 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
154	153	oveq2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) − ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝐵 / ( 2 ↑ 𝑚 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
155	139 142 154	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑚 ) + ( 𝐵 / ( 2 ↑ 𝑚 ) ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) − ( ( 1^st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝐵 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ) ) )
156	137 138 155	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑚 ) ) − ( 1^st ‘ ( 𝐺 ‘ 𝑚 ) ) ) = ( ( ( ( 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	syl5eq	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑇 ‘ 𝑘 ) = ( ( 𝑆 ‘ 𝑘 ) + ( 𝐵 − ( 𝐵 / ( 2 ↑ 𝑘 ) ) ) ) )
176	116 1	ovolsf	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
177	4 176	syl	⊢ ( 𝜑 → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
178	177	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ∈ ( 0 [,) +∞ ) )
179	115 178	sselid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ∈ ℝ )
180	169	rpred	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐵 ∈ ℝ )
181		nnnn0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀ )
182	181	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ₀ )
183		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑘 ∈ ℕ₀ ) → ( 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 𝑆 , ℝ^* , < ) + 𝐵 ) )

Metamath Proof Explorer

Theorem ovollb2lem

Proof