Step | Hyp | Ref
| Expression |
1 | | ax-icn 11168 |
. . . . . . . . . 10
β’ i β
β |
2 | | mulcl 11193 |
. . . . . . . . . 10
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
3 | 1, 2 | mpan 688 |
. . . . . . . . 9
β’ (π΄ β β β (i
Β· π΄) β
β) |
4 | | ax-1cn 11167 |
. . . . . . . . . . 11
β’ 1 β
β |
5 | | sqcl 14082 |
. . . . . . . . . . 11
β’ (π΄ β β β (π΄β2) β
β) |
6 | | subcl 11458 |
. . . . . . . . . . 11
β’ ((1
β β β§ (π΄β2) β β) β (1 β
(π΄β2)) β
β) |
7 | 4, 5, 6 | sylancr 587 |
. . . . . . . . . 10
β’ (π΄ β β β (1
β (π΄β2)) β
β) |
8 | 7 | sqrtcld 15383 |
. . . . . . . . 9
β’ (π΄ β β β
(ββ(1 β (π΄β2))) β β) |
9 | 3, 8 | addcld 11232 |
. . . . . . . 8
β’ (π΄ β β β ((i
Β· π΄) +
(ββ(1 β (π΄β2)))) β β) |
10 | | asinlem 26370 |
. . . . . . . 8
β’ (π΄ β β β ((i
Β· π΄) +
(ββ(1 β (π΄β2)))) β 0) |
11 | 9, 10 | logcld 26078 |
. . . . . . 7
β’ (π΄ β β β
(logβ((i Β· π΄)
+ (ββ(1 β (π΄β2))))) β
β) |
12 | | efneg 16040 |
. . . . . . 7
β’
((logβ((i Β· π΄) + (ββ(1 β (π΄β2))))) β β
β (expβ-(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) = (1 /
(expβ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))))) |
13 | 11, 12 | syl 17 |
. . . . . 6
β’ (π΄ β β β
(expβ-(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) = (1 /
(expβ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))))) |
14 | | eflog 26084 |
. . . . . . . 8
β’ ((((i
Β· π΄) +
(ββ(1 β (π΄β2)))) β β β§ ((i
Β· π΄) +
(ββ(1 β (π΄β2)))) β 0) β
(expβ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) = ((i Β·
π΄) + (ββ(1
β (π΄β2))))) |
15 | 9, 10, 14 | syl2anc 584 |
. . . . . . 7
β’ (π΄ β β β
(expβ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) = ((i Β·
π΄) + (ββ(1
β (π΄β2))))) |
16 | 15 | oveq2d 7424 |
. . . . . 6
β’ (π΄ β β β (1 /
(expβ(logβ((i Β· π΄) + (ββ(1 β (π΄β2))))))) = (1 / ((i
Β· π΄) +
(ββ(1 β (π΄β2)))))) |
17 | | asinlem2 26371 |
. . . . . . 7
β’ (π΄ β β β (((i
Β· π΄) +
(ββ(1 β (π΄β2)))) Β· ((i Β· -π΄) + (ββ(1 β
(-π΄β2))))) =
1) |
18 | 4 | a1i 11 |
. . . . . . . 8
β’ (π΄ β β β 1 β
β) |
19 | | negcl 11459 |
. . . . . . . . . 10
β’ (π΄ β β β -π΄ β
β) |
20 | | mulcl 11193 |
. . . . . . . . . 10
β’ ((i
β β β§ -π΄
β β) β (i Β· -π΄) β β) |
21 | 1, 19, 20 | sylancr 587 |
. . . . . . . . 9
β’ (π΄ β β β (i
Β· -π΄) β
β) |
22 | 19 | sqcld 14108 |
. . . . . . . . . . 11
β’ (π΄ β β β (-π΄β2) β
β) |
23 | | subcl 11458 |
. . . . . . . . . . 11
β’ ((1
β β β§ (-π΄β2) β β) β (1 β
(-π΄β2)) β
β) |
24 | 4, 22, 23 | sylancr 587 |
. . . . . . . . . 10
β’ (π΄ β β β (1
β (-π΄β2)) β
β) |
25 | 24 | sqrtcld 15383 |
. . . . . . . . 9
β’ (π΄ β β β
(ββ(1 β (-π΄β2))) β β) |
26 | 21, 25 | addcld 11232 |
. . . . . . . 8
β’ (π΄ β β β ((i
Β· -π΄) +
(ββ(1 β (-π΄β2)))) β β) |
27 | 18, 9, 26, 10 | divmuld 12011 |
. . . . . . 7
β’ (π΄ β β β ((1 / ((i
Β· π΄) +
(ββ(1 β (π΄β2))))) = ((i Β· -π΄) + (ββ(1 β
(-π΄β2)))) β (((i
Β· π΄) +
(ββ(1 β (π΄β2)))) Β· ((i Β· -π΄) + (ββ(1 β
(-π΄β2))))) =
1)) |
28 | 17, 27 | mpbird 256 |
. . . . . 6
β’ (π΄ β β β (1 / ((i
Β· π΄) +
(ββ(1 β (π΄β2))))) = ((i Β· -π΄) + (ββ(1 β
(-π΄β2))))) |
29 | 13, 16, 28 | 3eqtrd 2776 |
. . . . 5
β’ (π΄ β β β
(expβ-(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) = ((i Β·
-π΄) + (ββ(1
β (-π΄β2))))) |
30 | | asinlem 26370 |
. . . . . . 7
β’ (-π΄ β β β ((i
Β· -π΄) +
(ββ(1 β (-π΄β2)))) β 0) |
31 | 19, 30 | syl 17 |
. . . . . 6
β’ (π΄ β β β ((i
Β· -π΄) +
(ββ(1 β (-π΄β2)))) β 0) |
32 | 11 | negcld 11557 |
. . . . . . . 8
β’ (π΄ β β β
-(logβ((i Β· π΄)
+ (ββ(1 β (π΄β2))))) β
β) |
33 | 11 | imnegd 15156 |
. . . . . . . . 9
β’ (π΄ β β β
(ββ-(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) =
-(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2))))))) |
34 | 11 | imcld 15141 |
. . . . . . . . . . 11
β’ (π΄ β β β
(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β
β) |
35 | 34 | renegcld 11640 |
. . . . . . . . . 10
β’ (π΄ β β β
-(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β
β) |
36 | | pire 25967 |
. . . . . . . . . . . . 13
β’ Ο
β β |
37 | 36 | a1i 11 |
. . . . . . . . . . . 12
β’ (π΄ β β β Ο
β β) |
38 | 9, 10 | logimcld 26079 |
. . . . . . . . . . . . 13
β’ (π΄ β β β (-Ο
< (ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β§
(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β€
Ο)) |
39 | 38 | simprd 496 |
. . . . . . . . . . . 12
β’ (π΄ β β β
(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β€
Ο) |
40 | 9 | renegd 15155 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β
(ββ-((i Β· π΄) + (ββ(1 β (π΄β2))))) =
-(ββ((i Β· π΄) + (ββ(1 β (π΄β2)))))) |
41 | | asinlem3 26373 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β 0 β€
(ββ((i Β· π΄) + (ββ(1 β (π΄β2)))))) |
42 | 9 | recld 15140 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β β β
(ββ((i Β· π΄) + (ββ(1 β (π΄β2))))) β
β) |
43 | 42 | le0neg2d 11785 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β (0 β€
(ββ((i Β· π΄) + (ββ(1 β (π΄β2))))) β
-(ββ((i Β· π΄) + (ββ(1 β (π΄β2))))) β€
0)) |
44 | 41, 43 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β
-(ββ((i Β· π΄) + (ββ(1 β (π΄β2))))) β€
0) |
45 | 40, 44 | eqbrtrd 5170 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
(ββ-((i Β· π΄) + (ββ(1 β (π΄β2))))) β€
0) |
46 | 9 | negcld 11557 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β β β -((i
Β· π΄) +
(ββ(1 β (π΄β2)))) β β) |
47 | 46 | recld 15140 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β
(ββ-((i Β· π΄) + (ββ(1 β (π΄β2))))) β
β) |
48 | | 0re 11215 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β |
49 | | lenlt 11291 |
. . . . . . . . . . . . . . . 16
β’
(((ββ-((i Β· π΄) + (ββ(1 β (π΄β2))))) β β
β§ 0 β β) β ((ββ-((i Β· π΄) + (ββ(1 β (π΄β2))))) β€ 0 β Β¬
0 < (ββ-((i Β· π΄) + (ββ(1 β (π΄β2))))))) |
50 | 47, 48, 49 | sylancl 586 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
((ββ-((i Β· π΄) + (ββ(1 β (π΄β2))))) β€ 0 β Β¬
0 < (ββ-((i Β· π΄) + (ββ(1 β (π΄β2))))))) |
51 | 45, 50 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β Β¬ 0
< (ββ-((i Β· π΄) + (ββ(1 β (π΄β2)))))) |
52 | | lognegb 26097 |
. . . . . . . . . . . . . . . . 17
β’ ((((i
Β· π΄) +
(ββ(1 β (π΄β2)))) β β β§ ((i
Β· π΄) +
(ββ(1 β (π΄β2)))) β 0) β (-((i Β·
π΄) + (ββ(1
β (π΄β2))))
β β+ β (ββ(logβ((i Β· π΄) + (ββ(1 β
(π΄β2)))))) =
Ο)) |
53 | 9, 10, 52 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β β β (-((i
Β· π΄) +
(ββ(1 β (π΄β2)))) β β+
β (ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) =
Ο)) |
54 | | rpgt0 12985 |
. . . . . . . . . . . . . . . . 17
β’ (-((i
Β· π΄) +
(ββ(1 β (π΄β2)))) β β+
β 0 < -((i Β· π΄) + (ββ(1 β (π΄β2))))) |
55 | | rpre 12981 |
. . . . . . . . . . . . . . . . . 18
β’ (-((i
Β· π΄) +
(ββ(1 β (π΄β2)))) β β+
β -((i Β· π΄) +
(ββ(1 β (π΄β2)))) β β) |
56 | 55 | rered 15170 |
. . . . . . . . . . . . . . . . 17
β’ (-((i
Β· π΄) +
(ββ(1 β (π΄β2)))) β β+
β (ββ-((i Β· π΄) + (ββ(1 β (π΄β2))))) = -((i Β·
π΄) + (ββ(1
β (π΄β2))))) |
57 | 54, 56 | breqtrrd 5176 |
. . . . . . . . . . . . . . . 16
β’ (-((i
Β· π΄) +
(ββ(1 β (π΄β2)))) β β+
β 0 < (ββ-((i Β· π΄) + (ββ(1 β (π΄β2)))))) |
58 | 53, 57 | syl6bir 253 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β
((ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) = Ο β 0
< (ββ-((i Β· π΄) + (ββ(1 β (π΄β2))))))) |
59 | 58 | necon3bd 2954 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β (Β¬ 0
< (ββ-((i Β· π΄) + (ββ(1 β (π΄β2))))) β
(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β
Ο)) |
60 | 51, 59 | mpd 15 |
. . . . . . . . . . . . 13
β’ (π΄ β β β
(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β
Ο) |
61 | 60 | necomd 2996 |
. . . . . . . . . . . 12
β’ (π΄ β β β Ο β
(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2))))))) |
62 | 34, 37, 39, 61 | leneltd 11367 |
. . . . . . . . . . 11
β’ (π΄ β β β
(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) <
Ο) |
63 | | ltneg 11713 |
. . . . . . . . . . . 12
β’
(((ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β β
β§ Ο β β) β ((ββ(logβ((i Β· π΄) + (ββ(1 β
(π΄β2)))))) < Ο
β -Ο < -(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))))) |
64 | 34, 36, 63 | sylancl 586 |
. . . . . . . . . . 11
β’ (π΄ β β β
((ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) < Ο β
-Ο < -(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))))) |
65 | 62, 64 | mpbid 231 |
. . . . . . . . . 10
β’ (π΄ β β β -Ο
< -(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2))))))) |
66 | 38 | simpld 495 |
. . . . . . . . . . . 12
β’ (π΄ β β β -Ο
< (ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2))))))) |
67 | 36 | renegcli 11520 |
. . . . . . . . . . . . 13
β’ -Ο
β β |
68 | | ltle 11301 |
. . . . . . . . . . . . 13
β’ ((-Ο
β β β§ (ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β β)
β (-Ο < (ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β -Ο β€
(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))))) |
69 | 67, 34, 68 | sylancr 587 |
. . . . . . . . . . . 12
β’ (π΄ β β β (-Ο
< (ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β -Ο β€
(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))))) |
70 | 66, 69 | mpd 15 |
. . . . . . . . . . 11
β’ (π΄ β β β -Ο
β€ (ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2))))))) |
71 | | lenegcon1 11717 |
. . . . . . . . . . . 12
β’ ((Ο
β β β§ (ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β β)
β (-Ο β€ (ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β
-(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β€
Ο)) |
72 | 36, 34, 71 | sylancr 587 |
. . . . . . . . . . 11
β’ (π΄ β β β (-Ο
β€ (ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β
-(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β€
Ο)) |
73 | 70, 72 | mpbid 231 |
. . . . . . . . . 10
β’ (π΄ β β β
-(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β€
Ο) |
74 | 67 | rexri 11271 |
. . . . . . . . . . 11
β’ -Ο
β β* |
75 | | elioc2 13386 |
. . . . . . . . . . 11
β’ ((-Ο
β β* β§ Ο β β) β
(-(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β
(-Ο(,]Ο) β (-(ββ(logβ((i Β· π΄) + (ββ(1 β
(π΄β2)))))) β
β β§ -Ο < -(ββ(logβ((i Β· π΄) + (ββ(1 β
(π΄β2)))))) β§
-(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β€
Ο))) |
76 | 74, 36, 75 | mp2an 690 |
. . . . . . . . . 10
β’
(-(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β
(-Ο(,]Ο) β (-(ββ(logβ((i Β· π΄) + (ββ(1 β
(π΄β2)))))) β
β β§ -Ο < -(ββ(logβ((i Β· π΄) + (ββ(1 β
(π΄β2)))))) β§
-(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β€
Ο)) |
77 | 35, 65, 73, 76 | syl3anbrc 1343 |
. . . . . . . . 9
β’ (π΄ β β β
-(ββ(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β
(-Ο(,]Ο)) |
78 | 33, 77 | eqeltrd 2833 |
. . . . . . . 8
β’ (π΄ β β β
(ββ-(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β
(-Ο(,]Ο)) |
79 | | imf 15059 |
. . . . . . . . 9
β’
β:ββΆβ |
80 | | ffn 6717 |
. . . . . . . . 9
β’
(β:ββΆβ β β Fn
β) |
81 | | elpreima 7059 |
. . . . . . . . 9
β’ (β
Fn β β (-(logβ((i Β· π΄) + (ββ(1 β (π΄β2))))) β (β‘β β (-Ο(,]Ο)) β
(-(logβ((i Β· π΄) + (ββ(1 β (π΄β2))))) β β
β§ (ββ-(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β
(-Ο(,]Ο)))) |
82 | 79, 80, 81 | mp2b 10 |
. . . . . . . 8
β’
(-(logβ((i Β· π΄) + (ββ(1 β (π΄β2))))) β (β‘β β (-Ο(,]Ο)) β
(-(logβ((i Β· π΄) + (ββ(1 β (π΄β2))))) β β
β§ (ββ-(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) β
(-Ο(,]Ο))) |
83 | 32, 78, 82 | sylanbrc 583 |
. . . . . . 7
β’ (π΄ β β β
-(logβ((i Β· π΄)
+ (ββ(1 β (π΄β2))))) β (β‘β β
(-Ο(,]Ο))) |
84 | | logrn 26066 |
. . . . . . 7
β’ ran log =
(β‘β β
(-Ο(,]Ο)) |
85 | 83, 84 | eleqtrrdi 2844 |
. . . . . 6
β’ (π΄ β β β
-(logβ((i Β· π΄)
+ (ββ(1 β (π΄β2))))) β ran
log) |
86 | | logeftb 26091 |
. . . . . 6
β’ ((((i
Β· -π΄) +
(ββ(1 β (-π΄β2)))) β β β§ ((i
Β· -π΄) +
(ββ(1 β (-π΄β2)))) β 0 β§ -(logβ((i
Β· π΄) +
(ββ(1 β (π΄β2))))) β ran log) β
((logβ((i Β· -π΄) + (ββ(1 β (-π΄β2))))) = -(logβ((i
Β· π΄) +
(ββ(1 β (π΄β2))))) β
(expβ-(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) = ((i Β·
-π΄) + (ββ(1
β (-π΄β2)))))) |
87 | 26, 31, 85, 86 | syl3anc 1371 |
. . . . 5
β’ (π΄ β β β
((logβ((i Β· -π΄) + (ββ(1 β (-π΄β2))))) = -(logβ((i
Β· π΄) +
(ββ(1 β (π΄β2))))) β
(expβ-(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) = ((i Β·
-π΄) + (ββ(1
β (-π΄β2)))))) |
88 | 29, 87 | mpbird 256 |
. . . 4
β’ (π΄ β β β
(logβ((i Β· -π΄)
+ (ββ(1 β (-π΄β2))))) = -(logβ((i Β·
π΄) + (ββ(1
β (π΄β2)))))) |
89 | 88 | oveq2d 7424 |
. . 3
β’ (π΄ β β β (-i
Β· (logβ((i Β· -π΄) + (ββ(1 β (-π΄β2)))))) = (-i Β·
-(logβ((i Β· π΄)
+ (ββ(1 β (π΄β2))))))) |
90 | | negicn 11460 |
. . . 4
β’ -i β
β |
91 | | mulneg2 11650 |
. . . 4
β’ ((-i
β β β§ (logβ((i Β· π΄) + (ββ(1 β (π΄β2))))) β β)
β (-i Β· -(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) = -(-i Β·
(logβ((i Β· π΄)
+ (ββ(1 β (π΄β2))))))) |
92 | 90, 11, 91 | sylancr 587 |
. . 3
β’ (π΄ β β β (-i
Β· -(logβ((i Β· π΄) + (ββ(1 β (π΄β2)))))) = -(-i Β·
(logβ((i Β· π΄)
+ (ββ(1 β (π΄β2))))))) |
93 | 89, 92 | eqtrd 2772 |
. 2
β’ (π΄ β β β (-i
Β· (logβ((i Β· -π΄) + (ββ(1 β (-π΄β2)))))) = -(-i Β·
(logβ((i Β· π΄)
+ (ββ(1 β (π΄β2))))))) |
94 | | asinval 26384 |
. . 3
β’ (-π΄ β β β
(arcsinβ-π΄) = (-i
Β· (logβ((i Β· -π΄) + (ββ(1 β (-π΄β2))))))) |
95 | 19, 94 | syl 17 |
. 2
β’ (π΄ β β β
(arcsinβ-π΄) = (-i
Β· (logβ((i Β· -π΄) + (ββ(1 β (-π΄β2))))))) |
96 | | asinval 26384 |
. . 3
β’ (π΄ β β β
(arcsinβπ΄) = (-i
Β· (logβ((i Β· π΄) + (ββ(1 β (π΄β2))))))) |
97 | 96 | negeqd 11453 |
. 2
β’ (π΄ β β β
-(arcsinβπ΄) = -(-i
Β· (logβ((i Β· π΄) + (ββ(1 β (π΄β2))))))) |
98 | 93, 95, 97 | 3eqtr4d 2782 |
1
β’ (π΄ β β β
(arcsinβ-π΄) =
-(arcsinβπ΄)) |