Step |
Hyp |
Ref |
Expression |
1 |
|
atansopn.d |
|- D = ( CC \ ( -oo (,] 0 ) ) |
2 |
|
atansopn.s |
|- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D } |
3 |
|
sqcl |
|- ( A e. CC -> ( A ^ 2 ) e. CC ) |
4 |
3
|
adantr |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( A ^ 2 ) e. CC ) |
5 |
4
|
sqsqrtd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( ( sqrt ` ( A ^ 2 ) ) ^ 2 ) = ( A ^ 2 ) ) |
6 |
5
|
eqcomd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( A ^ 2 ) = ( ( sqrt ` ( A ^ 2 ) ) ^ 2 ) ) |
7 |
4
|
sqrtcld |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( sqrt ` ( A ^ 2 ) ) e. CC ) |
8 |
|
sqeqor |
|- ( ( A e. CC /\ ( sqrt ` ( A ^ 2 ) ) e. CC ) -> ( ( A ^ 2 ) = ( ( sqrt ` ( A ^ 2 ) ) ^ 2 ) <-> ( A = ( sqrt ` ( A ^ 2 ) ) \/ A = -u ( sqrt ` ( A ^ 2 ) ) ) ) ) |
9 |
7 8
|
syldan |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( ( A ^ 2 ) = ( ( sqrt ` ( A ^ 2 ) ) ^ 2 ) <-> ( A = ( sqrt ` ( A ^ 2 ) ) \/ A = -u ( sqrt ` ( A ^ 2 ) ) ) ) ) |
10 |
6 9
|
mpbid |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( A = ( sqrt ` ( A ^ 2 ) ) \/ A = -u ( sqrt ` ( A ^ 2 ) ) ) ) |
11 |
|
1re |
|- 1 e. RR |
12 |
11
|
a1i |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> 1 e. RR ) |
13 |
4
|
negnegd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> -u -u ( A ^ 2 ) = ( A ^ 2 ) ) |
14 |
13
|
fveq2d |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( sqrt ` -u -u ( A ^ 2 ) ) = ( sqrt ` ( A ^ 2 ) ) ) |
15 |
|
ax-1cn |
|- 1 e. CC |
16 |
|
pncan2 |
|- ( ( 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( ( 1 + ( A ^ 2 ) ) - 1 ) = ( A ^ 2 ) ) |
17 |
15 4 16
|
sylancr |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 + ( A ^ 2 ) ) - 1 ) = ( A ^ 2 ) ) |
18 |
|
simpr |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) |
19 |
|
mnfxr |
|- -oo e. RR* |
20 |
|
0re |
|- 0 e. RR |
21 |
|
elioc2 |
|- ( ( -oo e. RR* /\ 0 e. RR ) -> ( ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) <-> ( ( 1 + ( A ^ 2 ) ) e. RR /\ -oo < ( 1 + ( A ^ 2 ) ) /\ ( 1 + ( A ^ 2 ) ) <_ 0 ) ) ) |
22 |
19 20 21
|
mp2an |
|- ( ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) <-> ( ( 1 + ( A ^ 2 ) ) e. RR /\ -oo < ( 1 + ( A ^ 2 ) ) /\ ( 1 + ( A ^ 2 ) ) <_ 0 ) ) |
23 |
18 22
|
sylib |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 + ( A ^ 2 ) ) e. RR /\ -oo < ( 1 + ( A ^ 2 ) ) /\ ( 1 + ( A ^ 2 ) ) <_ 0 ) ) |
24 |
23
|
simp1d |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 + ( A ^ 2 ) ) e. RR ) |
25 |
|
resubcl |
|- ( ( ( 1 + ( A ^ 2 ) ) e. RR /\ 1 e. RR ) -> ( ( 1 + ( A ^ 2 ) ) - 1 ) e. RR ) |
26 |
24 11 25
|
sylancl |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 + ( A ^ 2 ) ) - 1 ) e. RR ) |
27 |
17 26
|
eqeltrrd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( A ^ 2 ) e. RR ) |
28 |
27
|
renegcld |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> -u ( A ^ 2 ) e. RR ) |
29 |
|
0red |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> 0 e. RR ) |
30 |
|
0le1 |
|- 0 <_ 1 |
31 |
30
|
a1i |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> 0 <_ 1 ) |
32 |
|
subneg |
|- ( ( 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( 1 - -u ( A ^ 2 ) ) = ( 1 + ( A ^ 2 ) ) ) |
33 |
15 4 32
|
sylancr |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 - -u ( A ^ 2 ) ) = ( 1 + ( A ^ 2 ) ) ) |
34 |
23
|
simp3d |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 + ( A ^ 2 ) ) <_ 0 ) |
35 |
33 34
|
eqbrtrd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 - -u ( A ^ 2 ) ) <_ 0 ) |
36 |
|
suble0 |
|- ( ( 1 e. RR /\ -u ( A ^ 2 ) e. RR ) -> ( ( 1 - -u ( A ^ 2 ) ) <_ 0 <-> 1 <_ -u ( A ^ 2 ) ) ) |
37 |
11 28 36
|
sylancr |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 - -u ( A ^ 2 ) ) <_ 0 <-> 1 <_ -u ( A ^ 2 ) ) ) |
38 |
35 37
|
mpbid |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> 1 <_ -u ( A ^ 2 ) ) |
39 |
29 12 28 31 38
|
letrd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> 0 <_ -u ( A ^ 2 ) ) |
40 |
28 39
|
sqrtnegd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( sqrt ` -u -u ( A ^ 2 ) ) = ( _i x. ( sqrt ` -u ( A ^ 2 ) ) ) ) |
41 |
14 40
|
eqtr3d |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( sqrt ` ( A ^ 2 ) ) = ( _i x. ( sqrt ` -u ( A ^ 2 ) ) ) ) |
42 |
41
|
oveq2d |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( _i x. ( sqrt ` ( A ^ 2 ) ) ) = ( _i x. ( _i x. ( sqrt ` -u ( A ^ 2 ) ) ) ) ) |
43 |
|
ax-icn |
|- _i e. CC |
44 |
43
|
a1i |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> _i e. CC ) |
45 |
28 39
|
resqrtcld |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( sqrt ` -u ( A ^ 2 ) ) e. RR ) |
46 |
45
|
recnd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( sqrt ` -u ( A ^ 2 ) ) e. CC ) |
47 |
44 44 46
|
mulassd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( ( _i x. _i ) x. ( sqrt ` -u ( A ^ 2 ) ) ) = ( _i x. ( _i x. ( sqrt ` -u ( A ^ 2 ) ) ) ) ) |
48 |
|
ixi |
|- ( _i x. _i ) = -u 1 |
49 |
48
|
oveq1i |
|- ( ( _i x. _i ) x. ( sqrt ` -u ( A ^ 2 ) ) ) = ( -u 1 x. ( sqrt ` -u ( A ^ 2 ) ) ) |
50 |
46
|
mulm1d |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( -u 1 x. ( sqrt ` -u ( A ^ 2 ) ) ) = -u ( sqrt ` -u ( A ^ 2 ) ) ) |
51 |
49 50
|
syl5eq |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( ( _i x. _i ) x. ( sqrt ` -u ( A ^ 2 ) ) ) = -u ( sqrt ` -u ( A ^ 2 ) ) ) |
52 |
42 47 51
|
3eqtr2d |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( _i x. ( sqrt ` ( A ^ 2 ) ) ) = -u ( sqrt ` -u ( A ^ 2 ) ) ) |
53 |
45
|
renegcld |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> -u ( sqrt ` -u ( A ^ 2 ) ) e. RR ) |
54 |
52 53
|
eqeltrd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( _i x. ( sqrt ` ( A ^ 2 ) ) ) e. RR ) |
55 |
12 54
|
readdcld |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) e. RR ) |
56 |
55
|
mnfltd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> -oo < ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) ) |
57 |
52
|
oveq2d |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) = ( 1 + -u ( sqrt ` -u ( A ^ 2 ) ) ) ) |
58 |
|
negsub |
|- ( ( 1 e. CC /\ ( sqrt ` -u ( A ^ 2 ) ) e. CC ) -> ( 1 + -u ( sqrt ` -u ( A ^ 2 ) ) ) = ( 1 - ( sqrt ` -u ( A ^ 2 ) ) ) ) |
59 |
15 46 58
|
sylancr |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 + -u ( sqrt ` -u ( A ^ 2 ) ) ) = ( 1 - ( sqrt ` -u ( A ^ 2 ) ) ) ) |
60 |
57 59
|
eqtrd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) = ( 1 - ( sqrt ` -u ( A ^ 2 ) ) ) ) |
61 |
|
sq1 |
|- ( 1 ^ 2 ) = 1 |
62 |
61
|
a1i |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 ^ 2 ) = 1 ) |
63 |
28
|
recnd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> -u ( A ^ 2 ) e. CC ) |
64 |
63
|
sqsqrtd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( ( sqrt ` -u ( A ^ 2 ) ) ^ 2 ) = -u ( A ^ 2 ) ) |
65 |
38 62 64
|
3brtr4d |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 ^ 2 ) <_ ( ( sqrt ` -u ( A ^ 2 ) ) ^ 2 ) ) |
66 |
28 39
|
sqrtge0d |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> 0 <_ ( sqrt ` -u ( A ^ 2 ) ) ) |
67 |
12 45 31 66
|
le2sqd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 <_ ( sqrt ` -u ( A ^ 2 ) ) <-> ( 1 ^ 2 ) <_ ( ( sqrt ` -u ( A ^ 2 ) ) ^ 2 ) ) ) |
68 |
65 67
|
mpbird |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> 1 <_ ( sqrt ` -u ( A ^ 2 ) ) ) |
69 |
12 45
|
suble0d |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 - ( sqrt ` -u ( A ^ 2 ) ) ) <_ 0 <-> 1 <_ ( sqrt ` -u ( A ^ 2 ) ) ) ) |
70 |
68 69
|
mpbird |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 - ( sqrt ` -u ( A ^ 2 ) ) ) <_ 0 ) |
71 |
60 70
|
eqbrtrd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) <_ 0 ) |
72 |
|
elioc2 |
|- ( ( -oo e. RR* /\ 0 e. RR ) -> ( ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) e. ( -oo (,] 0 ) <-> ( ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) e. RR /\ -oo < ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) /\ ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) <_ 0 ) ) ) |
73 |
19 20 72
|
mp2an |
|- ( ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) e. ( -oo (,] 0 ) <-> ( ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) e. RR /\ -oo < ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) /\ ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) <_ 0 ) ) |
74 |
55 56 71 73
|
syl3anbrc |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) e. ( -oo (,] 0 ) ) |
75 |
|
oveq2 |
|- ( A = ( sqrt ` ( A ^ 2 ) ) -> ( _i x. A ) = ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) |
76 |
75
|
oveq2d |
|- ( A = ( sqrt ` ( A ^ 2 ) ) -> ( 1 + ( _i x. A ) ) = ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) ) |
77 |
76
|
eleq1d |
|- ( A = ( sqrt ` ( A ^ 2 ) ) -> ( ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) <-> ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) e. ( -oo (,] 0 ) ) ) |
78 |
74 77
|
syl5ibrcom |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( A = ( sqrt ` ( A ^ 2 ) ) -> ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) |
79 |
|
mulneg2 |
|- ( ( _i e. CC /\ ( sqrt ` ( A ^ 2 ) ) e. CC ) -> ( _i x. -u ( sqrt ` ( A ^ 2 ) ) ) = -u ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) |
80 |
43 7 79
|
sylancr |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( _i x. -u ( sqrt ` ( A ^ 2 ) ) ) = -u ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) |
81 |
80
|
oveq2d |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 - ( _i x. -u ( sqrt ` ( A ^ 2 ) ) ) ) = ( 1 - -u ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) ) |
82 |
|
mulcl |
|- ( ( _i e. CC /\ ( sqrt ` ( A ^ 2 ) ) e. CC ) -> ( _i x. ( sqrt ` ( A ^ 2 ) ) ) e. CC ) |
83 |
43 7 82
|
sylancr |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( _i x. ( sqrt ` ( A ^ 2 ) ) ) e. CC ) |
84 |
|
subneg |
|- ( ( 1 e. CC /\ ( _i x. ( sqrt ` ( A ^ 2 ) ) ) e. CC ) -> ( 1 - -u ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) = ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) ) |
85 |
15 83 84
|
sylancr |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 - -u ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) = ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) ) |
86 |
81 85
|
eqtrd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 - ( _i x. -u ( sqrt ` ( A ^ 2 ) ) ) ) = ( 1 + ( _i x. ( sqrt ` ( A ^ 2 ) ) ) ) ) |
87 |
86 74
|
eqeltrd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 - ( _i x. -u ( sqrt ` ( A ^ 2 ) ) ) ) e. ( -oo (,] 0 ) ) |
88 |
|
oveq2 |
|- ( A = -u ( sqrt ` ( A ^ 2 ) ) -> ( _i x. A ) = ( _i x. -u ( sqrt ` ( A ^ 2 ) ) ) ) |
89 |
88
|
oveq2d |
|- ( A = -u ( sqrt ` ( A ^ 2 ) ) -> ( 1 - ( _i x. A ) ) = ( 1 - ( _i x. -u ( sqrt ` ( A ^ 2 ) ) ) ) ) |
90 |
89
|
eleq1d |
|- ( A = -u ( sqrt ` ( A ^ 2 ) ) -> ( ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) <-> ( 1 - ( _i x. -u ( sqrt ` ( A ^ 2 ) ) ) ) e. ( -oo (,] 0 ) ) ) |
91 |
87 90
|
syl5ibrcom |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( A = -u ( sqrt ` ( A ^ 2 ) ) -> ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) |
92 |
78 91
|
orim12d |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( ( A = ( sqrt ` ( A ^ 2 ) ) \/ A = -u ( sqrt ` ( A ^ 2 ) ) ) -> ( ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) \/ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) ) |
93 |
10 92
|
mpd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) \/ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) |
94 |
93
|
orcomd |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) \/ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) |
95 |
61
|
a1i |
|- ( A e. CC -> ( 1 ^ 2 ) = 1 ) |
96 |
|
sqmul |
|- ( ( _i e. CC /\ A e. CC ) -> ( ( _i x. A ) ^ 2 ) = ( ( _i ^ 2 ) x. ( A ^ 2 ) ) ) |
97 |
43 96
|
mpan |
|- ( A e. CC -> ( ( _i x. A ) ^ 2 ) = ( ( _i ^ 2 ) x. ( A ^ 2 ) ) ) |
98 |
|
i2 |
|- ( _i ^ 2 ) = -u 1 |
99 |
98
|
oveq1i |
|- ( ( _i ^ 2 ) x. ( A ^ 2 ) ) = ( -u 1 x. ( A ^ 2 ) ) |
100 |
3
|
mulm1d |
|- ( A e. CC -> ( -u 1 x. ( A ^ 2 ) ) = -u ( A ^ 2 ) ) |
101 |
99 100
|
syl5eq |
|- ( A e. CC -> ( ( _i ^ 2 ) x. ( A ^ 2 ) ) = -u ( A ^ 2 ) ) |
102 |
97 101
|
eqtrd |
|- ( A e. CC -> ( ( _i x. A ) ^ 2 ) = -u ( A ^ 2 ) ) |
103 |
95 102
|
oveq12d |
|- ( A e. CC -> ( ( 1 ^ 2 ) - ( ( _i x. A ) ^ 2 ) ) = ( 1 - -u ( A ^ 2 ) ) ) |
104 |
|
mulcl |
|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC ) |
105 |
43 104
|
mpan |
|- ( A e. CC -> ( _i x. A ) e. CC ) |
106 |
|
subsq |
|- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( ( 1 ^ 2 ) - ( ( _i x. A ) ^ 2 ) ) = ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) ) |
107 |
15 105 106
|
sylancr |
|- ( A e. CC -> ( ( 1 ^ 2 ) - ( ( _i x. A ) ^ 2 ) ) = ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) ) |
108 |
15 3 32
|
sylancr |
|- ( A e. CC -> ( 1 - -u ( A ^ 2 ) ) = ( 1 + ( A ^ 2 ) ) ) |
109 |
103 107 108
|
3eqtr3d |
|- ( A e. CC -> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) = ( 1 + ( A ^ 2 ) ) ) |
110 |
109
|
adantr |
|- ( ( A e. CC /\ ( ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) \/ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) -> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) = ( 1 + ( A ^ 2 ) ) ) |
111 |
|
2cn |
|- 2 e. CC |
112 |
111
|
a1i |
|- ( A e. CC -> 2 e. CC ) |
113 |
15
|
a1i |
|- ( A e. CC -> 1 e. CC ) |
114 |
112 113 105
|
subsubd |
|- ( A e. CC -> ( 2 - ( 1 - ( _i x. A ) ) ) = ( ( 2 - 1 ) + ( _i x. A ) ) ) |
115 |
|
2m1e1 |
|- ( 2 - 1 ) = 1 |
116 |
115
|
oveq1i |
|- ( ( 2 - 1 ) + ( _i x. A ) ) = ( 1 + ( _i x. A ) ) |
117 |
114 116
|
eqtrdi |
|- ( A e. CC -> ( 2 - ( 1 - ( _i x. A ) ) ) = ( 1 + ( _i x. A ) ) ) |
118 |
117
|
adantr |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 2 - ( 1 - ( _i x. A ) ) ) = ( 1 + ( _i x. A ) ) ) |
119 |
|
2re |
|- 2 e. RR |
120 |
|
simpr |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) |
121 |
|
elioc2 |
|- ( ( -oo e. RR* /\ 0 e. RR ) -> ( ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) <-> ( ( 1 - ( _i x. A ) ) e. RR /\ -oo < ( 1 - ( _i x. A ) ) /\ ( 1 - ( _i x. A ) ) <_ 0 ) ) ) |
122 |
19 20 121
|
mp2an |
|- ( ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) <-> ( ( 1 - ( _i x. A ) ) e. RR /\ -oo < ( 1 - ( _i x. A ) ) /\ ( 1 - ( _i x. A ) ) <_ 0 ) ) |
123 |
120 122
|
sylib |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 - ( _i x. A ) ) e. RR /\ -oo < ( 1 - ( _i x. A ) ) /\ ( 1 - ( _i x. A ) ) <_ 0 ) ) |
124 |
123
|
simp1d |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 1 - ( _i x. A ) ) e. RR ) |
125 |
|
resubcl |
|- ( ( 2 e. RR /\ ( 1 - ( _i x. A ) ) e. RR ) -> ( 2 - ( 1 - ( _i x. A ) ) ) e. RR ) |
126 |
119 124 125
|
sylancr |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 2 - ( 1 - ( _i x. A ) ) ) e. RR ) |
127 |
118 126
|
eqeltrrd |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 1 + ( _i x. A ) ) e. RR ) |
128 |
127 124
|
remulcld |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) e. RR ) |
129 |
128
|
mnfltd |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> -oo < ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) ) |
130 |
123
|
simp3d |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 1 - ( _i x. A ) ) <_ 0 ) |
131 |
|
0red |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> 0 e. RR ) |
132 |
119
|
a1i |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> 2 e. RR ) |
133 |
|
2pos |
|- 0 < 2 |
134 |
133
|
a1i |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> 0 < 2 ) |
135 |
111
|
subid1i |
|- ( 2 - 0 ) = 2 |
136 |
124 131 132 130
|
lesub2dd |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 2 - 0 ) <_ ( 2 - ( 1 - ( _i x. A ) ) ) ) |
137 |
135 136
|
eqbrtrrid |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> 2 <_ ( 2 - ( 1 - ( _i x. A ) ) ) ) |
138 |
137 118
|
breqtrd |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> 2 <_ ( 1 + ( _i x. A ) ) ) |
139 |
131 132 127 134 138
|
ltletrd |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> 0 < ( 1 + ( _i x. A ) ) ) |
140 |
|
lemul2 |
|- ( ( ( 1 - ( _i x. A ) ) e. RR /\ 0 e. RR /\ ( ( 1 + ( _i x. A ) ) e. RR /\ 0 < ( 1 + ( _i x. A ) ) ) ) -> ( ( 1 - ( _i x. A ) ) <_ 0 <-> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) <_ ( ( 1 + ( _i x. A ) ) x. 0 ) ) ) |
141 |
124 131 127 139 140
|
syl112anc |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 - ( _i x. A ) ) <_ 0 <-> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) <_ ( ( 1 + ( _i x. A ) ) x. 0 ) ) ) |
142 |
130 141
|
mpbid |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) <_ ( ( 1 + ( _i x. A ) ) x. 0 ) ) |
143 |
|
addcl |
|- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) e. CC ) |
144 |
15 105 143
|
sylancr |
|- ( A e. CC -> ( 1 + ( _i x. A ) ) e. CC ) |
145 |
144
|
adantr |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 1 + ( _i x. A ) ) e. CC ) |
146 |
145
|
mul01d |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 + ( _i x. A ) ) x. 0 ) = 0 ) |
147 |
142 146
|
breqtrd |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) <_ 0 ) |
148 |
|
elioc2 |
|- ( ( -oo e. RR* /\ 0 e. RR ) -> ( ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) e. ( -oo (,] 0 ) <-> ( ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) e. RR /\ -oo < ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) /\ ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) <_ 0 ) ) ) |
149 |
19 20 148
|
mp2an |
|- ( ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) e. ( -oo (,] 0 ) <-> ( ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) e. RR /\ -oo < ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) /\ ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) <_ 0 ) ) |
150 |
128 129 147 149
|
syl3anbrc |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) e. ( -oo (,] 0 ) ) |
151 |
|
simpr |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) |
152 |
|
elioc2 |
|- ( ( -oo e. RR* /\ 0 e. RR ) -> ( ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) <-> ( ( 1 + ( _i x. A ) ) e. RR /\ -oo < ( 1 + ( _i x. A ) ) /\ ( 1 + ( _i x. A ) ) <_ 0 ) ) ) |
153 |
19 20 152
|
mp2an |
|- ( ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) <-> ( ( 1 + ( _i x. A ) ) e. RR /\ -oo < ( 1 + ( _i x. A ) ) /\ ( 1 + ( _i x. A ) ) <_ 0 ) ) |
154 |
151 153
|
sylib |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 + ( _i x. A ) ) e. RR /\ -oo < ( 1 + ( _i x. A ) ) /\ ( 1 + ( _i x. A ) ) <_ 0 ) ) |
155 |
154
|
simp1d |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 1 + ( _i x. A ) ) e. RR ) |
156 |
112 113 105
|
subsub4d |
|- ( A e. CC -> ( ( 2 - 1 ) - ( _i x. A ) ) = ( 2 - ( 1 + ( _i x. A ) ) ) ) |
157 |
115
|
oveq1i |
|- ( ( 2 - 1 ) - ( _i x. A ) ) = ( 1 - ( _i x. A ) ) |
158 |
156 157
|
eqtr3di |
|- ( A e. CC -> ( 2 - ( 1 + ( _i x. A ) ) ) = ( 1 - ( _i x. A ) ) ) |
159 |
158
|
adantr |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 2 - ( 1 + ( _i x. A ) ) ) = ( 1 - ( _i x. A ) ) ) |
160 |
|
resubcl |
|- ( ( 2 e. RR /\ ( 1 + ( _i x. A ) ) e. RR ) -> ( 2 - ( 1 + ( _i x. A ) ) ) e. RR ) |
161 |
119 155 160
|
sylancr |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 2 - ( 1 + ( _i x. A ) ) ) e. RR ) |
162 |
159 161
|
eqeltrrd |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 1 - ( _i x. A ) ) e. RR ) |
163 |
155 162
|
remulcld |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) e. RR ) |
164 |
163
|
mnfltd |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> -oo < ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) ) |
165 |
154
|
simp3d |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 1 + ( _i x. A ) ) <_ 0 ) |
166 |
|
0red |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> 0 e. RR ) |
167 |
119
|
a1i |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> 2 e. RR ) |
168 |
133
|
a1i |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> 0 < 2 ) |
169 |
155 166 167 165
|
lesub2dd |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 2 - 0 ) <_ ( 2 - ( 1 + ( _i x. A ) ) ) ) |
170 |
135 169
|
eqbrtrrid |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> 2 <_ ( 2 - ( 1 + ( _i x. A ) ) ) ) |
171 |
170 159
|
breqtrd |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> 2 <_ ( 1 - ( _i x. A ) ) ) |
172 |
166 167 162 168 171
|
ltletrd |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> 0 < ( 1 - ( _i x. A ) ) ) |
173 |
|
lemul1 |
|- ( ( ( 1 + ( _i x. A ) ) e. RR /\ 0 e. RR /\ ( ( 1 - ( _i x. A ) ) e. RR /\ 0 < ( 1 - ( _i x. A ) ) ) ) -> ( ( 1 + ( _i x. A ) ) <_ 0 <-> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) <_ ( 0 x. ( 1 - ( _i x. A ) ) ) ) ) |
174 |
155 166 162 172 173
|
syl112anc |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 + ( _i x. A ) ) <_ 0 <-> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) <_ ( 0 x. ( 1 - ( _i x. A ) ) ) ) ) |
175 |
165 174
|
mpbid |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) <_ ( 0 x. ( 1 - ( _i x. A ) ) ) ) |
176 |
162
|
recnd |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 1 - ( _i x. A ) ) e. CC ) |
177 |
176
|
mul02d |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( 0 x. ( 1 - ( _i x. A ) ) ) = 0 ) |
178 |
175 177
|
breqtrd |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) <_ 0 ) |
179 |
163 164 178 149
|
syl3anbrc |
|- ( ( A e. CC /\ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) -> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) e. ( -oo (,] 0 ) ) |
180 |
150 179
|
jaodan |
|- ( ( A e. CC /\ ( ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) \/ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) -> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) e. ( -oo (,] 0 ) ) |
181 |
110 180
|
eqeltrrd |
|- ( ( A e. CC /\ ( ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) \/ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) -> ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) |
182 |
94 181
|
impbida |
|- ( A e. CC -> ( ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) <-> ( ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) \/ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) ) |
183 |
182
|
notbid |
|- ( A e. CC -> ( -. ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) <-> -. ( ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) \/ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) ) |
184 |
|
ioran |
|- ( -. ( ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) \/ ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) <-> ( -. ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) /\ -. ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) |
185 |
183 184
|
bitrdi |
|- ( A e. CC -> ( -. ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) <-> ( -. ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) /\ -. ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) ) |
186 |
|
addcl |
|- ( ( 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( 1 + ( A ^ 2 ) ) e. CC ) |
187 |
15 3 186
|
sylancr |
|- ( A e. CC -> ( 1 + ( A ^ 2 ) ) e. CC ) |
188 |
1
|
eleq2i |
|- ( ( 1 + ( A ^ 2 ) ) e. D <-> ( 1 + ( A ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) ) |
189 |
|
eldif |
|- ( ( 1 + ( A ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) <-> ( ( 1 + ( A ^ 2 ) ) e. CC /\ -. ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) ) |
190 |
188 189
|
bitri |
|- ( ( 1 + ( A ^ 2 ) ) e. D <-> ( ( 1 + ( A ^ 2 ) ) e. CC /\ -. ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) ) |
191 |
190
|
baib |
|- ( ( 1 + ( A ^ 2 ) ) e. CC -> ( ( 1 + ( A ^ 2 ) ) e. D <-> -. ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) ) |
192 |
187 191
|
syl |
|- ( A e. CC -> ( ( 1 + ( A ^ 2 ) ) e. D <-> -. ( 1 + ( A ^ 2 ) ) e. ( -oo (,] 0 ) ) ) |
193 |
|
subcl |
|- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - ( _i x. A ) ) e. CC ) |
194 |
15 105 193
|
sylancr |
|- ( A e. CC -> ( 1 - ( _i x. A ) ) e. CC ) |
195 |
1
|
eleq2i |
|- ( ( 1 - ( _i x. A ) ) e. D <-> ( 1 - ( _i x. A ) ) e. ( CC \ ( -oo (,] 0 ) ) ) |
196 |
|
eldif |
|- ( ( 1 - ( _i x. A ) ) e. ( CC \ ( -oo (,] 0 ) ) <-> ( ( 1 - ( _i x. A ) ) e. CC /\ -. ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) |
197 |
195 196
|
bitri |
|- ( ( 1 - ( _i x. A ) ) e. D <-> ( ( 1 - ( _i x. A ) ) e. CC /\ -. ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) |
198 |
197
|
baib |
|- ( ( 1 - ( _i x. A ) ) e. CC -> ( ( 1 - ( _i x. A ) ) e. D <-> -. ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) |
199 |
194 198
|
syl |
|- ( A e. CC -> ( ( 1 - ( _i x. A ) ) e. D <-> -. ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) |
200 |
1
|
eleq2i |
|- ( ( 1 + ( _i x. A ) ) e. D <-> ( 1 + ( _i x. A ) ) e. ( CC \ ( -oo (,] 0 ) ) ) |
201 |
|
eldif |
|- ( ( 1 + ( _i x. A ) ) e. ( CC \ ( -oo (,] 0 ) ) <-> ( ( 1 + ( _i x. A ) ) e. CC /\ -. ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) |
202 |
200 201
|
bitri |
|- ( ( 1 + ( _i x. A ) ) e. D <-> ( ( 1 + ( _i x. A ) ) e. CC /\ -. ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) |
203 |
202
|
baib |
|- ( ( 1 + ( _i x. A ) ) e. CC -> ( ( 1 + ( _i x. A ) ) e. D <-> -. ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) |
204 |
144 203
|
syl |
|- ( A e. CC -> ( ( 1 + ( _i x. A ) ) e. D <-> -. ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) |
205 |
199 204
|
anbi12d |
|- ( A e. CC -> ( ( ( 1 - ( _i x. A ) ) e. D /\ ( 1 + ( _i x. A ) ) e. D ) <-> ( -. ( 1 - ( _i x. A ) ) e. ( -oo (,] 0 ) /\ -. ( 1 + ( _i x. A ) ) e. ( -oo (,] 0 ) ) ) ) |
206 |
185 192 205
|
3bitr4d |
|- ( A e. CC -> ( ( 1 + ( A ^ 2 ) ) e. D <-> ( ( 1 - ( _i x. A ) ) e. D /\ ( 1 + ( _i x. A ) ) e. D ) ) ) |
207 |
206
|
pm5.32i |
|- ( ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. D ) <-> ( A e. CC /\ ( ( 1 - ( _i x. A ) ) e. D /\ ( 1 + ( _i x. A ) ) e. D ) ) ) |
208 |
1 2
|
atans |
|- ( A e. S <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. D ) ) |
209 |
|
3anass |
|- ( ( A e. CC /\ ( 1 - ( _i x. A ) ) e. D /\ ( 1 + ( _i x. A ) ) e. D ) <-> ( A e. CC /\ ( ( 1 - ( _i x. A ) ) e. D /\ ( 1 + ( _i x. A ) ) e. D ) ) ) |
210 |
207 208 209
|
3bitr4i |
|- ( A e. S <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) e. D /\ ( 1 + ( _i x. A ) ) e. D ) ) |