Proof of Theorem asinsinlem
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ax-icn 11214 |
. . . . . 6
⊢ i ∈
ℂ |
| 2 | | simpl 482 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 𝐴 ∈ ℂ) |
| 3 | | mulcl 11239 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 4 | 1, 2, 3 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ℂ) |
| 5 | 4 | recld 15233 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(i · 𝐴)) ∈ ℝ) |
| 6 | 5 | reefcld 16124 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(ℜ‘(i · 𝐴))) ∈
ℝ) |
| 7 | | simpr 484 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ∈ (-(π / 2)(,)(π /
2))) |
| 8 | | neghalfpirx 26508 |
. . . . . . 7
⊢ -(π /
2) ∈ ℝ* |
| 9 | | halfpire 26506 |
. . . . . . . 8
⊢ (π /
2) ∈ ℝ |
| 10 | 9 | rexri 11319 |
. . . . . . 7
⊢ (π /
2) ∈ ℝ* |
| 11 | | elioo2 13428 |
. . . . . . 7
⊢ ((-(π
/ 2) ∈ ℝ* ∧ (π / 2) ∈ ℝ*)
→ ((ℜ‘𝐴)
∈ (-(π / 2)(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ -(π / 2) <
(ℜ‘𝐴) ∧
(ℜ‘𝐴) < (π
/ 2)))) |
| 12 | 8, 10, 11 | mp2an 692 |
. . . . . 6
⊢
((ℜ‘𝐴)
∈ (-(π / 2)(,)(π / 2)) ↔ ((ℜ‘𝐴) ∈ ℝ ∧ -(π / 2) <
(ℜ‘𝐴) ∧
(ℜ‘𝐴) < (π
/ 2))) |
| 13 | 7, 12 | sylib 218 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((ℜ‘𝐴) ∈ ℝ ∧ -(π / 2) <
(ℜ‘𝐴) ∧
(ℜ‘𝐴) < (π
/ 2))) |
| 14 | 13 | simp1d 1143 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ∈ ℝ) |
| 15 | 14 | recoscld 16180 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘(ℜ‘𝐴)) ∈ ℝ) |
| 16 | | efgt0 16139 |
. . . 4
⊢
((ℜ‘(i · 𝐴)) ∈ ℝ → 0 <
(exp‘(ℜ‘(i · 𝐴)))) |
| 17 | 5, 16 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (exp‘(ℜ‘(i ·
𝐴)))) |
| 18 | | cosq14gt0 26552 |
. . . 4
⊢
((ℜ‘𝐴)
∈ (-(π / 2)(,)(π / 2)) → 0 < (cos‘(ℜ‘𝐴))) |
| 19 | 18 | adantl 481 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (cos‘(ℜ‘𝐴))) |
| 20 | 6, 15, 17, 19 | mulgt0d 11416 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < ((exp‘(ℜ‘(i ·
𝐴))) ·
(cos‘(ℜ‘𝐴)))) |
| 21 | | efeul 16198 |
. . . . 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 6910 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(exp‘(i · 𝐴))) =
(ℜ‘((exp‘(ℜ‘(i · 𝐴))) · ((cos‘(ℑ‘(i
· 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴)))))))) |
| 24 | 4 | imcld 15234 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) ∈ ℝ) |
| 25 | 24 | recoscld 16180 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘(ℑ‘(i · 𝐴))) ∈
ℝ) |
| 26 | 25 | recnd 11289 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘(ℑ‘(i · 𝐴))) ∈
ℂ) |
| 27 | 24 | resincld 16179 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (sin‘(ℑ‘(i · 𝐴))) ∈
ℝ) |
| 28 | 27 | recnd 11289 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (sin‘(ℑ‘(i · 𝐴))) ∈
ℂ) |
| 29 | | mulcl 11239 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ (sin‘(ℑ‘(i · 𝐴))) ∈ ℂ) → (i ·
(sin‘(ℑ‘(i · 𝐴)))) ∈ ℂ) |
| 30 | 1, 28, 29 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (sin‘(ℑ‘(i
· 𝐴)))) ∈
ℂ) |
| 31 | 26, 30 | addcld 11280 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴))))) ∈ ℂ) |
| 32 | 6, 31 | remul2d 15266 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((exp‘(ℜ‘(i
· 𝐴))) ·
((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴))))))) = ((exp‘(ℜ‘(i
· 𝐴))) ·
(ℜ‘((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴)))))))) |
| 33 | 25, 27 | crred 15270 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((cos‘(ℑ‘(i
· 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴)))))) = (cos‘(ℑ‘(i
· 𝐴)))) |
| 34 | | imre 15147 |
. . . . . . . 8
⊢ ((i
· 𝐴) ∈ ℂ
→ (ℑ‘(i · 𝐴)) = (ℜ‘(-i · (i ·
𝐴)))) |
| 35 | 4, 34 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) = (ℜ‘(-i · (i ·
𝐴)))) |
| 36 | 1, 1 | mulneg1i 11709 |
. . . . . . . . . . 11
⊢ (-i
· i) = -(i · i) |
| 37 | | ixi 11892 |
. . . . . . . . . . . 12
⊢ (i
· i) = -1 |
| 38 | 37 | negeqi 11501 |
. . . . . . . . . . 11
⊢ -(i
· i) = --1 |
| 39 | | negneg1e1 12384 |
. . . . . . . . . . 11
⊢ --1 =
1 |
| 40 | 36, 38, 39 | 3eqtri 2769 |
. . . . . . . . . 10
⊢ (-i
· i) = 1 |
| 41 | 40 | oveq1i 7441 |
. . . . . . . . 9
⊢ ((-i
· i) · 𝐴) =
(1 · 𝐴) |
| 42 | | negicn 11509 |
. . . . . . . . . . 11
⊢ -i ∈
ℂ |
| 43 | 42 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -i ∈ ℂ) |
| 44 | 1 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → i ∈ ℂ) |
| 45 | 43, 44, 2 | mulassd 11284 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((-i · i) · 𝐴) = (-i · (i · 𝐴))) |
| 46 | | mullid 11260 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (1
· 𝐴) = 𝐴) |
| 47 | 46 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 · 𝐴) = 𝐴) |
| 48 | 41, 45, 47 | 3eqtr3a 2801 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-i · (i · 𝐴)) = 𝐴) |
| 49 | 48 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(-i · (i · 𝐴))) = (ℜ‘𝐴)) |
| 50 | 35, 49 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) = (ℜ‘𝐴)) |
| 51 | 50 | fveq2d 6910 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘(ℑ‘(i · 𝐴))) =
(cos‘(ℜ‘𝐴))) |
| 52 | 33, 51 | eqtrd 2777 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((cos‘(ℑ‘(i
· 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴)))))) = (cos‘(ℜ‘𝐴))) |
| 53 | 52 | oveq2d 7447 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(ℜ‘(i · 𝐴))) ·
(ℜ‘((cos‘(ℑ‘(i · 𝐴))) + (i ·
(sin‘(ℑ‘(i · 𝐴))))))) = ((exp‘(ℜ‘(i
· 𝐴))) ·
(cos‘(ℜ‘𝐴)))) |
| 54 | 23, 32, 53 | 3eqtrd 2781 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(exp‘(i · 𝐴))) =
((exp‘(ℜ‘(i · 𝐴))) · (cos‘(ℜ‘𝐴)))) |
| 55 | 20, 54 | breqtrrd 5171 |
1
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i ·
𝐴)))) |
