Proof of Theorem asinsinlem
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ax-icn 11216 |
. . . . . 6
⊢ i ∈
ℂ |
| 2 | | simpl 488 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 𝐴 ∈ ℂ) |
| 3 | | mulcl 11241 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 4 | 1, 2, 3 | sylancr 599 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ℂ) |
| 5 | 4 | recld 15314 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(i · 𝐴)) ∈ ℝ) |
| 6 | 5 | reefcld 16207 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(ℜ‘(i · 𝐴))) ∈
ℝ) |
| 7 | | neghalfpirx 26744 |
. . . . . . 7
⊢ -(π /
2) ∈ ℝ* |
| 8 | | halfpire 26742 |
. . . . . . . 8
⊢ (π /
2) ∈ ℝ |
| 9 | 8 | rexri 11324 |
. . . . . . 7
⊢ (π /
2) ∈ ℝ* |
| 10 | | elioo2 13472 |
. . . . . . 7
⊢ ((-(π
/ 2) ∈ ℝ* ∧ (π / 2) ∈ ℝ*)
→ ((ℜ‘𝐴)
∈ (-(π / 2)(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ -(π / 2) <
(ℜ‘𝐴) ∧
(ℜ‘𝐴) < (π
/ 2)))) |
| 11 | 7, 9, 10 | mp2an 705 |
. . . . . 6
⊢
((ℜ‘𝐴)
∈ (-(π / 2)(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ -(π / 2) <
(ℜ‘𝐴) ∧
(ℜ‘𝐴) < (π
/ 2))) |
| 12 | 11 | bilani 510 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((ℜ‘𝐴) ∈ ℝ ∧ -(π / 2) <
(ℜ‘𝐴) ∧
(ℜ‘𝐴) < (π
/ 2))) |
| 13 | 12 | simp1d 1160 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ∈ ℝ) |
| 14 | 13 | recoscld 16265 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘(ℜ‘𝐴)) ∈ ℝ) |
| 15 | | efgt0 16224 |
. . . 4
⊢
((ℜ‘(i · 𝐴)) ∈ ℝ → 0 <
(exp‘(ℜ‘(i · 𝐴)))) |
| 16 | 5, 15 | syl 18 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (exp‘(ℜ‘(i ·
𝐴)))) |
| 17 | | cosq14gt0 26788 |
. . . 4
⊢
((ℜ‘𝐴)
∈ (-(π / 2)(,)(π / 2)) → 0 < (cos‘(ℜ‘𝐴))) |
| 18 | 17 | adantl 487 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (cos‘(ℜ‘𝐴))) |
| 19 | 6, 14, 16, 18 | mulgt0d 11422 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < ((exp‘(ℜ‘(i ·
𝐴))) ·
(cos‘(ℜ‘𝐴)))) |
| 20 | | efeul 16283 |
. . . . 5
⊢ ((i
· 𝐴) ∈ ℂ
→ (exp‘(i · 𝐴)) = ((exp‘(ℜ‘(i ·
𝐴))) ·
((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴))))))) |
| 21 | 4, 20 | syl 18 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) = ((exp‘(ℜ‘(i ·
𝐴))) ·
((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴))))))) |
| 22 | 21 | fveq2d 6878 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(exp‘(i · 𝐴))) =
(ℜ‘((exp‘(ℜ‘(i · 𝐴))) · ((cos‘(ℑ‘(i
· 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴)))))))) |
| 23 | 4 | imcld 15315 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) ∈ ℝ) |
| 24 | 23 | recoscld 16265 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘(ℑ‘(i · 𝐴))) ∈
ℝ) |
| 25 | 24 | recnd 11294 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘(ℑ‘(i · 𝐴))) ∈
ℂ) |
| 26 | 23 | resincld 16264 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (sin‘(ℑ‘(i · 𝐴))) ∈
ℝ) |
| 27 | 26 | recnd 11294 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (sin‘(ℑ‘(i · 𝐴))) ∈
ℂ) |
| 28 | | mulcl 11241 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ (sin‘(ℑ‘(i · 𝐴))) ∈ ℂ) → (i ·
(sin‘(ℑ‘(i · 𝐴)))) ∈ ℂ) |
| 29 | 1, 27, 28 | sylancr 599 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (sin‘(ℑ‘(i
· 𝐴)))) ∈
ℂ) |
| 30 | 25, 29 | addcld 11285 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴))))) ∈ ℂ) |
| 31 | 6, 30 | remul2d 15347 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((exp‘(ℜ‘(i
· 𝐴))) ·
((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴))))))) = ((exp‘(ℜ‘(i
· 𝐴))) ·
(ℜ‘((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴)))))))) |
| 32 | 24, 26 | crred 15351 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((cos‘(ℑ‘(i
· 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴)))))) = (cos‘(ℑ‘(i
· 𝐴)))) |
| 33 | | imre 15228 |
. . . . . . . 8
⊢ ((i
· 𝐴) ∈ ℂ
→ (ℑ‘(i · 𝐴)) = (ℜ‘(-i · (i ·
𝐴)))) |
| 34 | 4, 33 | syl 18 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) = (ℜ‘(-i · (i ·
𝐴)))) |
| 35 | 1, 1 | mulneg1i 11717 |
. . . . . . . . . . 11
⊢ (-i
· i) = -(i · i) |
| 36 | | ixi 11900 |
. . . . . . . . . . . 12
⊢ (i
· i) = -1 |
| 37 | 36 | negeqi 11507 |
. . . . . . . . . . 11
⊢ -(i
· i) = --1 |
| 38 | | negneg1e1 12264 |
. . . . . . . . . . 11
⊢ --1 =
1 |
| 39 | 35, 37, 38 | 3eqtri 2787 |
. . . . . . . . . 10
⊢ (-i
· i) = 1 |
| 40 | 39 | oveq1i 7419 |
. . . . . . . . 9
⊢ ((-i
· i) · 𝐴) =
(1 · 𝐴) |
| 41 | | negicn 11515 |
. . . . . . . . . . 11
⊢ -i ∈
ℂ |
| 42 | 41 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -i ∈ ℂ) |
| 43 | 1 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → i ∈ ℂ) |
| 44 | 42, 43, 2 | mulassd 11289 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((-i · i) · 𝐴) = (-i · (i · 𝐴))) |
| 45 | | mullid 11264 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (1
· 𝐴) = 𝐴) |
| 46 | 45 | adantr 486 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 · 𝐴) = 𝐴) |
| 47 | 40, 44, 46 | 3eqtr3a 2819 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-i · (i · 𝐴)) = 𝐴) |
| 48 | 47 | fveq2d 6878 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(-i · (i · 𝐴))) = (ℜ‘𝐴)) |
| 49 | 34, 48 | eqtrd 2795 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) = (ℜ‘𝐴)) |
| 50 | 49 | fveq2d 6878 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘(ℑ‘(i · 𝐴))) =
(cos‘(ℜ‘𝐴))) |
| 51 | 32, 50 | eqtrd 2795 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((cos‘(ℑ‘(i
· 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴)))))) = (cos‘(ℜ‘𝐴))) |
| 52 | 51 | oveq2d 7425 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(ℜ‘(i · 𝐴))) ·
(ℜ‘((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴))))))) = ((exp‘(ℜ‘(i
· 𝐴))) ·
(cos‘(ℜ‘𝐴)))) |
| 53 | 22, 31, 52 | 3eqtrd 2799 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(exp‘(i · 𝐴))) =
((exp‘(ℜ‘(i · 𝐴))) · (cos‘(ℜ‘𝐴)))) |
| 54 | 19, 53 | breqtrrd 5133 |
1
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i ·
𝐴)))) |
