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