Theorem tanval 15477

Description: Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.)

Assertion

Ref	Expression
tanval	⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))

Proof of Theorem tanval

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 485	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → 𝐴 ∈ ℂ)
2		coscl 15476	. . . . 5 ⊢ (𝐴 ∈ ℂ → (cos‘𝐴) ∈ ℂ)
3	2	anim1i 616	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → ((cos‘𝐴) ∈ ℂ ∧ (cos‘𝐴) ≠ 0))
4		eldifsn 4716	. . . 4 ⊢ ((cos‘𝐴) ∈ (ℂ ∖ {0}) ↔ ((cos‘𝐴) ∈ ℂ ∧ (cos‘𝐴) ≠ 0))
5	3, 4	sylibr 236	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (cos‘𝐴) ∈ (ℂ ∖ {0}))
6		cosf 15474	. . . 4 ⊢ cos:ℂ⟶ℂ
7		ffn 6511	. . . 4 ⊢ (cos:ℂ⟶ℂ → cos Fn ℂ)
8		elpreima 6825	. . . 4 ⊢ (cos Fn ℂ → (𝐴 ∈ (◡cos “ (ℂ ∖ {0})) ↔ (𝐴 ∈ ℂ ∧ (cos‘𝐴) ∈ (ℂ ∖ {0}))))
9	6, 7, 8	mp2b 10	. . 3 ⊢ (𝐴 ∈ (◡cos “ (ℂ ∖ {0})) ↔ (𝐴 ∈ ℂ ∧ (cos‘𝐴) ∈ (ℂ ∖ {0})))
10	1, 5, 9	sylanbrc 585	. 2 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → 𝐴 ∈ (◡cos “ (ℂ ∖ {0})))
11		fveq2 6667	. . . 4 ⊢ (𝑥 = 𝐴 → (sin‘𝑥) = (sin‘𝐴))
12		fveq2 6667	. . . 4 ⊢ (𝑥 = 𝐴 → (cos‘𝑥) = (cos‘𝐴))
13	11, 12	oveq12d 7171	. . 3 ⊢ (𝑥 = 𝐴 → ((sin‘𝑥) / (cos‘𝑥)) = ((sin‘𝐴) / (cos‘𝐴)))
14		df-tan 15421	. . 3 ⊢ tan = (𝑥 ∈ (◡cos “ (ℂ ∖ {0})) ↦ ((sin‘𝑥) / (cos‘𝑥)))
15		ovex 7186	. . 3 ⊢ ((sin‘𝐴) / (cos‘𝐴)) ∈ V
16	13, 14, 15	fvmpt 6765	. 2 ⊢ (𝐴 ∈ (◡cos “ (ℂ ∖ {0})) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
17	10, 16	syl 17	1 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1536   ∈ wcel 2113   ≠ wne 3015   ∖ cdif 3930  {csn 4564  ^◡ccnv 5551   “ cima 5555   Fn wfn 6347  ⟶wf 6348  ‘cfv 6352  (class class class)co 7153  ℂcc 10532  0cc0 10534   / cdiv 11294  sincsin 15413  cosccos 15414  tanctan 15415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5327  ax-un 7458  ax-inf2 9101  ax-cnex 10590  ax-resscn 10591  ax-1cn 10592  ax-icn 10593  ax-addcl 10594  ax-addrcl 10595  ax-mulcl 10596  ax-mulrcl 10597  ax-mulcom 10598  ax-addass 10599  ax-mulass 10600  ax-distr 10601  ax-i2m1 10602  ax-1ne0 10603  ax-1rid 10604  ax-rnegex 10605  ax-rrecex 10606  ax-cnre 10607  ax-pre-lttri 10608  ax-pre-lttrn 10609  ax-pre-ltadd 10610  ax-pre-mulgt0 10611  ax-pre-sup 10612  ax-addf 10613  ax-mulf 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1539  df-fal 1549  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-nel 3123  df-ral 3142  df-rex 3143  df-reu 3144  df-rmo 3145  df-rab 3146  df-v 3495  df-sbc 3771  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4465  df-pw 4538  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4836  df-int 4874  df-iun 4918  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5457  df-eprel 5462  df-po 5471  df-so 5472  df-fr 5511  df-se 5512  df-we 5513  df-xp 5558  df-rel 5559  df-cnv 5560  df-co 5561  df-dm 5562  df-rn 5563  df-res 5564  df-ima 5565  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-isom 6361  df-riota 7111  df-ov 7156  df-oprab 7157  df-mpo 7158  df-om 7578  df-1st 7686  df-2nd 7687  df-wrecs 7944  df-recs 8005  df-rdg 8043  df-1o 8099  df-oadd 8103  df-er 8286  df-pm 8406  df-en 8507  df-dom 8508  df-sdom 8509  df-fin 8510  df-sup 8903  df-inf 8904  df-oi 8971  df-card 9365  df-pnf 10674  df-mnf 10675  df-xr 10676  df-ltxr 10677  df-le 10678  df-sub 10869  df-neg 10870  df-div 11295  df-nn 11636  df-2 11698  df-3 11699  df-n0 11896  df-z 11980  df-uz 12242  df-rp 12388  df-ico 12742  df-fz 12891  df-fzo 13032  df-fl 13160  df-seq 13368  df-exp 13428  df-fac 13632  df-hash 13689  df-shft 14422  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-limsup 14824  df-clim 14841  df-rlim 14842  df-sum 15039  df-ef 15417  df-cos 15420  df-tan 15421

This theorem is referenced by:  tancl  15478  tanval2  15482  retancl  15491  tanneg  15497  tan0  15500  retanhcl  15508  tanhlt1  15509  tanaddlem  15515  tanadd  15516  tanrpcl  25088  tangtx  25089  tan4thpi  25098  tanord1  25119  atandmtan  25496  atantan  25499  basellem3  25658  basellem8  25663  tan2h  34922  reccot  44931  rectan  44932  onetansqsecsq  44934