Metamath Proof Explorer

Theorem atandm4

Description: A compact form of atandm . (Contributed by Mario Carneiro, 3-Apr-2015)

Ref Expression
Assertion atandm4 
|- ( A e. dom arctan <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) =/= 0 ) )

Proof

Step Hyp Ref Expression
1 atandm3 
 |-  ( A e. dom arctan <-> ( A e. CC /\ ( A ^ 2 ) =/= -u 1 ) )
2 sqcl 
 |-  ( A e. CC -> ( A ^ 2 ) e. CC )
3 neg1cn 
 |-  -u 1 e. CC
4 subeq0 
 |-  ( ( ( A ^ 2 ) e. CC /\ -u 1 e. CC ) -> ( ( ( A ^ 2 ) - -u 1 ) = 0 <-> ( A ^ 2 ) = -u 1 ) )
5 2 3 4 sylancl 
 |-  ( A e. CC -> ( ( ( A ^ 2 ) - -u 1 ) = 0 <-> ( A ^ 2 ) = -u 1 ) )
6 ax-1cn 
 |-  1 e. CC
7 subneg 
 |-  ( ( ( A ^ 2 ) e. CC /\ 1 e. CC ) -> ( ( A ^ 2 ) - -u 1 ) = ( ( A ^ 2 ) + 1 ) )
8 2 6 7 sylancl 
 |-  ( A e. CC -> ( ( A ^ 2 ) - -u 1 ) = ( ( A ^ 2 ) + 1 ) )
9 addcom 
 |-  ( ( ( A ^ 2 ) e. CC /\ 1 e. CC ) -> ( ( A ^ 2 ) + 1 ) = ( 1 + ( A ^ 2 ) ) )
10 2 6 9 sylancl 
 |-  ( A e. CC -> ( ( A ^ 2 ) + 1 ) = ( 1 + ( A ^ 2 ) ) )
11 8 10 eqtrd 
 |-  ( A e. CC -> ( ( A ^ 2 ) - -u 1 ) = ( 1 + ( A ^ 2 ) ) )
12 11 eqeq1d 
 |-  ( A e. CC -> ( ( ( A ^ 2 ) - -u 1 ) = 0 <-> ( 1 + ( A ^ 2 ) ) = 0 ) )
13 5 12 bitr3d 
 |-  ( A e. CC -> ( ( A ^ 2 ) = -u 1 <-> ( 1 + ( A ^ 2 ) ) = 0 ) )
14 13 necon3bid 
 |-  ( A e. CC -> ( ( A ^ 2 ) =/= -u 1 <-> ( 1 + ( A ^ 2 ) ) =/= 0 ) )
15 14 pm5.32i 
 |-  ( ( A e. CC /\ ( A ^ 2 ) =/= -u 1 ) <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) =/= 0 ) )
16 1 15 bitri 
 |-  ( A e. dom arctan <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) =/= 0 ) )