Proof of Theorem asinsinlem
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ax-icn 10930 |
. . . . . 6
⊢ i ∈
ℂ |
| 2 | | simpl 483 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 𝐴 ∈ ℂ) |
| 3 | | mulcl 10955 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 4 | 1, 2, 3 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ℂ) |
| 5 | 4 | recld 14905 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(i · 𝐴)) ∈ ℝ) |
| 6 | 5 | reefcld 15797 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(ℜ‘(i · 𝐴))) ∈
ℝ) |
| 7 | | simpr 485 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ∈ (-(π / 2)(,)(π /
2))) |
| 8 | | neghalfpirx 25623 |
. . . . . . 7
⊢ -(π /
2) ∈ ℝ* |
| 9 | | halfpire 25621 |
. . . . . . . 8
⊢ (π /
2) ∈ ℝ |
| 10 | 9 | rexri 11033 |
. . . . . . 7
⊢ (π /
2) ∈ ℝ* |
| 11 | | elioo2 13120 |
. . . . . . 7
⊢ ((-(π
/ 2) ∈ ℝ* ∧ (π / 2) ∈ ℝ*)
→ ((ℜ‘𝐴)
∈ (-(π / 2)(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ -(π / 2) <
(ℜ‘𝐴) ∧
(ℜ‘𝐴) < (π
/ 2)))) |
| 12 | 8, 10, 11 | mp2an 689 |
. . . . . 6
⊢
((ℜ‘𝐴)
∈ (-(π / 2)(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ -(π / 2) <
(ℜ‘𝐴) ∧
(ℜ‘𝐴) < (π
/ 2))) |
| 13 | 7, 12 | sylib 217 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((ℜ‘𝐴) ∈ ℝ ∧ -(π / 2) <
(ℜ‘𝐴) ∧
(ℜ‘𝐴) < (π
/ 2))) |
| 14 | 13 | simp1d 1141 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ∈ ℝ) |
| 15 | 14 | recoscld 15853 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘(ℜ‘𝐴)) ∈ ℝ) |
| 16 | | efgt0 15812 |
. . . 4
⊢
((ℜ‘(i · 𝐴)) ∈ ℝ → 0 <
(exp‘(ℜ‘(i · 𝐴)))) |
| 17 | 5, 16 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (exp‘(ℜ‘(i ·
𝐴)))) |
| 18 | | cosq14gt0 25667 |
. . . 4
⊢
((ℜ‘𝐴)
∈ (-(π / 2)(,)(π / 2)) → 0 < (cos‘(ℜ‘𝐴))) |
| 19 | 18 | adantl 482 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (cos‘(ℜ‘𝐴))) |
| 20 | 6, 15, 17, 19 | mulgt0d 11130 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < ((exp‘(ℜ‘(i ·
𝐴))) ·
(cos‘(ℜ‘𝐴)))) |
| 21 | | efeul 15871 |
. . . . 5
⊢ ((i
· 𝐴) ∈ ℂ
→ (exp‘(i · 𝐴)) = ((exp‘(ℜ‘(i ·
𝐴))) ·
((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴))))))) |
| 22 | 4, 21 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) = ((exp‘(ℜ‘(i ·
𝐴))) ·
((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴))))))) |
| 23 | 22 | fveq2d 6778 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(exp‘(i · 𝐴))) =
(ℜ‘((exp‘(ℜ‘(i · 𝐴))) · ((cos‘(ℑ‘(i
· 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴)))))))) |
| 24 | 4 | imcld 14906 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) ∈ ℝ) |
| 25 | 24 | recoscld 15853 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘(ℑ‘(i · 𝐴))) ∈
ℝ) |
| 26 | 25 | recnd 11003 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘(ℑ‘(i · 𝐴))) ∈
ℂ) |
| 27 | 24 | resincld 15852 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (sin‘(ℑ‘(i · 𝐴))) ∈
ℝ) |
| 28 | 27 | recnd 11003 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (sin‘(ℑ‘(i · 𝐴))) ∈
ℂ) |
| 29 | | mulcl 10955 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ (sin‘(ℑ‘(i · 𝐴))) ∈ ℂ) → (i ·
(sin‘(ℑ‘(i · 𝐴)))) ∈ ℂ) |
| 30 | 1, 28, 29 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (sin‘(ℑ‘(i
· 𝐴)))) ∈
ℂ) |
| 31 | 26, 30 | addcld 10994 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴))))) ∈ ℂ) |
| 32 | 6, 31 | remul2d 14938 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((exp‘(ℜ‘(i
· 𝐴))) ·
((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴))))))) = ((exp‘(ℜ‘(i
· 𝐴))) ·
(ℜ‘((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴)))))))) |
| 33 | 25, 27 | crred 14942 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((cos‘(ℑ‘(i
· 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴)))))) = (cos‘(ℑ‘(i
· 𝐴)))) |
| 34 | | imre 14819 |
. . . . . . . 8
⊢ ((i
· 𝐴) ∈ ℂ
→ (ℑ‘(i · 𝐴)) = (ℜ‘(-i · (i ·
𝐴)))) |
| 35 | 4, 34 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) = (ℜ‘(-i · (i ·
𝐴)))) |
| 36 | 1, 1 | mulneg1i 11421 |
. . . . . . . . . . 11
⊢ (-i
· i) = -(i · i) |
| 37 | | ixi 11604 |
. . . . . . . . . . . 12
⊢ (i
· i) = -1 |
| 38 | 37 | negeqi 11214 |
. . . . . . . . . . 11
⊢ -(i
· i) = --1 |
| 39 | | negneg1e1 12091 |
. . . . . . . . . . 11
⊢ --1 =
1 |
| 40 | 36, 38, 39 | 3eqtri 2770 |
. . . . . . . . . 10
⊢ (-i
· i) = 1 |
| 41 | 40 | oveq1i 7285 |
. . . . . . . . 9
⊢ ((-i
· i) · 𝐴) =
(1 · 𝐴) |
| 42 | | negicn 11222 |
. . . . . . . . . . 11
⊢ -i ∈
ℂ |
| 43 | 42 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -i ∈ ℂ) |
| 44 | 1 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → i ∈ ℂ) |
| 45 | 43, 44, 2 | mulassd 10998 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((-i · i) · 𝐴) = (-i · (i · 𝐴))) |
| 46 | | mulid2 10974 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (1
· 𝐴) = 𝐴) |
| 47 | 46 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 · 𝐴) = 𝐴) |
| 48 | 41, 45, 47 | 3eqtr3a 2802 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-i · (i · 𝐴)) = 𝐴) |
| 49 | 48 | fveq2d 6778 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(-i · (i · 𝐴))) = (ℜ‘𝐴)) |
| 50 | 35, 49 | eqtrd 2778 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) = (ℜ‘𝐴)) |
| 51 | 50 | fveq2d 6778 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘(ℑ‘(i · 𝐴))) =
(cos‘(ℜ‘𝐴))) |
| 52 | 33, 51 | eqtrd 2778 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((cos‘(ℑ‘(i
· 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴)))))) = (cos‘(ℜ‘𝐴))) |
| 53 | 52 | oveq2d 7291 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(ℜ‘(i · 𝐴))) ·
(ℜ‘((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴))))))) = ((exp‘(ℜ‘(i
· 𝐴))) ·
(cos‘(ℜ‘𝐴)))) |
| 54 | 23, 32, 53 | 3eqtrd 2782 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(exp‘(i · 𝐴))) =
((exp‘(ℜ‘(i · 𝐴))) · (cos‘(ℜ‘𝐴)))) |
| 55 | 20, 54 | breqtrrd 5102 |
1
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i ·
𝐴)))) |
