Proof of Theorem asinlem3
| Step | Hyp | Ref
| Expression |
| 1 | | 0red 11264 |
. 2
⊢ (𝐴 ∈ ℂ → 0 ∈
ℝ) |
| 2 | | imcl 15150 |
. 2
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) |
| 3 | | ax-icn 11214 |
. . . . . . . . 9
⊢ i ∈
ℂ |
| 4 | | negcl 11508 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → -𝐴 ∈
ℂ) |
| 5 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
-𝐴 ∈
ℂ) |
| 6 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ -𝐴
∈ ℂ) → (i · -𝐴) ∈ ℂ) |
| 7 | 3, 5, 6 | sylancr 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(i · -𝐴) ∈
ℂ) |
| 8 | | ax-1cn 11213 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
| 9 | 5 | sqcld 14184 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(-𝐴↑2) ∈
ℂ) |
| 10 | | subcl 11507 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ (-𝐴↑2) ∈ ℂ) → (1 −
(-𝐴↑2)) ∈
ℂ) |
| 11 | 8, 9, 10 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(1 − (-𝐴↑2))
∈ ℂ) |
| 12 | 11 | sqrtcld 15476 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(√‘(1 − (-𝐴↑2))) ∈ ℂ) |
| 13 | 7, 12 | addcld 11280 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
((i · -𝐴) +
(√‘(1 − (-𝐴↑2)))) ∈ ℂ) |
| 14 | | asinlem 26911 |
. . . . . . . 8
⊢ (-𝐴 ∈ ℂ → ((i
· -𝐴) +
(√‘(1 − (-𝐴↑2)))) ≠ 0) |
| 15 | 5, 14 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
((i · -𝐴) +
(√‘(1 − (-𝐴↑2)))) ≠ 0) |
| 16 | 13, 15 | absrpcld 15487 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(abs‘((i · -𝐴)
+ (√‘(1 − (-𝐴↑2))))) ∈
ℝ+) |
| 17 | | 2z 12649 |
. . . . . 6
⊢ 2 ∈
ℤ |
| 18 | | rpexpcl 14121 |
. . . . . 6
⊢
(((abs‘((i · -𝐴) + (√‘(1 − (-𝐴↑2))))) ∈
ℝ+ ∧ 2 ∈ ℤ) → ((abs‘((i ·
-𝐴) + (√‘(1
− (-𝐴↑2)))))↑2) ∈
ℝ+) |
| 19 | 16, 17, 18 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
((abs‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))↑2) ∈
ℝ+) |
| 20 | 19 | rprecred 13088 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(1 / ((abs‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))↑2)) ∈
ℝ) |
| 21 | 13 | cjcld 15235 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(∗‘((i · -𝐴) + (√‘(1 − (-𝐴↑2))))) ∈
ℂ) |
| 22 | 21 | recld 15233 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(ℜ‘(∗‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))) ∈
ℝ) |
| 23 | 19 | rpreccld 13087 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(1 / ((abs‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))↑2)) ∈
ℝ+) |
| 24 | 23 | rpge0d 13081 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) → 0
≤ (1 / ((abs‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))↑2))) |
| 25 | | imneg 15172 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(ℑ‘-𝐴) =
-(ℑ‘𝐴)) |
| 26 | 25 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(ℑ‘-𝐴) =
-(ℑ‘𝐴)) |
| 27 | 2 | le0neg2d 11835 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (0 ≤
(ℑ‘𝐴) ↔
-(ℑ‘𝐴) ≤
0)) |
| 28 | 27 | biimpa 476 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
-(ℑ‘𝐴) ≤
0) |
| 29 | 26, 28 | eqbrtrd 5165 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(ℑ‘-𝐴) ≤
0) |
| 30 | | asinlem3a 26913 |
. . . . . 6
⊢ ((-𝐴 ∈ ℂ ∧
(ℑ‘-𝐴) ≤ 0)
→ 0 ≤ (ℜ‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))) |
| 31 | 5, 29, 30 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) → 0
≤ (ℜ‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))) |
| 32 | 13 | recjd 15243 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(ℜ‘(∗‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))) =
(ℜ‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))) |
| 33 | 31, 32 | breqtrrd 5171 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) → 0
≤ (ℜ‘(∗‘((i · -𝐴) + (√‘(1 − (-𝐴↑2))))))) |
| 34 | 20, 22, 24, 33 | mulge0d 11840 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) → 0
≤ ((1 / ((abs‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))↑2)) ·
(ℜ‘(∗‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))))) |
| 35 | | recval 15361 |
. . . . . . 7
⊢ ((((i
· -𝐴) +
(√‘(1 − (-𝐴↑2)))) ∈ ℂ ∧ ((i
· -𝐴) +
(√‘(1 − (-𝐴↑2)))) ≠ 0) → (1 / ((i ·
-𝐴) + (√‘(1
− (-𝐴↑2))))) =
((∗‘((i · -𝐴) + (√‘(1 − (-𝐴↑2))))) / ((abs‘((i
· -𝐴) +
(√‘(1 − (-𝐴↑2)))))↑2))) |
| 36 | 13, 15, 35 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(1 / ((i · -𝐴) +
(√‘(1 − (-𝐴↑2))))) = ((∗‘((i ·
-𝐴) + (√‘(1
− (-𝐴↑2))))) /
((abs‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))↑2))) |
| 37 | | asinlem2 26912 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))) · ((i · -𝐴) + (√‘(1 −
(-𝐴↑2))))) =
1) |
| 38 | 37 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(((i · 𝐴) +
(√‘(1 − (𝐴↑2)))) · ((i · -𝐴) + (√‘(1 −
(-𝐴↑2))))) =
1) |
| 39 | 38 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) → 1
= (((i · 𝐴) +
(√‘(1 − (𝐴↑2)))) · ((i · -𝐴) + (√‘(1 −
(-𝐴↑2)))))) |
| 40 | | 1cnd 11256 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) → 1
∈ ℂ) |
| 41 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
𝐴 ∈
ℂ) |
| 42 | | mulcl 11239 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 43 | 3, 41, 42 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(i · 𝐴) ∈
ℂ) |
| 44 | | sqcl 14158 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (𝐴↑2) ∈
ℂ) |
| 45 | 44 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(𝐴↑2) ∈
ℂ) |
| 46 | | subcl 11507 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (1 −
(𝐴↑2)) ∈
ℂ) |
| 47 | 8, 45, 46 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(1 − (𝐴↑2))
∈ ℂ) |
| 48 | 47 | sqrtcld 15476 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(√‘(1 − (𝐴↑2))) ∈ ℂ) |
| 49 | 43, 48 | addcld 11280 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
((i · 𝐴) +
(√‘(1 − (𝐴↑2)))) ∈ ℂ) |
| 50 | 40, 49, 13, 15 | divmul3d 12077 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
((1 / ((i · -𝐴) +
(√‘(1 − (-𝐴↑2))))) = ((i · 𝐴) + (√‘(1 −
(𝐴↑2)))) ↔ 1 =
(((i · 𝐴) +
(√‘(1 − (𝐴↑2)))) · ((i · -𝐴) + (√‘(1 −
(-𝐴↑2))))))) |
| 51 | 39, 50 | mpbird 257 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(1 / ((i · -𝐴) +
(√‘(1 − (-𝐴↑2))))) = ((i · 𝐴) + (√‘(1 −
(𝐴↑2))))) |
| 52 | 19 | rpcnd 13079 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
((abs‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))↑2) ∈
ℂ) |
| 53 | 19 | rpne0d 13082 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
((abs‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))↑2) ≠
0) |
| 54 | 21, 52, 53 | divrec2d 12047 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
((∗‘((i · -𝐴) + (√‘(1 − (-𝐴↑2))))) / ((abs‘((i
· -𝐴) +
(√‘(1 − (-𝐴↑2)))))↑2)) = ((1 /
((abs‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))↑2)) ·
(∗‘((i · -𝐴) + (√‘(1 − (-𝐴↑2))))))) |
| 55 | 36, 51, 54 | 3eqtr3d 2785 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
((i · 𝐴) +
(√‘(1 − (𝐴↑2)))) = ((1 / ((abs‘((i ·
-𝐴) + (√‘(1
− (-𝐴↑2)))))↑2)) ·
(∗‘((i · -𝐴) + (√‘(1 − (-𝐴↑2))))))) |
| 56 | 55 | fveq2d 6910 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))) = (ℜ‘((1
/ ((abs‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))↑2)) ·
(∗‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))))) |
| 57 | 20, 21 | remul2d 15266 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(ℜ‘((1 / ((abs‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))↑2)) ·
(∗‘((i · -𝐴) + (√‘(1 − (-𝐴↑2))))))) = ((1 /
((abs‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))↑2)) ·
(ℜ‘(∗‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))))) |
| 58 | 56, 57 | eqtrd 2777 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) →
(ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))) = ((1 /
((abs‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))↑2)) ·
(ℜ‘(∗‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))))) |
| 59 | 34, 58 | breqtrrd 5171 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 0 ≤
(ℑ‘𝐴)) → 0
≤ (ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) |
| 60 | | asinlem3a 26913 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) ≤ 0)
→ 0 ≤ (ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) |
| 61 | 1, 2, 59, 60 | lecasei 11367 |
1
⊢ (𝐴 ∈ ℂ → 0 ≤
(ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) |