| Step | Hyp | Ref
| Expression |
| 1 | | eqidd 2738 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) |
| 2 | | eqidd 2738 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐵 / (i↑𝑘))) = (ℜ‘(𝐵 / (i↑𝑘)))) |
| 3 | | itgcnlem1.v |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
| 4 | 1, 2, 3 | isibl2 25801 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ))) |
| 5 | | c0ex 11255 |
. . . . . . . 8
⊢ 0 ∈
V |
| 6 | | 1ex 11257 |
. . . . . . . 8
⊢ 1 ∈
V |
| 7 | | ax-icn 11214 |
. . . . . . . . . . 11
⊢ i ∈
ℂ |
| 8 | | exp0 14106 |
. . . . . . . . . . 11
⊢ (i ∈
ℂ → (i↑0) = 1) |
| 9 | 7, 8 | ax-mp 5 |
. . . . . . . . . 10
⊢
(i↑0) = 1 |
| 10 | 9 | itgvallem 25820 |
. . . . . . . . 9
⊢ (𝑘 = 0 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 / 1))),
(ℜ‘(𝐵 / 1)),
0)))) |
| 11 | 10 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑘 = 0 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) ∈
ℝ)) |
| 12 | | exp1 14108 |
. . . . . . . . . . 11
⊢ (i ∈
ℂ → (i↑1) = i) |
| 13 | 7, 12 | ax-mp 5 |
. . . . . . . . . 10
⊢
(i↑1) = i |
| 14 | 13 | itgvallem 25820 |
. . . . . . . . 9
⊢ (𝑘 = 1 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 / i))),
(ℜ‘(𝐵 / i)),
0)))) |
| 15 | 14 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑘 = 1 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) ∈
ℝ)) |
| 16 | 5, 6, 11, 15 | ralpr 4700 |
. . . . . . 7
⊢
(∀𝑘 ∈
{0, 1} (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) ∈ ℝ
∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) ∈
ℝ)) |
| 17 | 3 | div1d 12035 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 1) = 𝐵) |
| 18 | 17 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐵 / 1)) = (ℜ‘𝐵)) |
| 19 | 18 | ibllem 25799 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)) |
| 20 | 19 | mpteq2dv 5244 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)) = (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘𝐵)),
(ℜ‘𝐵),
0))) |
| 21 | 20 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)))) |
| 22 | | itgcnlem.r |
. . . . . . . . . 10
⊢ 𝑅 =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))) |
| 23 | 21, 22 | eqtr4di 2795 |
. . . . . . . . 9
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) = 𝑅) |
| 24 | 23 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) ∈ ℝ
↔ 𝑅 ∈
ℝ)) |
| 25 | | itgcnlem.t |
. . . . . . . . . 10
⊢ 𝑇 =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) |
| 26 | | imval 15146 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ℂ →
(ℑ‘𝐵) =
(ℜ‘(𝐵 /
i))) |
| 27 | 3, 26 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) = (ℜ‘(𝐵 / i))) |
| 28 | 27 | ibllem 25799 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0)) |
| 29 | 28 | mpteq2dv 5244 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) |
| 30 | 29 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0)))) |
| 31 | 25, 30 | eqtr2id 2790 |
. . . . . . . . 9
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) = 𝑇) |
| 32 | 31 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) ∈ ℝ
↔ 𝑇 ∈
ℝ)) |
| 33 | 24, 32 | anbi12d 632 |
. . . . . . 7
⊢ (𝜑 →
(((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) ∈ ℝ
∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) ∈ ℝ)
↔ (𝑅 ∈ ℝ
∧ 𝑇 ∈
ℝ))) |
| 34 | 16, 33 | bitrid 283 |
. . . . . 6
⊢ (𝜑 → (∀𝑘 ∈ {0, 1}
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ (𝑅 ∈ ℝ ∧ 𝑇 ∈
ℝ))) |
| 35 | | 2ex 12343 |
. . . . . . . 8
⊢ 2 ∈
V |
| 36 | | 3ex 12348 |
. . . . . . . 8
⊢ 3 ∈
V |
| 37 | | i2 14241 |
. . . . . . . . . 10
⊢
(i↑2) = -1 |
| 38 | 37 | itgvallem 25820 |
. . . . . . . . 9
⊢ (𝑘 = 2 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 / -1))),
(ℜ‘(𝐵 / -1)),
0)))) |
| 39 | 38 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑘 = 2 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) ∈
ℝ)) |
| 40 | | i3 14242 |
. . . . . . . . . 10
⊢
(i↑3) = -i |
| 41 | 40 | itgvallem 25820 |
. . . . . . . . 9
⊢ (𝑘 = 3 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 / -i))),
(ℜ‘(𝐵 / -i)),
0)))) |
| 42 | 41 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑘 = 3 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) ∈
ℝ)) |
| 43 | 35, 36, 39, 42 | ralpr 4700 |
. . . . . . 7
⊢
(∀𝑘 ∈
{2, 3} (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) ∈ ℝ
∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) ∈
ℝ)) |
| 44 | | itgcnlem.s |
. . . . . . . . . 10
⊢ 𝑆 =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) |
| 45 | 3 | renegd 15248 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘-𝐵) = -(ℜ‘𝐵)) |
| 46 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ |
| 47 | 46 | negnegi 11579 |
. . . . . . . . . . . . . . . . . 18
⊢ --1 =
1 |
| 48 | 47 | oveq2i 7442 |
. . . . . . . . . . . . . . . . 17
⊢ (-𝐵 / --1) = (-𝐵 / 1) |
| 49 | 3 | negcld 11607 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℂ) |
| 50 | 49 | div1d 12035 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / 1) = -𝐵) |
| 51 | 48, 50 | eqtrid 2789 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / --1) = -𝐵) |
| 52 | 46 | negcli 11577 |
. . . . . . . . . . . . . . . . . 18
⊢ -1 ∈
ℂ |
| 53 | | neg1ne0 12382 |
. . . . . . . . . . . . . . . . . 18
⊢ -1 ≠
0 |
| 54 | | div2neg 11990 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ ℂ ∧ -1 ∈
ℂ ∧ -1 ≠ 0) → (-𝐵 / --1) = (𝐵 / -1)) |
| 55 | 52, 53, 54 | mp3an23 1455 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ ℂ → (-𝐵 / --1) = (𝐵 / -1)) |
| 56 | 3, 55 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / --1) = (𝐵 / -1)) |
| 57 | 51, 56 | eqtr3d 2779 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 = (𝐵 / -1)) |
| 58 | 57 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘-𝐵) = (ℜ‘(𝐵 / -1))) |
| 59 | 45, 58 | eqtr3d 2779 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℜ‘𝐵) = (ℜ‘(𝐵 / -1))) |
| 60 | 59 | ibllem 25799 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)) |
| 61 | 60 | mpteq2dv 5244 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) |
| 62 | 61 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)))) |
| 63 | 44, 62 | eqtr2id 2790 |
. . . . . . . . 9
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) = 𝑆) |
| 64 | 63 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) ∈ ℝ
↔ 𝑆 ∈
ℝ)) |
| 65 | | itgcnlem.u |
. . . . . . . . . 10
⊢ 𝑈 =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) |
| 66 | | imval 15146 |
. . . . . . . . . . . . . . 15
⊢ (-𝐵 ∈ ℂ →
(ℑ‘-𝐵) =
(ℜ‘(-𝐵 /
i))) |
| 67 | 49, 66 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘-𝐵) = (ℜ‘(-𝐵 / i))) |
| 68 | 3 | imnegd 15249 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘-𝐵) = -(ℑ‘𝐵)) |
| 69 | 7 | negnegi 11579 |
. . . . . . . . . . . . . . . . . 18
⊢ --i =
i |
| 70 | 69 | eqcomi 2746 |
. . . . . . . . . . . . . . . . 17
⊢ i =
--i |
| 71 | 70 | oveq2i 7442 |
. . . . . . . . . . . . . . . 16
⊢ (-𝐵 / i) = (-𝐵 / --i) |
| 72 | 7 | negcli 11577 |
. . . . . . . . . . . . . . . . . 18
⊢ -i ∈
ℂ |
| 73 | | ine0 11698 |
. . . . . . . . . . . . . . . . . . 19
⊢ i ≠
0 |
| 74 | 7, 73 | negne0i 11584 |
. . . . . . . . . . . . . . . . . 18
⊢ -i ≠
0 |
| 75 | | div2neg 11990 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ ℂ ∧ -i ∈
ℂ ∧ -i ≠ 0) → (-𝐵 / --i) = (𝐵 / -i)) |
| 76 | 72, 74, 75 | mp3an23 1455 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ ℂ → (-𝐵 / --i) = (𝐵 / -i)) |
| 77 | 3, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / --i) = (𝐵 / -i)) |
| 78 | 71, 77 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / i) = (𝐵 / -i)) |
| 79 | 78 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(-𝐵 / i)) = (ℜ‘(𝐵 / -i))) |
| 80 | 67, 68, 79 | 3eqtr3d 2785 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘𝐵) = (ℜ‘(𝐵 / -i))) |
| 81 | 80 | ibllem 25799 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)) |
| 82 | 81 | mpteq2dv 5244 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) |
| 83 | 82 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)))) |
| 84 | 65, 83 | eqtr2id 2790 |
. . . . . . . . 9
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) = 𝑈) |
| 85 | 84 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) ∈ ℝ
↔ 𝑈 ∈
ℝ)) |
| 86 | 64, 85 | anbi12d 632 |
. . . . . . 7
⊢ (𝜑 →
(((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) ∈ ℝ
∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) ∈ ℝ)
↔ (𝑆 ∈ ℝ
∧ 𝑈 ∈
ℝ))) |
| 87 | 43, 86 | bitrid 283 |
. . . . . 6
⊢ (𝜑 → (∀𝑘 ∈ {2, 3}
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ (𝑆 ∈ ℝ ∧ 𝑈 ∈
ℝ))) |
| 88 | 34, 87 | anbi12d 632 |
. . . . 5
⊢ (𝜑 → ((∀𝑘 ∈ {0, 1}
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ∧ ∀𝑘 ∈ {2, 3}
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) ↔ ((𝑅 ∈ ℝ ∧ 𝑇 ∈ ℝ) ∧ (𝑆 ∈ ℝ ∧ 𝑈 ∈
ℝ)))) |
| 89 | | fz0to3un2pr 13669 |
. . . . . . 7
⊢ (0...3) =
({0, 1} ∪ {2, 3}) |
| 90 | 89 | raleqi 3324 |
. . . . . 6
⊢
(∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ ∀𝑘 ∈ ({0, 1} ∪ {2,
3})(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) |
| 91 | | ralunb 4197 |
. . . . . 6
⊢
(∀𝑘 ∈
({0, 1} ∪ {2, 3})(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔
(∀𝑘 ∈ {0, 1}
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ∧ ∀𝑘 ∈ {2, 3}
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ)) |
| 92 | 90, 91 | bitri 275 |
. . . . 5
⊢
(∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔
(∀𝑘 ∈ {0, 1}
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ∧ ∀𝑘 ∈ {2, 3}
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ)) |
| 93 | | an4 656 |
. . . . 5
⊢ (((𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)) ↔ ((𝑅 ∈ ℝ ∧ 𝑇 ∈ ℝ) ∧ (𝑆 ∈ ℝ ∧ 𝑈 ∈
ℝ))) |
| 94 | 88, 92, 93 | 3bitr4g 314 |
. . . 4
⊢ (𝜑 → (∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ ((𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈
ℝ)))) |
| 95 | 94 | anbi2d 630 |
. . 3
⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ((𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ))))) |
| 96 | | 3anass 1095 |
. . 3
⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ((𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)))) |
| 97 | 95, 96 | bitr4di 289 |
. 2
⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)))) |
| 98 | 4, 97 | bitrd 279 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)))) |