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 ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( 1 + ( ( tan ‘ 𝐴 ) ↑ 2 ) ) = ( ( sec ‘ 𝐴 ) ↑ 2 ) )

Proof

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