ovolval5lem1 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ovolval5lem1		Structured version Visualization version GIF version

Theorem ovolval5lem1 42941

Description: (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛) ))(,)𝐵)))) ≤ ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵) ))) +_𝑒 𝑊)) (Contributed by Glauco Siliprandi, 3-Mar-2021.)

**Hypotheses**
Ref	Expression
ovolval5lem1.a	⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℝ)
ovolval5lem1.b	⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℝ)
ovolval5lem1.w	⊢ (𝜑 → 𝑊 ∈ ℝ⁺)
ovolval5lem1.c	⊢ 𝐶 = {𝑛 ∈ ℕ ∣ 𝐴 < 𝐵}

**Assertion**
Ref	Expression
ovolval5lem1	⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)))) ≤ ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +_𝑒 𝑊))

Distinct variable groups: 𝐶,𝑛 𝑛,𝑊 𝜑,𝑛 Allowed substitution hints: 𝐴(𝑛) 𝐵(𝑛)

**Proof of Theorem ovolval5lem1**
Step	Hyp	Ref	Expression
1		nfv 1915	. . 3 ⊢ Ⅎ𝑛𝜑
2		nnex 11646	. . . 4 ⊢ ℕ ∈ V
3	2	a1i 11	. . 3 ⊢ (𝜑 → ℕ ∈ V)
4		volf 24132	. . . . 5 ⊢ vol:dom vol⟶(0[,]+∞)
5	4	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → vol:dom vol⟶(0[,]+∞))
6		ioombl 24168	. . . . 5 ⊢ ((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵) ∈ dom vol
7	6	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵) ∈ dom vol)
8	5, 7	ffvelrnd 6854	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ∈ (0[,]+∞))
9	1, 3, 8	sge0xrclmpt 42717	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)))) ∈ ℝ^*)
10		0xr 10690	. . . . 5 ⊢ 0 ∈ ℝ^*
11	10	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ∈ ℝ^*)
12		pnfxr 10697	. . . . 5 ⊢ +∞ ∈ ℝ^*
13	12	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → +∞ ∈ ℝ^*)
14		ovolval5lem1.a	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℝ)
15		ovolval5lem1.b	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℝ)
16		volicore 42870	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,)𝐵)) ∈ ℝ)
17	14, 15, 16	syl2anc 586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐴[,)𝐵)) ∈ ℝ)
18		ovolval5lem1.w	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ ℝ⁺)
19	18	rpred 12434	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ ℝ)
20	19	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑊 ∈ ℝ)
21		2nn 11713	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
22	21	a1i 11	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 2 ∈ ℕ)
23		nnnn0 11907	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
24		nnexpcl 13445	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ₀) → (2↑𝑛) ∈ ℕ)
25	22, 23, 24	syl2anc 586	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
26	25	nnred 11655	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ)
27	26	adantl 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ)
28	25	nnne0d 11690	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (2↑𝑛) ≠ 0)
29	28	adantl 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ≠ 0)
30	20, 27, 29	redivcld 11470	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ)
31	17, 30	readdcld 10672	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ)
32	31	rexrd 10693	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ^*)
33	15	rexrd 10693	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℝ^*)
34		icombl 24167	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐴[,)𝐵) ∈ dom vol)
35	14, 33, 34	syl2anc 586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴[,)𝐵) ∈ dom vol)
36		volge0 42253	. . . . . 6 ⊢ ((𝐴[,)𝐵) ∈ dom vol → 0 ≤ (vol‘(𝐴[,)𝐵)))
37	35, 36	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (vol‘(𝐴[,)𝐵)))
38	18	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑊 ∈ ℝ⁺)
39	25	nnrpd 12432	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ⁺)
40	39	adantl 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ⁺)
41	38, 40	rpdivcld 12451	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ⁺)
42	41	rpge0d 12438	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (𝑊 / (2↑𝑛)))
43	17, 30, 37, 42	addge0d 11218	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
44		rexr 10689	. . . . . 6 ⊢ (((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ^*)
45	12	a1i 11	. . . . . 6 ⊢ (((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → +∞ ∈ ℝ^*)
46		ltpnf 12518	. . . . . 6 ⊢ (((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) < +∞)
47	44, 45, 46	xrltled 12546	. . . . 5 ⊢ (((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ≤ +∞)
48	31, 47	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ≤ +∞)
49	11, 13, 32, 43, 48	eliccxrd 41810	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ (0[,]+∞))
50	1, 3, 49	sge0xrclmpt 42717	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) ∈ ℝ^*)
51	5, 35	ffvelrnd 6854	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐴[,)𝐵)) ∈ (0[,]+∞))
52	1, 3, 51	sge0xrclmpt 42717	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) ∈ ℝ^*)
53	19	rexrd 10693	. . 3 ⊢ (𝜑 → 𝑊 ∈ ℝ^*)
54	52, 53	xaddcld 12697	. 2 ⊢ (𝜑 → ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +_𝑒 𝑊) ∈ ℝ^*)
55	14, 30	resubcld 11070	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 − (𝑊 / (2↑𝑛))) ∈ ℝ)
56		volioore 42282	. . . . . . . 8 ⊢ (((𝐴 − (𝑊 / (2↑𝑛))) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0))
57	55, 15, 56	syl2anc 586	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0))
58	57	adantr 483	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0))
59		iftrue 4475	. . . . . . 7 ⊢ ((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵 → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))))
60	59	adantl 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))))
61	15	recnd 10671	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℂ)
62	14	recnd 10671	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℂ)
63	30	recnd 10671	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℂ)
64	61, 62, 63	subsubd 11027	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))) = ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛))))
65	64	adantr 483	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))) = ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛))))
66	58, 60, 65	3eqtrd 2862	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛))))
67	15, 14	resubcld 11070	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 − 𝐴) ∈ ℝ)
68	14, 15	sublevolico 42276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 − 𝐴) ≤ (vol‘(𝐴[,)𝐵)))
69	67, 17, 30, 68	leadd1dd 11256	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛))) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
70	69	adantr 483	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛))) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
71	66, 70	eqbrtrd 5090	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
72	57	adantr 483	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0))
73		iffalse 4478	. . . . . . 7 ⊢ (¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵 → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = 0)
74	73	adantl 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = 0)
75	72, 74	eqtrd 2858	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = 0)
76	43	adantr 483	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → 0 ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
77	75, 76	eqbrtrd 5090	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
78	71, 77	pm2.61dan 811	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
79	1, 3, 8, 49, 78	sge0lempt 42699	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)))) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))))
80	17, 30	rexaddd 12630	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) +_𝑒 (𝑊 / (2↑𝑛))) = ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
81	80	eqcomd 2829	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) = ((vol‘(𝐴[,)𝐵)) +_𝑒 (𝑊 / (2↑𝑛))))
82	81	mpteq2dva 5163	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) = (𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) +_𝑒 (𝑊 / (2↑𝑛)))))
83	82	fveq2d 6676	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) = (Σ^{^}‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) +_𝑒 (𝑊 / (2↑𝑛))))))
84	30	rexrd 10693	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ^*)
85		rexr 10689	. . . . . . . 8 ⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → (𝑊 / (2↑𝑛)) ∈ ℝ^*)
86	12	a1i 11	. . . . . . . 8 ⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → +∞ ∈ ℝ^*)
87		ltpnf 12518	. . . . . . . 8 ⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → (𝑊 / (2↑𝑛)) < +∞)
88	85, 86, 87	xrltled 12546	. . . . . . 7 ⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → (𝑊 / (2↑𝑛)) ≤ +∞)
89	30, 88	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ≤ +∞)
90	11, 13, 84, 42, 89	eliccxrd 41810	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ (0[,]+∞))
91	1, 3, 51, 90	sge0xadd 42724	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) +_𝑒 (𝑊 / (2↑𝑛))))) = ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑊 / (2↑𝑛))))))
92	10	a1i 11	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℝ^*)
93	12	a1i 11	. . . . . . 7 ⊢ (𝜑 → +∞ ∈ ℝ^*)
94	18	rpge0d 12438	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 𝑊)
95	19	ltpnfd 12519	. . . . . . 7 ⊢ (𝜑 → 𝑊 < +∞)
96	92, 93, 53, 94, 95	elicod 12790	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ (0[,)+∞))
97	96	sge0ad2en 42720	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑊 / (2↑𝑛)))) = 𝑊)
98	97	oveq2d 7174	. . . 4 ⊢ (𝜑 → ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +_𝑒 (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑊 / (2↑𝑛))))) = ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +_𝑒 𝑊))
99	83, 91, 98	3eqtrd 2862	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) = ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +_𝑒 𝑊))
100	50, 99	xreqled 41605	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) ≤ ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +_𝑒 𝑊))
101	9, 50, 54, 79, 100	xrletrd 12558	1 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)))) ≤ ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +_𝑒 𝑊))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ≠ wne 3018 {crab 3144 Vcvv 3496 ifcif 4469 class class class wbr 5068 ↦ cmpt 5148 dom cdm 5557 ⟶wf 6353 ‘cfv 6357 (class class class)co 7158 ℝcr 10538 0cc0 10539 + caddc 10542 +∞cpnf 10674 ℝ^*cxr 10676 < clt 10677 ≤ cle 10678 − cmin 10872 / cdiv 11299 ℕcn 11640 2c2 11695 ℕ₀cn0 11900 ℝ⁺crp 12392 +_𝑒 cxad 12508 (,)cioo 12741 [,)cico 12743 [,]cicc 12744 ↑cexp 13432 volcvol 24066 Σ^{^}csumge0 42651

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-inf2 9106 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616 ax-pre-sup 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-se 5517 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-isom 6366 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-of 7411 df-om 7583 df-1st 7691 df-2nd 7692 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-2o 8105 df-oadd 8108 df-er 8291 df-map 8410 df-pm 8411 df-en 8512 df-dom 8513 df-sdom 8514 df-fin 8515 df-fi 8877 df-sup 8908 df-inf 8909 df-oi 8976 df-dju 9332 df-card 9370 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-div 11300 df-nn 11641 df-2 11703 df-3 11704 df-n0 11901 df-z 11985 df-uz 12247 df-q 12352 df-rp 12393 df-xneg 12510 df-xadd 12511 df-xmul 12512 df-ioo 12745 df-ico 12747 df-icc 12748 df-fz 12896 df-fzo 13037 df-fl 13165 df-seq 13373 df-exp 13433 df-hash 13694 df-cj 14460 df-re 14461 df-im 14462 df-sqrt 14596 df-abs 14597 df-clim 14847 df-rlim 14848 df-sum 15045 df-rest 16698 df-topgen 16719 df-psmet 20539 df-xmet 20540 df-met 20541 df-bl 20542 df-mopn 20543 df-top 21504 df-topon 21521 df-bases 21556 df-cmp 21997 df-ovol 24067 df-vol 24068 df-sumge0 42652

This theorem is referenced by: ovolval5lem2 42942

W3C validator