Metamath Proof Explorer

Theorem onetansqsecsq

Description: Prove the tangent squared secant squared identity ( 1 + ( ( tanA ) ^ 2 ) ) = ( ( secA ) ^ 2 ) ) . (Contributed by David A. Wheeler, 25-May-2015)

Ref Expression
Assertion onetansqsecsq 
|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( 1 + ( ( tan ` A ) ^ 2 ) ) = ( ( sec ` A ) ^ 2 ) )

Proof

Step Hyp Ref Expression
1 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
2 sqeq0 
 |-  ( ( cos ` A ) e. CC -> ( ( ( cos ` A ) ^ 2 ) = 0 <-> ( cos ` A ) = 0 ) )
3 1 2 syl 
 |-  ( A e. CC -> ( ( ( cos ` A ) ^ 2 ) = 0 <-> ( cos ` A ) = 0 ) )
4 3 necon3bid 
 |-  ( A e. CC -> ( ( ( cos ` A ) ^ 2 ) =/= 0 <-> ( cos ` A ) =/= 0 ) )
5 4 biimpar 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( cos ` A ) ^ 2 ) =/= 0 )
6 1 sqcld 
 |-  ( A e. CC -> ( ( cos ` A ) ^ 2 ) e. CC )
7 divid 
 |-  ( ( ( ( cos ` A ) ^ 2 ) e. CC /\ ( ( cos ` A ) ^ 2 ) =/= 0 ) -> ( ( ( cos ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) = 1 )
8 6 7 sylan 
 |-  ( ( A e. CC /\ ( ( cos ` A ) ^ 2 ) =/= 0 ) -> ( ( ( cos ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) = 1 )
9 5 8 syldan 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( cos ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) = 1 )
10 9 eqcomd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> 1 = ( ( ( cos ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) )
11 tanval 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )
12 11 oveq1d 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( tan ` A ) ^ 2 ) = ( ( ( sin ` A ) / ( cos ` A ) ) ^ 2 ) )
13 2nn0 
 |-  2 e. NN0
14 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
15 expdiv 
 |-  ( ( ( sin ` A ) e. CC /\ ( ( cos ` A ) e. CC /\ ( cos ` A ) =/= 0 ) /\ 2 e. NN0 ) -> ( ( ( sin ` A ) / ( cos ` A ) ) ^ 2 ) = ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) )
16 14 15 syl3an1 
 |-  ( ( A e. CC /\ ( ( cos ` A ) e. CC /\ ( cos ` A ) =/= 0 ) /\ 2 e. NN0 ) -> ( ( ( sin ` A ) / ( cos ` A ) ) ^ 2 ) = ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) )
17 13 16 mp3an3 
 |-  ( ( A e. CC /\ ( ( cos ` A ) e. CC /\ ( cos ` A ) =/= 0 ) ) -> ( ( ( sin ` A ) / ( cos ` A ) ) ^ 2 ) = ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) )
18 17 3impb 
 |-  ( ( A e. CC /\ ( cos ` A ) e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( sin ` A ) / ( cos ` A ) ) ^ 2 ) = ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) )
19 1 18 syl3an2 
 |-  ( ( A e. CC /\ A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( sin ` A ) / ( cos ` A ) ) ^ 2 ) = ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) )
20 19 3anidm12 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( sin ` A ) / ( cos ` A ) ) ^ 2 ) = ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) )
21 12 20 eqtrd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( tan ` A ) ^ 2 ) = ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) )
22 10 21 oveq12d 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( 1 + ( ( tan ` A ) ^ 2 ) ) = ( ( ( ( cos ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) + ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) ) )
23 14 sqcld 
 |-  ( A e. CC -> ( ( sin ` A ) ^ 2 ) e. CC )
24 divdir 
 |-  ( ( ( ( cos ` A ) ^ 2 ) e. CC /\ ( ( sin ` A ) ^ 2 ) e. CC /\ ( ( ( cos ` A ) ^ 2 ) e. CC /\ ( ( cos ` A ) ^ 2 ) =/= 0 ) ) -> ( ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) / ( ( cos ` A ) ^ 2 ) ) = ( ( ( ( cos ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) + ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) ) )
25 6 24 syl3an1 
 |-  ( ( A e. CC /\ ( ( sin ` A ) ^ 2 ) e. CC /\ ( ( ( cos ` A ) ^ 2 ) e. CC /\ ( ( cos ` A ) ^ 2 ) =/= 0 ) ) -> ( ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) / ( ( cos ` A ) ^ 2 ) ) = ( ( ( ( cos ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) + ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) ) )
26 23 25 syl3an2 
 |-  ( ( A e. CC /\ A e. CC /\ ( ( ( cos ` A ) ^ 2 ) e. CC /\ ( ( cos ` A ) ^ 2 ) =/= 0 ) ) -> ( ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) / ( ( cos ` A ) ^ 2 ) ) = ( ( ( ( cos ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) + ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) ) )
