Metamath Proof Explorer


Theorem atans2

Description: It suffices to show that 1 -i A and 1 + i A are in the continuity domain of log to show that A is in the continuity domain of arctangent. (Contributed by Mario Carneiro, 7-Apr-2015)

Ref Expression
Hypotheses atansopn.d
|- D = ( CC \ ( -oo (,] 0 ) )
atansopn.s
|- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }
Assertion atans2
|- ( A e. S <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) e. D /\ ( 1 + ( _i x. A ) ) e. D ) )

Proof

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 ) )