iblmulc2nc - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > iblmulc2nc		Structured version Visualization version GIF version

Theorem iblmulc2nc 33800

Description: Choice-free analogue of iblmulc2 23810. (Contributed by Brendan Leahy, 17-Nov-2017.)

**Hypotheses**
Ref	Expression
itgmulc2nc.1	⊢ (𝜑 → 𝐶 ∈ ℂ)
itgmulc2nc.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
itgmulc2nc.3	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹)
itgmulc2nc.m	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)

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

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

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

Step	Hyp	Ref	Expression
1		itgmulc2nc.m	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)
2		ifan 4273	. . . . . 6 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0)
3		itgmulc2nc.1	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4	3	adantr 466	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
5		itgmulc2nc.3	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹)
6		iblmbf 23747	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹ → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
7	5, 6	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
8		itgmulc2nc.2	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
9	7, 8	mbfmptcl 23617	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
10	4, 9	mulcld 10260	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ ℂ)
11	10	adantlr 694	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ ℂ)
12		elfzelz 12542	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...3) → 𝑘 ∈ ℤ)
13	12	ad2antlr 706	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 𝑘 ∈ ℤ)
14		ax-icn 10195	. . . . . . . . . . . . . . 15 ⊢ i ∈ ℂ
15		ine0 10665	. . . . . . . . . . . . . . 15 ⊢ i ≠ 0
16		expclz 13085	. . . . . . . . . . . . . . 15 ⊢ ((i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ∈ ℂ)
17	14, 15, 16	mp3an12 1562	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℤ → (i↑𝑘) ∈ ℂ)
18	13, 17	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (i↑𝑘) ∈ ℂ)
19		expne0i 13092	. . . . . . . . . . . . . . 15 ⊢ ((i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ≠ 0)
20	14, 15, 19	mp3an12 1562	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℤ → (i↑𝑘) ≠ 0)
21	13, 20	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (i↑𝑘) ≠ 0)
22	11, 18, 21	divcld 11001	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((𝐶 · 𝐵) / (i↑𝑘)) ∈ ℂ)
23	22	recld 14135	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ∈ ℝ)
24		0re 10240	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
25		ifcl 4269	. . . . . . . . . . 11 ⊢ (((ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ)
26	23, 24, 25	sylancl 574	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ)
27	26	rexrd 10289	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ^*)
28		max1 12214	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ∈ ℝ) → 0 ≤ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))
29	24, 23, 28	sylancr 575	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))
30		elxrge0 12481	. . . . . . . . 9 ⊢ (if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ (0[,]+∞) ↔ (if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ^* ∧ 0 ≤ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)))
31	27, 29, 30	sylanbrc 572	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ (0[,]+∞))
32		0e0iccpnf 12483	. . . . . . . . 9 ⊢ 0 ∈ (0[,]+∞)
33	32	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ (0[,]+∞))
34	31, 33	ifclda 4259	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ∈ (0[,]+∞))
35	34	adantr 466	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ∈ (0[,]+∞))
36	2, 35	syl5eqel 2854	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ (0[,]+∞))
37		eqid 2771	. . . . 5 ⊢ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))
38	36, 37	fmptd 6525	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞))
39	9	recld 14135	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℝ)
40	39	recnd 10268	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℂ)
41	40	abscld 14376	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℜ‘𝐵)) ∈ ℝ)
42	9	imcld 14136	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℝ)
43	42	recnd 10268	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℂ)
44	43	abscld 14376	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) ∈ ℝ)
45	41, 44	readdcld 10269	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))) ∈ ℝ)
46	40	absge0d 14384	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (abs‘(ℜ‘𝐵)))
47	43	absge0d 14384	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (abs‘(ℑ‘𝐵)))
48	41, 44, 46, 47	addge0d 10803	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))))
49		elrege0 12478	. . . . . . . . . . . 12 ⊢ (((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))) ∈ (0[,)+∞) ↔ (((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))) ∈ ℝ ∧ 0 ≤ ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))))
50	45, 48, 49	sylanbrc 572	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))) ∈ (0[,)+∞))
51		0e0icopnf 12482	. . . . . . . . . . . 12 ⊢ 0 ∈ (0[,)+∞)
52	51	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ (0[,)+∞))
53	50, 52	ifclda 4259	. . . . . . . . . 10 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0) ∈ (0[,)+∞))
54	53	adantr 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0) ∈ (0[,)+∞))
55		eqid 2771	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))
56	54, 55	fmptd 6525	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)):ℝ⟶(0[,)+∞))
57		reex 10227	. . . . . . . . . . . . . 14 ⊢ ℝ ∈ V
58	57	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℝ ∈ V)
59		elrege0 12478	. . . . . . . . . . . . . . . 16 ⊢ ((abs‘(ℜ‘𝐵)) ∈ (0[,)+∞) ↔ ((abs‘(ℜ‘𝐵)) ∈ ℝ ∧ 0 ≤ (abs‘(ℜ‘𝐵))))
60	41, 46, 59	sylanbrc 572	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℜ‘𝐵)) ∈ (0[,)+∞))
61	60, 52	ifclda 4259	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) ∈ (0[,)+∞))
62	61	adantr 466	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) ∈ (0[,)+∞))
63		elrege0 12478	. . . . . . . . . . . . . . . 16 ⊢ ((abs‘(ℑ‘𝐵)) ∈ (0[,)+∞) ↔ ((abs‘(ℑ‘𝐵)) ∈ ℝ ∧ 0 ≤ (abs‘(ℑ‘𝐵))))
64	44, 47, 63	sylanbrc 572	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) ∈ (0[,)+∞))
65	64, 52	ifclda 4259	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) ∈ (0[,)+∞))
66	65	adantr 466	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) ∈ (0[,)+∞))
67		eqidd 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)))
68		eqidd 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))
69	58, 62, 66, 67, 68	offval2 7059	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘_𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))
70		iftrue 4231	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) = (abs‘(ℜ‘𝐵)))
71		iftrue 4231	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) = (abs‘(ℑ‘𝐵)))
72	70, 71	oveq12d 6809	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))))
73		iftrue 4231	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0) = ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))))
74	72, 73	eqtr4d 2808	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))
75		00id 10411	. . . . . . . . . . . . . . 15 ⊢ (0 + 0) = 0
76		iffalse 4234	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) = 0)
77		iffalse 4234	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) = 0)
78	76, 77	oveq12d 6809	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = (0 + 0))
79		iffalse 4234	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0) = 0)
80	75, 78, 79	3eqtr4a 2831	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))
81	74, 80	pm2.61i 176	. . . . . . . . . . . . 13 ⊢ (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)
82	81	mpteq2i 4875	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))
83	69, 82	syl6req 2822	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘_𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))
84	83	fveq2d 6334	. . . . . . . . . 10 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) = (∫₂‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘_𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))))
85		eqid 2771	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))
86	9	iblcn 23778	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿¹)))
87	5, 86	mpbid 222	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿¹))
88	87	simpld 482	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿¹)
89	8, 5, 85, 88, 39	iblabsnclem 33798	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∈ MblFn ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) ∈ ℝ))
90	89	simpld 482	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∈ MblFn)
91	62, 85	fmptd 6525	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)):ℝ⟶(0[,)+∞))
92	89	simprd 483	. . . . . . . . . . 11 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) ∈ ℝ)
93		eqid 2771	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))
94	66, 93	fmptd 6525	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)):ℝ⟶(0[,)+∞))
95	87	simprd 483	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿¹)
96	8, 5, 93, 95, 42	iblabsnclem 33798	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) ∈ MblFn ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) ∈ ℝ))
97	96	simprd 483	. . . . . . . . . . 11 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) ∈ ℝ)
98	90, 91, 92, 94, 97	itg2addnc 33789	. . . . . . . . . 10 ⊢ (𝜑 → (∫₂‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘_𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))))
99	84, 98	eqtrd 2805	. . . . . . . . 9 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))))
100	92, 97	readdcld 10269	. . . . . . . . 9 ⊢ (𝜑 → ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) ∈ ℝ)
101	99, 100	eqeltrd 2850	. . . . . . . 8 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) ∈ ℝ)
102	3	abscld 14376	. . . . . . . . 9 ⊢ (𝜑 → (abs‘𝐶) ∈ ℝ)
103	3	absge0d 14384	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (abs‘𝐶))
104		elrege0 12478	. . . . . . . . 9 ⊢ ((abs‘𝐶) ∈ (0[,)+∞) ↔ ((abs‘𝐶) ∈ ℝ ∧ 0 ≤ (abs‘𝐶)))
105	102, 103, 104	sylanbrc 572	. . . . . . . 8 ⊢ (𝜑 → (abs‘𝐶) ∈ (0[,)+∞))
106	56, 101, 105	itg2mulc 23727	. . . . . . 7 ⊢ (𝜑 → (∫₂‘((ℝ × {(abs‘𝐶)}) ∘_𝑓 · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))) = ((abs‘𝐶) · (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))))
107	102	adantr 466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝐶) ∈ ℝ)
108		fconstmpt 5301	. . . . . . . . . . 11 ⊢ (ℝ × {(abs‘𝐶)}) = (𝑥 ∈ ℝ ↦ (abs‘𝐶))
109	108	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ × {(abs‘𝐶)}) = (𝑥 ∈ ℝ ↦ (abs‘𝐶)))
110		eqidd 2772	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))
111	58, 107, 54, 109, 110	offval2 7059	. . . . . . . . 9 ⊢ (𝜑 → ((ℝ × {(abs‘𝐶)}) ∘_𝑓 · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) = (𝑥 ∈ ℝ ↦ ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))))
112	73	oveq2d 6807	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)) = ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))))
113		iftrue 4231	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0) = ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))))
114	112, 113	eqtr4d 2808	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 → ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)) = if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))
115	114	adantl 467	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)) = if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))
116	102	recnd 10268	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘𝐶) ∈ ℂ)
117	116	mul01d 10435	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((abs‘𝐶) · 0) = 0)
118	117	adantr 466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · 0) = 0)
119	79	adantl 467	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0) = 0)
120	119	oveq2d 6807	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)) = ((abs‘𝐶) · 0))
121		iffalse 4234	. . . . . . . . . . . . 13 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0) = 0)
122	121	adantl 467	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0) = 0)
123	118, 120, 122	3eqtr4d 2815	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)) = if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))
124	115, 123	pm2.61dan 814	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)) = if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))
125	124	mpteq2dv 4879	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)))
126	111, 125	eqtrd 2805	. . . . . . . 8 ⊢ (𝜑 → ((ℝ × {(abs‘𝐶)}) ∘_𝑓 · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)))
127	126	fveq2d 6334	. . . . . . 7 ⊢ (𝜑 → (∫₂‘((ℝ × {(abs‘𝐶)}) ∘_𝑓 · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))) = (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))))
128	99	oveq2d 6807	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐶) · (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))) = ((abs‘𝐶) · ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))))
129	106, 127, 128	3eqtr3d 2813	. . . . . 6 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))) = ((abs‘𝐶) · ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))))
130	102, 100	remulcld 10270	. . . . . 6 ⊢ (𝜑 → ((abs‘𝐶) · ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))) ∈ ℝ)
131	129, 130	eqeltrd 2850	. . . . 5 ⊢ (𝜑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))) ∈ ℝ)
132	131	adantr 466	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))) ∈ ℝ)
133	102	adantr 466	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐶) ∈ ℝ)
134	133, 45	remulcld 10270	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) ∈ ℝ)
135	134	rexrd 10289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) ∈ ℝ^*)
136	103	adantr 466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (abs‘𝐶))
137	133, 45, 136, 48	mulge0d 10804	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))))
138		elxrge0 12481	. . . . . . . . 9 ⊢ (((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) ∈ (0[,]+∞) ↔ (((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) ∈ ℝ^* ∧ 0 ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))))))
139	135, 137, 138	sylanbrc 572	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) ∈ (0[,]+∞))
140	32	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈ (0[,]+∞))
141	139, 140	ifclda 4259	. . . . . . 7 ⊢ (𝜑 → if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0) ∈ (0[,]+∞))
142	141	ad2antrr 705	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0) ∈ (0[,]+∞))
143		eqid 2771	. . . . . 6 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))
144	142, 143	fmptd 6525	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)):ℝ⟶(0[,]+∞))
145	9	abscld 14376	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ ℝ)
146	133, 145	remulcld 10270	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · (abs‘𝐵)) ∈ ℝ)
147	146	adantlr 694	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · (abs‘𝐵)) ∈ ℝ)
148	134	adantlr 694	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) ∈ ℝ)
149	22	releabsd 14391	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ (abs‘((𝐶 · 𝐵) / (i↑𝑘))))
150	11, 18, 21	absdivd 14395	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘((𝐶 · 𝐵) / (i↑𝑘))) = ((abs‘(𝐶 · 𝐵)) / (abs‘(i↑𝑘))))
151		elfznn0 12633	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (0...3) → 𝑘 ∈ ℕ₀)
152		absexp 14245	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((i ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (abs‘(i↑𝑘)) = ((abs‘i)↑𝑘))
153	14, 151, 152	sylancr 575	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (0...3) → (abs‘(i↑𝑘)) = ((abs‘i)↑𝑘))
154		absi 14227	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs‘i) = 1
155	154	oveq1i 6801	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((abs‘i)↑𝑘) = (1↑𝑘)
156		1exp 13089	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℤ → (1↑𝑘) = 1)
157	12, 156	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (0...3) → (1↑𝑘) = 1)
158	155, 157	syl5eq 2817	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (0...3) → ((abs‘i)↑𝑘) = 1)
159	153, 158	eqtrd 2805	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (0...3) → (abs‘(i↑𝑘)) = 1)
160	159	oveq2d 6807	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...3) → ((abs‘(𝐶 · 𝐵)) / (abs‘(i↑𝑘))) = ((abs‘(𝐶 · 𝐵)) / 1))
161	160	ad2antlr 706	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘(𝐶 · 𝐵)) / (abs‘(i↑𝑘))) = ((abs‘(𝐶 · 𝐵)) / 1))
162	10	abscld 14376	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℝ)
163	162	recnd 10268	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℂ)
164	163	adantlr 694	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℂ)
165	164	div1d 10993	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘(𝐶 · 𝐵)) / 1) = (abs‘(𝐶 · 𝐵)))
166	150, 161, 165	3eqtrd 2809	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘((𝐶 · 𝐵) / (i↑𝑘))) = (abs‘(𝐶 · 𝐵)))
167	4, 9	absmuld 14394	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) = ((abs‘𝐶) · (abs‘𝐵)))
168	167	adantlr 694	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) = ((abs‘𝐶) · (abs‘𝐵)))
169	166, 168	eqtrd 2805	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘((𝐶 · 𝐵) / (i↑𝑘))) = ((abs‘𝐶) · (abs‘𝐵)))
170	149, 169	breqtrd 4812	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ ((abs‘𝐶) · (abs‘𝐵)))
171		mulcl 10220	. . . . . . . . . . . . . . . . . 18 ⊢ ((i ∈ ℂ ∧ (ℑ‘𝐵) ∈ ℂ) → (i · (ℑ‘𝐵)) ∈ ℂ)
172	14, 43, 171	sylancr 575	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (i · (ℑ‘𝐵)) ∈ ℂ)
173	40, 172	abstrid 14396	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘((ℜ‘𝐵) + (i · (ℑ‘𝐵)))) ≤ ((abs‘(ℜ‘𝐵)) + (abs‘(i · (ℑ‘𝐵)))))
174	9	replimd 14138	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = ((ℜ‘𝐵) + (i · (ℑ‘𝐵))))
175	174	fveq2d 6334	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) = (abs‘((ℜ‘𝐵) + (i · (ℑ‘𝐵)))))
176		absmul 14235	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((i ∈ ℂ ∧ (ℑ‘𝐵) ∈ ℂ) → (abs‘(i · (ℑ‘𝐵))) = ((abs‘i) · (abs‘(ℑ‘𝐵))))
177	14, 43, 176	sylancr 575	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(i · (ℑ‘𝐵))) = ((abs‘i) · (abs‘(ℑ‘𝐵))))
178	154	oveq1i 6801	. . . . . . . . . . . . . . . . . . 19 ⊢ ((abs‘i) · (abs‘(ℑ‘𝐵))) = (1 · (abs‘(ℑ‘𝐵)))
179	177, 178	syl6eq 2821	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(i · (ℑ‘𝐵))) = (1 · (abs‘(ℑ‘𝐵))))
180	44	recnd 10268	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) ∈ ℂ)
181	180	mulid2d 10258	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 · (abs‘(ℑ‘𝐵))) = (abs‘(ℑ‘𝐵)))
182	179, 181	eqtr2d 2806	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) = (abs‘(i · (ℑ‘𝐵))))
183	182	oveq2d 6807	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))) = ((abs‘(ℜ‘𝐵)) + (abs‘(i · (ℑ‘𝐵)))))
184	173, 175, 183	3brtr4d 4818	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ≤ ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))))
185	145, 45, 133, 136, 184	lemul2ad 11164	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · (abs‘𝐵)) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))))
186	185	adantlr 694	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · (abs‘𝐵)) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))))
187	23, 147, 148, 170, 186	letrd 10394	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))))
188	137	adantlr 694	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 0 ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))))
189		breq1 4789	. . . . . . . . . . . . 13 ⊢ ((ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) = if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) → ((ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) ↔ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))))))
190		breq1 4789	. . . . . . . . . . . . 13 ⊢ (0 = if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) → (0 ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) ↔ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))))))
191	189, 190	ifboth 4263	. . . . . . . . . . . 12 ⊢ (((ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) ∧ 0 ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))))) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))))
192	187, 188, 191	syl2anc 573	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))))
193		iftrue 4231	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))
194	193	adantl 467	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))
195	113	adantl 467	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0) = ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))))
196	192, 194, 195	3brtr4d 4818	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))
197	196	ex 397	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)))
198		0le0 11310	. . . . . . . . . . 11 ⊢ 0 ≤ 0
199	198	a1i 11	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝐴 → 0 ≤ 0)
200		iffalse 4234	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) = 0)
201	199, 200, 121	3brtr4d 4818	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))
202	197, 201	pm2.61d1 172	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))
203	2, 202	syl5eqbr 4821	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))
204	203	ralrimivw 3116	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))
205	57	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ℝ ∈ V)
206		eqidd 2772	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)))
207		eqidd 2772	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)))
208	205, 36, 142, 206, 207	ofrfval2 7060	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) ∘_𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)) ↔ ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)))
209	204, 208	mpbird 247	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) ∘_𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)))
210		itg2le 23719	. . . . 5 ⊢ (((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) ∘_𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))))
211	38, 144, 209, 210	syl3anc 1476	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))))
212		itg2lecl 23718	. . . 4 ⊢ (((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)))) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ)
213	38, 132, 211, 212	syl3anc 1476	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ)
214	213	ralrimiva 3115	. 2 ⊢ (𝜑 → ∀𝑘 ∈ (0...3)(∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ)
215		eqidd 2772	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)))
216		eqidd 2772	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) = (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))))
217	215, 216, 10	isibl2 23746	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ)))
218	1, 214, 217	mpbir2and 692	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿¹)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 382 = wceq 1631 ∈ wcel 2145 ≠ wne 2943 ∀wral 3061 Vcvv 3351 ifcif 4225 {csn 4316 class class class wbr 4786 ↦ cmpt 4863 × cxp 5247 ⟶wf 6025 ‘cfv 6029 (class class class)co 6791 ∘_𝑓 cof 7040 ∘_𝑟 cofr 7041 ℂcc 10134 ℝcr 10135 0cc0 10136 1c1 10137 ici 10138 + caddc 10139 · cmul 10141 +∞cpnf 10271 ℝ^*cxr 10273 ≤ cle 10275 / cdiv 10884 3c3 11271 ℕ₀cn0 11492 ℤcz 11577 [,)cico 12375 [,]cicc 12376 ...cfz 12526 ↑cexp 13060 ℜcre 14038 ℑcim 14039 abscabs 14175 MblFncmbf 23595 ∫₂citg2 23597 𝐿¹cibl 23598

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4904 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7094 ax-inf2 8700 ax-cnex 10192 ax-resscn 10193 ax-1cn 10194 ax-icn 10195 ax-addcl 10196 ax-addrcl 10197 ax-mulcl 10198 ax-mulrcl 10199 ax-mulcom 10200 ax-addass 10201 ax-mulass 10202 ax-distr 10203 ax-i2m1 10204 ax-1ne0 10205 ax-1rid 10206 ax-rnegex 10207 ax-rrecex 10208 ax-cnre 10209 ax-pre-lttri 10210 ax-pre-lttrn 10211 ax-pre-ltadd 10212 ax-pre-mulgt0 10213 ax-pre-sup 10214 ax-addf 10215

This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-3an 1073 df-tru 1634 df-fal 1637 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-tp 4321 df-op 4323 df-uni 4575 df-int 4612 df-iun 4656 df-disj 4755 df-br 4787 df-opab 4847 df-mpt 4864 df-tr 4887 df-id 5157 df-eprel 5162 df-po 5170 df-so 5171 df-fr 5208 df-se 5209 df-we 5210 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-pred 5821 df-ord 5867 df-on 5868 df-lim 5869 df-suc 5870 df-iota 5992 df-fun 6031 df-fn 6032 df-f 6033 df-f1 6034 df-fo 6035 df-f1o 6036 df-fv 6037 df-isom 6038 df-riota 6752 df-ov 6794 df-oprab 6795 df-mpt2 6796 df-of 7042 df-ofr 7043 df-om 7211 df-1st 7313 df-2nd 7314 df-wrecs 7557 df-recs 7619 df-rdg 7657 df-1o 7711 df-2o 7712 df-oadd 7715 df-er 7894 df-map 8009 df-pm 8010 df-en 8108 df-dom 8109 df-sdom 8110 df-fin 8111 df-fi 8471 df-sup 8502 df-inf 8503 df-oi 8569 df-card 8963 df-cda 9190 df-pnf 10276 df-mnf 10277 df-xr 10278 df-ltxr 10279 df-le 10280 df-sub 10468 df-neg 10469 df-div 10885 df-nn 11221 df-2 11279 df-3 11280 df-n0 11493 df-z 11578 df-uz 11887 df-q 11990 df-rp 12029 df-xneg 12144 df-xadd 12145 df-xmul 12146 df-ioo 12377 df-ico 12379 df-icc 12380 df-fz 12527 df-fzo 12667 df-fl 12794 df-seq 13002 df-exp 13061 df-hash 13315 df-cj 14040 df-re 14041 df-im 14042 df-sqrt 14176 df-abs 14177 df-clim 14420 df-sum 14618 df-rest 16284 df-topgen 16305 df-psmet 19946 df-xmet 19947 df-met 19948 df-bl 19949 df-mopn 19950 df-top 20912 df-topon 20929 df-bases 20964 df-cmp 21404 df-ovol 23445 df-vol 23446 df-mbf 23600 df-itg1 23601 df-itg2 23602 df-ibl 23603 df-0p 23650

This theorem is referenced by: itgmulc2nclem1 33801 itgmulc2nclem2 33802 itgmulc2nc 33803 itgabsnc 33804 ftc1anclem6 33815

W3C validator