Metamath Proof Explorer

Theorem iblabsnc

Description: Choice-free analogue of iblabs . As with ibladdnc , a measurability hypothesis is needed. (Contributed by Brendan Leahy, 7-Nov-2017)

Ref Expression
Hypotheses iblabsnc.1 ⊢ φ ∧ x ∈ A → B ∈ V
iblabsnc.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
iblabsnc.m ⊢ φ → x ∈ A ⟼ B ∈ MblFn
Assertion iblabsnc ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1

Proof

Step Hyp Ref Expression
1 iblabsnc.1 ⊢ φ ∧ x ∈ A → B ∈ V
2 iblabsnc.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
3 iblabsnc.m ⊢ φ → x ∈ A ⟼ B ∈ MblFn
4 iblmbf ⊢ x ∈ A ⟼ B ∈ 𝐿 1 → x ∈ A ⟼ B ∈ MblFn
5 2 4 syl ⊢ φ → x ∈ A ⟼ B ∈ MblFn
6 5 1 mbfmptcl ⊢ φ ∧ x ∈ A → B ∈ ℂ
7 6 abscld ⊢ φ ∧ x ∈ A → B ∈ ℝ
8 7 rexrd ⊢ φ ∧ x ∈ A → B ∈ ℝ *
9 6 absge0d ⊢ φ ∧ x ∈ A → 0 ≤ B
10 elxrge0 ⊢ B ∈ 0 +∞ ↔ B ∈ ℝ * ∧ 0 ≤ B
11 8 9 10 sylanbrc ⊢ φ ∧ x ∈ A → B ∈ 0 +∞
12 0e0iccpnf ⊢ 0 ∈ 0 +∞
13 12 a1i ⊢ φ ∧ ¬ x ∈ A → 0 ∈ 0 +∞
14 11 13 ifclda ⊢ φ → if x ∈ A B 0 ∈ 0 +∞
15 14 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A B 0 ∈ 0 +∞
16 15 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A B 0 : ℝ ⟶ 0 +∞
17 reex ⊢ ℝ ∈ V
18 17 a1i ⊢ φ → ℝ ∈ V
19 6 recld ⊢ φ ∧ x ∈ A → ℜ ⁡ B ∈ ℝ
20 19 recnd ⊢ φ ∧ x ∈ A → ℜ ⁡ B ∈ ℂ
21 20 abscld ⊢ φ ∧ x ∈ A → ℜ ⁡ B ∈ ℝ
22 20 absge0d ⊢ φ ∧ x ∈ A → 0 ≤ ℜ ⁡ B
23 elrege0 ⊢ ℜ ⁡ B ∈ 0 +∞ ↔ ℜ ⁡ B ∈ ℝ ∧ 0 ≤ ℜ ⁡ B
24 21 22 23 sylanbrc ⊢ φ ∧ x ∈ A → ℜ ⁡ B ∈ 0 +∞
25 0e0icopnf ⊢ 0 ∈ 0 +∞
26 25 a1i ⊢ φ ∧ ¬ x ∈ A → 0 ∈ 0 +∞
27 24 26 ifclda ⊢ φ → if x ∈ A ℜ ⁡ B 0 ∈ 0 +∞
28 27 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A ℜ ⁡ B 0 ∈ 0 +∞
29 6 imcld ⊢ φ ∧ x ∈ A → ℑ ⁡ B ∈ ℝ
30 29 recnd ⊢ φ ∧ x ∈ A → ℑ ⁡ B ∈ ℂ
31 30 abscld ⊢ φ ∧ x ∈ A → ℑ ⁡ B ∈ ℝ
32 30 absge0d ⊢ φ ∧ x ∈ A → 0 ≤ ℑ ⁡ B
33 elrege0 ⊢ ℑ ⁡ B ∈ 0 +∞ ↔ ℑ ⁡ B ∈ ℝ ∧ 0 ≤ ℑ ⁡ B
34 31 32 33 sylanbrc ⊢ φ ∧ x ∈ A → ℑ ⁡ B ∈ 0 +∞
35 34 26 ifclda ⊢ φ → if x ∈ A ℑ ⁡ B 0 ∈ 0 +∞
36 35 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A ℑ ⁡ B 0 ∈ 0 +∞
37 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0
38 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0
39 18 28 36 37 38 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
40 iftrue ⊢ x ∈ A → if x ∈ A ℜ ⁡ B 0 = ℜ ⁡ B
41 iftrue ⊢ x ∈ A → if x ∈ A ℑ ⁡ B 0 = ℑ ⁡ B
42 40 41 oveq12d ⊢ x ∈ A → if x ∈ A ℜ ⁡ B 0 + if x ∈ A ℑ ⁡ B 0 = ℜ ⁡ B + ℑ ⁡ B
43 iftrue ⊢ x ∈ A → if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = ℜ ⁡ B + ℑ ⁡ B
44 42 43 eqtr4d ⊢ x ∈ A → if x ∈ A ℜ ⁡ B 0 + if x ∈ A ℑ ⁡ B 0 = if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
45 00id ⊢ 0 + 0 = 0
46 iffalse ⊢ ¬ x ∈ A → if x ∈ A ℜ ⁡ B 0 = 0
47 iffalse ⊢ ¬ x ∈ A → if x ∈ A ℑ ⁡ B 0 = 0
48 46 47 oveq12d ⊢ ¬ x ∈ A → if x ∈ A ℜ ⁡ B 0 + if x ∈ A ℑ ⁡ B 0 = 0 + 0
49 iffalse ⊢ ¬ x ∈ A → if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = 0
50 45 48 49 3eqtr4a ⊢ ¬ x ∈ A → if x ∈ A ℜ ⁡ B 0 + if x ∈ A ℑ ⁡ B 0 = if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
51 44 50 pm2.61i ⊢ if x ∈ A ℜ ⁡ B 0 + if x ∈ A ℑ ⁡ B 0 = if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
52 51 mpteq2i ⊢ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + if x ∈ A ℑ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
53 39 52 eqtr2di ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + f x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0
54 53 fveq2d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + f x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0
55 eqid ⊢ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0
56 6 iblcn ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1 ∧ x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1
57 2 56 mpbid ⊢ φ → x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1 ∧ x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1
58 57 simpld ⊢ φ → x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1
59 1 2 55 58 19 iblabsnclem ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 ∈ ℝ
60 59 simpld ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 ∈ MblFn
61 28 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 : ℝ ⟶ 0 +∞
62 59 simprd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 ∈ ℝ
63 36 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 : ℝ ⟶ 0 +∞
64 eqid ⊢ x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0
65 57 simprd ⊢ φ → x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1
66 1 2 64 65 29 iblabsnclem ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 ∈ ℝ
67 66 simprd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 ∈ ℝ
68 60 61 62 63 67 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
69 54 68 eqtrd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0
70 62 67 readdcld ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 ∈ ℝ
71 69 70 eqeltrd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 ∈ ℝ
72 21 31 readdcld ⊢ φ ∧ x ∈ A → ℜ ⁡ B + ℑ ⁡ B ∈ ℝ
73 72 rexrd ⊢ φ ∧ x ∈ A → ℜ ⁡ B + ℑ ⁡ B ∈ ℝ *
74 21 31 22 32 addge0d ⊢ φ ∧ x ∈ A → 0 ≤ ℜ ⁡ B + ℑ ⁡ B
75 elxrge0 ⊢ ℜ ⁡ B + ℑ ⁡ B ∈ 0 +∞ ↔ ℜ ⁡ B + ℑ ⁡ B ∈ ℝ * ∧ 0 ≤ ℜ ⁡ B + ℑ ⁡ B
76 73 74 75 sylanbrc ⊢ φ ∧ x ∈ A → ℜ ⁡ B + ℑ ⁡ B ∈ 0 +∞
77 76 13 ifclda ⊢ φ → if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 ∈ 0 +∞
78 77 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 ∈ 0 +∞
79 78 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 : ℝ ⟶ 0 +∞
80 ax-icn ⊢ i ∈ ℂ
81 mulcl ⊢ i ∈ ℂ ∧ ℑ ⁡ B ∈ ℂ → i ⁢ ℑ ⁡ B ∈ ℂ
82 80 30 81 sylancr ⊢ φ ∧ x ∈ A → i ⁢ ℑ ⁡ B ∈ ℂ
83 20 82 abstrid ⊢ φ ∧ x ∈ A → ℜ ⁡ B + i ⁢ ℑ ⁡ B ≤ ℜ ⁡ B + i ⁢ ℑ ⁡ B
84 iftrue ⊢ x ∈ A → if x ∈ A B 0 = B
85 84 adantl ⊢ φ ∧ x ∈ A → if x ∈ A B 0 = B
86 6 replimd ⊢ φ ∧ x ∈ A → B = ℜ ⁡ B + i ⁢ ℑ ⁡ B
87 86 fveq2d ⊢ φ ∧ x ∈ A → B = ℜ ⁡ B + i ⁢ ℑ ⁡ B
88 85 87 eqtrd ⊢ φ ∧ x ∈ A → if x ∈ A B 0 = ℜ ⁡ B + i ⁢ ℑ ⁡ B
89 43 adantl ⊢ φ ∧ x ∈ A → if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = ℜ ⁡ B + ℑ ⁡ B
90 absmul ⊢ i ∈ ℂ ∧ ℑ ⁡ B ∈ ℂ → i ⁢ ℑ ⁡ B = i ⁢ ℑ ⁡ B
91 80 30 90 sylancr ⊢ φ ∧ x ∈ A → i ⁢ ℑ ⁡ B = i ⁢ ℑ ⁡ B
92 absi ⊢ i = 1
93 92 oveq1i ⊢ i ⁢ ℑ ⁡ B = 1 ⁢ ℑ ⁡ B
94 31 recnd ⊢ φ ∧ x ∈ A → ℑ ⁡ B ∈ ℂ
95 94 mulid2d ⊢ φ ∧ x ∈ A → 1 ⁢ ℑ ⁡ B = ℑ ⁡ B
96 93 95 syl5eq ⊢ φ ∧ x ∈ A → i ⁢ ℑ ⁡ B = ℑ ⁡ B
97 91 96 eqtr2d ⊢ φ ∧ x ∈ A → ℑ ⁡ B = i ⁢ ℑ ⁡ B
98 97 oveq2d ⊢ φ ∧ x ∈ A → ℜ ⁡ B + ℑ ⁡ B = ℜ ⁡ B + i ⁢ ℑ ⁡ B
99 89 98 eqtrd ⊢ φ ∧ x ∈ A → if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = ℜ ⁡ B + i ⁢ ℑ ⁡ B
100 83 88 99 3brtr4d ⊢ φ ∧ x ∈ A → if x ∈ A B 0 ≤ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
101 100 ex ⊢ φ → x ∈ A → if x ∈ A B 0 ≤ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
102 0le0 ⊢ 0 ≤ 0
103 102 a1i ⊢ ¬ x ∈ A → 0 ≤ 0
104 iffalse ⊢ ¬ x ∈ A → if x ∈ A B 0 = 0
105 103 104 49 3brtr4d ⊢ ¬ x ∈ A → if x ∈ A B 0 ≤ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
106 101 105 pm2.61d1 ⊢ φ → if x ∈ A B 0 ≤ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
107 106 ralrimivw ⊢ φ → ∀ x ∈ ℝ if x ∈ A B 0 ≤ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
108 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A B 0 = x ∈ ℝ ⟼ if x ∈ A B 0
109 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
110 18 15 78 108 109 ofrfval2 ⊢ φ → x ∈ ℝ ⟼ if x ∈ A B 0 ≤ f x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 ↔ ∀ x ∈ ℝ if x ∈ A B 0 ≤ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
111 107 110 mpbird ⊢ φ → x ∈ ℝ ⟼ if x ∈ A B 0 ≤ f x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
112 itg2le ⊢ x ∈ ℝ ⟼ if x ∈ A B 0 : ℝ ⟶ 0 +∞ ∧ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 : ℝ ⟶ 0 +∞ ∧ x ∈ ℝ ⟼ if x ∈ A B 0 ≤ f x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
113 16 79 111 112 syl3anc ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
114 itg2lecl ⊢ x ∈ ℝ ⟼ if x ∈ A B 0 : ℝ ⟶ 0 +∞ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
115 16 71 113 114 syl3anc ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
116 7 9 iblpos ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
117 3 115 116 mpbir2and ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1