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