Metamath Proof Explorer

Theorem iblneg

Description: The negative of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgcnval.1 ⊢φ∧x∈A→B∈V
itgcnval.2 ⊢φ→x∈A⟼B∈𝐿1
Assertion iblneg ⊢φ→x∈A⟼−B∈𝐿1

Proof

Step Hyp Ref Expression
1 itgcnval.1 ⊢φ∧x∈A→B∈V
2 itgcnval.2 ⊢φ→x∈A⟼B∈𝐿1
3 iblmbf ⊢x∈A⟼B∈𝐿1→x∈A⟼B∈MblFn
4 2 3 syl ⊢φ→x∈A⟼B∈MblFn
5 4 1 mbfmptcl ⊢φ∧x∈A→B∈ℂ
6 5 renegd ⊢φ∧x∈A→ℜ⁡−B=−ℜ⁡B
7 6 breq2d ⊢φ∧x∈A→0≤ℜ⁡−B↔0≤−ℜ⁡B
8 7 6 ifbieq1d ⊢φ∧x∈A→if0≤ℜ⁡−Bℜ⁡−B0=if0≤−ℜ⁡B−ℜ⁡B0
9 8 mpteq2dva ⊢φ→x∈A⟼if0≤ℜ⁡−Bℜ⁡−B0=x∈A⟼if0≤−ℜ⁡B−ℜ⁡B0
10 5 iblcn ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼ℜ⁡B∈𝐿1∧x∈A⟼ℑ⁡B∈𝐿1
11 2 10 mpbid ⊢φ→x∈A⟼ℜ⁡B∈𝐿1∧x∈A⟼ℑ⁡B∈𝐿1
12 11 simpld ⊢φ→x∈A⟼ℜ⁡B∈𝐿1
13 5 recld ⊢φ∧x∈A→ℜ⁡B∈ℝ
14 13 iblre ⊢φ→x∈A⟼ℜ⁡B∈𝐿1↔x∈A⟼if0≤ℜ⁡Bℜ⁡B0∈𝐿1∧x∈A⟼if0≤−ℜ⁡B−ℜ⁡B0∈𝐿1
15 12 14 mpbid ⊢φ→x∈A⟼if0≤ℜ⁡Bℜ⁡B0∈𝐿1∧x∈A⟼if0≤−ℜ⁡B−ℜ⁡B0∈𝐿1
16 15 simprd ⊢φ→x∈A⟼if0≤−ℜ⁡B−ℜ⁡B0∈𝐿1
17 9 16 eqeltrd ⊢φ→x∈A⟼if0≤ℜ⁡−Bℜ⁡−B0∈𝐿1
18 6 negeqd ⊢φ∧x∈A→−ℜ⁡−B=−−ℜ⁡B
19 13 recnd ⊢φ∧x∈A→ℜ⁡B∈ℂ
20 19 negnegd ⊢φ∧x∈A→−−ℜ⁡B=ℜ⁡B
21 18 20 eqtrd ⊢φ∧x∈A→−ℜ⁡−B=ℜ⁡B
22 21 breq2d ⊢φ∧x∈A→0≤−ℜ⁡−B↔0≤ℜ⁡B
23 22 21 ifbieq1d ⊢φ∧x∈A→if0≤−ℜ⁡−B−ℜ⁡−B0=if0≤ℜ⁡Bℜ⁡B0
24 23 mpteq2dva ⊢φ→x∈A⟼if0≤−ℜ⁡−B−ℜ⁡−B0=x∈A⟼if0≤ℜ⁡Bℜ⁡B0
25 15 simpld ⊢φ→x∈A⟼if0≤ℜ⁡Bℜ⁡B0∈𝐿1
26 24 25 eqeltrd ⊢φ→x∈A⟼if0≤−ℜ⁡−B−ℜ⁡−B0∈𝐿1
27 5 negcld ⊢φ∧x∈A→−B∈ℂ
28 27 recld ⊢φ∧x∈A→ℜ⁡−B∈ℝ
29 28 iblre ⊢φ→x∈A⟼ℜ⁡−B∈𝐿1↔x∈A⟼if0≤ℜ⁡−Bℜ⁡−B0∈𝐿1∧x∈A⟼if0≤−ℜ⁡−B−ℜ⁡−B0∈𝐿1
30 17 26 29 mpbir2and ⊢φ→x∈A⟼ℜ⁡−B∈𝐿1
31 5 imnegd ⊢φ∧x∈A→ℑ⁡−B=−ℑ⁡B
32 31 breq2d ⊢φ∧x∈A→0≤ℑ⁡−B↔0≤−ℑ⁡B
33 32 31 ifbieq1d ⊢φ∧x∈A→if0≤ℑ⁡−Bℑ⁡−B0=if0≤−ℑ⁡B−ℑ⁡B0
34 33 mpteq2dva ⊢φ→x∈A⟼if0≤ℑ⁡−Bℑ⁡−B0=x∈A⟼if0≤−ℑ⁡B−ℑ⁡B0
35 11 simprd ⊢φ→x∈A⟼ℑ⁡B∈𝐿1
36 5 imcld ⊢φ∧x∈A→ℑ⁡B∈ℝ
37 36 iblre ⊢φ→x∈A⟼ℑ⁡B∈𝐿1↔x∈A⟼if0≤ℑ⁡Bℑ⁡B0∈𝐿1∧x∈A⟼if0≤−ℑ⁡B−ℑ⁡B0∈𝐿1
38 35 37 mpbid ⊢φ→x∈A⟼if0≤ℑ⁡Bℑ⁡B0∈𝐿1∧x∈A⟼if0≤−ℑ⁡B−ℑ⁡B0∈𝐿1
39 38 simprd ⊢φ→x∈A⟼if0≤−ℑ⁡B−ℑ⁡B0∈𝐿1
40 34 39 eqeltrd ⊢φ→x∈A⟼if0≤ℑ⁡−Bℑ⁡−B0∈𝐿1
41 31 negeqd ⊢φ∧x∈A→−ℑ⁡−B=−−ℑ⁡B
42 36 recnd ⊢φ∧x∈A→ℑ⁡B∈ℂ
43 42 negnegd ⊢φ∧x∈A→−−ℑ⁡B=ℑ⁡B
44 41 43 eqtrd ⊢φ∧x∈A→−ℑ⁡−B=ℑ⁡B
45 44 breq2d ⊢φ∧x∈A→0≤−ℑ⁡−B↔0≤ℑ⁡B
46 45 44 ifbieq1d ⊢φ∧x∈A→if0≤−ℑ⁡−B−ℑ⁡−B0=if0≤ℑ⁡Bℑ⁡B0
47 46 mpteq2dva ⊢φ→x∈A⟼if0≤−ℑ⁡−B−ℑ⁡−B0=x∈A⟼if0≤ℑ⁡Bℑ⁡B0
48 38 simpld ⊢φ→x∈A⟼if0≤ℑ⁡Bℑ⁡B0∈𝐿1
49 47 48 eqeltrd ⊢φ→x∈A⟼if0≤−ℑ⁡−B−ℑ⁡−B0∈𝐿1
50 27 imcld ⊢φ∧x∈A→ℑ⁡−B∈ℝ
51 50 iblre ⊢φ→x∈A⟼ℑ⁡−B∈𝐿1↔x∈A⟼if0≤ℑ⁡−Bℑ⁡−B0∈𝐿1∧x∈A⟼if0≤−ℑ⁡−B−ℑ⁡−B0∈𝐿1
52 40 49 51 mpbir2and ⊢φ→x∈A⟼ℑ⁡−B∈𝐿1
53 27 iblcn ⊢φ→x∈A⟼−B∈𝐿1↔x∈A⟼ℜ⁡−B∈𝐿1∧x∈A⟼ℑ⁡−B∈𝐿1
54 30 52 53 mpbir2and ⊢φ→x∈A⟼−B∈𝐿1