Proof of Theorem iblneg
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | itgcnval.2 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) | 
| 2 |  | iblmbf 25803 | . . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) | 
| 3 | 1, 2 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) | 
| 4 |  | itgcnval.1 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) | 
| 5 | 3, 4 | mbfmptcl 25672 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) | 
| 6 | 5 | renegd 15249 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘-𝐵) = -(ℜ‘𝐵)) | 
| 7 | 6 | breq2d 5154 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ (ℜ‘-𝐵) ↔ 0 ≤
-(ℜ‘𝐵))) | 
| 8 | 7, 6 | ifbieq1d 4549 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘-𝐵), (ℜ‘-𝐵), 0) = if(0 ≤
-(ℜ‘𝐵),
-(ℜ‘𝐵),
0)) | 
| 9 | 8 | mpteq2dva 5241 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℜ‘-𝐵), (ℜ‘-𝐵), 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0))) | 
| 10 | 5 | iblcn 25835 | . . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1
∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1))) | 
| 11 | 1, 10 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1)) | 
| 12 | 11 | simpld 494 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈
𝐿1) | 
| 13 | 5 | recld 15234 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℝ) | 
| 14 | 13 | iblre 25830 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ if(0 ≤
(ℜ‘𝐵),
(ℜ‘𝐵), 0))
∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0)) ∈
𝐿1))) | 
| 15 | 12, 14 | mpbid 232 | . . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0)) ∈
𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0)) ∈
𝐿1)) | 
| 16 | 15 | simprd 495 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0)) ∈
𝐿1) | 
| 17 | 9, 16 | eqeltrd 2840 | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℜ‘-𝐵), (ℜ‘-𝐵), 0)) ∈
𝐿1) | 
| 18 | 6 | negeqd 11503 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℜ‘-𝐵) = --(ℜ‘𝐵)) | 
| 19 | 13 | recnd 11290 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℂ) | 
| 20 | 19 | negnegd 11612 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → --(ℜ‘𝐵) = (ℜ‘𝐵)) | 
| 21 | 18, 20 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℜ‘-𝐵) = (ℜ‘𝐵)) | 
| 22 | 21 | breq2d 5154 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ -(ℜ‘-𝐵) ↔ 0 ≤
(ℜ‘𝐵))) | 
| 23 | 22, 21 | ifbieq1d 4549 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(ℜ‘-𝐵), -(ℜ‘-𝐵), 0) = if(0 ≤
(ℜ‘𝐵),
(ℜ‘𝐵),
0)) | 
| 24 | 23 | mpteq2dva 5241 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘-𝐵), -(ℜ‘-𝐵), 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0))) | 
| 25 | 15 | simpld 494 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0)) ∈
𝐿1) | 
| 26 | 24, 25 | eqeltrd 2840 | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘-𝐵), -(ℜ‘-𝐵), 0)) ∈
𝐿1) | 
| 27 | 5 | negcld 11608 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℂ) | 
| 28 | 27 | recld 15234 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘-𝐵) ∈ ℝ) | 
| 29 | 28 | iblre 25830 | . . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘-𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ if(0 ≤
(ℜ‘-𝐵),
(ℜ‘-𝐵), 0))
∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘-𝐵), -(ℜ‘-𝐵), 0)) ∈
𝐿1))) | 
| 30 | 17, 26, 29 | mpbir2and 713 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘-𝐵)) ∈
𝐿1) | 
| 31 | 5 | imnegd 15250 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘-𝐵) = -(ℑ‘𝐵)) | 
| 32 | 31 | breq2d 5154 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ (ℑ‘-𝐵) ↔ 0 ≤
-(ℑ‘𝐵))) | 
| 33 | 32, 31 | ifbieq1d 4549 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℑ‘-𝐵), (ℑ‘-𝐵), 0) = if(0 ≤
-(ℑ‘𝐵),
-(ℑ‘𝐵),
0)) | 
| 34 | 33 | mpteq2dva 5241 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℑ‘-𝐵), (ℑ‘-𝐵), 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0))) | 
| 35 | 11 | simprd 495 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1) | 
| 36 | 5 | imcld 15235 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℝ) | 
| 37 | 36 | iblre 25830 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ if(0 ≤
(ℑ‘𝐵),
(ℑ‘𝐵), 0))
∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0)) ∈
𝐿1))) | 
| 38 | 35, 37 | mpbid 232 | . . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0)) ∈
𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0)) ∈
𝐿1)) | 
| 39 | 38 | simprd 495 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0)) ∈
𝐿1) | 
| 40 | 34, 39 | eqeltrd 2840 | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℑ‘-𝐵), (ℑ‘-𝐵), 0)) ∈
𝐿1) | 
| 41 | 31 | negeqd 11503 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘-𝐵) = --(ℑ‘𝐵)) | 
| 42 | 36 | recnd 11290 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℂ) | 
| 43 | 42 | negnegd 11612 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → --(ℑ‘𝐵) = (ℑ‘𝐵)) | 
| 44 | 41, 43 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘-𝐵) = (ℑ‘𝐵)) | 
| 45 | 44 | breq2d 5154 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ -(ℑ‘-𝐵) ↔ 0 ≤
(ℑ‘𝐵))) | 
| 46 | 45, 44 | ifbieq1d 4549 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(ℑ‘-𝐵), -(ℑ‘-𝐵), 0) = if(0 ≤
(ℑ‘𝐵),
(ℑ‘𝐵),
0)) | 
| 47 | 46 | mpteq2dva 5241 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘-𝐵), -(ℑ‘-𝐵), 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0))) | 
| 48 | 38 | simpld 494 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0)) ∈
𝐿1) | 
| 49 | 47, 48 | eqeltrd 2840 | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘-𝐵), -(ℑ‘-𝐵), 0)) ∈
𝐿1) | 
| 50 | 27 | imcld 15235 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘-𝐵) ∈ ℝ) | 
| 51 | 50 | iblre 25830 | . . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℑ‘-𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ if(0 ≤
(ℑ‘-𝐵),
(ℑ‘-𝐵), 0))
∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘-𝐵), -(ℑ‘-𝐵), 0)) ∈
𝐿1))) | 
| 52 | 40, 49, 51 | mpbir2and 713 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘-𝐵)) ∈
𝐿1) | 
| 53 | 27 | iblcn 25835 | . 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ -𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (ℜ‘-𝐵)) ∈ 𝐿1
∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘-𝐵)) ∈
𝐿1))) | 
| 54 | 30, 52, 53 | mpbir2and 713 | 1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈
𝐿1) |