iblss - Metamath Proof Explorer

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

Theorem iblss 25762

Description: A subset of an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)

**Hypotheses**
Ref	Expression
iblss.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
iblss.2	⊢ (𝜑 → 𝐴 ∈ dom vol)
iblss.3	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)
iblss.4	⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿¹)

**Assertion**
Ref	Expression
iblss	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿¹)

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

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

Step	Hyp	Ref	Expression
1		iblss.1	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2	1	resmptd 5999	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝐶))
3		iblss.4	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿¹)
4		iblmbf 25724	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿¹ → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn)
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn)
6		iblss.2	. . . 4 ⊢ (𝜑 → 𝐴 ∈ dom vol)
7		mbfres 25601	. . . 4 ⊢ (((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn ∧ 𝐴 ∈ dom vol) → ((𝑥 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴) ∈ MblFn)
8	5, 6, 7	syl2anc 584	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴) ∈ MblFn)
9	2, 8	eqeltrrd 2837	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
10		ifan 4533	. . . . . 6 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)
11	1	sselda 3933	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)
12	11	ad4ant14 752	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)
13		iblss.3	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)
14	5, 13	mbfmptcl 25593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ)
15	14	ad4ant14 752	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ)
16		ax-icn 11085	. . . . . . . . . . . . . 14 ⊢ i ∈ ℂ
17		ine0 11572	. . . . . . . . . . . . . 14 ⊢ i ≠ 0
18		elfzelz 13440	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...3) → 𝑘 ∈ ℤ)
19	18	ad3antlr 731	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℤ)
20		expclz 14007	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ∈ ℂ)
21	16, 17, 19, 20	mp3an12i 1467	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (i↑𝑘) ∈ ℂ)
22		expne0i 14017	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ≠ 0)
23	16, 17, 19, 22	mp3an12i 1467	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (i↑𝑘) ≠ 0)
24	15, 21, 23	divcld 11917	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝐶 / (i↑𝑘)) ∈ ℂ)
25	24	recld 15117	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (ℜ‘(𝐶 / (i↑𝑘))) ∈ ℝ)
26		0re 11134	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
27		ifcl 4525	. . . . . . . . . . 11 ⊢ (((ℜ‘(𝐶 / (i↑𝑘))) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈ ℝ)
28	25, 26, 27	sylancl 586	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈ ℝ)
29	28	rexrd 11182	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈ ℝ^*)
30		max1 13100	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ (ℜ‘(𝐶 / (i↑𝑘))) ∈ ℝ) → 0 ≤ if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0))
31	26, 25, 30	sylancr 587	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 0 ≤ if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0))
32		elxrge0 13373	. . . . . . . . 9 ⊢ (if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈ (0[,]+∞) ↔ (if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈ ℝ^* ∧ 0 ≤ if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))
33	29, 31, 32	sylanbrc 583	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈ (0[,]+∞))
34	12, 33	syldan 591	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈ (0[,]+∞))
35		0e0iccpnf 13375	. . . . . . . 8 ⊢ 0 ∈ (0[,]+∞)
36	35	a1i 11	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ (0[,]+∞))
37	34, 36	ifclda 4515	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) ∈ (0[,]+∞))
38	10, 37	eqeltrid 2840	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈ (0[,]+∞))
39	38	fmpttd 7060	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞))
40		eqidd 2737	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))
41		eqidd 2737	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘))))
42	40, 41, 3, 13	iblitg 25725	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)
43	18, 42	sylan2 593	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)
44		ifan 4533	. . . . . . 7 ⊢ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)
45	35	a1i 11	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐵) → 0 ∈ (0[,]+∞))
46	33, 45	ifclda 4515	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) ∈ (0[,]+∞))
47	44, 46	eqeltrid 2840	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈ (0[,]+∞))
48	47	fmpttd 7060	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞))
49	28	leidd 11703	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ≤ if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0))
50		breq1 5101	. . . . . . . . . . . 12 ⊢ (if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) → (if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ≤ if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ↔ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) ≤ if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))
51		breq1 5101	. . . . . . . . . . . 12 ⊢ (0 = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) → (0 ≤ if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ↔ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) ≤ if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))
52	50, 51	ifboth 4519	. . . . . . . . . . 11 ⊢ ((if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ≤ if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∧ 0 ≤ if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) ≤ if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0))
53	49, 31, 52	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) ≤ if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0))
54		iftrue 4485	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐵 → if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0))
55	54	adantl 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0))
56	53, 55	breqtrrd 5126	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0))
57		0le0 12246	. . . . . . . . . . 11 ⊢ 0 ≤ 0
58	57	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐵) → 0 ≤ 0)
59	12	stoic1a 1773	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐵) → ¬ 𝑥 ∈ 𝐴)
60	59	iffalsed 4490	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = 0)
61		iffalse 4488	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ 𝐵 → if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = 0)
62	61	adantl 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) = 0)
63	58, 60, 62	3brtr4d 5130	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ 𝐵) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0))
64	56, 63	pm2.61dan 812	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0))
65	64, 10, 44	3brtr4g 5132	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ≤ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))
66	65	ralrimiva 3128	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ≤ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))
67		reex 11117	. . . . . . . 8 ⊢ ℝ ∈ V
68	67	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ℝ ∈ V)
69		eqidd 2737	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))
70		eqidd 2737	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))
71	68, 38, 47, 69, 70	ofrfval2 7643	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) ↔ ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ≤ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))
72	66, 71	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))
73		itg2le 25696	. . . . 5 ⊢ (((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))))
74	39, 48, 72, 73	syl3anc 1373	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))))
75		itg2lecl 25695	. . . 4 ⊢ (((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)
76	39, 43, 74, 75	syl3anc 1373	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)
77	76	ralrimiva 3128	. 2 ⊢ (𝜑 → ∀𝑘 ∈ (0...3)(∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)
78		eqidd 2737	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))
79		eqidd 2737	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘))))
80	11, 14	syldan 591	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
81	78, 79, 80	isibl2 25723	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)))
82	9, 77, 81	mpbir2and 713	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿¹)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ≠ wne 2932 ∀wral 3051 Vcvv 3440 ⊆ wss 3901 ifcif 4479 class class class wbr 5098 ↦ cmpt 5179 dom cdm 5624 ↾ cres 5626 ⟶wf 6488 ‘cfv 6492 (class class class)co 7358 ∘_r cofr 7621 ℂcc 11024 ℝcr 11025 0cc0 11026 ici 11028 +∞cpnf 11163 ℝ^*cxr 11165 ≤ cle 11167 / cdiv 11794 3c3 12201 ℤcz 12488 [,]cicc 13264 ...cfz 13423 ↑cexp 13984 ℜcre 15020 volcvol 25420 MblFncmbf 25571 ∫₂citg2 25573 𝐿¹cibl 25574

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 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-inf2 9550 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-ofr 7623 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-2o 8398 df-er 8635 df-map 8765 df-pm 8766 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9345 df-inf 9346 df-oi 9415 df-dju 9813 df-card 9851 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-n0 12402 df-z 12489 df-uz 12752 df-q 12862 df-rp 12906 df-xadd 13027 df-ioo 13265 df-ico 13267 df-icc 13268 df-fz 13424 df-fzo 13571 df-fl 13712 df-mod 13790 df-seq 13925 df-exp 13985 df-hash 14254 df-cj 15022 df-re 15023 df-im 15024 df-sqrt 15158 df-abs 15159 df-clim 15411 df-sum 15610 df-xmet 21302 df-met 21303 df-ovol 25421 df-vol 25422 df-mbf 25576 df-itg1 25577 df-itg2 25578 df-ibl 25579

This theorem is referenced by: itgss3 25772 itgless 25774 bddmulibl 25796 itgcn 25802 ditgcl 25815 ditgswap 25816 ditgsplitlem 25817 ftc1lem1 25998 ftc1lem2 25999 ftc1a 26000 ftc1lem4 26002 ftc2 26007 ftc2ditglem 26008 itgsubstlem 26011 itgpowd 26013 fdvposlt 34756 fdvposle 34758 circlemeth 34797 ftc1cnnclem 37892 ftc1anc 37902 ftc2nc 37903 areacirc 37914 lcmineqlem10 42292 lcmineqlem12 42294 lhe4.4ex1a 44570 itgsin0pilem1 46194 iblioosinexp 46197 itgsinexplem1 46198 itgsinexp 46199 itgcoscmulx 46213 itgsincmulx 46218 iblcncfioo 46222 dirkeritg 46346 fourierdlem87 46437 fourierdlem95 46445 fourierdlem103 46453 fourierdlem104 46454 fourierdlem107 46457 fourierdlem111 46461 fourierdlem112 46462 sqwvfoura 46472 sqwvfourb 46473 etransclem18 46496

W3C validator