27 26 3anidm12 
 |-  ( ( A e. CC /\ ( ( ( cos ` A ) ^ 2 ) e. CC /\ ( ( cos ` A ) ^ 2 ) =/= 0 ) ) -> ( ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) / ( ( cos ` A ) ^ 2 ) ) = ( ( ( ( cos ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) + ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) ) )
28 27 3impb 
 |-  ( ( A e. CC /\ ( ( cos ` A ) ^ 2 ) e. CC /\ ( ( cos ` A ) ^ 2 ) =/= 0 ) -> ( ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) / ( ( cos ` A ) ^ 2 ) ) = ( ( ( ( cos ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) + ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) ) )
29 6 28 syl3an2 
 |-  ( ( A e. CC /\ A e. CC /\ ( ( cos ` A ) ^ 2 ) =/= 0 ) -> ( ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) / ( ( cos ` A ) ^ 2 ) ) = ( ( ( ( cos ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) + ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) ) )
30 29 3anidm12 
 |-  ( ( A e. CC /\ ( ( cos ` A ) ^ 2 ) =/= 0 ) -> ( ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) / ( ( cos ` A ) ^ 2 ) ) = ( ( ( ( cos ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) + ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) ) )
31 5 30 syldan 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) / ( ( cos ` A ) ^ 2 ) ) = ( ( ( ( cos ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) + ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) ) )
32 22 31 eqtr4d 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( 1 + ( ( tan ` A ) ^ 2 ) ) = ( ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) / ( ( cos ` A ) ^ 2 ) ) )
33 23 6 addcomd 
 |-  ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) )
34 sincossq 
 |-  ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
35 33 34 eqtr3d 
 |-  ( A e. CC -> ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) = 1 )
36 35 oveq1d 
 |-  ( A e. CC -> ( ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) / ( ( cos ` A ) ^ 2 ) ) = ( 1 / ( ( cos ` A ) ^ 2 ) ) )
37 36 adantr 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) / ( ( cos ` A ) ^ 2 ) ) = ( 1 / ( ( cos ` A ) ^ 2 ) ) )
38 32 37 eqtrd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( 1 + ( ( tan ` A ) ^ 2 ) ) = ( 1 / ( ( cos ` A ) ^ 2 ) ) )
39 secval 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( sec ` A ) = ( 1 / ( cos ` A ) ) )
40 39 oveq1d 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( sec ` A ) ^ 2 ) = ( ( 1 / ( cos ` A ) ) ^ 2 ) )
41 ax-1cn 
 |-  1 e. CC
42 expdiv 
 |-  ( ( 1 e. CC /\ ( ( cos ` A ) e. CC /\ ( cos ` A ) =/= 0 ) /\ 2 e. NN0 ) -> ( ( 1 / ( cos ` A ) ) ^ 2 ) = ( ( 1 ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) )
43 41 13 42 mp3an13 
 |-  ( ( ( cos ` A ) e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( 1 / ( cos ` A ) ) ^ 2 ) = ( ( 1 ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) )
44 1 43 sylan 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( 1 / ( cos ` A ) ) ^ 2 ) = ( ( 1 ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) )
45 sq1 
 |-  ( 1 ^ 2 ) = 1
46 45 oveq1i 
 |-  ( ( 1 ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) = ( 1 / ( ( cos ` A ) ^ 2 ) )
47 44 46 eqtrdi 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( 1 / ( cos ` A ) ) ^ 2 ) = ( 1 / ( ( cos ` A ) ^ 2 ) ) )
48 40 47 eqtrd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( sec ` A ) ^ 2 ) = ( 1 / ( ( cos ` A ) ^ 2 ) ) )
49 38 48 eqtr4d 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( 1 + ( ( tan ` A ) ^ 2 ) ) = ( ( sec ` A ) ^ 2 ) )