Metamath Proof Explorer

Theorem atandm2

Description: This form of atandm is a bit more useful for showing that the logarithms in df-atan are well-defined. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion atandm2 
|- ( A e. dom arctan <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )

Proof

Step Hyp Ref Expression
1 atandm 
 |-  ( A e. dom arctan <-> ( A e. CC /\ A =/= -u _i /\ A =/= _i ) )
2 3anass 
 |-  ( ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) <-> ( A e. CC /\ ( ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) ) )
3 ax-1cn 
 |-  1 e. CC
4 ax-icn 
 |-  _i e. CC
5 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
6 4 5 mpan 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
7 subeq0 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( ( 1 - ( _i x. A ) ) = 0 <-> 1 = ( _i x. A ) ) )
8 3 6 7 sylancr 
 |-  ( A e. CC -> ( ( 1 - ( _i x. A ) ) = 0 <-> 1 = ( _i x. A ) ) )
9 4 4 mulneg2i 
 |-  ( _i x. -u _i ) = -u ( _i x. _i )
10 ixi 
 |-  ( _i x. _i ) = -u 1
11 10 negeqi 
 |-  -u ( _i x. _i ) = -u -u 1
12 negneg1e1 
 |-  -u -u 1 = 1
13 9 11 12 3eqtri 
 |-  ( _i x. -u _i ) = 1
14 13 eqeq2i 
 |-  ( ( _i x. A ) = ( _i x. -u _i ) <-> ( _i x. A ) = 1 )
15 eqcom 
 |-  ( ( _i x. A ) = 1 <-> 1 = ( _i x. A ) )
16 14 15 bitri 
 |-  ( ( _i x. A ) = ( _i x. -u _i ) <-> 1 = ( _i x. A ) )
17 8 16 bitr4di 
 |-  ( A e. CC -> ( ( 1 - ( _i x. A ) ) = 0 <-> ( _i x. A ) = ( _i x. -u _i ) ) )
18 id 
 |-  ( A e. CC -> A e. CC )
19 4 negcli 
 |-  -u _i e. CC
20 19 a1i 
 |-  ( A e. CC -> -u _i e. CC )
21 4 a1i 
 |-  ( A e. CC -> _i e. CC )
22 ine0 
 |-  _i =/= 0
23 22 a1i 
 |-  ( A e. CC -> _i =/= 0 )
24 18 20 21 23 mulcand 
 |-  ( A e. CC -> ( ( _i x. A ) = ( _i x. -u _i ) <-> A = -u _i ) )
25 17 24 bitrd 
 |-  ( A e. CC -> ( ( 1 - ( _i x. A ) ) = 0 <-> A = -u _i ) )
26 25 necon3bid 
 |-  ( A e. CC -> ( ( 1 - ( _i x. A ) ) =/= 0 <-> A =/= -u _i ) )
27 addcom 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) = ( ( _i x. A ) + 1 ) )
28 3 6 27 sylancr 
 |-  ( A e. CC -> ( 1 + ( _i x. A ) ) = ( ( _i x. A ) + 1 ) )
29 subneg 
 |-  ( ( ( _i x. A ) e. CC /\ 1 e. CC ) -> ( ( _i x. A ) - -u 1 ) = ( ( _i x. A ) + 1 ) )
30 6 3 29 sylancl 
 |-  ( A e. CC -> ( ( _i x. A ) - -u 1 ) = ( ( _i x. A ) + 1 ) )
31 28 30 eqtr4d 
 |-  ( A e. CC -> ( 1 + ( _i x. A ) ) = ( ( _i x. A ) - -u 1 ) )
32 31 eqeq1d 
 |-  ( A e. CC -> ( ( 1 + ( _i x. A ) ) = 0 <-> ( ( _i x. A ) - -u 1 ) = 0 ) )
33 3 negcli 
 |-  -u 1 e. CC
34 subeq0 
 |-  ( ( ( _i x. A ) e. CC /\ -u 1 e. CC ) -> ( ( ( _i x. A ) - -u 1 ) = 0 <-> ( _i x. A ) = -u 1 ) )
35 6 33 34 sylancl 
 |-  ( A e. CC -> ( ( ( _i x. A ) - -u 1 ) = 0 <-> ( _i x. A ) = -u 1 ) )
36 32 35 bitrd 
 |-  ( A e. CC -> ( ( 1 + ( _i x. A ) ) = 0 <-> ( _i x. A ) = -u 1 ) )
37 10 eqeq2i 
 |-  ( ( _i x. A ) = ( _i x. _i ) <-> ( _i x. A ) = -u 1 )
38 36 37 bitr4di 
 |-  ( A e. CC -> ( ( 1 + ( _i x. A ) ) = 0 <-> ( _i x. A ) = ( _i x. _i ) ) )
39 18 21 21 23 mulcand 
 |-  ( A e. CC -> ( ( _i x. A ) = ( _i x. _i ) <-> A = _i ) )
40 38 39 bitrd 
 |-  ( A e. CC -> ( ( 1 + ( _i x. A ) ) = 0 <-> A = _i ) )
41 40 necon3bid 
 |-  ( A e. CC -> ( ( 1 + ( _i x. A ) ) =/= 0 <-> A =/= _i ) )
42 26 41 anbi12d 
 |-  ( A e. CC -> ( ( ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) <-> ( A =/= -u _i /\ A =/= _i ) ) )
43 42 pm5.32i 
 |-  ( ( A e. CC /\ ( ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) ) <-> ( A e. CC /\ ( A =/= -u _i /\ A =/= _i ) ) )
44 3anass 
 |-  ( ( A e. CC /\ A =/= -u _i /\ A =/= _i ) <-> ( A e. CC /\ ( A =/= -u _i /\ A =/= _i ) ) )
45 43 44 bitr4i 
 |-  ( ( A e. CC /\ ( ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) ) <-> ( A e. CC /\ A =/= -u _i /\ A =/= _i ) )
46 2 45 bitri 
 |-  ( ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) <-> ( A e. CC /\ A =/= -u _i /\ A =/= _i ) )
47 1 46 bitr4i 
 |-  ( A e. dom arctan <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )