HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem cos2pi 14048
Description: The cosine of is 1. (Contributed by Paul Chapman, 23-Jan-2008.)
Assertion
Ref Expression
cos2pi

Proof of Theorem cos2pi
StepHypRef Expression
1 pire 14038 . . . 4
21recni 7299 . . 3
3 cos2t 9793 . . 3
42, 3ax-mp 8 . 2
5 cospi 14044 . . . . . . 7
65oveq1i 5010 . . . . . 6
7 ax-1cn 7267 . . . . . . 7
8 sqneg 8928 . . . . . . 7
97, 8ax-mp 8 . . . . . 6
10 sq1 8959 . . . . . 6
116, 9, 103eqtri 1942 . . . . 5
1211oveq2i 5011 . . . 4
13 2cn 7977 . . . . 5
1413mulid1i 7312 . . . 4
1512, 14eqtri 1938 . . 3
1615oveq1i 5010 . 2
17 1p1e2 7998 . . 3
1813, 7, 7, 17subaddrii 7474 . 2
194, 16, 183eqtri 1942 1
Colors of variables: wff set class
Syntax hints:   wceq 1414   wcel 1416  cfv 4033  (class class class)co 5002  cc 7210  c1 7213   cmul 7217   cmin 7436  cneg 7437  c2 7958  cexp 8872  ccos 9690  cpi 9692
This theorem is referenced by:  ef2pi 14049
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-13 1422  ax-14 1423  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-15 1792  ax-ext 1900  ax-rep 3469  ax-sep 3479  ax-nul 3488  ax-pow 3524  ax-pr 3548  ax-un 3823  ax-inf2 6256  ax-resscn 7266  ax-1cn 7267  ax-icn 7268  ax-addcl 7269  ax-addrcl 7270  ax-mulcl 7271  ax-mulrcl 7272  ax-mulcom 7273  ax-addass 7274  ax-mulass 7275  ax-distr 7276  ax-i2m1 7277  ax-1ne0 7278  ax-1rid 7279  ax-rnegex 7280  ax-rrecex 7281  ax-cnre 7282  ax-pre-lttri 7283  ax-pre-lttrn 7284  ax-pre-ltadd 7285  ax-pre-mulgt0 7286  ax-pre-sup 7287
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1309  df-ex 1336  df-sb 1591  df-eu 1818  df-mo 1819  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-nel 2038  df-ral 2131  df-rex 2132  df-reu 2133  df-rab 2134  df-v 2328  df-sbc 2495  df-csb 2577  df-dif 2639  df-un 2641  df-in 2643  df-ss 2647  df-pss 2649  df-nul 2905  df-if 3012  df-pw 3072  df-sn 3089  df-pr 3090  df-tp 3091  df-op 3092  df-uni 3234  df-int 3268  df-iun 3307  df-br 3384  df-opab 3438  df-tr 3453  df-eprel 3634  df-id 3637  df-po 3642  df-so 3656  df-fr 3676  df-we 3692  df-ord 3708  df-on 3709  df-lim 3710  df-suc 3711  df-om 3988  df-xp 4035  df-rel 4036  df-cnv 4037  df-co 4038  df-dm 4039  df-rn 4040  df-res 4041  df-ima 4042  df-fun 4043  df-fn 4044  df-f 4045  df-f1 4046  df-fo 4047  df-f1o 4048  df-fv 4049  df-iso 4050  df-ov 5004  df-oprab 5005  df-mpt 5165  df-mpt2 5166  df-1st 5296  df-2nd 5297  df-iota 5407  df-rdg 5498  df-1o 5535  df-oadd 5539  df-er 5673  df-map 5765  df-pm 5766  df-en 5830  df-dom 5831  df-sdom 5832  df-fin 5833  df-riota 5987  df-sup 6170  df-card 6420  df-pnf 7325  df-mnf 7326  df-xr 7327  df-ltxr 7328  df-le 7329  df-sub 7455  df-neg 7457  df-div 7682  df-n 7921  df-2 7967  df-3 7968  df-4 7969  df-5 7970  df-6 7971  df-7 7972  df-8 7973  df-9 7974  df-n0 8105  df-z 8150  df-uz 8272  df-q 8354  df-rp 8481  df-ioo 8516  df-ioc 8517  df-ico 8518  df-icc 8519  df-fz 8630  df-fl 8724  df-seq 8819  df-exp 8873  df-fac 9006  df-bc 9031  df-hash 9053  df-shft 9098  df-cj 9120  df-re 9121  df-im 9122  df-sqr 9216  df-abs 9217  df-limsup 9374  df-clim 9390  df-rlim 9391  df-sum 9525  df-ef 9693  df-sin 9695  df-cos 9696  df-pi 9698  df-topgen 10403  df-top 11789  df-bases 11791  df-cn 12024  df-cnp 12025  df-tx 12244  df-met 12506  df-bl 12507  df-opn 12508  df-cncf 13270
Copyright terms: Public domain