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 47801

Description: (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛) ))(,)𝐵)))) ≤ ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵) ))) +_e 𝑊)). (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‘(𝐴[,)𝐵)))) +_e 𝑊))

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

**Proof of Theorem ovolval5lem1**
Step	Hyp	Ref	Expression
1		nfv 1948	. . 3 ⊢ Ⅎ𝑛𝜑
2		nnex 12351	. . . 4 ⊢ ℕ ∈ V
3	2	a1i 11	. . 3 ⊢ (𝜑 → ℕ ∈ V)
4		volf 25862	. . . . 5 ⊢ vol:dom vol⟶(0[,]+∞)
5	4	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → vol:dom vol⟶(0[,]+∞))
6		ioombl 25898	. . . . 5 ⊢ ((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵) ∈ dom vol
7	6	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵) ∈ dom vol)
8	5, 7	ffvelcdmd 7093	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ∈ (0[,]+∞))
9	1, 3, 8	sge0xrclmpt 47577	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)))) ∈ ℝ^*)
10		0xr 11366	. . . . 5 ⊢ 0 ∈ ℝ^*
11	10	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ∈ ℝ^*)
12		pnfxr 11373	. . . . 5 ⊢ +∞ ∈ ℝ^*
13	12	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → +∞ ∈ ℝ^*)
14		ovolval5lem1.a	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℝ)
15		ovolval5lem1.b	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℝ)
16		volicore 47730	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,)𝐵)) ∈ ℝ)
17	14, 15, 16	syl2anc 596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐴[,)𝐵)) ∈ ℝ)
18		ovolval5lem1.w	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ ℝ⁺)
19	18	rpred 13174	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ ℝ)
20	19	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑊 ∈ ℝ)
21		2nn 12426	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
22	21	a1i 11	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 2 ∈ ℕ)
23		nnnn0 12623	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
24		nnexpcl 14227	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ₀) → (2↑𝑛) ∈ ℕ)
25	22, 23, 24	syl2anc 596	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
26	25	nnred 12360	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ)
27	26	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ)
28	25	nnne0d 12398	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (2↑𝑛) ≠ 0)
29	28	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ≠ 0)
30	20, 27, 29	redivcld 12155	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ)
31	17, 30	readdcld 11348	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ)
32	31	rexrd 11369	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ^*)
33	15	rexrd 11369	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℝ^*)
34		icombl 25897	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐴[,)𝐵) ∈ dom vol)
35	14, 33, 34	syl2anc 596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴[,)𝐵) ∈ dom vol)
36		volge0 47110	. . . . . 6 ⊢ ((𝐴[,)𝐵) ∈ dom vol → 0 ≤ (vol‘(𝐴[,)𝐵)))
37	35, 36	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (vol‘(𝐴[,)𝐵)))
38	18	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑊 ∈ ℝ⁺)
39	25	nnrpd 13172	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ⁺)
40	39	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ⁺)
41	38, 40	rpdivcld 13191	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ⁺)
42	41	rpge0d 13178	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (𝑊 / (2↑𝑛)))
43	17, 30, 37, 42	addge0d 11902	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
44		rexr 11365	. . . . . 6 ⊢ (((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ^*)
45	12	a1i 11	. . . . . 6 ⊢ (((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → +∞ ∈ ℝ^*)
46		ltpnf 13259	. . . . . 6 ⊢ (((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) < +∞)
47	44, 45, 46	xrltled 13289	. . . . 5 ⊢ (((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ ℝ → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ≤ +∞)
48	31, 47	syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ≤ +∞)
49	11, 13, 32, 43, 48	eliccxrd 46678	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) ∈ (0[,]+∞))
50	1, 3, 49	sge0xrclmpt 47577	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) ∈ ℝ^*)
51	5, 35	ffvelcdmd 7093	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(𝐴[,)𝐵)) ∈ (0[,]+∞))
52	1, 3, 51	sge0xrclmpt 47577	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) ∈ ℝ^*)
53	19	rexrd 11369	. . 3 ⊢ (𝜑 → 𝑊 ∈ ℝ^*)
54	52, 53	xaddcld 13441	. 2 ⊢ (𝜑 → ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +_e 𝑊) ∈ ℝ^*)
55	14, 30	resubcld 11754	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 − (𝑊 / (2↑𝑛))) ∈ ℝ)
56		volioore 47139	. . . . . . . 8 ⊢ (((𝐴 − (𝑊 / (2↑𝑛))) ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0))
57	55, 15, 56	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0))
58	57	adantr 486	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0))
59		iftrue 4490	. . . . . . 7 ⊢ ((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵 → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))))
60	59	adantl 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))))
61	15	recnd 11347	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵 ∈ ℂ)
62	14	recnd 11347	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℂ)
63	30	recnd 11347	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℂ)
64	61, 62, 63	subsubd 11707	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))) = ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛))))
65	64	adantr 486	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))) = ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛))))
66	58, 60, 65	3eqtrd 2802	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛))))
67	15, 14	resubcld 11754	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 − 𝐴) ∈ ℝ)
68	14, 15	sublevolico 47133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 − 𝐴) ≤ (vol‘(𝐴[,)𝐵)))
69	67, 17, 30, 68	leadd1dd 11940	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛))) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
70	69	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → ((𝐵 − 𝐴) + (𝑊 / (2↑𝑛))) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
71	66, 70	eqbrtrd 5129	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
72	57	adantr 486	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0))
73		iffalse 4493	. . . . . . 7 ⊢ (¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵 → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = 0)
74	73	adantl 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → if((𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵, (𝐵 − (𝐴 − (𝑊 / (2↑𝑛)))), 0) = 0)
75	72, 74	eqtrd 2798	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) = 0)
76	43	adantr 486	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → 0 ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
77	75, 76	eqbrtrd 5129	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ (𝐴 − (𝑊 / (2↑𝑛))) ≤ 𝐵) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
78	71, 77	pm2.61dan 825	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)) ≤ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
79	1, 3, 8, 49, 78	sge0lempt 47559	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)))) ≤ (Σ^{^}‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))))
80	17, 30	rexaddd 13374	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) +_e (𝑊 / (2↑𝑛))) = ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))
81	80	eqcomd 2769	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))) = ((vol‘(𝐴[,)𝐵)) +_e (𝑊 / (2↑𝑛))))
82	81	mpteq2dva 5200	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛)))) = (𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) +_e (𝑊 / (2↑𝑛)))))
83	82	fveq2d 6897	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) = (Σ^{^}‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) +_e (𝑊 / (2↑𝑛))))))
84	30	rexrd 11369	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ ℝ^*)
85		rexr 11365	. . . . . . . 8 ⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → (𝑊 / (2↑𝑛)) ∈ ℝ^*)
86	12	a1i 11	. . . . . . . 8 ⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → +∞ ∈ ℝ^*)
87		ltpnf 13259	. . . . . . . 8 ⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → (𝑊 / (2↑𝑛)) < +∞)
88	85, 86, 87	xrltled 13289	. . . . . . 7 ⊢ ((𝑊 / (2↑𝑛)) ∈ ℝ → (𝑊 / (2↑𝑛)) ≤ +∞)
89	30, 88	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ≤ +∞)
90	11, 13, 84, 42, 89	eliccxrd 46678	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑊 / (2↑𝑛)) ∈ (0[,]+∞))
91	1, 3, 51, 90	sge0xadd 47584	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) +_e (𝑊 / (2↑𝑛))))) = ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +_e (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑊 / (2↑𝑛))))))
92	10	a1i 11	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℝ^*)
93	12	a1i 11	. . . . . . 7 ⊢ (𝜑 → +∞ ∈ ℝ^*)
94	18	rpge0d 13178	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 𝑊)
95	19	ltpnfd 13260	. . . . . . 7 ⊢ (𝜑 → 𝑊 < +∞)
96	92, 93, 53, 94, 95	elicod 13536	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ (0[,)+∞))
97	96	sge0ad2en 47580	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑊 / (2↑𝑛)))) = 𝑊)
98	97	oveq2d 7443	. . . 4 ⊢ (𝜑 → ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +_e (Σ^{^}‘(𝑛 ∈ ℕ ↦ (𝑊 / (2↑𝑛))))) = ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +_e 𝑊))
99	83, 91, 98	3eqtrd 2802	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) = ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +_e 𝑊))
100	50, 99	xreqled 46481	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ ((vol‘(𝐴[,)𝐵)) + (𝑊 / (2↑𝑛))))) ≤ ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +_e 𝑊))
101	9, 50, 54, 79, 100	xrletrd 13301	1 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘((𝐴 − (𝑊 / (2↑𝑛)))(,)𝐵)))) ≤ ((Σ^{^}‘(𝑛 ∈ ℕ ↦ (vol‘(𝐴[,)𝐵)))) +_e 𝑊))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2146 ≠ wne 2958 {crab 3415 Vcvv 3453 ifcif 4484 class class class wbr 5105 ↦ cmpt 5188 dom cdm 5654 ⟶wf 6542 ‘cfv 6546 (class class class)co 7427 ℝcr 11209 0cc0 11210 + caddc 11213 +∞cpnf 11350 ℝ^*cxr 11352 < clt 11353 ≤ cle 11354 − cmin 11551 / cdiv 11983 ℕcn 12345 2c2 12407 ℕ₀cn0 12616 ℝ⁺crp 13130 +_e cxad 13249 (,)cioo 13486 [,)cico 13488 [,]cicc 13489 ↑cexp 14214 volcvol 25796 Σ^{^}csumge0 47511

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-rep 5234 ax-sep 5251 ax-nul 5262 ax-pow 5330 ax-pr 5394 ax-un 7758 ax-inf2 9652 ax-cnex 11266 ax-resscn 11267 ax-1cn 11268 ax-icn 11269 ax-addcl 11270 ax-addrcl 11271 ax-mulcl 11272 ax-mulrcl 11273 ax-mulcom 11274 ax-addass 11275 ax-mulass 11276 ax-distr 11277 ax-i2m1 11278 ax-1ne0 11279 ax-1rid 11280 ax-rnegex 11281 ax-rrecex 11282 ax-cnre 11283 ax-pre-lttri 11284 ax-pre-lttrn 11285 ax-pre-ltadd 11286 ax-pre-mulgt0 11287 ax-pre-sup 11288

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3455 df-sbc 3742 df-csb 3851 df-ss 3900 df-pss 4016 df-dif 4049 df-in 4093 df-un 4153 df-nul 4281 df-if 4485 df-pw 4561 df-sn 4588 df-pr 4590 df-op 4838 df-uni 4870 df-int 4910 df-iun 4955 df-br 5106 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5549 df-eprel 5554 df-po 5562 df-so 5563 df-fr 5607 df-se 5608 df-we 5609 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6310 df-ord 6371 df-on 6372 df-lim 6373 df-suc 6374 df-iota 6500 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554 df-isom 6555 df-riota 7384 df-ov 7430 df-oprab 7431 df-mpo 7432 df-of 7700 df-om 7885 df-1st 8008 df-2nd 8009 df-frecs 8310 df-wrecs 8341 df-recs 8390 df-rdg 8429 df-1o 8487 df-2o 8488 df-er 8728 df-map 8860 df-pm 8861 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-fi 9413 df-sup 9444 df-inf 9445 df-oi 9514 df-dju 9992 df-card 10030 df-pnf 11355 df-mnf 11356 df-xr 11357 df-ltxr 11358 df-le 11359 df-sub 11553 df-neg 11554 df-div 11984 df-nn 12346 df-2 12415 df-3 12416 df-n0 12617 df-z 12704 df-uz 12976 df-q 13086 df-rp 13131 df-xneg 13251 df-xadd 13252 df-xmul 13253 df-ioo 13490 df-ico 13492 df-icc 13493 df-fz 13650 df-fzo 13799 df-fl 13942 df-seq 14155 df-exp 14215 df-hash 14485 df-cj 15278 df-re 15279 df-im 15280 df-sqrt 15414 df-abs 15415 df-clim 15667 df-rlim 15668 df-sum 15866 df-rest 17605 df-topgen 17626 df-psmet 21682 df-xmet 21683 df-met 21684 df-bl 21685 df-mopn 21686 df-top 23224 df-topon 23241 df-bases 23276 df-cmp 23717 df-ovol 25797 df-vol 25798 df-sumge0 47512

This theorem is used by: ovolval5lem2 47802

W3C validator