Theorem itgmulc2nc 32472

Description: Choice-free analogue of itgmulc2 23351. (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 13731	. . . . . . . 8 ⊢ (𝜑 → (ℜ‘𝐶) ∈ ℝ)
3	2	recnd 9925	. . . . . . 7 ⊢ (𝜑 → (ℜ‘𝐶) ∈ ℂ)
4	3	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐶) ∈ ℂ)
5		itgmulc2nc.3	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)
6		iblmbf 23285	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
7	5, 6	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
8		itgmulc2nc.2	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
9	7, 8	mbfmptcl 23155	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
10	9	recld 13731	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℝ)
11	10	recnd 9925	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℂ)
12	4, 11	mulcld 9917	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℜ‘𝐶) · (ℜ‘𝐵)) ∈ ℂ)
13	9	iblcn 23316	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1)))
14	5, 13	mpbid 220	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1))
15	14	simpld 473	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1)
16		itgmulc2nc.m	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)
17		ovex 6555	. . . . . . . . . 10 ⊢ (𝐶 · 𝐵) ∈ V
18	17	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ V)
19	16, 18	mbfdm2 23156	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ dom vol)
20		fconstmpt 5075	. . . . . . . . 9 ⊢ (𝐴 × {(ℜ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶))
21	20	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝐴 × {(ℜ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶)))
22		eqidd 2610	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)))
23	19, 4, 10, 21, 22	offval2 6790	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘𝑓 · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))))
24		iblmbf 23285	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn)
25	15, 24	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn)
26		eqid 2609	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))
27	11, 26	fmptd 6277	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)):𝐴⟶ℂ)
28	25, 2, 27	mbfmulc2re 23166	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘𝑓 · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) ∈ MblFn)
29	23, 28	eqeltrrd 2688	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))) ∈ MblFn)
30	3, 10, 15, 29	iblmulc2nc 32469	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))) ∈ 𝐿1)
31	12, 30	itgcl 23301	. . . 4 ⊢ (𝜑 → ∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ)
32		ax-icn 9852	. . . . 5 ⊢ i ∈ ℂ
33	9	imcld 13732	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℝ)
34	33	recnd 9925	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℂ)
35	4, 34	mulcld 9917	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℜ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ)
36	14	simprd 477	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1)
37		eqidd 2610	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)))
38	19, 4, 33, 21, 37	offval2 6790	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘𝑓 · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))))
39		iblmbf 23285	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn)
40	36, 39	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn)
41		eqid 2609	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))
42	34, 41	fmptd 6277	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)):𝐴⟶ℂ)
43	40, 2, 42	mbfmulc2re 23166	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘𝑓 · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn)
44	38, 43	eqeltrrd 2688	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn)
45	3, 33, 36, 44	iblmulc2nc 32469	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))) ∈ 𝐿1)
46	35, 45	itgcl 23301	. . . . 5 ⊢ (𝜑 → ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ)
47		mulcl 9877	. . . . 5 ⊢ ((i ∈ ℂ ∧ ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ) → (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) ∈ ℂ)
48	32, 46, 47	sylancr 693	. . . 4 ⊢ (𝜑 → (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) ∈ ℂ)
49	1	imcld 13732	. . . . . . . . 9 ⊢ (𝜑 → (ℑ‘𝐶) ∈ ℝ)
50	49	recnd 9925	. . . . . . . 8 ⊢ (𝜑 → (ℑ‘𝐶) ∈ ℂ)
51	50	negcld 10231	. . . . . . 7 ⊢ (𝜑 → -(ℑ‘𝐶) ∈ ℂ)
52	51	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘𝐶) ∈ ℂ)
53	52, 34	mulcld 9917	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(ℑ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ)
54		fconstmpt 5075	. . . . . . . . 9 ⊢ (𝐴 × {-(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ -(ℑ‘𝐶))
55	54	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝐴 × {-(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ -(ℑ‘𝐶)))
56	19, 52, 33, 55, 37	offval2 6790	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {-(ℑ‘𝐶)}) ∘𝑓 · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))))
57	49	renegcld 10309	. . . . . . . 8 ⊢ (𝜑 → -(ℑ‘𝐶) ∈ ℝ)
58	40, 57, 42	mbfmulc2re 23166	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {-(ℑ‘𝐶)}) ∘𝑓 · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn)
59	56, 58	eqeltrrd 2688	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn)
60	51, 33, 36, 59	iblmulc2nc 32469	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))) ∈ 𝐿1)
61	53, 60	itgcl 23301	. . . 4 ⊢ (𝜑 → ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ)
62	50	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐶) ∈ ℂ)
63	62, 11	mulcld 9917	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℑ‘𝐶) · (ℜ‘𝐵)) ∈ ℂ)
64		fconstmpt 5075	. . . . . . . . . 10 ⊢ (𝐴 × {(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶))
65	64	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 × {(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶)))
66	19, 62, 10, 65, 22	offval2 6790	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘𝑓 · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))))
67	25, 49, 27	mbfmulc2re 23166	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘𝑓 · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) ∈ MblFn)
68	66, 67	eqeltrrd 2688	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))) ∈ MblFn)
69	50, 10, 15, 68	iblmulc2nc 32469	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))) ∈ 𝐿1)
70	63, 69	itgcl 23301	. . . . 5 ⊢ (𝜑 → ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ)
71		mulcl 9877	. . . . 5 ⊢ ((i ∈ ℂ ∧ ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ) → (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) ∈ ℂ)
72	32, 70, 71	sylancr 693	. . . 4 ⊢ (𝜑 → (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) ∈ ℂ)
73	31, 48, 61, 72	add4d 10116	. . 3 ⊢ (𝜑 → ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) + ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
74	32	a1i 11	. . . . . 6 ⊢ (𝜑 → i ∈ ℂ)
75	74, 50	mulcld 9917	. . . . 5 ⊢ (𝜑 → (i · (ℑ‘𝐶)) ∈ ℂ)
76	8, 5	itgcl 23301	. . . . 5 ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ∈ ℂ)
77	3, 75, 76	adddird 9922	. . . 4 ⊢ (𝜑 → (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥) = (((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) + ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥)))
78	8, 5	itgcnval 23317	. . . . . . 7 ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)))
79	78	oveq2d 6543	. . . . . 6 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) = ((ℜ‘𝐶) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
80	10, 15	itgcl 23301	. . . . . . 7 ⊢ (𝜑 → ∫𝐴(ℜ‘𝐵) d𝑥 ∈ ℂ)
81	33, 36	itgcl 23301	. . . . . . . 8 ⊢ (𝜑 → ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ)
82		mulcl 9877	. . . . . . . 8 ⊢ ((i ∈ ℂ ∧ ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ) → (i · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ)
83	32, 81, 82	sylancr 693	. . . . . . 7 ⊢ (𝜑 → (i · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ)
84	3, 80, 83	adddid 9921	. . . . . 6 ⊢ (𝜑 → ((ℜ‘𝐶) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
85	3, 10, 15, 29, 2, 10	itgmulc2nclem2 32471	. . . . . . 7 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) = ∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥)
86	3, 74, 81	mul12d 10097	. . . . . . . 8 ⊢ (𝜑 → ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)))
87	3, 33, 36, 44, 2, 33	itgmulc2nclem2 32471	. . . . . . . . 9 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)
88	87	oveq2d 6543	. . . . . . . 8 ⊢ (𝜑 → (i · ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥))
89	86, 88	eqtrd 2643	. . . . . . 7 ⊢ (𝜑 → ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥))
90	85, 89	oveq12d 6545	. . . . . 6 ⊢ (𝜑 → (((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)))
91	79, 84, 90	3eqtrd 2647	. . . . 5 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)))
92	78	oveq2d 6543	. . . . . 6 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥) = ((i · (ℑ‘𝐶)) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
93	75, 80, 83	adddid 9921	. . . . . 6 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
94	74, 50, 80	mulassd 9920	. . . . . . . . 9 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) = (i · ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥)))
95	50, 10, 15, 68, 49, 10	itgmulc2nclem2 32471	. . . . . . . . . 10 ⊢ (𝜑 → ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) = ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)
96	95	oveq2d 6543	. . . . . . . . 9 ⊢ (𝜑 → (i · ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥)) = (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
97	94, 96	eqtrd 2643	. . . . . . . 8 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) = (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
98	74, 50, 74, 81	mul4d 10100	. . . . . . . . 9 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = ((i · i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)))
99		ixi 10508	. . . . . . . . . . 11 ⊢ (i · i) = -1
100	99	oveq1i 6537	. . . . . . . . . 10 ⊢ ((i · i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = (-1 · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
101	50, 81	mulcld 9917	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ)
102	101	mulm1d 10334	. . . . . . . . . 10 ⊢ (𝜑 → (-1 · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
103	100, 102	syl5eq 2655	. . . . . . . . 9 ⊢ (𝜑 → ((i · i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
104	50, 81	mulneg1d 10335	. . . . . . . . . 10 ⊢ (𝜑 → (-(ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
105	51, 33, 36, 59, 57, 33	itgmulc2nclem2 32471	. . . . . . . . . 10 ⊢ (𝜑 → (-(ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
106	104, 105	eqtr3d 2645	. . . . . . . . 9 ⊢ (𝜑 → -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
107	98, 103, 106	3eqtrd 2647	. . . . . . . 8 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
108	97, 107	oveq12d 6545	. . . . . . 7 ⊢ (𝜑 → (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = ((i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
109	72, 61	addcomd 10090	. . . . . . 7 ⊢ (𝜑 → ((i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
110	108, 109	eqtrd 2643	. . . . . 6 ⊢ (𝜑 → (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
111	92, 93, 110	3eqtrd 2647	. . . . 5 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
112	91, 111	oveq12d 6545	. . . 4 ⊢ (𝜑 → (((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) + ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥)) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
113	77, 112	eqtrd 2643	. . 3 ⊢ (𝜑 → (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
114	62, 34	mulcld 9917	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℑ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ)
115	19, 62, 33, 65, 37	offval2 6790	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘𝑓 · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))))
116	40, 49, 42	mbfmulc2re 23166	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘𝑓 · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn)
117	115, 116	eqeltrrd 2688	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn)
118	50, 33, 36, 117	iblmulc2nc 32469	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))) ∈ 𝐿1)
119	1	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
120	119, 9	mulcld 9917	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ ℂ)
121		eqidd 2610	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)))
122		ref 13649	. . . . . . . . . . 11 ⊢ ℜ:ℂ⟶ℝ
123	122	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℜ:ℂ⟶ℝ)
124	123	feqmptd 6144	. . . . . . . . 9 ⊢ (𝜑 → ℜ = (𝑘 ∈ ℂ ↦ (ℜ‘𝑘)))
125		fveq2 6088	. . . . . . . . 9 ⊢ (𝑘 = (𝐶 · 𝐵) → (ℜ‘𝑘) = (ℜ‘(𝐶 · 𝐵)))
126	120, 121, 124, 125	fmptco 6288	. . . . . . . 8 ⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐶 · 𝐵))))
127	119, 9	remuld 13755	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐶 · 𝐵)) = (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))))
128	127	mpteq2dva 4666	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))))
129	126, 128	eqtrd 2643	. . . . . . 7 ⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))))
130		eqid 2609	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))
131	120, 130	fmptd 6277	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ)
132		ismbfcn 23149	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ↔ ((ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)))
133	131, 132	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ↔ ((ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)))
134	16, 133	mpbid 220	. . . . . . . 8 ⊢ (𝜑 → ((ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn))
135	134	simpld 473	. . . . . . 7 ⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)
136	129, 135	eqeltrrd 2688	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))) ∈ MblFn)
137	12, 30, 114, 118, 136	itgsubnc 32466	. . . . 5 ⊢ (𝜑 → ∫𝐴(((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
138	127	itgeq2dv 23299	. . . . 5 ⊢ (𝜑 → ∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 = ∫𝐴(((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))) d𝑥)
139	114, 118	itgneg 23321	. . . . . . . 8 ⊢ (𝜑 → -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴-((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
140	62, 34	mulneg1d 10335	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(ℑ‘𝐶) · (ℑ‘𝐵)) = -((ℑ‘𝐶) · (ℑ‘𝐵)))
141	140	itgeq2dv 23299	. . . . . . . 8 ⊢ (𝜑 → ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴-((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
142	139, 141	eqtr4d 2646	. . . . . . 7 ⊢ (𝜑 → -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
143	142	oveq2d 6543	. . . . . 6 ⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
144	114, 118	itgcl 23301	. . . . . . 7 ⊢ (𝜑 → ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ)
145	31, 144	negsubd 10250	. . . . . 6 ⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
146	143, 145	eqtr3d 2645	. . . . 5 ⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
147	137, 138, 146	3eqtr4d 2653	. . . 4 ⊢ (𝜑 → ∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
148	119, 9	immuld 13756	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘(𝐶 · 𝐵)) = (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))))
149	148	itgeq2dv 23299	. . . . . . 7 ⊢ (𝜑 → ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥 = ∫𝐴(((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))) d𝑥)
150		imf 13650	. . . . . . . . . . . . 13 ⊢ ℑ:ℂ⟶ℝ
151	150	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℑ:ℂ⟶ℝ)
152	151	feqmptd 6144	. . . . . . . . . . 11 ⊢ (𝜑 → ℑ = (𝑘 ∈ ℂ ↦ (ℑ‘𝑘)))
153		fveq2 6088	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐶 · 𝐵) → (ℑ‘𝑘) = (ℑ‘(𝐶 · 𝐵)))
154	120, 121, 152, 153	fmptco 6288	. . . . . . . . . 10 ⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐶 · 𝐵))))
155	148	mpteq2dva 4666	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))))
156	154, 155	eqtrd 2643	. . . . . . . . 9 ⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))))
157	134	simprd 477	. . . . . . . . 9 ⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)
158	156, 157	eqeltrrd 2688	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))) ∈ MblFn)
159	35, 45, 63, 69, 158	itgaddnc 32464	. . . . . . 7 ⊢ (𝜑 → ∫𝐴(((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
160	149, 159	eqtrd 2643	. . . . . 6 ⊢ (𝜑 → ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
161	160	oveq2d 6543	. . . . 5 ⊢ (𝜑 → (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥) = (i · (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
162	74, 46, 70	adddid 9921	. . . . 5 ⊢ (𝜑 → (i · (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)) = ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
163	161, 162	eqtrd 2643	. . . 4 ⊢ (𝜑 → (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥) = ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
164	147, 163	oveq12d 6545	. . 3 ⊢ (𝜑 → (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) + ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
165	73, 113, 164	3eqtr4d 2653	. 2 ⊢ (𝜑 → (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥) = (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)))
166	1	replimd 13734	. . 3 ⊢ (𝜑 → 𝐶 = ((ℜ‘𝐶) + (i · (ℑ‘𝐶))))
167	166	oveq1d 6542	. 2 ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥))
168	1, 8, 5, 16	iblmulc2nc 32469	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1)
169	120, 168	itgcnval 23317	. 2 ⊢ (𝜑 → ∫𝐴(𝐶 · 𝐵) d𝑥 = (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)))
170	165, 167, 169	3eqtr4d 2653	1 ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)

Syntax hints:   → wi 4   ↔ wb 194   ∧ wa 382   = wceq 1474   ∈ wcel 1976  Vcvv 3172  {csn 4124   ↦ cmpt 4637   × cxp 5026  dom cdm 5028   ∘ ccom 5032  ⟶wf 5786  ‘cfv 5790  (class class class)co 6527   ∘_𝑓 cof 6771  ℂcc 9791  ℝcr 9792  1c1 9794  ici 9795   + caddc 9796   · cmul 9798   − cmin 10118  -cneg 10119  ℜcre 13634  ℑcim 13635  volcvol 22984  MblFncmbf 23134  𝐿¹cibl 23137  ∫citg 23138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871  ax-addf 9872

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-disj 4548  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-ofr 6774  df-om 6936  df-1st 7037  df-2nd 7038  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-map 7724  df-pm 7725  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fi 8178  df-sup 8209  df-inf 8210  df-oi 8276  df-card 8626  df-cda 8851  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-4 10931  df-n0 11143  df-z 11214  df-uz 11523  df-q 11624  df-rp 11668  df-xneg 11781  df-xadd 11782  df-xmul 11783  df-ioo 12009  df-ico 12011  df-icc 12012  df-fz 12156  df-fzo 12293  df-fl 12413  df-mod 12489  df-seq 12622  df-exp 12681  df-hash 12938  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-clim 14016  df-sum 14214  df-rest 15855  df-topgen 15876  df-psmet 19508  df-xmet 19509  df-met 19510  df-bl 19511  df-mopn 19512  df-top 20469  df-bases 20470  df-topon 20471  df-cmp 20948  df-ovol 22985  df-vol 22986  df-mbf 23139  df-itg1 23140  df-itg2 23141  df-ibl 23142  df-itg 23143  df-0p 23188

This theorem is referenced by:  itgabsnc  32473