Metamath Proof Explorer


Definition df-sec

Description: Define the secant function. We define it this way for cmpt , which requires the form ( x e. A |-> B ) . The sec function is defined in ISO 80000-2:2009(E) operation 2-13.6 and "NIST Digital Library of Mathematical Functions" section on "Trigonometric Functions" http://dlmf.nist.gov/4.14 . (Contributed by David A. Wheeler, 14-Mar-2014)

Ref Expression
Assertion df-sec sec = ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ ( 1 / ( cos ‘ 𝑥 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csec sec
1 vx 𝑥
2 vy 𝑦
3 cc
4 ccos cos
5 2 cv 𝑦
6 5 4 cfv ( cos ‘ 𝑦 )
7 cc0 0
8 6 7 wne ( cos ‘ 𝑦 ) ≠ 0
9 8 2 3 crab { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 }
10 c1 1
11 cdiv /
12 1 cv 𝑥
13 12 4 cfv ( cos ‘ 𝑥 )
14 10 13 11 co ( 1 / ( cos ‘ 𝑥 ) )
15 1 9 14 cmpt ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ ( 1 / ( cos ‘ 𝑥 ) ) )
16 0 15 wceq sec = ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ ( 1 / ( cos ‘ 𝑥 ) ) )