iblabsr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > iblabsr		Structured version Visualization version GIF version

Theorem iblabsr 25788

Description: A measurable function is integrable iff its absolute value is integrable. (See iblabs 25787 for the forward implication.) (Contributed by Mario Carneiro, 25-Aug-2014.)

**Hypotheses**
Ref	Expression
iblabsr.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
iblabsr.2	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
iblabsr.3	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿¹)

**Assertion**
Ref	Expression
iblabsr	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹)

Distinct variable groups: 𝑥,𝐴 𝜑,𝑥 𝑥,𝑉 Allowed substitution hint: 𝐵(𝑥)

Proof of Theorem iblabsr Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iblabsr.2	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
2		ifan 4559	. . . . . . 7 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0), 0)
3		iblabsr.1	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
4	1, 3	mbfmptcl 25594	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
5	4	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
6		ax-icn 11193	. . . . . . . . . . . . . 14 ⊢ i ∈ ℂ
7		ine0 11677	. . . . . . . . . . . . . 14 ⊢ i ≠ 0
8		elfzelz 13546	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...3) → 𝑘 ∈ ℤ)
9	8	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 𝑘 ∈ ℤ)
10		expclz 14107	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ∈ ℂ)
11	6, 7, 9, 10	mp3an12i 1467	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (i↑𝑘) ∈ ℂ)
12		expne0i 14117	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ≠ 0)
13	6, 7, 9, 12	mp3an12i 1467	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (i↑𝑘) ≠ 0)
14	5, 11, 13	divcld 12022	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (𝐵 / (i↑𝑘)) ∈ ℂ)
15	14	recld 15218	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐵 / (i↑𝑘))) ∈ ℝ)
16		0re 11242	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
17		ifcl 4551	. . . . . . . . . . 11 ⊢ (((ℜ‘(𝐵 / (i↑𝑘))) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ∈ ℝ)
18	15, 16, 17	sylancl 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ∈ ℝ)
19	18	rexrd 11290	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ∈ ℝ^*)
20		max1 13206	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ (ℜ‘(𝐵 / (i↑𝑘))) ∈ ℝ) → 0 ≤ if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0))
21	16, 15, 20	sylancr 587	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0))
22		elxrge0 13479	. . . . . . . . 9 ⊢ (if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ∈ (0[,]+∞) ↔ (if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ∈ ℝ^* ∧ 0 ≤ if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))
23	19, 21, 22	sylanbrc 583	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ∈ (0[,]+∞))
24		0e0iccpnf 13481	. . . . . . . . 9 ⊢ 0 ∈ (0[,]+∞)
25	24	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ (0[,]+∞))
26	23, 25	ifclda 4541	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0), 0) ∈ (0[,]+∞))
27	2, 26	eqeltrid 2839	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ∈ (0[,]+∞))
28	27	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ∈ (0[,]+∞))
29	28	fmpttd 7110	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞))
30		iblabsr.3	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿¹)
31	4	abscld 15460	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ ℝ)
32	4	absge0d 15468	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (abs‘𝐵))
33	31, 32	iblpos 25751	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) ∈ ℝ)))
34	30, 33	mpbid 232	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) ∈ ℝ))
35	34	simprd 495	. . . . 5 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) ∈ ℝ)
36	35	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) ∈ ℝ)
37	31	rexrd 11290	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ ℝ^*)
38		elxrge0 13479	. . . . . . . . . 10 ⊢ ((abs‘𝐵) ∈ (0[,]+∞) ↔ ((abs‘𝐵) ∈ ℝ^* ∧ 0 ≤ (abs‘𝐵)))
39	37, 32, 38	sylanbrc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ (0[,]+∞))
40	24	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ (0[,]+∞))
41	39, 40	ifclda 4541	. . . . . . . 8 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ∈ (0[,]+∞))
42	41	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ∈ (0[,]+∞))
43	42	fmpttd 7110	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)):ℝ⟶(0[,]+∞))
44	43	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)):ℝ⟶(0[,]+∞))
45	14	releabsd 15475	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐵 / (i↑𝑘))) ≤ (abs‘(𝐵 / (i↑𝑘))))
46	5, 11, 13	absdivd 15479	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐵 / (i↑𝑘))) = ((abs‘𝐵) / (abs‘(i↑𝑘))))
47		elfznn0 13642	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (0...3) → 𝑘 ∈ ℕ₀)
48	47	ad2antlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 𝑘 ∈ ℕ₀)
49		absexp 15328	. . . . . . . . . . . . . . . . 17 ⊢ ((i ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (abs‘(i↑𝑘)) = ((abs‘i)↑𝑘))
50	6, 48, 49	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘(i↑𝑘)) = ((abs‘i)↑𝑘))
51		absi 15310	. . . . . . . . . . . . . . . . . 18 ⊢ (abs‘i) = 1
52	51	oveq1i 7420	. . . . . . . . . . . . . . . . 17 ⊢ ((abs‘i)↑𝑘) = (1↑𝑘)
53		1exp 14114	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℤ → (1↑𝑘) = 1)
54	9, 53	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (1↑𝑘) = 1)
55	52, 54	eqtrid 2783	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘i)↑𝑘) = 1)
56	50, 55	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘(i↑𝑘)) = 1)
57	56	oveq2d 7426	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐵) / (abs‘(i↑𝑘))) = ((abs‘𝐵) / 1))
58	31	recnd 11268	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ ℂ)
59	58	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ ℂ)
60	59	div1d 12014	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐵) / 1) = (abs‘𝐵))
61	46, 57, 60	3eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐵 / (i↑𝑘))) = (abs‘𝐵))
62	45, 61	breqtrd 5150	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐵 / (i↑𝑘))) ≤ (abs‘𝐵))
63	5	absge0d 15468	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 0 ≤ (abs‘𝐵))
64		breq1 5127	. . . . . . . . . . . . 13 ⊢ ((ℜ‘(𝐵 / (i↑𝑘))) = if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) → ((ℜ‘(𝐵 / (i↑𝑘))) ≤ (abs‘𝐵) ↔ if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ≤ (abs‘𝐵)))
65		breq1 5127	. . . . . . . . . . . . 13 ⊢ (0 = if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) → (0 ≤ (abs‘𝐵) ↔ if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ≤ (abs‘𝐵)))
66	64, 65	ifboth 4545	. . . . . . . . . . . 12 ⊢ (((ℜ‘(𝐵 / (i↑𝑘))) ≤ (abs‘𝐵) ∧ 0 ≤ (abs‘𝐵)) → if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ≤ (abs‘𝐵))
67	62, 63, 66	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ≤ (abs‘𝐵))
68		iftrue 4511	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0))
69	68	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0))
70		iftrue 4511	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) = (abs‘𝐵))
71	70	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) = (abs‘𝐵))
72	67, 69, 71	3brtr4d 5156	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))
73	72	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)))
74		0le0 12346	. . . . . . . . . . 11 ⊢ 0 ≤ 0
75	74	a1i 11	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝐴 → 0 ≤ 0)
76		iffalse 4514	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0), 0) = 0)
77		iffalse 4514	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) = 0)
78	75, 76, 77	3brtr4d 5156	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))
79	73, 78	pm2.61d1 180	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐵 / (i↑𝑘))), (ℜ‘(𝐵 / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))
80	2, 79	eqbrtrid 5159	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))
81	80	ralrimivw 3137	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))
82		reex 11225	. . . . . . . 8 ⊢ ℝ ∈ V
83	82	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ℝ ∈ V)
84	37	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ ℝ^*)
85	84, 63, 38	sylanbrc 583	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ (0[,]+∞))
86	85, 25	ifclda 4541	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ∈ (0[,]+∞))
87	86	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ∈ (0[,]+∞))
88		eqidd 2737	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))
89		eqidd 2737	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)))
90	83, 28, 87, 88, 89	ofrfval2 7697	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) ↔ ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)))
91	81, 90	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)))
92		itg2le 25697	. . . . 5 ⊢ (((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))))
93	29, 44, 91, 92	syl3anc 1373	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))))
94		itg2lecl 25696	. . . 4 ⊢ (((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)))) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ)
95	29, 36, 93, 94	syl3anc 1373	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ)
96	95	ralrimiva 3133	. 2 ⊢ (𝜑 → ∀𝑘 ∈ (0...3)(∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ)
97		eqidd 2737	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)))
98		eqidd 2737	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐵 / (i↑𝑘))) = (ℜ‘(𝐵 / (i↑𝑘))))
99	97, 98, 3	isibl2 25724	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ)))
100	1, 96, 99	mpbir2and 713	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2933 ∀wral 3052 Vcvv 3464 ifcif 4505 class class class wbr 5124 ↦ cmpt 5206 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ∘_r cofr 7675 ℂcc 11132 ℝcr 11133 0cc0 11134 1c1 11135 ici 11136 +∞cpnf 11271 ℝ^*cxr 11273 ≤ cle 11275 / cdiv 11899 3c3 12301 ℕ₀cn0 12506 ℤcz 12593 [,]cicc 13370 ...cfz 13529 ↑cexp 14084 ℜcre 15121 abscabs 15258 MblFncmbf 25572 ∫₂citg2 25574 𝐿¹cibl 25575

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-inf2 9660 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212 ax-addf 11213

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-disj 5092 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7676 df-ofr 7677 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-er 8724 df-map 8847 df-pm 8848 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-sup 9459 df-inf 9460 df-oi 9529 df-dju 9920 df-card 9958 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-n0 12507 df-z 12594 df-uz 12858 df-q 12970 df-rp 13014 df-xadd 13134 df-ioo 13371 df-ico 13373 df-icc 13374 df-fz 13530 df-fzo 13677 df-fl 13814 df-seq 14025 df-exp 14085 df-hash 14354 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260 df-clim 15509 df-sum 15708 df-xmet 21313 df-met 21314 df-ovol 25422 df-vol 25423 df-mbf 25577 df-itg1 25578 df-itg2 25579 df-ibl 25580 df-0p 25628

This theorem is referenced by: bddmulibl 25797

W3C validator