Metamath Proof Explorer

Theorem cosatanne0

Description: The arctangent function has range contained in the domain of the tangent. (Contributed by Mario Carneiro, 3-Apr-2015)

Ref Expression
Assertion cosatanne0 
|- ( A e. dom arctan -> ( cos ` ( arctan ` A ) ) =/= 0 )

Proof

Step Hyp Ref Expression
1 cosatan 
 |-  ( A e. dom arctan -> ( cos ` ( arctan ` A ) ) = ( 1 / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) )
2 ax-1cn 
 |-  1 e. CC
3 atandm4 
 |-  ( A e. dom arctan <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) =/= 0 ) )
4 3 simplbi 
 |-  ( A e. dom arctan -> A e. CC )
5 4 sqcld 
 |-  ( A e. dom arctan -> ( A ^ 2 ) e. CC )
6 addcl 
 |-  ( ( 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( 1 + ( A ^ 2 ) ) e. CC )
7 2 5 6 sylancr 
 |-  ( A e. dom arctan -> ( 1 + ( A ^ 2 ) ) e. CC )
8 7 sqrtcld 
 |-  ( A e. dom arctan -> ( sqrt ` ( 1 + ( A ^ 2 ) ) ) e. CC )
9 7 sqsqrtd 
 |-  ( A e. dom arctan -> ( ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) = ( 1 + ( A ^ 2 ) ) )
10 3 simprbi 
 |-  ( A e. dom arctan -> ( 1 + ( A ^ 2 ) ) =/= 0 )
11 9 10 eqnetrd 
 |-  ( A e. dom arctan -> ( ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) =/= 0 )
12 sqne0 
 |-  ( ( sqrt ` ( 1 + ( A ^ 2 ) ) ) e. CC -> ( ( ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) =/= 0 <-> ( sqrt ` ( 1 + ( A ^ 2 ) ) ) =/= 0 ) )
13 8 12 syl 
 |-  ( A e. dom arctan -> ( ( ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) =/= 0 <-> ( sqrt ` ( 1 + ( A ^ 2 ) ) ) =/= 0 ) )
14 11 13 mpbid 
 |-  ( A e. dom arctan -> ( sqrt ` ( 1 + ( A ^ 2 ) ) ) =/= 0 )
15 8 14 recne0d 
 |-  ( A e. dom arctan -> ( 1 / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) =/= 0 )
16 1 15 eqnetrd 
 |-  ( A e. dom arctan -> ( cos ` ( arctan ` A ) ) =/= 0 )