Metamath Proof Explorer


Theorem onetansqsecsq

Description: Prove the tangent squared secant squared identity ( 1 + ( ( tan A ) ^ 2 ) ) = ( ( sec A ) ^ 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 ) )