Step | Hyp | Ref
| Expression |
1 | | ax-icn 11169 |
. . 3
β’ i β
β |
2 | | sqrtcl 15308 |
. . . 4
β’ (π΄ β β β
(ββπ΄) β
β) |
3 | 2 | ad2antrr 725 |
. . 3
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β (ββπ΄)
β β) |
4 | | mulcl 11194 |
. . 3
β’ ((i
β β β§ (ββπ΄) β β) β (i Β·
(ββπ΄)) β
β) |
5 | 1, 3, 4 | sylancr 588 |
. 2
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β (i Β· (ββπ΄)) β β) |
6 | | imval 15054 |
. . . 4
β’ ((i
Β· (ββπ΄))
β β β (ββ(i Β· (ββπ΄))) = (ββ((i Β·
(ββπ΄)) /
i))) |
7 | 5, 6 | syl 17 |
. . 3
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β (ββ(i Β· (ββπ΄))) = (ββ((i Β·
(ββπ΄)) /
i))) |
8 | | ine0 11649 |
. . . . . 6
β’ i β
0 |
9 | | divcan3 11898 |
. . . . . 6
β’
(((ββπ΄)
β β β§ i β β β§ i β 0) β ((i Β·
(ββπ΄)) / i) =
(ββπ΄)) |
10 | 1, 8, 9 | mp3an23 1454 |
. . . . 5
β’
((ββπ΄)
β β β ((i Β· (ββπ΄)) / i) = (ββπ΄)) |
11 | 3, 10 | syl 17 |
. . . 4
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β ((i Β· (ββπ΄)) / i) = (ββπ΄)) |
12 | 11 | fveq2d 6896 |
. . 3
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β (ββ((i Β· (ββπ΄)) / i)) =
(ββ(ββπ΄))) |
13 | | halfre 12426 |
. . . . . . . . . . . . 13
β’ (1 / 2)
β β |
14 | 13 | recni 11228 |
. . . . . . . . . . . 12
β’ (1 / 2)
β β |
15 | | logcl 26077 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π΄ β 0) β (logβπ΄) β
β) |
16 | | mulcl 11194 |
. . . . . . . . . . . 12
β’ (((1 / 2)
β β β§ (logβπ΄) β β) β ((1 / 2) Β·
(logβπ΄)) β
β) |
17 | 14, 15, 16 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΄ β 0) β ((1 / 2)
Β· (logβπ΄))
β β) |
18 | 17 | recld 15141 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΄ β 0) β
(ββ((1 / 2) Β· (logβπ΄))) β β) |
19 | 18 | reefcld 16031 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΄ β 0) β
(expβ(ββ((1 / 2) Β· (logβπ΄)))) β β) |
20 | 17 | imcld 15142 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΄ β 0) β
(ββ((1 / 2) Β· (logβπ΄))) β β) |
21 | 20 | recoscld 16087 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΄ β 0) β
(cosβ(ββ((1 / 2) Β· (logβπ΄)))) β β) |
22 | 18 | rpefcld 16048 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΄ β 0) β
(expβ(ββ((1 / 2) Β· (logβπ΄)))) β
β+) |
23 | 22 | rpge0d 13020 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΄ β 0) β 0 β€
(expβ(ββ((1 / 2) Β· (logβπ΄))))) |
24 | | immul2 15084 |
. . . . . . . . . . . . 13
β’ (((1 / 2)
β β β§ (logβπ΄) β β) β (ββ((1
/ 2) Β· (logβπ΄))) = ((1 / 2) Β·
(ββ(logβπ΄)))) |
25 | 13, 15, 24 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π΄ β 0) β
(ββ((1 / 2) Β· (logβπ΄))) = ((1 / 2) Β·
(ββ(logβπ΄)))) |
26 | 15 | imcld 15142 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ π΄ β 0) β
(ββ(logβπ΄)) β β) |
27 | 26 | recnd 11242 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΄ β 0) β
(ββ(logβπ΄)) β β) |
28 | | mulcom 11196 |
. . . . . . . . . . . . 13
β’ (((1 / 2)
β β β§ (ββ(logβπ΄)) β β) β ((1 / 2) Β·
(ββ(logβπ΄))) = ((ββ(logβπ΄)) Β· (1 /
2))) |
29 | 14, 27, 28 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π΄ β 0) β ((1 / 2)
Β· (ββ(logβπ΄))) = ((ββ(logβπ΄)) Β· (1 /
2))) |
30 | 25, 29 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΄ β 0) β
(ββ((1 / 2) Β· (logβπ΄))) = ((ββ(logβπ΄)) Β· (1 /
2))) |
31 | | logimcl 26078 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β β§ π΄ β 0) β (-Ο <
(ββ(logβπ΄)) β§ (ββ(logβπ΄)) β€ Ο)) |
32 | 31 | simpld 496 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ π΄ β 0) β -Ο <
(ββ(logβπ΄))) |
33 | | pire 25968 |
. . . . . . . . . . . . . . . 16
β’ Ο
β β |
34 | 33 | renegcli 11521 |
. . . . . . . . . . . . . . 15
β’ -Ο
β β |
35 | | ltle 11302 |
. . . . . . . . . . . . . . 15
β’ ((-Ο
β β β§ (ββ(logβπ΄)) β β) β (-Ο <
(ββ(logβπ΄)) β -Ο β€
(ββ(logβπ΄)))) |
36 | 34, 26, 35 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ π΄ β 0) β (-Ο <
(ββ(logβπ΄)) β -Ο β€
(ββ(logβπ΄)))) |
37 | 32, 36 | mpd 15 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΄ β 0) β -Ο β€
(ββ(logβπ΄))) |
38 | 31 | simprd 497 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΄ β 0) β
(ββ(logβπ΄)) β€ Ο) |
39 | 34, 33 | elicc2i 13390 |
. . . . . . . . . . . . 13
β’
((ββ(logβπ΄)) β (-Ο[,]Ο) β
((ββ(logβπ΄)) β β β§ -Ο β€
(ββ(logβπ΄)) β§ (ββ(logβπ΄)) β€ Ο)) |
40 | 26, 37, 38, 39 | syl3anbrc 1344 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π΄ β 0) β
(ββ(logβπ΄)) β (-Ο[,]Ο)) |
41 | | halfgt0 12428 |
. . . . . . . . . . . . . 14
β’ 0 < (1
/ 2) |
42 | 13, 41 | elrpii 12977 |
. . . . . . . . . . . . 13
β’ (1 / 2)
β β+ |
43 | 33 | recni 11228 |
. . . . . . . . . . . . . . 15
β’ Ο
β β |
44 | | 2cn 12287 |
. . . . . . . . . . . . . . 15
β’ 2 β
β |
45 | | 2ne0 12316 |
. . . . . . . . . . . . . . 15
β’ 2 β
0 |
46 | | divneg 11906 |
. . . . . . . . . . . . . . 15
β’ ((Ο
β β β§ 2 β β β§ 2 β 0) β -(Ο / 2) =
(-Ο / 2)) |
47 | 43, 44, 45, 46 | mp3an 1462 |
. . . . . . . . . . . . . 14
β’ -(Ο /
2) = (-Ο / 2) |
48 | 34 | recni 11228 |
. . . . . . . . . . . . . . 15
β’ -Ο
β β |
49 | 48, 44, 45 | divreci 11959 |
. . . . . . . . . . . . . 14
β’ (-Ο /
2) = (-Ο Β· (1 / 2)) |
50 | 47, 49 | eqtr2i 2762 |
. . . . . . . . . . . . 13
β’ (-Ο
Β· (1 / 2)) = -(Ο / 2) |
51 | 43, 44, 45 | divreci 11959 |
. . . . . . . . . . . . . 14
β’ (Ο /
2) = (Ο Β· (1 / 2)) |
52 | 51 | eqcomi 2742 |
. . . . . . . . . . . . 13
β’ (Ο
Β· (1 / 2)) = (Ο / 2) |
53 | 34, 33, 42, 50, 52 | iccdili 13468 |
. . . . . . . . . . . 12
β’
((ββ(logβπ΄)) β (-Ο[,]Ο) β
((ββ(logβπ΄)) Β· (1 / 2)) β (-(Ο /
2)[,](Ο / 2))) |
54 | 40, 53 | syl 17 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΄ β 0) β
((ββ(logβπ΄)) Β· (1 / 2)) β (-(Ο /
2)[,](Ο / 2))) |
55 | 30, 54 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΄ β 0) β
(ββ((1 / 2) Β· (logβπ΄))) β (-(Ο / 2)[,](Ο /
2))) |
56 | | cosq14ge0 26021 |
. . . . . . . . . 10
β’
((ββ((1 / 2) Β· (logβπ΄))) β (-(Ο / 2)[,](Ο / 2)) β
0 β€ (cosβ(ββ((1 / 2) Β· (logβπ΄))))) |
57 | 55, 56 | syl 17 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΄ β 0) β 0 β€
(cosβ(ββ((1 / 2) Β· (logβπ΄))))) |
58 | 19, 21, 23, 57 | mulge0d 11791 |
. . . . . . . 8
β’ ((π΄ β β β§ π΄ β 0) β 0 β€
((expβ(ββ((1 / 2) Β· (logβπ΄)))) Β· (cosβ(ββ((1
/ 2) Β· (logβπ΄)))))) |
59 | | cxpef 26173 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π΄ β 0 β§ (1 / 2) β
β) β (π΄βπ(1 / 2)) =
(expβ((1 / 2) Β· (logβπ΄)))) |
60 | 14, 59 | mp3an3 1451 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΄ β 0) β (π΄βπ(1 /
2)) = (expβ((1 / 2) Β· (logβπ΄)))) |
61 | | efeul 16105 |
. . . . . . . . . . . 12
β’ (((1 / 2)
Β· (logβπ΄))
β β β (expβ((1 / 2) Β· (logβπ΄))) = ((expβ(ββ((1 / 2)
Β· (logβπ΄))))
Β· ((cosβ(ββ((1 / 2) Β· (logβπ΄)))) + (i Β·
(sinβ(ββ((1 / 2) Β· (logβπ΄)))))))) |
62 | 17, 61 | syl 17 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΄ β 0) β (expβ((1 /
2) Β· (logβπ΄)))
= ((expβ(ββ((1 / 2) Β· (logβπ΄)))) Β· ((cosβ(ββ((1
/ 2) Β· (logβπ΄)))) + (i Β·
(sinβ(ββ((1 / 2) Β· (logβπ΄)))))))) |
63 | 60, 62 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΄ β 0) β (π΄βπ(1 /
2)) = ((expβ(ββ((1 / 2) Β· (logβπ΄)))) Β· ((cosβ(ββ((1
/ 2) Β· (logβπ΄)))) + (i Β·
(sinβ(ββ((1 / 2) Β· (logβπ΄)))))))) |
64 | 63 | fveq2d 6896 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΄ β 0) β
(ββ(π΄βπ(1 / 2))) =
(ββ((expβ(ββ((1 / 2) Β· (logβπ΄)))) Β·
((cosβ(ββ((1 / 2) Β· (logβπ΄)))) + (i Β·
(sinβ(ββ((1 / 2) Β· (logβπ΄))))))))) |
65 | 21 | recnd 11242 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΄ β 0) β
(cosβ(ββ((1 / 2) Β· (logβπ΄)))) β β) |
66 | 20 | resincld 16086 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΄ β 0) β
(sinβ(ββ((1 / 2) Β· (logβπ΄)))) β β) |
67 | 66 | recnd 11242 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π΄ β 0) β
(sinβ(ββ((1 / 2) Β· (logβπ΄)))) β β) |
68 | | mulcl 11194 |
. . . . . . . . . . . 12
β’ ((i
β β β§ (sinβ(ββ((1 / 2) Β·
(logβπ΄)))) β
β) β (i Β· (sinβ(ββ((1 / 2) Β·
(logβπ΄))))) β
β) |
69 | 1, 67, 68 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΄ β 0) β (i Β·
(sinβ(ββ((1 / 2) Β· (logβπ΄))))) β β) |
70 | 65, 69 | addcld 11233 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΄ β 0) β
((cosβ(ββ((1 / 2) Β· (logβπ΄)))) + (i Β·
(sinβ(ββ((1 / 2) Β· (logβπ΄)))))) β β) |
71 | 19, 70 | remul2d 15174 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΄ β 0) β
(ββ((expβ(ββ((1 / 2) Β· (logβπ΄)))) Β·
((cosβ(ββ((1 / 2) Β· (logβπ΄)))) + (i Β·
(sinβ(ββ((1 / 2) Β· (logβπ΄)))))))) = ((expβ(ββ((1 /
2) Β· (logβπ΄)))) Β·
(ββ((cosβ(ββ((1 / 2) Β· (logβπ΄)))) + (i Β·
(sinβ(ββ((1 / 2) Β· (logβπ΄))))))))) |
72 | 21, 66 | crred 15178 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΄ β 0) β
(ββ((cosβ(ββ((1 / 2) Β· (logβπ΄)))) + (i Β·
(sinβ(ββ((1 / 2) Β· (logβπ΄))))))) = (cosβ(ββ((1 / 2)
Β· (logβπ΄))))) |
73 | 72 | oveq2d 7425 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΄ β 0) β
((expβ(ββ((1 / 2) Β· (logβπ΄)))) Β·
(ββ((cosβ(ββ((1 / 2) Β· (logβπ΄)))) + (i Β·
(sinβ(ββ((1 / 2) Β· (logβπ΄)))))))) = ((expβ(ββ((1 /
2) Β· (logβπ΄)))) Β· (cosβ(ββ((1
/ 2) Β· (logβπ΄)))))) |
74 | 64, 71, 73 | 3eqtrd 2777 |
. . . . . . . 8
β’ ((π΄ β β β§ π΄ β 0) β
(ββ(π΄βπ(1 / 2))) =
((expβ(ββ((1 / 2) Β· (logβπ΄)))) Β· (cosβ(ββ((1
/ 2) Β· (logβπ΄)))))) |
75 | 58, 74 | breqtrrd 5177 |
. . . . . . 7
β’ ((π΄ β β β§ π΄ β 0) β 0 β€
(ββ(π΄βπ(1 /
2)))) |
76 | 75 | adantr 482 |
. . . . . 6
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β 0 β€ (ββ(π΄βπ(1 /
2)))) |
77 | | simpr 486 |
. . . . . . . 8
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β (π΄βπ(1 / 2)) =
-(ββπ΄)) |
78 | 77 | fveq2d 6896 |
. . . . . . 7
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β (ββ(π΄βπ(1 / 2))) =
(ββ-(ββπ΄))) |
79 | 3 | renegd 15156 |
. . . . . . 7
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β (ββ-(ββπ΄)) = -(ββ(ββπ΄))) |
80 | 78, 79 | eqtrd 2773 |
. . . . . 6
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β (ββ(π΄βπ(1 / 2))) =
-(ββ(ββπ΄))) |
81 | 76, 80 | breqtrd 5175 |
. . . . 5
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β 0 β€ -(ββ(ββπ΄))) |
82 | 3 | recld 15141 |
. . . . . 6
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β (ββ(ββπ΄)) β β) |
83 | 82 | le0neg1d 11785 |
. . . . 5
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β ((ββ(ββπ΄)) β€ 0 β 0 β€
-(ββ(ββπ΄)))) |
84 | 81, 83 | mpbird 257 |
. . . 4
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β (ββ(ββπ΄)) β€ 0) |
85 | | sqrtrege0 15312 |
. . . . 5
β’ (π΄ β β β 0 β€
(ββ(ββπ΄))) |
86 | 85 | ad2antrr 725 |
. . . 4
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β 0 β€ (ββ(ββπ΄))) |
87 | | 0re 11216 |
. . . . 5
β’ 0 β
β |
88 | | letri3 11299 |
. . . . 5
β’
(((ββ(ββπ΄)) β β β§ 0 β β)
β ((ββ(ββπ΄)) = 0 β
((ββ(ββπ΄)) β€ 0 β§ 0 β€
(ββ(ββπ΄))))) |
89 | 82, 87, 88 | sylancl 587 |
. . . 4
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β ((ββ(ββπ΄)) = 0 β
((ββ(ββπ΄)) β€ 0 β§ 0 β€
(ββ(ββπ΄))))) |
90 | 84, 86, 89 | mpbir2and 712 |
. . 3
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β (ββ(ββπ΄)) = 0) |
91 | 7, 12, 90 | 3eqtrd 2777 |
. 2
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β (ββ(i Β· (ββπ΄))) = 0) |
92 | 5, 91 | reim0bd 15147 |
1
β’ (((π΄ β β β§ π΄ β 0) β§ (π΄βπ(1 /
2)) = -(ββπ΄))
β (i Β· (ββπ΄)) β β) |