Proof of Theorem iblneg
Step | Hyp | Ref
| Expression |
1 | | itgcnval.2 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) |
2 | | iblmbf 24932 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
3 | 1, 2 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
4 | | itgcnval.1 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
5 | 3, 4 | mbfmptcl 24800 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
6 | 5 | renegd 14920 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘-𝐵) = -(ℜ‘𝐵)) |
7 | 6 | breq2d 5086 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ (ℜ‘-𝐵) ↔ 0 ≤
-(ℜ‘𝐵))) |
8 | 7, 6 | ifbieq1d 4483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘-𝐵), (ℜ‘-𝐵), 0) = if(0 ≤
-(ℜ‘𝐵),
-(ℜ‘𝐵),
0)) |
9 | 8 | mpteq2dva 5174 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℜ‘-𝐵), (ℜ‘-𝐵), 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0))) |
10 | 5 | iblcn 24963 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1
∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1))) |
11 | 1, 10 | mpbid 231 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1)) |
12 | 11 | simpld 495 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈
𝐿1) |
13 | 5 | recld 14905 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℝ) |
14 | 13 | iblre 24958 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ if(0 ≤
(ℜ‘𝐵),
(ℜ‘𝐵), 0))
∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0)) ∈
𝐿1))) |
15 | 12, 14 | mpbid 231 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0)) ∈
𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0)) ∈
𝐿1)) |
16 | 15 | simprd 496 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘𝐵), -(ℜ‘𝐵), 0)) ∈
𝐿1) |
17 | 9, 16 | eqeltrd 2839 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℜ‘-𝐵), (ℜ‘-𝐵), 0)) ∈
𝐿1) |
18 | 6 | negeqd 11215 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℜ‘-𝐵) = --(ℜ‘𝐵)) |
19 | 13 | recnd 11003 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℂ) |
20 | 19 | negnegd 11323 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → --(ℜ‘𝐵) = (ℜ‘𝐵)) |
21 | 18, 20 | eqtrd 2778 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℜ‘-𝐵) = (ℜ‘𝐵)) |
22 | 21 | breq2d 5086 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ -(ℜ‘-𝐵) ↔ 0 ≤
(ℜ‘𝐵))) |
23 | 22, 21 | ifbieq1d 4483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(ℜ‘-𝐵), -(ℜ‘-𝐵), 0) = if(0 ≤
(ℜ‘𝐵),
(ℜ‘𝐵),
0)) |
24 | 23 | mpteq2dva 5174 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘-𝐵), -(ℜ‘-𝐵), 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0))) |
25 | 15 | simpld 495 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℜ‘𝐵), (ℜ‘𝐵), 0)) ∈
𝐿1) |
26 | 24, 25 | eqeltrd 2839 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘-𝐵), -(ℜ‘-𝐵), 0)) ∈
𝐿1) |
27 | 5 | negcld 11319 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℂ) |
28 | 27 | recld 14905 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘-𝐵) ∈ ℝ) |
29 | 28 | iblre 24958 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘-𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ if(0 ≤
(ℜ‘-𝐵),
(ℜ‘-𝐵), 0))
∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℜ‘-𝐵), -(ℜ‘-𝐵), 0)) ∈
𝐿1))) |
30 | 17, 26, 29 | mpbir2and 710 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘-𝐵)) ∈
𝐿1) |
31 | 5 | imnegd 14921 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘-𝐵) = -(ℑ‘𝐵)) |
32 | 31 | breq2d 5086 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ (ℑ‘-𝐵) ↔ 0 ≤
-(ℑ‘𝐵))) |
33 | 32, 31 | ifbieq1d 4483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℑ‘-𝐵), (ℑ‘-𝐵), 0) = if(0 ≤
-(ℑ‘𝐵),
-(ℑ‘𝐵),
0)) |
34 | 33 | mpteq2dva 5174 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℑ‘-𝐵), (ℑ‘-𝐵), 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0))) |
35 | 11 | simprd 496 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1) |
36 | 5 | imcld 14906 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℝ) |
37 | 36 | iblre 24958 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ if(0 ≤
(ℑ‘𝐵),
(ℑ‘𝐵), 0))
∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0)) ∈
𝐿1))) |
38 | 35, 37 | mpbid 231 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0)) ∈
𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0)) ∈
𝐿1)) |
39 | 38 | simprd 496 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘𝐵), -(ℑ‘𝐵), 0)) ∈
𝐿1) |
40 | 34, 39 | eqeltrd 2839 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℑ‘-𝐵), (ℑ‘-𝐵), 0)) ∈
𝐿1) |
41 | 31 | negeqd 11215 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘-𝐵) = --(ℑ‘𝐵)) |
42 | 36 | recnd 11003 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℂ) |
43 | 42 | negnegd 11323 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → --(ℑ‘𝐵) = (ℑ‘𝐵)) |
44 | 41, 43 | eqtrd 2778 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘-𝐵) = (ℑ‘𝐵)) |
45 | 44 | breq2d 5086 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ -(ℑ‘-𝐵) ↔ 0 ≤
(ℑ‘𝐵))) |
46 | 45, 44 | ifbieq1d 4483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(ℑ‘-𝐵), -(ℑ‘-𝐵), 0) = if(0 ≤
(ℑ‘𝐵),
(ℑ‘𝐵),
0)) |
47 | 46 | mpteq2dva 5174 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘-𝐵), -(ℑ‘-𝐵), 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0))) |
48 | 38 | simpld 495 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (ℑ‘𝐵), (ℑ‘𝐵), 0)) ∈
𝐿1) |
49 | 47, 48 | eqeltrd 2839 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘-𝐵), -(ℑ‘-𝐵), 0)) ∈
𝐿1) |
50 | 27 | imcld 14906 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘-𝐵) ∈ ℝ) |
51 | 50 | iblre 24958 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℑ‘-𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ if(0 ≤
(ℑ‘-𝐵),
(ℑ‘-𝐵), 0))
∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(ℑ‘-𝐵), -(ℑ‘-𝐵), 0)) ∈
𝐿1))) |
52 | 40, 49, 51 | mpbir2and 710 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘-𝐵)) ∈
𝐿1) |
53 | 27 | iblcn 24963 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ -𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (ℜ‘-𝐵)) ∈ 𝐿1
∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘-𝐵)) ∈
𝐿1))) |
54 | 30, 52, 53 | mpbir2and 710 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈
𝐿1) |