Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Brendan Leahy
iblmulc2nc
Next ⟩
itgmulc2nclem1
Metamath Proof Explorer
Ascii
Unicode
Theorem
iblmulc2nc
Description:
Choice-free analogue of
iblmulc2
.
(Contributed by
Brendan Leahy
, 17-Nov-2017)
Ref
Expression
Hypotheses
itgmulc2nc.1
⊢
φ
→
C
∈
ℂ
itgmulc2nc.2
⊢
φ
∧
x
∈
A
→
B
∈
V
itgmulc2nc.3
⊢
φ
→
x
∈
A
⟼
B
∈
𝐿
1
itgmulc2nc.m
⊢
φ
→
x
∈
A
⟼
C
B
∈
MblFn
Assertion
iblmulc2nc
⊢
φ
→
x
∈
A
⟼
C
B
∈
𝐿
1
Proof
Step
Hyp
Ref
Expression
1
itgmulc2nc.1
⊢
φ
→
C
∈
ℂ
2
itgmulc2nc.2
⊢
φ
∧
x
∈
A
→
B
∈
V
3
itgmulc2nc.3
⊢
φ
→
x
∈
A
⟼
B
∈
𝐿
1
4
itgmulc2nc.m
⊢
φ
→
x
∈
A
⟼
C
B
∈
MblFn
5
ifan
⊢
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
=
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
6
1
adantr
⊢
φ
∧
x
∈
A
→
C
∈
ℂ
7
iblmbf
⊢
x
∈
A
⟼
B
∈
𝐿
1
→
x
∈
A
⟼
B
∈
MblFn
8
3
7
syl
⊢
φ
→
x
∈
A
⟼
B
∈
MblFn
9
8
2
mbfmptcl
⊢
φ
∧
x
∈
A
→
B
∈
ℂ
10
6
9
mulcld
⊢
φ
∧
x
∈
A
→
C
B
∈
ℂ
11
10
adantlr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
∈
ℂ
12
elfzelz
⊢
k
∈
0
…
3
→
k
∈
ℤ
13
12
ad2antlr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
k
∈
ℤ
14
ax-icn
⊢
i
∈
ℂ
15
ine0
⊢
i
≠
0
16
expclz
⊢
i
∈
ℂ
∧
i
≠
0
∧
k
∈
ℤ
→
i
k
∈
ℂ
17
14
15
16
mp3an12
⊢
k
∈
ℤ
→
i
k
∈
ℂ
18
13
17
syl
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
i
k
∈
ℂ
19
expne0i
⊢
i
∈
ℂ
∧
i
≠
0
∧
k
∈
ℤ
→
i
k
≠
0
20
14
15
19
mp3an12
⊢
k
∈
ℤ
→
i
k
≠
0
21
13
20
syl
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
i
k
≠
0
22
11
18
21
divcld
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
i
k
∈
ℂ
23
22
recld
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
ℜ
C
B
i
k
∈
ℝ
24
0re
⊢
0
∈
ℝ
25
ifcl
⊢
ℜ
C
B
i
k
∈
ℝ
∧
0
∈
ℝ
→
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
26
23
24
25
sylancl
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
27
26
rexrd
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
*
28
max1
⊢
0
∈
ℝ
∧
ℜ
C
B
i
k
∈
ℝ
→
0
≤
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
29
24
23
28
sylancr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
0
≤
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
30
elxrge0
⊢
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
0
+∞
↔
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
*
∧
0
≤
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
31
27
29
30
sylanbrc
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
0
+∞
32
0e0iccpnf
⊢
0
∈
0
+∞
33
32
a1i
⊢
φ
∧
k
∈
0
…
3
∧
¬
x
∈
A
→
0
∈
0
+∞
34
31
33
ifclda
⊢
φ
∧
k
∈
0
…
3
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
∈
0
+∞
35
34
adantr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
ℝ
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
∈
0
+∞
36
5
35
eqeltrid
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
ℝ
→
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
0
+∞
37
36
fmpttd
⊢
φ
∧
k
∈
0
…
3
→
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
:
ℝ
⟶
0
+∞
38
9
recld
⊢
φ
∧
x
∈
A
→
ℜ
B
∈
ℝ
39
38
recnd
⊢
φ
∧
x
∈
A
→
ℜ
B
∈
ℂ
40
39
abscld
⊢
φ
∧
x
∈
A
→
ℜ
B
∈
ℝ
41
9
imcld
⊢
φ
∧
x
∈
A
→
ℑ
B
∈
ℝ
42
41
recnd
⊢
φ
∧
x
∈
A
→
ℑ
B
∈
ℂ
43
42
abscld
⊢
φ
∧
x
∈
A
→
ℑ
B
∈
ℝ
44
40
43
readdcld
⊢
φ
∧
x
∈
A
→
ℜ
B
+
ℑ
B
∈
ℝ
45
39
absge0d
⊢
φ
∧
x
∈
A
→
0
≤
ℜ
B
46
42
absge0d
⊢
φ
∧
x
∈
A
→
0
≤
ℑ
B
47
40
43
45
46
addge0d
⊢
φ
∧
x
∈
A
→
0
≤
ℜ
B
+
ℑ
B
48
elrege0
⊢
ℜ
B
+
ℑ
B
∈
0
+∞
↔
ℜ
B
+
ℑ
B
∈
ℝ
∧
0
≤
ℜ
B
+
ℑ
B
49
44
47
48
sylanbrc
⊢
φ
∧
x
∈
A
→
ℜ
B
+
ℑ
B
∈
0
+∞
50
0e0icopnf
⊢
0
∈
0
+∞
51
50
a1i
⊢
φ
∧
¬
x
∈
A
→
0
∈
0
+∞
52
49
51
ifclda
⊢
φ
→
if
x
∈
A
ℜ
B
+
ℑ
B
0
∈
0
+∞
53
52
adantr
⊢
φ
∧
x
∈
ℝ
→
if
x
∈
A
ℜ
B
+
ℑ
B
0
∈
0
+∞
54
53
fmpttd
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
+
ℑ
B
0
:
ℝ
⟶
0
+∞
55
reex
⊢
ℝ
∈
V
56
55
a1i
⊢
φ
→
ℝ
∈
V
57
elrege0
⊢
ℜ
B
∈
0
+∞
↔
ℜ
B
∈
ℝ
∧
0
≤
ℜ
B
58
40
45
57
sylanbrc
⊢
φ
∧
x
∈
A
→
ℜ
B
∈
0
+∞
59
58
51
ifclda
⊢
φ
→
if
x
∈
A
ℜ
B
0
∈
0
+∞
60
59
adantr
⊢
φ
∧
x
∈
ℝ
→
if
x
∈
A
ℜ
B
0
∈
0
+∞
61
elrege0
⊢
ℑ
B
∈
0
+∞
↔
ℑ
B
∈
ℝ
∧
0
≤
ℑ
B
62
43
46
61
sylanbrc
⊢
φ
∧
x
∈
A
→
ℑ
B
∈
0
+∞
63
62
51
ifclda
⊢
φ
→
if
x
∈
A
ℑ
B
0
∈
0
+∞
64
63
adantr
⊢
φ
∧
x
∈
ℝ
→
if
x
∈
A
ℑ
B
0
∈
0
+∞
65
eqidd
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
=
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
66
eqidd
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
=
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
67
56
60
64
65
66
offval2
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
+
f
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
=
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
+
if
x
∈
A
ℑ
B
0
68
iftrue
⊢
x
∈
A
→
if
x
∈
A
ℜ
B
0
=
ℜ
B
69
iftrue
⊢
x
∈
A
→
if
x
∈
A
ℑ
B
0
=
ℑ
B
70
68
69
oveq12d
⊢
x
∈
A
→
if
x
∈
A
ℜ
B
0
+
if
x
∈
A
ℑ
B
0
=
ℜ
B
+
ℑ
B
71
iftrue
⊢
x
∈
A
→
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
ℜ
B
+
ℑ
B
72
70
71
eqtr4d
⊢
x
∈
A
→
if
x
∈
A
ℜ
B
0
+
if
x
∈
A
ℑ
B
0
=
if
x
∈
A
ℜ
B
+
ℑ
B
0
73
00id
⊢
0
+
0
=
0
74
iffalse
⊢
¬
x
∈
A
→
if
x
∈
A
ℜ
B
0
=
0
75
iffalse
⊢
¬
x
∈
A
→
if
x
∈
A
ℑ
B
0
=
0
76
74
75
oveq12d
⊢
¬
x
∈
A
→
if
x
∈
A
ℜ
B
0
+
if
x
∈
A
ℑ
B
0
=
0
+
0
77
iffalse
⊢
¬
x
∈
A
→
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
0
78
73
76
77
3eqtr4a
⊢
¬
x
∈
A
→
if
x
∈
A
ℜ
B
0
+
if
x
∈
A
ℑ
B
0
=
if
x
∈
A
ℜ
B
+
ℑ
B
0
79
72
78
pm2.61i
⊢
if
x
∈
A
ℜ
B
0
+
if
x
∈
A
ℑ
B
0
=
if
x
∈
A
ℜ
B
+
ℑ
B
0
80
79
mpteq2i
⊢
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
+
if
x
∈
A
ℑ
B
0
=
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
+
ℑ
B
0
81
67
80
eqtr2di
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
+
f
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
82
81
fveq2d
⊢
φ
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
+
f
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
83
eqid
⊢
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
=
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
84
9
iblcn
⊢
φ
→
x
∈
A
⟼
B
∈
𝐿
1
↔
x
∈
A
⟼
ℜ
B
∈
𝐿
1
∧
x
∈
A
⟼
ℑ
B
∈
𝐿
1
85
3
84
mpbid
⊢
φ
→
x
∈
A
⟼
ℜ
B
∈
𝐿
1
∧
x
∈
A
⟼
ℑ
B
∈
𝐿
1
86
85
simpld
⊢
φ
→
x
∈
A
⟼
ℜ
B
∈
𝐿
1
87
2
3
83
86
38
iblabsnclem
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
∈
MblFn
∧
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
∈
ℝ
88
87
simpld
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
∈
MblFn
89
60
fmpttd
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
:
ℝ
⟶
0
+∞
90
87
simprd
⊢
φ
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
∈
ℝ
91
64
fmpttd
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
:
ℝ
⟶
0
+∞
92
eqid
⊢
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
=
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
93
85
simprd
⊢
φ
→
x
∈
A
⟼
ℑ
B
∈
𝐿
1
94
2
3
92
93
41
iblabsnclem
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
∈
MblFn
∧
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
∈
ℝ
95
94
simprd
⊢
φ
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
∈
ℝ
96
88
89
90
91
95
itg2addnc
⊢
φ
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
+
f
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
=
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
+
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
97
82
96
eqtrd
⊢
φ
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
+
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
98
90
95
readdcld
⊢
φ
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
+
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
∈
ℝ
99
97
98
eqeltrd
⊢
φ
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
+
ℑ
B
0
∈
ℝ
100
1
abscld
⊢
φ
→
C
∈
ℝ
101
1
absge0d
⊢
φ
→
0
≤
C
102
elrege0
⊢
C
∈
0
+∞
↔
C
∈
ℝ
∧
0
≤
C
103
100
101
102
sylanbrc
⊢
φ
→
C
∈
0
+∞
104
54
99
103
itg2mulc
⊢
φ
→
∫
2
ℝ
×
C
×
f
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
C
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
+
ℑ
B
0
105
100
adantr
⊢
φ
∧
x
∈
ℝ
→
C
∈
ℝ
106
fconstmpt
⊢
ℝ
×
C
=
x
∈
ℝ
⟼
C
107
106
a1i
⊢
φ
→
ℝ
×
C
=
x
∈
ℝ
⟼
C
108
eqidd
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
+
ℑ
B
0
109
56
105
53
107
108
offval2
⊢
φ
→
ℝ
×
C
×
f
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
x
∈
ℝ
⟼
C
if
x
∈
A
ℜ
B
+
ℑ
B
0
110
71
oveq2d
⊢
x
∈
A
→
C
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
C
ℜ
B
+
ℑ
B
111
iftrue
⊢
x
∈
A
→
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
=
C
ℜ
B
+
ℑ
B
112
110
111
eqtr4d
⊢
x
∈
A
→
C
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
113
112
adantl
⊢
φ
∧
x
∈
A
→
C
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
114
100
recnd
⊢
φ
→
C
∈
ℂ
115
114
mul01d
⊢
φ
→
C
⋅
0
=
0
116
115
adantr
⊢
φ
∧
¬
x
∈
A
→
C
⋅
0
=
0
117
77
adantl
⊢
φ
∧
¬
x
∈
A
→
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
0
118
117
oveq2d
⊢
φ
∧
¬
x
∈
A
→
C
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
C
⋅
0
119
iffalse
⊢
¬
x
∈
A
→
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
=
0
120
119
adantl
⊢
φ
∧
¬
x
∈
A
→
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
=
0
121
116
118
120
3eqtr4d
⊢
φ
∧
¬
x
∈
A
→
C
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
122
113
121
pm2.61dan
⊢
φ
→
C
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
123
122
mpteq2dv
⊢
φ
→
x
∈
ℝ
⟼
C
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
124
109
123
eqtrd
⊢
φ
→
ℝ
×
C
×
f
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
125
124
fveq2d
⊢
φ
→
∫
2
ℝ
×
C
×
f
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
126
97
oveq2d
⊢
φ
→
C
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
+
ℑ
B
0
=
C
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
+
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
127
104
125
126
3eqtr3d
⊢
φ
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
=
C
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
+
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
128
100
98
remulcld
⊢
φ
→
C
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℜ
B
0
+
∫
2
x
∈
ℝ
⟼
if
x
∈
A
ℑ
B
0
∈
ℝ
129
127
128
eqeltrd
⊢
φ
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
∈
ℝ
130
129
adantr
⊢
φ
∧
k
∈
0
…
3
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
∈
ℝ
131
100
adantr
⊢
φ
∧
x
∈
A
→
C
∈
ℝ
132
131
44
remulcld
⊢
φ
∧
x
∈
A
→
C
ℜ
B
+
ℑ
B
∈
ℝ
133
132
rexrd
⊢
φ
∧
x
∈
A
→
C
ℜ
B
+
ℑ
B
∈
ℝ
*
134
101
adantr
⊢
φ
∧
x
∈
A
→
0
≤
C
135
131
44
134
47
mulge0d
⊢
φ
∧
x
∈
A
→
0
≤
C
ℜ
B
+
ℑ
B
136
elxrge0
⊢
C
ℜ
B
+
ℑ
B
∈
0
+∞
↔
C
ℜ
B
+
ℑ
B
∈
ℝ
*
∧
0
≤
C
ℜ
B
+
ℑ
B
137
133
135
136
sylanbrc
⊢
φ
∧
x
∈
A
→
C
ℜ
B
+
ℑ
B
∈
0
+∞
138
32
a1i
⊢
φ
∧
¬
x
∈
A
→
0
∈
0
+∞
139
137
138
ifclda
⊢
φ
→
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
∈
0
+∞
140
139
ad2antrr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
ℝ
→
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
∈
0
+∞
141
140
fmpttd
⊢
φ
∧
k
∈
0
…
3
→
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
:
ℝ
⟶
0
+∞
142
9
abscld
⊢
φ
∧
x
∈
A
→
B
∈
ℝ
143
131
142
remulcld
⊢
φ
∧
x
∈
A
→
C
B
∈
ℝ
144
143
adantlr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
∈
ℝ
145
132
adantlr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
ℜ
B
+
ℑ
B
∈
ℝ
146
22
releabsd
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
ℜ
C
B
i
k
≤
C
B
i
k
147
11
18
21
absdivd
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
i
k
=
C
B
i
k
148
elfznn0
⊢
k
∈
0
…
3
→
k
∈
ℕ
0
149
absexp
⊢
i
∈
ℂ
∧
k
∈
ℕ
0
→
i
k
=
i
k
150
14
148
149
sylancr
⊢
k
∈
0
…
3
→
i
k
=
i
k
151
absi
⊢
i
=
1
152
151
oveq1i
⊢
i
k
=
1
k
153
1exp
⊢
k
∈
ℤ
→
1
k
=
1
154
12
153
syl
⊢
k
∈
0
…
3
→
1
k
=
1
155
152
154
eqtrid
⊢
k
∈
0
…
3
→
i
k
=
1
156
150
155
eqtrd
⊢
k
∈
0
…
3
→
i
k
=
1
157
156
oveq2d
⊢
k
∈
0
…
3
→
C
B
i
k
=
C
B
1
158
157
ad2antlr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
i
k
=
C
B
1
159
10
abscld
⊢
φ
∧
x
∈
A
→
C
B
∈
ℝ
160
159
recnd
⊢
φ
∧
x
∈
A
→
C
B
∈
ℂ
161
160
adantlr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
∈
ℂ
162
161
div1d
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
1
=
C
B
163
147
158
162
3eqtrd
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
i
k
=
C
B
164
6
9
absmuld
⊢
φ
∧
x
∈
A
→
C
B
=
C
B
165
164
adantlr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
=
C
B
166
163
165
eqtrd
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
i
k
=
C
B
167
146
166
breqtrd
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
ℜ
C
B
i
k
≤
C
B
168
mulcl
⊢
i
∈
ℂ
∧
ℑ
B
∈
ℂ
→
i
ℑ
B
∈
ℂ
169
14
42
168
sylancr
⊢
φ
∧
x
∈
A
→
i
ℑ
B
∈
ℂ
170
39
169
abstrid
⊢
φ
∧
x
∈
A
→
ℜ
B
+
i
ℑ
B
≤
ℜ
B
+
i
ℑ
B
171
9
replimd
⊢
φ
∧
x
∈
A
→
B
=
ℜ
B
+
i
ℑ
B
172
171
fveq2d
⊢
φ
∧
x
∈
A
→
B
=
ℜ
B
+
i
ℑ
B
173
absmul
⊢
i
∈
ℂ
∧
ℑ
B
∈
ℂ
→
i
ℑ
B
=
i
ℑ
B
174
14
42
173
sylancr
⊢
φ
∧
x
∈
A
→
i
ℑ
B
=
i
ℑ
B
175
151
oveq1i
⊢
i
ℑ
B
=
1
ℑ
B
176
174
175
eqtrdi
⊢
φ
∧
x
∈
A
→
i
ℑ
B
=
1
ℑ
B
177
43
recnd
⊢
φ
∧
x
∈
A
→
ℑ
B
∈
ℂ
178
177
mulid2d
⊢
φ
∧
x
∈
A
→
1
ℑ
B
=
ℑ
B
179
176
178
eqtr2d
⊢
φ
∧
x
∈
A
→
ℑ
B
=
i
ℑ
B
180
179
oveq2d
⊢
φ
∧
x
∈
A
→
ℜ
B
+
ℑ
B
=
ℜ
B
+
i
ℑ
B
181
170
172
180
3brtr4d
⊢
φ
∧
x
∈
A
→
B
≤
ℜ
B
+
ℑ
B
182
142
44
131
134
181
lemul2ad
⊢
φ
∧
x
∈
A
→
C
B
≤
C
ℜ
B
+
ℑ
B
183
182
adantlr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
C
B
≤
C
ℜ
B
+
ℑ
B
184
23
144
145
167
183
letrd
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
ℜ
C
B
i
k
≤
C
ℜ
B
+
ℑ
B
185
135
adantlr
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
0
≤
C
ℜ
B
+
ℑ
B
186
breq1
⊢
ℜ
C
B
i
k
=
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
→
ℜ
C
B
i
k
≤
C
ℜ
B
+
ℑ
B
↔
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
C
ℜ
B
+
ℑ
B
187
breq1
⊢
0
=
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
→
0
≤
C
ℜ
B
+
ℑ
B
↔
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
C
ℜ
B
+
ℑ
B
188
186
187
ifboth
⊢
ℜ
C
B
i
k
≤
C
ℜ
B
+
ℑ
B
∧
0
≤
C
ℜ
B
+
ℑ
B
→
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
C
ℜ
B
+
ℑ
B
189
184
185
188
syl2anc
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
C
ℜ
B
+
ℑ
B
190
iftrue
⊢
x
∈
A
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
=
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
191
190
adantl
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
=
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
192
111
adantl
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
=
C
ℜ
B
+
ℑ
B
193
189
191
192
3brtr4d
⊢
φ
∧
k
∈
0
…
3
∧
x
∈
A
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
≤
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
194
193
ex
⊢
φ
∧
k
∈
0
…
3
→
x
∈
A
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
≤
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
195
0le0
⊢
0
≤
0
196
195
a1i
⊢
¬
x
∈
A
→
0
≤
0
197
iffalse
⊢
¬
x
∈
A
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
=
0
198
196
197
119
3brtr4d
⊢
¬
x
∈
A
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
≤
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
199
194
198
pm2.61d1
⊢
φ
∧
k
∈
0
…
3
→
if
x
∈
A
if
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
0
≤
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
200
5
199
eqbrtrid
⊢
φ
∧
k
∈
0
…
3
→
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
201
200
ralrimivw
⊢
φ
∧
k
∈
0
…
3
→
∀
x
∈
ℝ
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
202
55
a1i
⊢
φ
∧
k
∈
0
…
3
→
ℝ
∈
V
203
eqidd
⊢
φ
∧
k
∈
0
…
3
→
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
=
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
204
eqidd
⊢
φ
∧
k
∈
0
…
3
→
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
=
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
205
202
36
140
203
204
ofrfval2
⊢
φ
∧
k
∈
0
…
3
→
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
f
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
↔
∀
x
∈
ℝ
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
206
201
205
mpbird
⊢
φ
∧
k
∈
0
…
3
→
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
f
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
207
itg2le
⊢
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
:
ℝ
⟶
0
+∞
∧
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
:
ℝ
⟶
0
+∞
∧
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
f
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
208
37
141
206
207
syl3anc
⊢
φ
∧
k
∈
0
…
3
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
209
itg2lecl
⊢
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
:
ℝ
⟶
0
+∞
∧
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
∈
ℝ
∧
∫
2
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
≤
∫
2
x
∈
ℝ
⟼
if
x
∈
A
C
ℜ
B
+
ℑ
B
0
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
210
37
130
208
209
syl3anc
⊢
φ
∧
k
∈
0
…
3
→
∫
2
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
211
210
ralrimiva
⊢
φ
→
∀
k
∈
0
…
3
∫
2
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
212
eqidd
⊢
φ
→
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
=
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
213
eqidd
⊢
φ
∧
x
∈
A
→
ℜ
C
B
i
k
=
ℜ
C
B
i
k
214
212
213
10
isibl2
⊢
φ
→
x
∈
A
⟼
C
B
∈
𝐿
1
↔
x
∈
A
⟼
C
B
∈
MblFn
∧
∀
k
∈
0
…
3
∫
2
x
∈
ℝ
⟼
if
x
∈
A
∧
0
≤
ℜ
C
B
i
k
ℜ
C
B
i
k
0
∈
ℝ
215
4
211
214
mpbir2and
⊢
φ
→
x
∈
A
⟼
C
B
∈
𝐿
1