Step | Hyp | Ref
| Expression |
1 | | eqidd 2623 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) |
2 | | eqidd 2623 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐵 / (i↑𝑘))) = (ℜ‘(𝐵 / (i↑𝑘)))) |
3 | | itgcnlem1.v |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
4 | 1, 2, 3 | isibl2 23533 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ))) |
5 | | c0ex 10034 |
. . . . . . . 8
⊢ 0 ∈
V |
6 | | 1ex 10035 |
. . . . . . . 8
⊢ 1 ∈
V |
7 | | ax-icn 9995 |
. . . . . . . . . . 11
⊢ i ∈
ℂ |
8 | | exp0 12864 |
. . . . . . . . . . 11
⊢ (i ∈
ℂ → (i↑0) = 1) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . 10
⊢
(i↑0) = 1 |
10 | 9 | itgvallem 23551 |
. . . . . . . . 9
⊢ (𝑘 = 0 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 / 1))),
(ℜ‘(𝐵 / 1)),
0)))) |
11 | 10 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑘 = 0 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) ∈
ℝ)) |
12 | | exp1 12866 |
. . . . . . . . . . 11
⊢ (i ∈
ℂ → (i↑1) = i) |
13 | 7, 12 | ax-mp 5 |
. . . . . . . . . 10
⊢
(i↑1) = i |
14 | 13 | itgvallem 23551 |
. . . . . . . . 9
⊢ (𝑘 = 1 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 / i))),
(ℜ‘(𝐵 / i)),
0)))) |
15 | 14 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑘 = 1 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) ∈
ℝ)) |
16 | 5, 6, 11, 15 | ralpr 4238 |
. . . . . . 7
⊢
(∀𝑘 ∈
{0, 1} (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) ∈ ℝ
∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) ∈
ℝ)) |
17 | 3 | div1d 10793 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 1) = 𝐵) |
18 | 17 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐵 / 1)) = (ℜ‘𝐵)) |
19 | 18 | ibllem 23531 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)) |
20 | 19 | mpteq2dv 4745 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0)) = (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘𝐵)),
(ℜ‘𝐵),
0))) |
21 | 20 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)))) |
22 | | itgcnlem.r |
. . . . . . . . . 10
⊢ 𝑅 =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0))) |
23 | 21, 22 | syl6eqr 2674 |
. . . . . . . . 9
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) = 𝑅) |
24 | 23 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) ∈ ℝ
↔ 𝑅 ∈
ℝ)) |
25 | | itgcnlem.t |
. . . . . . . . . 10
⊢ 𝑇 =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) |
26 | | imval 13847 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ℂ →
(ℑ‘𝐵) =
(ℜ‘(𝐵 /
i))) |
27 | 3, 26 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) = (ℜ‘(𝐵 / i))) |
28 | 27 | ibllem 23531 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0)) |
29 | 28 | mpteq2dv 4745 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) |
30 | 29 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0)))) |
31 | 25, 30 | syl5req 2669 |
. . . . . . . . 9
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) = 𝑇) |
32 | 31 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) ∈ ℝ
↔ 𝑇 ∈
ℝ)) |
33 | 24, 32 | anbi12d 747 |
. . . . . . 7
⊢ (𝜑 →
(((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 1))), (ℜ‘(𝐵 / 1)), 0))) ∈ ℝ
∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / i))), (ℜ‘(𝐵 / i)), 0))) ∈ ℝ)
↔ (𝑅 ∈ ℝ
∧ 𝑇 ∈
ℝ))) |
34 | 16, 33 | syl5bb 272 |
. . . . . 6
⊢ (𝜑 → (∀𝑘 ∈ {0, 1}
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ (𝑅 ∈ ℝ ∧ 𝑇 ∈
ℝ))) |
35 | | 2ex 11092 |
. . . . . . . 8
⊢ 2 ∈
V |
36 | | 3ex 11096 |
. . . . . . . 8
⊢ 3 ∈
V |
37 | | i2 12965 |
. . . . . . . . . 10
⊢
(i↑2) = -1 |
38 | 37 | itgvallem 23551 |
. . . . . . . . 9
⊢ (𝑘 = 2 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 / -1))),
(ℜ‘(𝐵 / -1)),
0)))) |
39 | 38 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑘 = 2 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) ∈
ℝ)) |
40 | | i3 12966 |
. . . . . . . . . 10
⊢
(i↑3) = -i |
41 | 40 | itgvallem 23551 |
. . . . . . . . 9
⊢ (𝑘 = 3 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 / -i))),
(ℜ‘(𝐵 / -i)),
0)))) |
42 | 41 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑘 = 3 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) ∈
ℝ)) |
43 | 35, 36, 39, 42 | ralpr 4238 |
. . . . . . 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 13949 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘-𝐵) = -(ℜ‘𝐵)) |
46 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ |
47 | 46 | negnegi 10351 |
. . . . . . . . . . . . . . . . . 18
⊢ --1 =
1 |
48 | 47 | oveq2i 6661 |
. . . . . . . . . . . . . . . . 17
⊢ (-𝐵 / --1) = (-𝐵 / 1) |
49 | 3 | negcld 10379 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℂ) |
50 | 49 | div1d 10793 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / 1) = -𝐵) |
51 | 48, 50 | syl5eq 2668 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / --1) = -𝐵) |
52 | 46 | negcli 10349 |
. . . . . . . . . . . . . . . . . 18
⊢ -1 ∈
ℂ |
53 | | neg1ne0 11126 |
. . . . . . . . . . . . . . . . . 18
⊢ -1 ≠
0 |
54 | | div2neg 10748 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ ℂ ∧ -1 ∈
ℂ ∧ -1 ≠ 0) → (-𝐵 / --1) = (𝐵 / -1)) |
55 | 52, 53, 54 | mp3an23 1416 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ ℂ → (-𝐵 / --1) = (𝐵 / -1)) |
56 | 3, 55 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / --1) = (𝐵 / -1)) |
57 | 51, 56 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 = (𝐵 / -1)) |
58 | 57 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘-𝐵) = (ℜ‘(𝐵 / -1))) |
59 | 45, 58 | eqtr3d 2658 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℜ‘𝐵) = (ℜ‘(𝐵 / -1))) |
60 | 59 | ibllem 23531 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)) |
61 | 60 | mpteq2dv 4745 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) |
62 | 61 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0)))) |
63 | 44, 62 | syl5req 2669 |
. . . . . . . . 9
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) = 𝑆) |
64 | 63 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) ∈ ℝ
↔ 𝑆 ∈
ℝ)) |
65 | | itgcnlem.u |
. . . . . . . . . 10
⊢ 𝑈 =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) |
66 | | imval 13847 |
. . . . . . . . . . . . . . 15
⊢ (-𝐵 ∈ ℂ →
(ℑ‘-𝐵) =
(ℜ‘(-𝐵 /
i))) |
67 | 49, 66 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘-𝐵) = (ℜ‘(-𝐵 / i))) |
68 | 3 | imnegd 13950 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘-𝐵) = -(ℑ‘𝐵)) |
69 | 7 | negnegi 10351 |
. . . . . . . . . . . . . . . . . 18
⊢ --i =
i |
70 | 69 | eqcomi 2631 |
. . . . . . . . . . . . . . . . 17
⊢ i =
--i |
71 | 70 | oveq2i 6661 |
. . . . . . . . . . . . . . . 16
⊢ (-𝐵 / i) = (-𝐵 / --i) |
72 | 7 | negcli 10349 |
. . . . . . . . . . . . . . . . . 18
⊢ -i ∈
ℂ |
73 | | ine0 10465 |
. . . . . . . . . . . . . . . . . . 19
⊢ i ≠
0 |
74 | 7, 73 | negne0i 10356 |
. . . . . . . . . . . . . . . . . 18
⊢ -i ≠
0 |
75 | | div2neg 10748 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ ℂ ∧ -i ∈
ℂ ∧ -i ≠ 0) → (-𝐵 / --i) = (𝐵 / -i)) |
76 | 72, 74, 75 | mp3an23 1416 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ ℂ → (-𝐵 / --i) = (𝐵 / -i)) |
77 | 3, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / --i) = (𝐵 / -i)) |
78 | 71, 77 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 / i) = (𝐵 / -i)) |
79 | 78 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(-𝐵 / i)) = (ℜ‘(𝐵 / -i))) |
80 | 67, 68, 79 | 3eqtr3d 2664 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(ℑ‘𝐵) = (ℜ‘(𝐵 / -i))) |
81 | 80 | ibllem 23531 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)) |
82 | 81 | mpteq2dv 4745 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) |
83 | 82 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0))) =
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0)))) |
84 | 65, 83 | syl5req 2669 |
. . . . . . . . 9
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) = 𝑈) |
85 | 84 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) ∈ ℝ
↔ 𝑈 ∈
ℝ)) |
86 | 64, 85 | anbi12d 747 |
. . . . . . 7
⊢ (𝜑 →
(((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -1))), (ℜ‘(𝐵 / -1)), 0))) ∈ ℝ
∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / -i))), (ℜ‘(𝐵 / -i)), 0))) ∈ ℝ)
↔ (𝑆 ∈ ℝ
∧ 𝑈 ∈
ℝ))) |
87 | 43, 86 | syl5bb 272 |
. . . . . 6
⊢ (𝜑 → (∀𝑘 ∈ {2, 3}
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ (𝑆 ∈ ℝ ∧ 𝑈 ∈
ℝ))) |
88 | 34, 87 | anbi12d 747 |
. . . . 5
⊢ (𝜑 → ((∀𝑘 ∈ {0, 1}
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ∧ ∀𝑘 ∈ {2, 3}
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) ↔ ((𝑅 ∈ ℝ ∧ 𝑇 ∈ ℝ) ∧ (𝑆 ∈ ℝ ∧ 𝑈 ∈
ℝ)))) |
89 | | 1le3 11244 |
. . . . . . . . . 10
⊢ 1 ≤
3 |
90 | | 1eluzge0 11732 |
. . . . . . . . . . 11
⊢ 1 ∈
(ℤ≥‘0) |
91 | | 3z 11410 |
. . . . . . . . . . 11
⊢ 3 ∈
ℤ |
92 | | elfz5 12334 |
. . . . . . . . . . 11
⊢ ((1
∈ (ℤ≥‘0) ∧ 3 ∈ ℤ) → (1
∈ (0...3) ↔ 1 ≤ 3)) |
93 | 90, 91, 92 | mp2an 708 |
. . . . . . . . . 10
⊢ (1 ∈
(0...3) ↔ 1 ≤ 3) |
94 | 89, 93 | mpbir 221 |
. . . . . . . . 9
⊢ 1 ∈
(0...3) |
95 | | fzsplit 12367 |
. . . . . . . . 9
⊢ (1 ∈
(0...3) → (0...3) = ((0...1) ∪ ((1 + 1)...3))) |
96 | 94, 95 | ax-mp 5 |
. . . . . . . 8
⊢ (0...3) =
((0...1) ∪ ((1 + 1)...3)) |
97 | | 0z 11388 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
98 | | fzpr 12396 |
. . . . . . . . . . 11
⊢ (0 ∈
ℤ → (0...(0 + 1)) = {0, (0 + 1)}) |
99 | 97, 98 | ax-mp 5 |
. . . . . . . . . 10
⊢ (0...(0 +
1)) = {0, (0 + 1)} |
100 | | 1e0p1 11552 |
. . . . . . . . . . 11
⊢ 1 = (0 +
1) |
101 | 100 | oveq2i 6661 |
. . . . . . . . . 10
⊢ (0...1) =
(0...(0 + 1)) |
102 | 100 | preq2i 4272 |
. . . . . . . . . 10
⊢ {0, 1} =
{0, (0 + 1)} |
103 | 99, 101, 102 | 3eqtr4i 2654 |
. . . . . . . . 9
⊢ (0...1) =
{0, 1} |
104 | | 2z 11409 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
105 | | fzpr 12396 |
. . . . . . . . . . 11
⊢ (2 ∈
ℤ → (2...(2 + 1)) = {2, (2 + 1)}) |
106 | 104, 105 | ax-mp 5 |
. . . . . . . . . 10
⊢ (2...(2 +
1)) = {2, (2 + 1)} |
107 | | 1p1e2 11134 |
. . . . . . . . . . 11
⊢ (1 + 1) =
2 |
108 | | df-3 11080 |
. . . . . . . . . . 11
⊢ 3 = (2 +
1) |
109 | 107, 108 | oveq12i 6662 |
. . . . . . . . . 10
⊢ ((1 +
1)...3) = (2...(2 + 1)) |
110 | 108 | preq2i 4272 |
. . . . . . . . . 10
⊢ {2, 3} =
{2, (2 + 1)} |
111 | 106, 109,
110 | 3eqtr4i 2654 |
. . . . . . . . 9
⊢ ((1 +
1)...3) = {2, 3} |
112 | 103, 111 | uneq12i 3765 |
. . . . . . . 8
⊢ ((0...1)
∪ ((1 + 1)...3)) = ({0, 1} ∪ {2, 3}) |
113 | 96, 112 | eqtri 2644 |
. . . . . . 7
⊢ (0...3) =
({0, 1} ∪ {2, 3}) |
114 | 113 | raleqi 3142 |
. . . . . 6
⊢
(∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ ∀𝑘 ∈ ({0, 1} ∪ {2,
3})(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) |
115 | | ralunb 3794 |
. . . . . 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))) ∈ ℝ)) |
116 | 114, 115 | bitri 264 |
. . . . 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))) ∈ ℝ)) |
117 | | an4 865 |
. . . . 5
⊢ (((𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)) ↔ ((𝑅 ∈ ℝ ∧ 𝑇 ∈ ℝ) ∧ (𝑆 ∈ ℝ ∧ 𝑈 ∈
ℝ))) |
118 | 88, 116, 117 | 3bitr4g 303 |
. . . 4
⊢ (𝜑 → (∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔ ((𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈
ℝ)))) |
119 | 118 | anbi2d 740 |
. . 3
⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ((𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ))))) |
120 | | 3anass 1042 |
. . 3
⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ((𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)))) |
121 | 119, 120 | syl6bbr 278 |
. 2
⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)))) |
122 | 4, 121 | bitrd 268 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ)))) |