Proof of Theorem itgneg
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | itgcnval.2 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) | 
| 2 |  | iblmbf 25802 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) | 
| 3 | 1, 2 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) | 
| 4 |  | itgcnval.1 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) | 
| 5 | 3, 4 | mbfmptcl 25671 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) | 
| 6 | 5 | recld 15233 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℝ) | 
| 7 | 5 | iblcn 25834 | . . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1
∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1))) | 
| 8 | 1, 7 | mpbid 232 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1)) | 
| 9 | 8 | simpld 494 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈
𝐿1) | 
| 10 | 6, 9 | itgcl 25819 | . . . 4
⊢ (𝜑 → ∫𝐴(ℜ‘𝐵) d𝑥 ∈ ℂ) | 
| 11 |  | ax-icn 11214 | . . . . 5
⊢ i ∈
ℂ | 
| 12 | 5 | imcld 15234 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℝ) | 
| 13 | 8 | simprd 495 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1) | 
| 14 | 12, 13 | itgcl 25819 | . . . . 5
⊢ (𝜑 → ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ) | 
| 15 |  | mulcl 11239 | . . . . 5
⊢ ((i
∈ ℂ ∧ ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ) → (i ·
∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ) | 
| 16 | 11, 14, 15 | sylancr 587 | . . . 4
⊢ (𝜑 → (i · ∫𝐴(ℑ‘𝐵) d𝑥) ∈ ℂ) | 
| 17 | 10, 16 | negdid 11633 | . . 3
⊢ (𝜑 → -(∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = (-∫𝐴(ℜ‘𝐵) d𝑥 + -(i · ∫𝐴(ℑ‘𝐵) d𝑥))) | 
| 18 |  | 0re 11263 | . . . . . . . 8
⊢ 0 ∈
ℝ | 
| 19 |  | ifcl 4571 | . . . . . . . 8
⊢
(((ℜ‘𝐵)
∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0) ∈
ℝ) | 
| 20 | 6, 18, 19 | sylancl 586 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0) ∈
ℝ) | 
| 21 | 6 | iblre 25829 | . . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ if(0 ≤
(ℜ‘𝐵),
(ℜ‘𝐵), 0))
∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0)) ∈
𝐿1))) | 
| 22 | 9, 21 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0)) ∈
𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0)) ∈
𝐿1)) | 
| 23 | 22 | simpld 494 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0)) ∈
𝐿1) | 
| 24 | 20, 23 | itgcl 25819 | . . . . . 6
⊢ (𝜑 → ∫𝐴if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0) d𝑥 ∈ ℂ) | 
| 25 | 6 | renegcld 11690 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℜ‘𝐵) ∈ ℝ) | 
| 26 |  | ifcl 4571 | . . . . . . . 8
⊢
((-(ℜ‘𝐵)
∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0) ∈
ℝ) | 
| 27 | 25, 18, 26 | sylancl 586 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0) ∈
ℝ) | 
| 28 | 22 | simprd 495 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0)) ∈
𝐿1) | 
| 29 | 27, 28 | itgcl 25819 | . . . . . 6
⊢ (𝜑 → ∫𝐴if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0) d𝑥 ∈ ℂ) | 
| 30 | 24, 29 | negsubdi2d 11636 | . . . . 5
⊢ (𝜑 → -(∫𝐴if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0) d𝑥) = (∫𝐴if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0) d𝑥)) | 
| 31 | 6, 9 | itgreval 25832 | . . . . . 6
⊢ (𝜑 → ∫𝐴(ℜ‘𝐵) d𝑥 = (∫𝐴if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0) d𝑥)) | 
| 32 | 31 | negeqd 11502 | . . . . 5
⊢ (𝜑 → -∫𝐴(ℜ‘𝐵) d𝑥 = -(∫𝐴if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0) d𝑥)) | 
| 33 | 5 | negcld 11607 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℂ) | 
| 34 | 33 | recld 15233 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘-𝐵) ∈ ℝ) | 
| 35 | 4, 1 | iblneg 25838 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈
𝐿1) | 
| 36 | 33 | iblcn 25834 | . . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ -𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (ℜ‘-𝐵)) ∈ 𝐿1
∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘-𝐵)) ∈
𝐿1))) | 
| 37 | 35, 36 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘-𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘-𝐵)) ∈
𝐿1)) | 
| 38 | 37 | simpld 494 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘-𝐵)) ∈
𝐿1) | 
| 39 | 34, 38 | itgreval 25832 | . . . . . 6
⊢ (𝜑 → ∫𝐴(ℜ‘-𝐵) d𝑥 = (∫𝐴if(0 ≤ (ℜ‘-𝐵), (ℜ‘-𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ -(ℜ‘-𝐵), -(ℜ‘-𝐵), 0) d𝑥)) | 
| 40 | 5 | renegd 15248 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘-𝐵) = -(ℜ‘𝐵)) | 
| 41 | 40 | breq2d 5155 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ (ℜ‘-𝐵) ↔ 0 ≤
-(ℜ‘𝐵))) | 
| 42 | 41, 40 | ifbieq1d 4550 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘-𝐵), (ℜ‘-𝐵), 0) = if(0 ≤
-(ℜ‘𝐵),
-(ℜ‘𝐵),
0)) | 
| 43 | 42 | itgeq2dv 25817 | . . . . . . 7
⊢ (𝜑 → ∫𝐴if(0 ≤ (ℜ‘-𝐵), (ℜ‘-𝐵), 0) d𝑥 = ∫𝐴if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0) d𝑥) | 
| 44 | 40 | negeqd 11502 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℜ‘-𝐵) = --(ℜ‘𝐵)) | 
| 45 | 6 | recnd 11289 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℂ) | 
| 46 | 45 | negnegd 11611 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → --(ℜ‘𝐵) = (ℜ‘𝐵)) | 
| 47 | 44, 46 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℜ‘-𝐵) = (ℜ‘𝐵)) | 
| 48 | 47 | breq2d 5155 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ -(ℜ‘-𝐵) ↔ 0 ≤
(ℜ‘𝐵))) | 
| 49 | 48, 47 | ifbieq1d 4550 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(ℜ‘-𝐵), -(ℜ‘-𝐵), 0) = if(0 ≤
(ℜ‘𝐵),
(ℜ‘𝐵),
0)) | 
| 50 | 49 | itgeq2dv 25817 | . . . . . . 7
⊢ (𝜑 → ∫𝐴if(0 ≤ -(ℜ‘-𝐵), -(ℜ‘-𝐵), 0) d𝑥 = ∫𝐴if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0) d𝑥) | 
| 51 | 43, 50 | oveq12d 7449 | . . . . . 6
⊢ (𝜑 → (∫𝐴if(0 ≤ (ℜ‘-𝐵), (ℜ‘-𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ -(ℜ‘-𝐵), -(ℜ‘-𝐵), 0) d𝑥) = (∫𝐴if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0) d𝑥)) | 
| 52 | 39, 51 | eqtrd 2777 | . . . . 5
⊢ (𝜑 → ∫𝐴(ℜ‘-𝐵) d𝑥 = (∫𝐴if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0) d𝑥)) | 
| 53 | 30, 32, 52 | 3eqtr4d 2787 | . . . 4
⊢ (𝜑 → -∫𝐴(ℜ‘𝐵) d𝑥 = ∫𝐴(ℜ‘-𝐵) d𝑥) | 
| 54 |  | mulneg2 11700 | . . . . . 6
⊢ ((i
∈ ℂ ∧ ∫𝐴(ℑ‘𝐵) d𝑥 ∈ ℂ) → (i ·
-∫𝐴(ℑ‘𝐵) d𝑥) = -(i · ∫𝐴(ℑ‘𝐵) d𝑥)) | 
| 55 | 11, 14, 54 | sylancr 587 | . . . . 5
⊢ (𝜑 → (i · -∫𝐴(ℑ‘𝐵) d𝑥) = -(i · ∫𝐴(ℑ‘𝐵) d𝑥)) | 
| 56 |  | ifcl 4571 | . . . . . . . . . . 11
⊢
(((ℑ‘𝐵)
∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0) ∈
ℝ) | 
| 57 | 12, 18, 56 | sylancl 586 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0) ∈
ℝ) | 
| 58 | 12 | iblre 25829 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ if(0 ≤
(ℑ‘𝐵),
(ℑ‘𝐵), 0))
∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0)) ∈
𝐿1))) | 
| 59 | 13, 58 | mpbid 232 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0)) ∈
𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0)) ∈
𝐿1)) | 
| 60 | 59 | simpld 494 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0)) ∈
𝐿1) | 
| 61 | 57, 60 | itgcl 25819 | . . . . . . . . 9
⊢ (𝜑 → ∫𝐴if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0) d𝑥 ∈ ℂ) | 
| 62 | 12 | renegcld 11690 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘𝐵) ∈ ℝ) | 
| 63 |  | ifcl 4571 | . . . . . . . . . . 11
⊢
((-(ℑ‘𝐵)
∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0) ∈
ℝ) | 
| 64 | 62, 18, 63 | sylancl 586 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0) ∈
ℝ) | 
| 65 | 59 | simprd 495 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0)) ∈
𝐿1) | 
| 66 | 64, 65 | itgcl 25819 | . . . . . . . . 9
⊢ (𝜑 → ∫𝐴if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0) d𝑥 ∈ ℂ) | 
| 67 | 61, 66 | negsubdi2d 11636 | . . . . . . . 8
⊢ (𝜑 → -(∫𝐴if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0) d𝑥) = (∫𝐴if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0) d𝑥)) | 
| 68 | 5 | imnegd 15249 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘-𝐵) = -(ℑ‘𝐵)) | 
| 69 | 68 | breq2d 5155 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ (ℑ‘-𝐵) ↔ 0 ≤
-(ℑ‘𝐵))) | 
| 70 | 69, 68 | ifbieq1d 4550 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℑ‘-𝐵), (ℑ‘-𝐵), 0) = if(0 ≤
-(ℑ‘𝐵),
-(ℑ‘𝐵),
0)) | 
| 71 | 70 | itgeq2dv 25817 | . . . . . . . . 9
⊢ (𝜑 → ∫𝐴if(0 ≤ (ℑ‘-𝐵), (ℑ‘-𝐵), 0) d𝑥 = ∫𝐴if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0) d𝑥) | 
| 72 | 68 | negeqd 11502 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘-𝐵) = --(ℑ‘𝐵)) | 
| 73 | 12 | recnd 11289 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℂ) | 
| 74 | 73 | negnegd 11611 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → --(ℑ‘𝐵) = (ℑ‘𝐵)) | 
| 75 | 72, 74 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘-𝐵) = (ℑ‘𝐵)) | 
| 76 | 75 | breq2d 5155 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ -(ℑ‘-𝐵) ↔ 0 ≤
(ℑ‘𝐵))) | 
| 77 | 76, 75 | ifbieq1d 4550 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(ℑ‘-𝐵), -(ℑ‘-𝐵), 0) = if(0 ≤
(ℑ‘𝐵),
(ℑ‘𝐵),
0)) | 
| 78 | 77 | itgeq2dv 25817 | . . . . . . . . 9
⊢ (𝜑 → ∫𝐴if(0 ≤ -(ℑ‘-𝐵), -(ℑ‘-𝐵), 0) d𝑥 = ∫𝐴if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0) d𝑥) | 
| 79 | 71, 78 | oveq12d 7449 | . . . . . . . 8
⊢ (𝜑 → (∫𝐴if(0 ≤ (ℑ‘-𝐵), (ℑ‘-𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ -(ℑ‘-𝐵), -(ℑ‘-𝐵), 0) d𝑥) = (∫𝐴if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0) d𝑥)) | 
| 80 | 67, 79 | eqtr4d 2780 | . . . . . . 7
⊢ (𝜑 → -(∫𝐴if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0) d𝑥) = (∫𝐴if(0 ≤ (ℑ‘-𝐵), (ℑ‘-𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ -(ℑ‘-𝐵), -(ℑ‘-𝐵), 0) d𝑥)) | 
| 81 | 12, 13 | itgreval 25832 | . . . . . . . 8
⊢ (𝜑 → ∫𝐴(ℑ‘𝐵) d𝑥 = (∫𝐴if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0) d𝑥)) | 
| 82 | 81 | negeqd 11502 | . . . . . . 7
⊢ (𝜑 → -∫𝐴(ℑ‘𝐵) d𝑥 = -(∫𝐴if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0) d𝑥)) | 
| 83 | 33 | imcld 15234 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘-𝐵) ∈ ℝ) | 
| 84 | 37 | simprd 495 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘-𝐵)) ∈
𝐿1) | 
| 85 | 83, 84 | itgreval 25832 | . . . . . . 7
⊢ (𝜑 → ∫𝐴(ℑ‘-𝐵) d𝑥 = (∫𝐴if(0 ≤ (ℑ‘-𝐵), (ℑ‘-𝐵), 0) d𝑥 − ∫𝐴if(0 ≤ -(ℑ‘-𝐵), -(ℑ‘-𝐵), 0) d𝑥)) | 
| 86 | 80, 82, 85 | 3eqtr4d 2787 | . . . . . 6
⊢ (𝜑 → -∫𝐴(ℑ‘𝐵) d𝑥 = ∫𝐴(ℑ‘-𝐵) d𝑥) | 
| 87 | 86 | oveq2d 7447 | . . . . 5
⊢ (𝜑 → (i · -∫𝐴(ℑ‘𝐵) d𝑥) = (i · ∫𝐴(ℑ‘-𝐵) d𝑥)) | 
| 88 | 55, 87 | eqtr3d 2779 | . . . 4
⊢ (𝜑 → -(i · ∫𝐴(ℑ‘𝐵) d𝑥) = (i · ∫𝐴(ℑ‘-𝐵) d𝑥)) | 
| 89 | 53, 88 | oveq12d 7449 | . . 3
⊢ (𝜑 → (-∫𝐴(ℜ‘𝐵) d𝑥 + -(i · ∫𝐴(ℑ‘𝐵) d𝑥)) = (∫𝐴(ℜ‘-𝐵) d𝑥 + (i · ∫𝐴(ℑ‘-𝐵) d𝑥))) | 
| 90 | 17, 89 | eqtrd 2777 | . 2
⊢ (𝜑 → -(∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)) = (∫𝐴(ℜ‘-𝐵) d𝑥 + (i · ∫𝐴(ℑ‘-𝐵) d𝑥))) | 
| 91 | 4, 1 | itgcnval 25835 | . . 3
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) | 
| 92 | 91 | negeqd 11502 | . 2
⊢ (𝜑 → -∫𝐴𝐵 d𝑥 = -(∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥))) | 
| 93 | 33, 35 | itgcnval 25835 | . 2
⊢ (𝜑 → ∫𝐴-𝐵 d𝑥 = (∫𝐴(ℜ‘-𝐵) d𝑥 + (i · ∫𝐴(ℑ‘-𝐵) d𝑥))) | 
| 94 | 90, 92, 93 | 3eqtr4d 2787 | 1
⊢ (𝜑 → -∫𝐴𝐵 d𝑥 = ∫𝐴-𝐵 d𝑥) |