ovolscalem1

	Ref	Expression
Hypotheses	ovolsca.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	ovolsca.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ⁺ )
	ovolsca.3	⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝐶 · 𝑥 ) ∈ 𝐴 } )
	ovolsca.4	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) ∈ ℝ )
	ovolsca.5	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
	ovolsca.6	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ⟩ )
	ovolsca.7	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
	ovolsca.8	⊢ ( 𝜑 → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) )
	ovolsca.9	⊢ ( 𝜑 → 𝑅 ∈ ℝ⁺ )
	ovolsca.10	⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ^* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) )
Assertion	ovolscalem1	⊢ ( 𝜑 → ( vol* ‘ 𝐵 ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		ovolsca.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		ovolsca.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ⁺ )
3		ovolsca.3	⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝐶 · 𝑥 ) ∈ 𝐴 } )
4		ovolsca.4	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) ∈ ℝ )
5		ovolsca.5	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
6		ovolsca.6	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ⟩ )
7		ovolsca.7	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
8		ovolsca.8	⊢ ( 𝜑 → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) )
9		ovolsca.9	⊢ ( 𝜑 → 𝑅 ∈ ℝ⁺ )
10		ovolsca.10	⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ^* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) )
11		ssrab2	⊢ { 𝑥 ∈ ℝ ∣ ( 𝐶 · 𝑥 ) ∈ 𝐴 } ⊆ ℝ
12	3 11	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
13		ovolcl	⊢ ( 𝐵 ⊆ ℝ → ( vol* ‘ 𝐵 ) ∈ ℝ^* )
14	12 13	syl	⊢ ( 𝜑 → ( vol* ‘ 𝐵 ) ∈ ℝ^* )
15		ovolfcl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
16	7 15	sylan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
17	16	simp3d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) )
18	16	simp1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
19	16	simp2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
20	2	rpregt0d	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) )
22		lediv1	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ≤ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ) )
23	18 19 21 22	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ≤ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ) )
24	17 23	mpbid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ≤ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) )
25		df-br	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ≤ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ↔ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ⟩ ∈ ≤ )
26	24 25	sylib	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ⟩ ∈ ≤ )
27	2	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐶 ∈ ℝ⁺ )
28	18 27	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ∈ ℝ )
29	19 27	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ∈ ℝ )
30	28 29	opelxpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ⟩ ∈ ( ℝ × ℝ ) )
31	26 30	elind	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
32	31 6	fmptd	⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
33		eqid	⊢ ( ( abs ∘ − ) ∘ 𝐺 ) = ( ( abs ∘ − ) ∘ 𝐺 )
34		eqid	⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
35	33 34	ovolsf	⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
36	32 35	syl	⊢ ( 𝜑 → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) : ℕ ⟶ ( 0 [,) +∞ ) )
37	36	frnd	⊢ ( 𝜑 → ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ⊆ ( 0 [,) +∞ ) )
38		icossxr	⊢ ( 0 [,) +∞ ) ⊆ ℝ^*
39	37 38	sstrdi	⊢ ( 𝜑 → ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ⊆ ℝ^* )
40		supxrcl	⊢ ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ⊆ ℝ^* → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ^* , < ) ∈ ℝ^* )
41	39 40	syl	⊢ ( 𝜑 → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ^* , < ) ∈ ℝ^* )
42	4 2	rerpdivcld	⊢ ( 𝜑 → ( ( vol* ‘ 𝐴 ) / 𝐶 ) ∈ ℝ )
43	9	rpred	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
44	42 43	readdcld	⊢ ( 𝜑 → ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ∈ ℝ )
45	44	rexrd	⊢ ( 𝜑 → ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ∈ ℝ^* )
46	3	eleq2d	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ { 𝑥 ∈ ℝ ∣ ( 𝐶 · 𝑥 ) ∈ 𝐴 } ) )
47		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) )
48	47	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐶 · 𝑥 ) ∈ 𝐴 ↔ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) )
49	48	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ ℝ ∣ ( 𝐶 · 𝑥 ) ∈ 𝐴 } ↔ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) )
50	46 49	bitrdi	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↔ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) )
51		breq2	⊢ ( 𝑥 = ( 𝐶 · 𝑦 ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ↔ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝐶 · 𝑦 ) ) )
52		breq1	⊢ ( 𝑥 = ( 𝐶 · 𝑦 ) → ( 𝑥 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ ( 𝐶 · 𝑦 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
53	51 52	anbi12d	⊢ ( 𝑥 = ( 𝐶 · 𝑦 ) → ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝐶 · 𝑦 ) ∧ ( 𝐶 · 𝑦 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
54	53	rexbidv	⊢ ( 𝑥 = ( 𝐶 · 𝑦 ) → ( ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝐶 · 𝑦 ) ∧ ( 𝐶 · 𝑦 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
55		ovolfioo	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
56	1 7 55	syl2anc	⊢ ( 𝜑 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
57	8 56	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
58	57	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
59		simprr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) → ( 𝐶 · 𝑦 ) ∈ 𝐴 )
60	54 58 59	rspcdva	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) → ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝐶 · 𝑦 ) ∧ ( 𝐶 · 𝑦 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
61		opex	⊢ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ⟩ ∈ V
62	6	fvmpt2	⊢ ( ( 𝑛 ∈ ℕ ∧ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ⟩ ∈ V ) → ( 𝐺 ‘ 𝑛 ) = ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ⟩ )
63	61 62	mpan2	⊢ ( 𝑛 ∈ ℕ → ( 𝐺 ‘ 𝑛 ) = ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ⟩ )
64	63	fveq2d	⊢ ( 𝑛 ∈ ℕ → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 1^st ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ⟩ ) )
65		ovex	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ∈ V
66		ovex	⊢ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ∈ V
67	65 66	op1st	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ⟩ ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 )
68	64 67	eqtrdi	⊢ ( 𝑛 ∈ ℕ → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) )
69	68	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) )
70	69	breq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) < 𝑦 ) )
71	18	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
72		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑦 ∈ ℝ )
73	21	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) )
74		ltdivmul	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) < 𝑦 ↔ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝐶 · 𝑦 ) ) )
75	71 72 73 74	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) < 𝑦 ↔ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝐶 · 𝑦 ) ) )
76	70 75	bitr2d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝐶 · 𝑦 ) ↔ ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ) )
77	19	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
78		ltmuldiv2	⊢ ( ( 𝑦 ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐶 · 𝑦 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ 𝑦 < ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ) )
79	72 77 73 78	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐶 · 𝑦 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ 𝑦 < ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ) )
80	63	fveq2d	⊢ ( 𝑛 ∈ ℕ → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 2^nd ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ⟩ ) )
81	65 66	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ⟩ ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 )
82	80 81	eqtrdi	⊢ ( 𝑛 ∈ ℕ → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) )
83	82	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) )
84	83	breq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ↔ 𝑦 < ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ) )
85	79 84	bitr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐶 · 𝑦 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
86	76 85	anbi12d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝐶 · 𝑦 ) ∧ ( 𝐶 · 𝑦 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
87	86	rexbidva	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) → ( ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝐶 · 𝑦 ) ∧ ( 𝐶 · 𝑦 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
88	60 87	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) ) → ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
89	88	ex	⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ 𝐴 ) → ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
90	50 89	sylbid	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
91	90	ralrimiv	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
92		ovolfioo	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
93	12 32 92	syl2anc	⊢ ( 𝜑 → ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
94	91 93	mpbird	⊢ ( 𝜑 → 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
95	34	ovollb	⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ) → ( vol* ‘ 𝐵 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ^* , < ) )
96	32 94 95	syl2anc	⊢ ( 𝜑 → ( vol* ‘ 𝐵 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ^* , < ) )
97		fzfid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 ... 𝑘 ) ∈ Fin )
98	2	rpcnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
99	98	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐶 ∈ ℂ )
100		simpl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝜑 )
101		elfznn	⊢ ( 𝑛 ∈ ( 1 ... 𝑘 ) → 𝑛 ∈ ℕ )
102	19 18	resubcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
103	100 101 102	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
104	103	recnd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℂ )
105	2	rpne0d	⊢ ( 𝜑 → 𝐶 ≠ 0 )
106	105	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐶 ≠ 0 )
107	97 99 104 106	fsumdivc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( Σ 𝑛 ∈ ( 1 ... 𝑘 ) ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) / 𝐶 ) = Σ 𝑛 ∈ ( 1 ... 𝑘 ) ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) / 𝐶 ) )
108	82 68	oveq12d	⊢ ( 𝑛 ∈ ℕ → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) − ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ) )
109	108	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) − ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ) )
110	33	ovolfsval	⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) = ( ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
111	32 110	sylan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) = ( ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
112	19	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℂ )
113	18	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℂ )
114	2	rpcnne0d	⊢ ( 𝜑 → ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) )
115	114	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) )
116		divsubdir	⊢ ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℂ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) / 𝐶 ) = ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) − ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ) )
117	112 113 115 116	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) / 𝐶 ) = ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) − ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) / 𝐶 ) ) )
118	109 111 117	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) = ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) / 𝐶 ) )
119	100 101 118	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) = ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) / 𝐶 ) )
120		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
121		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
122	120 121	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ_≥ ‘ 1 ) )
123	102 27	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) / 𝐶 ) ∈ ℝ )
124	123	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) / 𝐶 ) ∈ ℂ )
125	100 101 124	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) / 𝐶 ) ∈ ℂ )
126	119 122 125	fsumser	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑛 ∈ ( 1 ... 𝑘 ) ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) / 𝐶 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑘 ) )
127	107 126	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( Σ 𝑛 ∈ ( 1 ... 𝑘 ) ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) / 𝐶 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑘 ) )
128		eqid	⊢ ( ( abs ∘ − ) ∘ 𝐹 ) = ( ( abs ∘ − ) ∘ 𝐹 )
129	128 5	ovolsf	⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
130	7 129	syl	⊢ ( 𝜑 → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
131	130	frnd	⊢ ( 𝜑 → ran 𝑆 ⊆ ( 0 [,) +∞ ) )
132	131 38	sstrdi	⊢ ( 𝜑 → ran 𝑆 ⊆ ℝ^* )
133	2 9	rpmulcld	⊢ ( 𝜑 → ( 𝐶 · 𝑅 ) ∈ ℝ⁺ )
134	133	rpred	⊢ ( 𝜑 → ( 𝐶 · 𝑅 ) ∈ ℝ )
135	4 134	readdcld	⊢ ( 𝜑 → ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) ∈ ℝ )
136	135	rexrd	⊢ ( 𝜑 → ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) ∈ ℝ^* )
137		supxrleub	⊢ ( ( ran 𝑆 ⊆ ℝ^* ∧ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) ∈ ℝ^* ) → ( sup ( ran 𝑆 , ℝ^* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) ↔ ∀ 𝑥 ∈ ran 𝑆 𝑥 ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) ) )
138	132 136 137	syl2anc	⊢ ( 𝜑 → ( sup ( ran 𝑆 , ℝ^* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) ↔ ∀ 𝑥 ∈ ran 𝑆 𝑥 ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) ) )
139	10 138	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝑆 𝑥 ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) )
140	130	ffnd	⊢ ( 𝜑 → 𝑆 Fn ℕ )
141		breq1	⊢ ( 𝑥 = ( 𝑆 ‘ 𝑘 ) → ( 𝑥 ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) ↔ ( 𝑆 ‘ 𝑘 ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) ) )
142	141	ralrn	⊢ ( 𝑆 Fn ℕ → ( ∀ 𝑥 ∈ ran 𝑆 𝑥 ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) ↔ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) ) )
143	140 142	syl	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ran 𝑆 𝑥 ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) ↔ ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) ) )
144	139 143	mpbid	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝑆 ‘ 𝑘 ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) )
145	144	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑆 ‘ 𝑘 ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) )
146	7	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
147	128	ovolfsval	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
148	146 101 147	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ( 1 ... 𝑘 ) ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
149	148 122 104	fsumser	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑛 ∈ ( 1 ... 𝑘 ) ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑘 ) )
150	5	fveq1i	⊢ ( 𝑆 ‘ 𝑘 ) = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) ‘ 𝑘 )
151	149 150	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑛 ∈ ( 1 ... 𝑘 ) ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑆 ‘ 𝑘 ) )
152	42	recnd	⊢ ( 𝜑 → ( ( vol* ‘ 𝐴 ) / 𝐶 ) ∈ ℂ )
153	9	rpcnd	⊢ ( 𝜑 → 𝑅 ∈ ℂ )
154	98 152 153	adddid	⊢ ( 𝜑 → ( 𝐶 · ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ) = ( ( 𝐶 · ( ( vol* ‘ 𝐴 ) / 𝐶 ) ) + ( 𝐶 · 𝑅 ) ) )
155	4	recnd	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) ∈ ℂ )
156	155 98 105	divcan2d	⊢ ( 𝜑 → ( 𝐶 · ( ( vol* ‘ 𝐴 ) / 𝐶 ) ) = ( vol* ‘ 𝐴 ) )
157	156	oveq1d	⊢ ( 𝜑 → ( ( 𝐶 · ( ( vol* ‘ 𝐴 ) / 𝐶 ) ) + ( 𝐶 · 𝑅 ) ) = ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) )
158	154 157	eqtrd	⊢ ( 𝜑 → ( 𝐶 · ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ) = ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) )
159	158	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐶 · ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ) = ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑅 ) ) )
160	145 151 159	3brtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑛 ∈ ( 1 ... 𝑘 ) ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) ≤ ( 𝐶 · ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ) )
161	97 103	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → Σ 𝑛 ∈ ( 1 ... 𝑘 ) ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
162	44	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ∈ ℝ )
163	20	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) )
164		ledivmul	⊢ ( ( Σ 𝑛 ∈ ( 1 ... 𝑘 ) ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ ∧ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( Σ 𝑛 ∈ ( 1 ... 𝑘 ) ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) / 𝐶 ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ↔ Σ 𝑛 ∈ ( 1 ... 𝑘 ) ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) ≤ ( 𝐶 · ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ) ) )
165	161 162 163 164	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( Σ 𝑛 ∈ ( 1 ... 𝑘 ) ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) / 𝐶 ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ↔ Σ 𝑛 ∈ ( 1 ... 𝑘 ) ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) ≤ ( 𝐶 · ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ) ) )
166	160 165	mpbird	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( Σ 𝑛 ∈ ( 1 ... 𝑘 ) ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) / 𝐶 ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) )
167	127 166	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑘 ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) )
168	167	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑘 ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) )
169	36	ffnd	⊢ ( 𝜑 → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) Fn ℕ )
170		breq1	⊢ ( 𝑦 = ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑘 ) → ( 𝑦 ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ↔ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑘 ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ) )
171	170	ralrn	⊢ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) Fn ℕ → ( ∀ 𝑦 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) 𝑦 ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ↔ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑘 ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ) )
172	169 171	syl	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) 𝑦 ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ↔ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ‘ 𝑘 ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ) )
173	168 172	mpbird	⊢ ( 𝜑 → ∀ 𝑦 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) 𝑦 ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) )
174		supxrleub	⊢ ( ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) ⊆ ℝ^* ∧ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ∈ ℝ^* ) → ( sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ^* , < ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ↔ ∀ 𝑦 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) 𝑦 ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ) )
175	39 45 174	syl2anc	⊢ ( 𝜑 → ( sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ^* , < ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ↔ ∀ 𝑦 ∈ ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) 𝑦 ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) ) )
176	173 175	mpbird	⊢ ( 𝜑 → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ^* , < ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) )
177	14 41 45 96 176	xrletrd	⊢ ( 𝜑 → ( vol* ‘ 𝐵 ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑅 ) )

Metamath Proof Explorer

Theorem ovolscalem1

Proof