Theorem itgmulc2nc 38339

Description: Choice-free analogue of itgmulc2 25993. (Contributed by Brendan Leahy, 19-Nov-2017.)

Hypotheses

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

Assertion

Ref	Expression
itgmulc2nc	⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜑,𝑥   𝑥,𝑉

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem itgmulc2nc

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		itgmulc2nc.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℂ)
2	1	recld 15241	. . . . . . . 8 ⊢ (𝜑 → (ℜ‘𝐶) ∈ ℝ)
3	2	recnd 11232	. . . . . . 7 ⊢ (𝜑 → (ℜ‘𝐶) ∈ ℂ)
4	3	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐶) ∈ ℂ)
5		itgmulc2nc.3	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)
6		iblmbf 25926	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
7	5, 6	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
8		itgmulc2nc.2	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
9	7, 8	mbfmptcl 25795	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
10	9	recld 15241	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℝ)
11	10	recnd 11232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℂ)
12	4, 11	mulcld 11224	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℜ‘𝐶) · (ℜ‘𝐵)) ∈ ℂ)
13	9	iblcn 25958	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1)))
14	5, 13	mpbid 235	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1))
15	14	simpld 499	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1)
16		itgmulc2nc.m	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)
17		ovexd 7445	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ V)
18	16, 17	mbfdm2 25796	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ dom vol)
19		fconstmpt 5723	. . . . . . . . 9 ⊢ (𝐴 × {(ℜ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶))
20	19	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝐴 × {(ℜ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶)))
21		eqidd 2764	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)))
22	18, 4, 10, 20, 21	offval2 7694	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))))
23		iblmbf 25926	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn)
24	15, 23	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn)
25	11	fmpttd 7110	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)):𝐴⟶ℂ)
26	24, 2, 25	mbfmulc2re 25807	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) ∈ MblFn)
27	22, 26	eqeltrrd 2864	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))) ∈ MblFn)
28	3, 10, 15, 27	iblmulc2nc 38336	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))) ∈ 𝐿1)
29	12, 28	itgcl 25943	. . . 4 ⊢ (𝜑 → ∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ)
30		ax-icn 11154	. . . . 5 ⊢ i ∈ ℂ
31	9	imcld 15242	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℝ)
32	31	recnd 11232	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℂ)
33	4, 32	mulcld 11224	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℜ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ)
34	14	simprd 500	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1)
35		eqidd 2764	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)))
36	18, 4, 31, 20, 35	offval2 7694	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))))
37		iblmbf 25926	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn)
38	34, 37	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn)
39	32	fmpttd 7110	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)):𝐴⟶ℂ)
40	38, 2, 39	mbfmulc2re 25807	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn)
41	36, 40	eqeltrrd 2864	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn)
42	3, 31, 34, 41	iblmulc2nc 38336	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))) ∈ 𝐿1)
43	33, 42	itgcl 25943	. . . . 5 ⊢ (𝜑 → ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ)
44		mulcl 11179	. . . . 5 ⊢ ((i ∈ ℂ ∧ ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ) → (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) ∈ ℂ)
45	30, 43, 44	sylancr 598	. . . 4 ⊢ (𝜑 → (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) ∈ ℂ)
46	1	imcld 15242	. . . . . . . . 9 ⊢ (𝜑 → (ℑ‘𝐶) ∈ ℝ)
47	46	recnd 11232	. . . . . . . 8 ⊢ (𝜑 → (ℑ‘𝐶) ∈ ℂ)
48	47	negcld 11551	. . . . . . 7 ⊢ (𝜑 → -(ℑ‘𝐶) ∈ ℂ)
49	48	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘𝐶) ∈ ℂ)
50	49, 32	mulcld 11224	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(ℑ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ)
51		fconstmpt 5723	. . . . . . . . 9 ⊢ (𝐴 × {-(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ -(ℑ‘𝐶))
52	51	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝐴 × {-(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ -(ℑ‘𝐶)))
53	18, 49, 31, 52, 35	offval2 7694	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {-(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))))
54	46	renegcld 11636	. . . . . . . 8 ⊢ (𝜑 → -(ℑ‘𝐶) ∈ ℝ)
55	38, 54, 39	mbfmulc2re 25807	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {-(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn)
56	53, 55	eqeltrrd 2864	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn)
57	48, 31, 34, 56	iblmulc2nc 38336	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))) ∈ 𝐿1)
58	50, 57	itgcl 25943	. . . 4 ⊢ (𝜑 → ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ)
59	47	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐶) ∈ ℂ)
60	59, 11	mulcld 11224	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℑ‘𝐶) · (ℜ‘𝐵)) ∈ ℂ)
61		fconstmpt 5723	. . . . . . . . . 10 ⊢ (𝐴 × {(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶))
62	61	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 × {(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶)))
63	18, 59, 10, 62, 21	offval2 7694	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))))
64	24, 46, 25	mbfmulc2re 25807	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) ∈ MblFn)
65	63, 64	eqeltrrd 2864	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))) ∈ MblFn)
66	47, 10, 15, 65	iblmulc2nc 38336	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))) ∈ 𝐿1)
67	60, 66	itgcl 25943	. . . . 5 ⊢ (𝜑 → ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ)
68		mulcl 11179	. . . . 5 ⊢ ((i ∈ ℂ ∧ ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ) → (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) ∈ ℂ)
69	30, 67, 68	sylancr 598	. . . 4 ⊢ (𝜑 → (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) ∈ ℂ)
70	29, 45, 58, 69	add4d 11434	. . 3 ⊢ (𝜑 → ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) + ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
71	30	a1i 11	. . . . . 6 ⊢ (𝜑 → i ∈ ℂ)
72	71, 47	mulcld 11224	. . . . 5 ⊢ (𝜑 → (i · (ℑ‘𝐶)) ∈ ℂ)
73	8, 5	itgcl 25943	. . . . 5 ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ∈ ℂ)
74	3, 72, 73	adddird 11229	. . . 4 ⊢ (𝜑 → (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥) = (((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) + ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥)))
75	8, 5	itgcnval 25959	. . . . . . 7 ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)))
76	75	oveq2d 7426	. . . . . 6 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) = ((ℜ‘𝐶) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
77	10, 15	itgcl 25943	. . . . . . 7 ⊢ (𝜑 → ∫𝐴(ℜ‘𝐵) d𝑥 ∈ ℂ)
78	31, 34	itgcl 25943	. . . . . . . 8 ⊢ (𝜑 → ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ)
79		mulcl 11179	. . . . . . . 8 ⊢ ((i ∈ ℂ ∧ ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ) → (i · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ)
80	30, 78, 79	sylancr 598	. . . . . . 7 ⊢ (𝜑 → (i · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ)
81	3, 77, 80	adddid 11228	. . . . . 6 ⊢ (𝜑 → ((ℜ‘𝐶) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
82	3, 10, 15, 27, 2, 10	itgmulc2nclem2 38338	. . . . . . 7 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) = ∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥)
83	3, 71, 78	mul12d 11414	. . . . . . . 8 ⊢ (𝜑 → ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)))
84	3, 31, 34, 41, 2, 31	itgmulc2nclem2 38338	. . . . . . . . 9 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)
85	84	oveq2d 7426	. . . . . . . 8 ⊢ (𝜑 → (i · ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥))
86	83, 85	eqtrd 2798	. . . . . . 7 ⊢ (𝜑 → ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥))
87	82, 86	oveq12d 7428	. . . . . 6 ⊢ (𝜑 → (((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)))
88	76, 81, 87	3eqtrd 2802	. . . . 5 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)))
89	75	oveq2d 7426	. . . . . 6 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥) = ((i · (ℑ‘𝐶)) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
90	72, 77, 80	adddid 11228	. . . . . 6 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
91	71, 47, 77	mulassd 11227	. . . . . . . . 9 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) = (i · ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥)))
92	47, 10, 15, 65, 46, 10	itgmulc2nclem2 38338	. . . . . . . . . 10 ⊢ (𝜑 → ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) = ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)
93	92	oveq2d 7426	. . . . . . . . 9 ⊢ (𝜑 → (i · ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥)) = (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
94	91, 93	eqtrd 2798	. . . . . . . 8 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) = (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
95	71, 47, 71, 78	mul4d 11417	. . . . . . . . 9 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = ((i · i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)))
96		ixi 11838	. . . . . . . . . . 11 ⊢ (i · i) = -1
97	96	oveq1i 7420	. . . . . . . . . 10 ⊢ ((i · i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = (-1 · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
98	47, 78	mulcld 11224	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ)
99	98	mulm1d 11661	. . . . . . . . . 10 ⊢ (𝜑 → (-1 · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
100	97, 99	eqtrid 2810	. . . . . . . . 9 ⊢ (𝜑 → ((i · i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
101	47, 78	mulneg1d 11662	. . . . . . . . . 10 ⊢ (𝜑 → (-(ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
102	48, 31, 34, 56, 54, 31	itgmulc2nclem2 38338	. . . . . . . . . 10 ⊢ (𝜑 → (-(ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
103	101, 102	eqtr3d 2800	. . . . . . . . 9 ⊢ (𝜑 → -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
104	95, 100, 103	3eqtrd 2802	. . . . . . . 8 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
105	94, 104	oveq12d 7428	. . . . . . 7 ⊢ (𝜑 → (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = ((i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
106	69, 58	addcomd 11407	. . . . . . 7 ⊢ (𝜑 → ((i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
107	105, 106	eqtrd 2798	. . . . . 6 ⊢ (𝜑 → (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
108	89, 90, 107	3eqtrd 2802	. . . . 5 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
109	88, 108	oveq12d 7428	. . . 4 ⊢ (𝜑 → (((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) + ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥)) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
110	74, 109	eqtrd 2798	. . 3 ⊢ (𝜑 → (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
111	59, 32	mulcld 11224	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℑ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ)
112	18, 59, 31, 62, 35	offval2 7694	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))))
113	38, 46, 39	mbfmulc2re 25807	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn)
114	112, 113	eqeltrrd 2864	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn)
115	47, 31, 34, 114	iblmulc2nc 38336	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))) ∈ 𝐿1)
116	1	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
117	116, 9	mulcld 11224	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ ℂ)
118		eqidd 2764	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)))
119		ref 15159	. . . . . . . . . . 11 ⊢ ℜ:ℂ⟶ℝ
120	119	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℜ:ℂ⟶ℝ)
121	120	feqmptd 6949	. . . . . . . . 9 ⊢ (𝜑 → ℜ = (𝑘 ∈ ℂ ↦ (ℜ‘𝑘)))
122		fveq2 6881	. . . . . . . . 9 ⊢ (𝑘 = (𝐶 · 𝐵) → (ℜ‘𝑘) = (ℜ‘(𝐶 · 𝐵)))
123	117, 118, 121, 122	fmptco 7125	. . . . . . . 8 ⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐶 · 𝐵))))
124	116, 9	remuld 15265	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐶 · 𝐵)) = (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))))
125	124	mpteq2dva 5204	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))))
126	123, 125	eqtrd 2798	. . . . . . 7 ⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))))
127	117	fmpttd 7110	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ)
128		ismbfcn 25788	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ↔ ((ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)))
129	127, 128	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ↔ ((ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)))
130	16, 129	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → ((ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn))
131	130	simpld 499	. . . . . . 7 ⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)
132	126, 131	eqeltrrd 2864	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))) ∈ MblFn)
133	12, 28, 111, 115, 132	itgsubnc 38333	. . . . 5 ⊢ (𝜑 → ∫𝐴(((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
134	124	itgeq2dv 25941	. . . . 5 ⊢ (𝜑 → ∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 = ∫𝐴(((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))) d𝑥)
135	111, 115	itgneg 25963	. . . . . . . 8 ⊢ (𝜑 → -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴-((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
136	59, 32	mulneg1d 11662	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(ℑ‘𝐶) · (ℑ‘𝐵)) = -((ℑ‘𝐶) · (ℑ‘𝐵)))
137	136	itgeq2dv 25941	. . . . . . . 8 ⊢ (𝜑 → ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴-((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
138	135, 137	eqtr4d 2801	. . . . . . 7 ⊢ (𝜑 → -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
139	138	oveq2d 7426	. . . . . 6 ⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
140	111, 115	itgcl 25943	. . . . . . 7 ⊢ (𝜑 → ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ)
141	29, 140	negsubd 11570	. . . . . 6 ⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
142	139, 141	eqtr3d 2800	. . . . 5 ⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
143	133, 134, 142	3eqtr4d 2808	. . . 4 ⊢ (𝜑 → ∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
144	116, 9	immuld 15266	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘(𝐶 · 𝐵)) = (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))))
145	144	itgeq2dv 25941	. . . . . . 7 ⊢ (𝜑 → ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥 = ∫𝐴(((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))) d𝑥)
146		imf 15160	. . . . . . . . . . . . 13 ⊢ ℑ:ℂ⟶ℝ
147	146	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℑ:ℂ⟶ℝ)
148	147	feqmptd 6949	. . . . . . . . . . 11 ⊢ (𝜑 → ℑ = (𝑘 ∈ ℂ ↦ (ℑ‘𝑘)))
149		fveq2 6881	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐶 · 𝐵) → (ℑ‘𝑘) = (ℑ‘(𝐶 · 𝐵)))
150	117, 118, 148, 149	fmptco 7125	. . . . . . . . . 10 ⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐶 · 𝐵))))
151	144	mpteq2dva 5204	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))))
152	150, 151	eqtrd 2798	. . . . . . . . 9 ⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))))
153	130	simprd 500	. . . . . . . . 9 ⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)
154	152, 153	eqeltrrd 2864	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))) ∈ MblFn)
155	33, 42, 60, 66, 154	itgaddnc 38331	. . . . . . 7 ⊢ (𝜑 → ∫𝐴(((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
156	145, 155	eqtrd 2798	. . . . . 6 ⊢ (𝜑 → ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
157	156	oveq2d 7426	. . . . 5 ⊢ (𝜑 → (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥) = (i · (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
158	71, 43, 67	adddid 11228	. . . . 5 ⊢ (𝜑 → (i · (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)) = ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
159	157, 158	eqtrd 2798	. . . 4 ⊢ (𝜑 → (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥) = ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
160	143, 159	oveq12d 7428	. . 3 ⊢ (𝜑 → (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) + ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
161	70, 110, 160	3eqtr4d 2808	. 2 ⊢ (𝜑 → (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥) = (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)))
162	1	replimd 15244	. . 3 ⊢ (𝜑 → 𝐶 = ((ℜ‘𝐶) + (i · (ℑ‘𝐶))))
163	162	oveq1d 7425	. 2 ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥))
164	1, 8, 5, 16	iblmulc2nc 38336	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1)
165	117, 164	itgcnval 25959	. 2 ⊢ (𝜑 → ∫𝐴(𝐶 · 𝐵) d𝑥 = (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)))
166	161, 163, 165	3eqtr4d 2808	1 ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  Vcvv 3455  {csn 4589   ↦ cmpt 5192   × cxp 5659  dom cdm 5661   ∘ ccom 5665  ⟶wf 6532  ‘cfv 6536  (class class class)co 7410   ∘_f cof 7672  ℂcc 11093  ℝcr 11094  1c1 11096  ici 11097   + caddc 11098   · cmul 11100   − cmin 11436  -cneg 11437  ℜcre 15144  ℑcim 15145  volcvol 25622  MblFncmbf 25773  𝐿¹cibl 25776  ∫citg 25777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-inf2 9606  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172  ax-pre-sup 11173  ax-addf 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  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 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-disj 5077  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  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 7674  df-ofr 7675  df-om 7859  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-2o 8450  df-er 8690  df-map 8822  df-pm 8823  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fi 9367  df-sup 9398  df-inf 9399  df-oi 9468  df-dju 9883  df-card 9921  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-div 11867  df-nn 12229  df-2 12298  df-3 12299  df-4 12300  df-n0 12500  df-z 12587  df-uz 12858  df-q 12968  df-rp 13012  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-ioo 13371  df-ico 13373  df-icc 13374  df-fz 13531  df-fzo 13679  df-fl 13821  df-mod 13899  df-seq 14034  df-exp 14094  df-hash 14363  df-cj 15146  df-re 15147  df-im 15148  df-sqrt 15282  df-abs 15283  df-clim 15535  df-sum 15734  df-rest 17470  df-topgen 17491  df-psmet 21514  df-xmet 21515  df-met 21516  df-bl 21517  df-mopn 21518  df-top 23051  df-topon 23068  df-bases 23103  df-cmp 23544  df-ovol 25623  df-vol 25624  df-mbf 25778  df-itg1 25779  df-itg2 25780  df-ibl 25781  df-itg 25782  df-0p 25829

This theorem is referenced by:  itgabsnc  38340