Theorem itgmulc2nc 35439

Description: Choice-free analogue of itgmulc2 24546. (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 14614	. . . . . . . 8 ⊢ (𝜑 → (ℜ‘𝐶) ∈ ℝ)
3	2	recnd 10720	. . . . . . 7 ⊢ (𝜑 → (ℜ‘𝐶) ∈ ℂ)
4	3	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐶) ∈ ℂ)
5		itgmulc2nc.3	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)
6		iblmbf 24480	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
7	5, 6	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
8		itgmulc2nc.2	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
9	7, 8	mbfmptcl 24349	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
10	9	recld 14614	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℝ)
11	10	recnd 10720	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℂ)
12	4, 11	mulcld 10712	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℜ‘𝐶) · (ℜ‘𝐵)) ∈ ℂ)
13	9	iblcn 24511	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1)))
14	5, 13	mpbid 235	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1))
15	14	simpld 498	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1)
16		itgmulc2nc.m	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)
17		ovexd 7191	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ V)
18	16, 17	mbfdm2 24350	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ dom vol)
19		fconstmpt 5588	. . . . . . . . 9 ⊢ (𝐴 × {(ℜ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶))
20	19	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝐴 × {(ℜ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶)))
21		eqidd 2759	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)))
22	18, 4, 10, 20, 21	offval2 7430	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))))
23		iblmbf 24480	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn)
24	15, 23	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn)
25	11	fmpttd 6876	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)):𝐴⟶ℂ)
26	24, 2, 25	mbfmulc2re 24361	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) ∈ MblFn)
27	22, 26	eqeltrrd 2853	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))) ∈ MblFn)
28	3, 10, 15, 27	iblmulc2nc 35436	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))) ∈ 𝐿1)
29	12, 28	itgcl 24496	. . . 4 ⊢ (𝜑 → ∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ)
30		ax-icn 10647	. . . . 5 ⊢ i ∈ ℂ
31	9	imcld 14615	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℝ)
32	31	recnd 10720	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℂ)
33	4, 32	mulcld 10712	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℜ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ)
34	14	simprd 499	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1)
35		eqidd 2759	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)))
36	18, 4, 31, 20, 35	offval2 7430	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))))
37		iblmbf 24480	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn)
38	34, 37	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn)
39	32	fmpttd 6876	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)):𝐴⟶ℂ)
40	38, 2, 39	mbfmulc2re 24361	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn)
41	36, 40	eqeltrrd 2853	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn)
42	3, 31, 34, 41	iblmulc2nc 35436	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))) ∈ 𝐿1)
43	33, 42	itgcl 24496	. . . . 5 ⊢ (𝜑 → ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ)
44		mulcl 10672	. . . . 5 ⊢ ((i ∈ ℂ ∧ ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ) → (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) ∈ ℂ)
45	30, 43, 44	sylancr 590	. . . 4 ⊢ (𝜑 → (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) ∈ ℂ)
46	1	imcld 14615	. . . . . . . . 9 ⊢ (𝜑 → (ℑ‘𝐶) ∈ ℝ)
47	46	recnd 10720	. . . . . . . 8 ⊢ (𝜑 → (ℑ‘𝐶) ∈ ℂ)
48	47	negcld 11035	. . . . . . 7 ⊢ (𝜑 → -(ℑ‘𝐶) ∈ ℂ)
49	48	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘𝐶) ∈ ℂ)
50	49, 32	mulcld 10712	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(ℑ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ)
51		fconstmpt 5588	. . . . . . . . 9 ⊢ (𝐴 × {-(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ -(ℑ‘𝐶))
52	51	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝐴 × {-(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ -(ℑ‘𝐶)))
53	18, 49, 31, 52, 35	offval2 7430	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {-(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))))
54	46	renegcld 11118	. . . . . . . 8 ⊢ (𝜑 → -(ℑ‘𝐶) ∈ ℝ)
55	38, 54, 39	mbfmulc2re 24361	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {-(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn)
56	53, 55	eqeltrrd 2853	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn)
57	48, 31, 34, 56	iblmulc2nc 35436	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))) ∈ 𝐿1)
58	50, 57	itgcl 24496	. . . 4 ⊢ (𝜑 → ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ)
59	47	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐶) ∈ ℂ)
60	59, 11	mulcld 10712	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℑ‘𝐶) · (ℜ‘𝐵)) ∈ ℂ)
61		fconstmpt 5588	. . . . . . . . . 10 ⊢ (𝐴 × {(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶))
62	61	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 × {(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶)))
63	18, 59, 10, 62, 21	offval2 7430	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))))
64	24, 46, 25	mbfmulc2re 24361	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) ∈ MblFn)
65	63, 64	eqeltrrd 2853	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))) ∈ MblFn)
66	47, 10, 15, 65	iblmulc2nc 35436	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))) ∈ 𝐿1)
67	60, 66	itgcl 24496	. . . . 5 ⊢ (𝜑 → ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ)
68		mulcl 10672	. . . . 5 ⊢ ((i ∈ ℂ ∧ ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ) → (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) ∈ ℂ)
69	30, 67, 68	sylancr 590	. . . 4 ⊢ (𝜑 → (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) ∈ ℂ)
70	29, 45, 58, 69	add4d 10919	. . 3 ⊢ (𝜑 → ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) + ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
71	30	a1i 11	. . . . . 6 ⊢ (𝜑 → i ∈ ℂ)
72	71, 47	mulcld 10712	. . . . 5 ⊢ (𝜑 → (i · (ℑ‘𝐶)) ∈ ℂ)
73	8, 5	itgcl 24496	. . . . 5 ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ∈ ℂ)
74	3, 72, 73	adddird 10717	. . . 4 ⊢ (𝜑 → (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥) = (((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) + ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥)))
75	8, 5	itgcnval 24512	. . . . . . 7 ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)))
76	75	oveq2d 7172	. . . . . 6 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) = ((ℜ‘𝐶) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
77	10, 15	itgcl 24496	. . . . . . 7 ⊢ (𝜑 → ∫𝐴(ℜ‘𝐵) d𝑥 ∈ ℂ)
78	31, 34	itgcl 24496	. . . . . . . 8 ⊢ (𝜑 → ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ)
79		mulcl 10672	. . . . . . . 8 ⊢ ((i ∈ ℂ ∧ ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ) → (i · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ)
80	30, 78, 79	sylancr 590	. . . . . . 7 ⊢ (𝜑 → (i · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ)
81	3, 77, 80	adddid 10716	. . . . . 6 ⊢ (𝜑 → ((ℜ‘𝐶) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
82	3, 10, 15, 27, 2, 10	itgmulc2nclem2 35438	. . . . . . 7 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) = ∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥)
83	3, 71, 78	mul12d 10900	. . . . . . . 8 ⊢ (𝜑 → ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)))
84	3, 31, 34, 41, 2, 31	itgmulc2nclem2 35438	. . . . . . . . 9 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)
85	84	oveq2d 7172	. . . . . . . 8 ⊢ (𝜑 → (i · ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥))
86	83, 85	eqtrd 2793	. . . . . . 7 ⊢ (𝜑 → ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥))
87	82, 86	oveq12d 7174	. . . . . 6 ⊢ (𝜑 → (((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)))
88	76, 81, 87	3eqtrd 2797	. . . . 5 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)))
89	75	oveq2d 7172	. . . . . 6 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥) = ((i · (ℑ‘𝐶)) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
90	72, 77, 80	adddid 10716	. . . . . 6 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
91	71, 47, 77	mulassd 10715	. . . . . . . . 9 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) = (i · ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥)))
92	47, 10, 15, 65, 46, 10	itgmulc2nclem2 35438	. . . . . . . . . 10 ⊢ (𝜑 → ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) = ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)
93	92	oveq2d 7172	. . . . . . . . 9 ⊢ (𝜑 → (i · ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥)) = (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
94	91, 93	eqtrd 2793	. . . . . . . 8 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) = (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
95	71, 47, 71, 78	mul4d 10903	. . . . . . . . 9 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = ((i · i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)))
96		ixi 11320	. . . . . . . . . . 11 ⊢ (i · i) = -1
97	96	oveq1i 7166	. . . . . . . . . 10 ⊢ ((i · i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = (-1 · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
98	47, 78	mulcld 10712	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ)
99	98	mulm1d 11143	. . . . . . . . . 10 ⊢ (𝜑 → (-1 · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
100	97, 99	syl5eq 2805	. . . . . . . . 9 ⊢ (𝜑 → ((i · i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
101	47, 78	mulneg1d 11144	. . . . . . . . . 10 ⊢ (𝜑 → (-(ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
102	48, 31, 34, 56, 54, 31	itgmulc2nclem2 35438	. . . . . . . . . 10 ⊢ (𝜑 → (-(ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
103	101, 102	eqtr3d 2795	. . . . . . . . 9 ⊢ (𝜑 → -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
104	95, 100, 103	3eqtrd 2797	. . . . . . . 8 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
105	94, 104	oveq12d 7174	. . . . . . 7 ⊢ (𝜑 → (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = ((i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
106	69, 58	addcomd 10893	. . . . . . 7 ⊢ (𝜑 → ((i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
107	105, 106	eqtrd 2793	. . . . . 6 ⊢ (𝜑 → (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
108	89, 90, 107	3eqtrd 2797	. . . . 5 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
109	88, 108	oveq12d 7174	. . . 4 ⊢ (𝜑 → (((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) + ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥)) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
110	74, 109	eqtrd 2793	. . 3 ⊢ (𝜑 → (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
111	59, 32	mulcld 10712	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℑ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ)
112	18, 59, 31, 62, 35	offval2 7430	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))))
113	38, 46, 39	mbfmulc2re 24361	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn)
114	112, 113	eqeltrrd 2853	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn)
115	47, 31, 34, 114	iblmulc2nc 35436	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))) ∈ 𝐿1)
116	1	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
117	116, 9	mulcld 10712	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ ℂ)
118		eqidd 2759	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)))
119		ref 14532	. . . . . . . . . . 11 ⊢ ℜ:ℂ⟶ℝ
120	119	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℜ:ℂ⟶ℝ)
121	120	feqmptd 6726	. . . . . . . . 9 ⊢ (𝜑 → ℜ = (𝑘 ∈ ℂ ↦ (ℜ‘𝑘)))
122		fveq2 6663	. . . . . . . . 9 ⊢ (𝑘 = (𝐶 · 𝐵) → (ℜ‘𝑘) = (ℜ‘(𝐶 · 𝐵)))
123	117, 118, 121, 122	fmptco 6888	. . . . . . . 8 ⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐶 · 𝐵))))
124	116, 9	remuld 14638	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐶 · 𝐵)) = (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))))
125	124	mpteq2dva 5131	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))))
126	123, 125	eqtrd 2793	. . . . . . 7 ⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))))
127	117	fmpttd 6876	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ)
128		ismbfcn 24342	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ↔ ((ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)))
129	127, 128	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ↔ ((ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)))
130	16, 129	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → ((ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn))
131	130	simpld 498	. . . . . . 7 ⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)
132	126, 131	eqeltrrd 2853	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))) ∈ MblFn)
133	12, 28, 111, 115, 132	itgsubnc 35433	. . . . 5 ⊢ (𝜑 → ∫𝐴(((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
134	124	itgeq2dv 24494	. . . . 5 ⊢ (𝜑 → ∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 = ∫𝐴(((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))) d𝑥)
135	111, 115	itgneg 24516	. . . . . . . 8 ⊢ (𝜑 → -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴-((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
136	59, 32	mulneg1d 11144	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(ℑ‘𝐶) · (ℑ‘𝐵)) = -((ℑ‘𝐶) · (ℑ‘𝐵)))
137	136	itgeq2dv 24494	. . . . . . . 8 ⊢ (𝜑 → ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴-((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
138	135, 137	eqtr4d 2796	. . . . . . 7 ⊢ (𝜑 → -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
139	138	oveq2d 7172	. . . . . 6 ⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
140	111, 115	itgcl 24496	. . . . . . 7 ⊢ (𝜑 → ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ)
141	29, 140	negsubd 11054	. . . . . 6 ⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
142	139, 141	eqtr3d 2795	. . . . 5 ⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
143	133, 134, 142	3eqtr4d 2803	. . . 4 ⊢ (𝜑 → ∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
144	116, 9	immuld 14639	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘(𝐶 · 𝐵)) = (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))))
145	144	itgeq2dv 24494	. . . . . . 7 ⊢ (𝜑 → ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥 = ∫𝐴(((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))) d𝑥)
146		imf 14533	. . . . . . . . . . . . 13 ⊢ ℑ:ℂ⟶ℝ
147	146	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℑ:ℂ⟶ℝ)
148	147	feqmptd 6726	. . . . . . . . . . 11 ⊢ (𝜑 → ℑ = (𝑘 ∈ ℂ ↦ (ℑ‘𝑘)))
149		fveq2 6663	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐶 · 𝐵) → (ℑ‘𝑘) = (ℑ‘(𝐶 · 𝐵)))
150	117, 118, 148, 149	fmptco 6888	. . . . . . . . . 10 ⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐶 · 𝐵))))
151	144	mpteq2dva 5131	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))))
152	150, 151	eqtrd 2793	. . . . . . . . 9 ⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))))
153	130	simprd 499	. . . . . . . . 9 ⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)
154	152, 153	eqeltrrd 2853	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))) ∈ MblFn)
155	33, 42, 60, 66, 154	itgaddnc 35431	. . . . . . 7 ⊢ (𝜑 → ∫𝐴(((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
156	145, 155	eqtrd 2793	. . . . . 6 ⊢ (𝜑 → ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
157	156	oveq2d 7172	. . . . 5 ⊢ (𝜑 → (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥) = (i · (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
158	71, 43, 67	adddid 10716	. . . . 5 ⊢ (𝜑 → (i · (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)) = ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
159	157, 158	eqtrd 2793	. . . 4 ⊢ (𝜑 → (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥) = ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
160	143, 159	oveq12d 7174	. . 3 ⊢ (𝜑 → (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) + ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
161	70, 110, 160	3eqtr4d 2803	. 2 ⊢ (𝜑 → (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥) = (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)))
162	1	replimd 14617	. . 3 ⊢ (𝜑 → 𝐶 = ((ℜ‘𝐶) + (i · (ℑ‘𝐶))))
163	162	oveq1d 7171	. 2 ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥))
164	1, 8, 5, 16	iblmulc2nc 35436	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1)
165	117, 164	itgcnval 24512	. 2 ⊢ (𝜑 → ∫𝐴(𝐶 · 𝐵) d𝑥 = (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)))
166	161, 163, 165	3eqtr4d 2803	1 ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Vcvv 3409  {csn 4525   ↦ cmpt 5116   × cxp 5526  dom cdm 5528   ∘ ccom 5532  ⟶wf 6336  ‘cfv 6340  (class class class)co 7156   ∘_f cof 7409  ℂcc 10586  ℝcr 10587  1c1 10589  ici 10590   + caddc 10591   · cmul 10593   − cmin 10921  -cneg 10922  ℜcre 14517  ℑcim 14518  volcvol 24176  MblFncmbf 24327  𝐿¹cibl 24330  ∫citg 24331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-inf2 9150  ax-cnex 10644  ax-resscn 10645  ax-1cn 10646  ax-icn 10647  ax-addcl 10648  ax-addrcl 10649  ax-mulcl 10650  ax-mulrcl 10651  ax-mulcom 10652  ax-addass 10653  ax-mulass 10654  ax-distr 10655  ax-i2m1 10656  ax-1ne0 10657  ax-1rid 10658  ax-rnegex 10659  ax-rrecex 10660  ax-cnre 10661  ax-pre-lttri 10662  ax-pre-lttrn 10663  ax-pre-ltadd 10664  ax-pre-mulgt0 10665  ax-pre-sup 10666  ax-addf 10667

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-disj 5002  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-isom 6349  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-of 7411  df-ofr 7412  df-om 7586  df-1st 7699  df-2nd 7700  df-wrecs 7963  df-recs 8024  df-rdg 8062  df-1o 8118  df-2o 8119  df-er 8305  df-map 8424  df-pm 8425  df-en 8541  df-dom 8542  df-sdom 8543  df-fin 8544  df-fi 8921  df-sup 8952  df-inf 8953  df-oi 9020  df-dju 9376  df-card 9414  df-pnf 10728  df-mnf 10729  df-xr 10730  df-ltxr 10731  df-le 10732  df-sub 10923  df-neg 10924  df-div 11349  df-nn 11688  df-2 11750  df-3 11751  df-4 11752  df-n0 11948  df-z 12034  df-uz 12296  df-q 12402  df-rp 12444  df-xneg 12561  df-xadd 12562  df-xmul 12563  df-ioo 12796  df-ico 12798  df-icc 12799  df-fz 12953  df-fzo 13096  df-fl 13224  df-mod 13300  df-seq 13432  df-exp 13493  df-hash 13754  df-cj 14519  df-re 14520  df-im 14521  df-sqrt 14655  df-abs 14656  df-clim 14906  df-sum 15104  df-rest 16767  df-topgen 16788  df-psmet 20171  df-xmet 20172  df-met 20173  df-bl 20174  df-mopn 20175  df-top 21607  df-topon 21624  df-bases 21659  df-cmp 22100  df-ovol 24177  df-vol 24178  df-mbf 24332  df-itg1 24333  df-itg2 24334  df-ibl 24335  df-itg 24336  df-0p 24383

This theorem is referenced by:  itgabsnc  35440