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