Theorem itgmulc2nc 37648

Description: Choice-free analogue of itgmulc2 25889. (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 15243	. . . . . . . 8 ⊢ (𝜑 → (ℜ‘𝐶) ∈ ℝ)
3	2	recnd 11318	. . . . . . 7 ⊢ (𝜑 → (ℜ‘𝐶) ∈ ℂ)
4	3	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐶) ∈ ℂ)
5		itgmulc2nc.3	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)
6		iblmbf 25822	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
7	5, 6	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
8		itgmulc2nc.2	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
9	7, 8	mbfmptcl 25690	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
10	9	recld 15243	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℝ)
11	10	recnd 11318	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℂ)
12	4, 11	mulcld 11310	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℜ‘𝐶) · (ℜ‘𝐵)) ∈ ℂ)
13	9	iblcn 25854	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1)))
14	5, 13	mpbid 232	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1))
15	14	simpld 494	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1)
16		itgmulc2nc.m	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)
17		ovexd 7483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ V)
18	16, 17	mbfdm2 25691	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ dom vol)
19		fconstmpt 5762	. . . . . . . . 9 ⊢ (𝐴 × {(ℜ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶))
20	19	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝐴 × {(ℜ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐶)))
21		eqidd 2741	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)))
22	18, 4, 10, 20, 21	offval2 7734	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))))
23		iblmbf 25822	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn)
24	15, 23	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ MblFn)
25	11	fmpttd 7149	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)):𝐴⟶ℂ)
26	24, 2, 25	mbfmulc2re 25702	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) ∈ MblFn)
27	22, 26	eqeltrrd 2845	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))) ∈ MblFn)
28	3, 10, 15, 27	iblmulc2nc 37645	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℜ‘𝐵))) ∈ 𝐿1)
29	12, 28	itgcl 25839	. . . 4 ⊢ (𝜑 → ∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ)
30		ax-icn 11243	. . . . 5 ⊢ i ∈ ℂ
31	9	imcld 15244	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℝ)
32	31	recnd 11318	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℂ)
33	4, 32	mulcld 11310	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℜ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ)
34	14	simprd 495	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1)
35		eqidd 2741	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)))
36	18, 4, 31, 20, 35	offval2 7734	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))))
37		iblmbf 25822	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn)
38	34, 37	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ MblFn)
39	32	fmpttd 7149	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)):𝐴⟶ℂ)
40	38, 2, 39	mbfmulc2re 25702	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℜ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn)
41	36, 40	eqeltrrd 2845	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn)
42	3, 31, 34, 41	iblmulc2nc 37645	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℜ‘𝐶) · (ℑ‘𝐵))) ∈ 𝐿1)
43	33, 42	itgcl 25839	. . . . 5 ⊢ (𝜑 → ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ)
44		mulcl 11268	. . . . 5 ⊢ ((i ∈ ℂ ∧ ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ) → (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) ∈ ℂ)
45	30, 43, 44	sylancr 586	. . . 4 ⊢ (𝜑 → (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) ∈ ℂ)
46	1	imcld 15244	. . . . . . . . 9 ⊢ (𝜑 → (ℑ‘𝐶) ∈ ℝ)
47	46	recnd 11318	. . . . . . . 8 ⊢ (𝜑 → (ℑ‘𝐶) ∈ ℂ)
48	47	negcld 11634	. . . . . . 7 ⊢ (𝜑 → -(ℑ‘𝐶) ∈ ℂ)
49	48	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘𝐶) ∈ ℂ)
50	49, 32	mulcld 11310	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(ℑ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ)
51		fconstmpt 5762	. . . . . . . . 9 ⊢ (𝐴 × {-(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ -(ℑ‘𝐶))
52	51	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝐴 × {-(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ -(ℑ‘𝐶)))
53	18, 49, 31, 52, 35	offval2 7734	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {-(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))))
54	46	renegcld 11717	. . . . . . . 8 ⊢ (𝜑 → -(ℑ‘𝐶) ∈ ℝ)
55	38, 54, 39	mbfmulc2re 25702	. . . . . . 7 ⊢ (𝜑 → ((𝐴 × {-(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn)
56	53, 55	eqeltrrd 2845	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn)
57	48, 31, 34, 56	iblmulc2nc 37645	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(ℑ‘𝐶) · (ℑ‘𝐵))) ∈ 𝐿1)
58	50, 57	itgcl 25839	. . . 4 ⊢ (𝜑 → ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ)
59	47	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐶) ∈ ℂ)
60	59, 11	mulcld 11310	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℑ‘𝐶) · (ℜ‘𝐵)) ∈ ℂ)
61		fconstmpt 5762	. . . . . . . . . 10 ⊢ (𝐴 × {(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶))
62	61	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 × {(ℑ‘𝐶)}) = (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐶)))
63	18, 59, 10, 62, 21	offval2 7734	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))))
64	24, 46, 25	mbfmulc2re 25702	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵))) ∈ MblFn)
65	63, 64	eqeltrrd 2845	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))) ∈ MblFn)
66	47, 10, 15, 65	iblmulc2nc 37645	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℜ‘𝐵))) ∈ 𝐿1)
67	60, 66	itgcl 25839	. . . . 5 ⊢ (𝜑 → ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ)
68		mulcl 11268	. . . . 5 ⊢ ((i ∈ ℂ ∧ ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥 ∈ ℂ) → (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) ∈ ℂ)
69	30, 67, 68	sylancr 586	. . . 4 ⊢ (𝜑 → (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) ∈ ℂ)
70	29, 45, 58, 69	add4d 11518	. . 3 ⊢ (𝜑 → ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) + ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
71	30	a1i 11	. . . . . 6 ⊢ (𝜑 → i ∈ ℂ)
72	71, 47	mulcld 11310	. . . . 5 ⊢ (𝜑 → (i · (ℑ‘𝐶)) ∈ ℂ)
73	8, 5	itgcl 25839	. . . . 5 ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ∈ ℂ)
74	3, 72, 73	adddird 11315	. . . 4 ⊢ (𝜑 → (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥) = (((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) + ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥)))
75	8, 5	itgcnval 25855	. . . . . . 7 ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)))
76	75	oveq2d 7464	. . . . . 6 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) = ((ℜ‘𝐶) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
77	10, 15	itgcl 25839	. . . . . . 7 ⊢ (𝜑 → ∫𝐴(ℜ‘𝐵) d𝑥 ∈ ℂ)
78	31, 34	itgcl 25839	. . . . . . . 8 ⊢ (𝜑 → ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ)
79		mulcl 11268	. . . . . . . 8 ⊢ ((i ∈ ℂ ∧ ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ) → (i · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ)
80	30, 78, 79	sylancr 586	. . . . . . 7 ⊢ (𝜑 → (i · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ)
81	3, 77, 80	adddid 11314	. . . . . 6 ⊢ (𝜑 → ((ℜ‘𝐶) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
82	3, 10, 15, 27, 2, 10	itgmulc2nclem2 37647	. . . . . . 7 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) = ∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥)
83	3, 71, 78	mul12d 11499	. . . . . . . 8 ⊢ (𝜑 → ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)))
84	3, 31, 34, 41, 2, 31	itgmulc2nclem2 37647	. . . . . . . . 9 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)
85	84	oveq2d 7464	. . . . . . . 8 ⊢ (𝜑 → (i · ((ℜ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥))
86	83, 85	eqtrd 2780	. . . . . . 7 ⊢ (𝜑 → ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥))
87	82, 86	oveq12d 7466	. . . . . 6 ⊢ (𝜑 → (((ℜ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((ℜ‘𝐶) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)))
88	76, 81, 87	3eqtrd 2784	. . . . 5 ⊢ (𝜑 → ((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)))
89	75	oveq2d 7464	. . . . . 6 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥) = ((i · (ℑ‘𝐶)) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
90	72, 77, 80	adddid 11314	. . . . . 6 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))))
91	71, 47, 77	mulassd 11313	. . . . . . . . 9 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) = (i · ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥)))
92	47, 10, 15, 65, 46, 10	itgmulc2nclem2 37647	. . . . . . . . . 10 ⊢ (𝜑 → ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥) = ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)
93	92	oveq2d 7464	. . . . . . . . 9 ⊢ (𝜑 → (i · ((ℑ‘𝐶) · ∫𝐴(ℜ‘𝐵) d𝑥)) = (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
94	91, 93	eqtrd 2780	. . . . . . . 8 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) = (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
95	71, 47, 71, 78	mul4d 11502	. . . . . . . . 9 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = ((i · i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)))
96		ixi 11919	. . . . . . . . . . 11 ⊢ (i · i) = -1
97	96	oveq1i 7458	. . . . . . . . . 10 ⊢ ((i · i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = (-1 · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
98	47, 78	mulcld 11310	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ)
99	98	mulm1d 11742	. . . . . . . . . 10 ⊢ (𝜑 → (-1 · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
100	97, 99	eqtrid 2792	. . . . . . . . 9 ⊢ (𝜑 → ((i · i) · ((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥)) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
101	47, 78	mulneg1d 11743	. . . . . . . . . 10 ⊢ (𝜑 → (-(ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥))
102	48, 31, 34, 56, 54, 31	itgmulc2nclem2 37647	. . . . . . . . . 10 ⊢ (𝜑 → (-(ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
103	101, 102	eqtr3d 2782	. . . . . . . . 9 ⊢ (𝜑 → -((ℑ‘𝐶) · ∫𝐴(ℑ‘𝐵) d𝑥) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
104	95, 100, 103	3eqtrd 2784	. . . . . . . 8 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
105	94, 104	oveq12d 7466	. . . . . . 7 ⊢ (𝜑 → (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = ((i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
106	69, 58	addcomd 11492	. . . . . . 7 ⊢ (𝜑 → ((i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥) + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
107	105, 106	eqtrd 2780	. . . . . 6 ⊢ (𝜑 → (((i · (ℑ‘𝐶)) · ∫𝐴(ℜ‘𝐵) d𝑥) + ((i · (ℑ‘𝐶)) · (i · ∫𝐴(ℑ‘𝐵) d𝑥))) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
108	89, 90, 107	3eqtrd 2784	. . . . 5 ⊢ (𝜑 → ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥) = (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
109	88, 108	oveq12d 7466	. . . 4 ⊢ (𝜑 → (((ℜ‘𝐶) · ∫𝐴𝐵 d𝑥) + ((i · (ℑ‘𝐶)) · ∫𝐴𝐵 d𝑥)) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
110	74, 109	eqtrd 2780	. . 3 ⊢ (𝜑 → (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + (i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥)) + (∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
111	59, 32	mulcld 11310	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((ℑ‘𝐶) · (ℑ‘𝐵)) ∈ ℂ)
112	18, 59, 31, 62, 35	offval2 7734	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) = (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))))
113	38, 46, 39	mbfmulc2re 25702	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 × {(ℑ‘𝐶)}) ∘f · (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵))) ∈ MblFn)
114	112, 113	eqeltrrd 2845	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))) ∈ MblFn)
115	47, 31, 34, 114	iblmulc2nc 37645	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((ℑ‘𝐶) · (ℑ‘𝐵))) ∈ 𝐿1)
116	1	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
117	116, 9	mulcld 11310	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ ℂ)
118		eqidd 2741	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)))
119		ref 15161	. . . . . . . . . . 11 ⊢ ℜ:ℂ⟶ℝ
120	119	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℜ:ℂ⟶ℝ)
121	120	feqmptd 6990	. . . . . . . . 9 ⊢ (𝜑 → ℜ = (𝑘 ∈ ℂ ↦ (ℜ‘𝑘)))
122		fveq2 6920	. . . . . . . . 9 ⊢ (𝑘 = (𝐶 · 𝐵) → (ℜ‘𝑘) = (ℜ‘(𝐶 · 𝐵)))
123	117, 118, 121, 122	fmptco 7163	. . . . . . . 8 ⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐶 · 𝐵))))
124	116, 9	remuld 15267	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐶 · 𝐵)) = (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))))
125	124	mpteq2dva 5266	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))))
126	123, 125	eqtrd 2780	. . . . . . 7 ⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))))
127	117	fmpttd 7149	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ)
128		ismbfcn 25683	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)):𝐴⟶ℂ → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ↔ ((ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)))
129	127, 128	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ↔ ((ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)))
130	16, 129	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ((ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn ∧ (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn))
131	130	simpld 494	. . . . . . 7 ⊢ (𝜑 → (ℜ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)
132	126, 131	eqeltrrd 2845	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵)))) ∈ MblFn)
133	12, 28, 111, 115, 132	itgsubnc 37642	. . . . 5 ⊢ (𝜑 → ∫𝐴(((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
134	124	itgeq2dv 25837	. . . . 5 ⊢ (𝜑 → ∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 = ∫𝐴(((ℜ‘𝐶) · (ℜ‘𝐵)) − ((ℑ‘𝐶) · (ℑ‘𝐵))) d𝑥)
135	111, 115	itgneg 25859	. . . . . . . 8 ⊢ (𝜑 → -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴-((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
136	59, 32	mulneg1d 11743	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(ℑ‘𝐶) · (ℑ‘𝐵)) = -((ℑ‘𝐶) · (ℑ‘𝐵)))
137	136	itgeq2dv 25837	. . . . . . . 8 ⊢ (𝜑 → ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴-((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
138	135, 137	eqtr4d 2783	. . . . . . 7 ⊢ (𝜑 → -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 = ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥)
139	138	oveq2d 7464	. . . . . 6 ⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
140	111, 115	itgcl 25839	. . . . . . 7 ⊢ (𝜑 → ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥 ∈ ℂ)
141	29, 140	negsubd 11653	. . . . . 6 ⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + -∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
142	139, 141	eqtr3d 2782	. . . . 5 ⊢ (𝜑 → (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 − ∫𝐴((ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
143	133, 134, 142	3eqtr4d 2790	. . . 4 ⊢ (𝜑 → ∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥))
144	116, 9	immuld 15268	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘(𝐶 · 𝐵)) = (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))))
145	144	itgeq2dv 25837	. . . . . . 7 ⊢ (𝜑 → ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥 = ∫𝐴(((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))) d𝑥)
146		imf 15162	. . . . . . . . . . . . 13 ⊢ ℑ:ℂ⟶ℝ
147	146	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℑ:ℂ⟶ℝ)
148	147	feqmptd 6990	. . . . . . . . . . 11 ⊢ (𝜑 → ℑ = (𝑘 ∈ ℂ ↦ (ℑ‘𝑘)))
149		fveq2 6920	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐶 · 𝐵) → (ℑ‘𝑘) = (ℑ‘(𝐶 · 𝐵)))
150	117, 118, 148, 149	fmptco 7163	. . . . . . . . . 10 ⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐶 · 𝐵))))
151	144	mpteq2dva 5266	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))))
152	150, 151	eqtrd 2780	. . . . . . . . 9 ⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) = (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))))
153	130	simprd 495	. . . . . . . . 9 ⊢ (𝜑 → (ℑ ∘ (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵))) ∈ MblFn)
154	152, 153	eqeltrrd 2845	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵)))) ∈ MblFn)
155	33, 42, 60, 66, 154	itgaddnc 37640	. . . . . . 7 ⊢ (𝜑 → ∫𝐴(((ℜ‘𝐶) · (ℑ‘𝐵)) + ((ℑ‘𝐶) · (ℜ‘𝐵))) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
156	145, 155	eqtrd 2780	. . . . . 6 ⊢ (𝜑 → ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥 = (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))
157	156	oveq2d 7464	. . . . 5 ⊢ (𝜑 → (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥) = (i · (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
158	71, 43, 67	adddid 11314	. . . . 5 ⊢ (𝜑 → (i · (∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥 + ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)) = ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
159	157, 158	eqtrd 2780	. . . 4 ⊢ (𝜑 → (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥) = ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥)))
160	143, 159	oveq12d 7466	. . 3 ⊢ (𝜑 → (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)) = ((∫𝐴((ℜ‘𝐶) · (ℜ‘𝐵)) d𝑥 + ∫𝐴(-(ℑ‘𝐶) · (ℑ‘𝐵)) d𝑥) + ((i · ∫𝐴((ℜ‘𝐶) · (ℑ‘𝐵)) d𝑥) + (i · ∫𝐴((ℑ‘𝐶) · (ℜ‘𝐵)) d𝑥))))
161	70, 110, 160	3eqtr4d 2790	. 2 ⊢ (𝜑 → (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥) = (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)))
162	1	replimd 15246	. . 3 ⊢ (𝜑 → 𝐶 = ((ℜ‘𝐶) + (i · (ℑ‘𝐶))))
163	162	oveq1d 7463	. 2 ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = (((ℜ‘𝐶) + (i · (ℑ‘𝐶))) · ∫𝐴𝐵 d𝑥))
164	1, 8, 5, 16	iblmulc2nc 37645	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1)
165	117, 164	itgcnval 25855	. 2 ⊢ (𝜑 → ∫𝐴(𝐶 · 𝐵) d𝑥 = (∫𝐴(ℜ‘(𝐶 · 𝐵)) d𝑥 + (i · ∫𝐴(ℑ‘(𝐶 · 𝐵)) d𝑥)))
166	161, 163, 165	3eqtr4d 2790	1 ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  Vcvv 3488  {csn 4648   ↦ cmpt 5249   × cxp 5698  dom cdm 5700   ∘ ccom 5704  ⟶wf 6569  ‘cfv 6573  (class class class)co 7448   ∘_f cof 7712  ℂcc 11182  ℝcr 11183  1c1 11185  ici 11186   + caddc 11187   · cmul 11189   − cmin 11520  -cneg 11521  ℜcre 15146  ℑcim 15147  volcvol 25517  MblFncmbf 25668  𝐿¹cibl 25671  ∫citg 25672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-inf2 9710  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262  ax-addf 11263

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-disj 5134  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-ofr 7715  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-er 8763  df-map 8886  df-pm 8887  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fi 9480  df-sup 9511  df-inf 9512  df-oi 9579  df-dju 9970  df-card 10008  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-n0 12554  df-z 12640  df-uz 12904  df-q 13014  df-rp 13058  df-xneg 13175  df-xadd 13176  df-xmul 13177  df-ioo 13411  df-ico 13413  df-icc 13414  df-fz 13568  df-fzo 13712  df-fl 13843  df-mod 13921  df-seq 14053  df-exp 14113  df-hash 14380  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-clim 15534  df-sum 15735  df-rest 17482  df-topgen 17503  df-psmet 21379  df-xmet 21380  df-met 21381  df-bl 21382  df-mopn 21383  df-top 22921  df-topon 22938  df-bases 22974  df-cmp 23416  df-ovol 25518  df-vol 25519  df-mbf 25673  df-itg1 25674  df-itg2 25675  df-ibl 25676  df-itg 25677  df-0p 25724

This theorem is referenced by:  itgabsnc  37649