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

Theorem cos2pi 14299
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 14289 . . . 4
21recni 7344 . . 3
3 cos2t 9943 . . 3
42, 3ax-mp 8 . 2
5 cospi 14295 . . . . . . 7
65oveq1i 5040 . . . . . 6
7 ax-1cn 7312 . . . . . . 7
8 sqneg 9069 . . . . . . 7
97, 8ax-mp 8 . . . . . 6
10 sq1 9100 . . . . . 6
116, 9, 103eqtri 1942 . . . . 5
1211oveq2i 5041 . . . 4
13 2cn 8030 . . . . 5
1413mulid1i 7358 . . . 4
1512, 14eqtri 1938 . . 3
1615oveq1i 5040 . 2
17 1p1e2 8051 . . 3
1813, 7, 7, 17subaddrii 7525 . 2
194, 16, 183eqtri 1942 1
Colors of variables: wff set class
Syntax hints:   wceq 1414   wcel 1416  cfv 4046  (class class class)co 5032  cc 7255  c1 7258   cmul 7262   cmin 7487  cneg 7488  c2 8011  cexp 9012  ccos 9840  cpi 9842
This theorem is referenced by:  ef2pi 14300
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 3481  ax-sep 3491  ax-nul 3500  ax-pow 3536  ax-pr 3560  ax-un 3836  ax-inf2 6289  ax-resscn 7311  ax-1cn 7312  ax-icn 7313  ax-addcl 7314  ax-addrcl 7315  ax-mulcl 7316  ax-mulrcl 7317  ax-mulcom 7318  ax-addass 7319  ax-mulass 7320  ax-distr 7321  ax-i2m1 7322  ax-1ne0 7323  ax-1rid 7324  ax-rnegex 7325  ax-rrecex 7326  ax-cnre 7327  ax-pre-lttri 7328  ax-pre-lttrn 7329  ax-pre-ltadd 7330  ax-pre-mulgt0 7331  ax-pre-sup 7332
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 2329  df-sbc 2496  df-csb 2578  df-dif 2640  df-un 2642  df-in 2644  df-ss 2648  df-pss 2650  df-nul 2908  df-if 3015  df-pw 3075  df-sn 3092  df-pr 3093  df-tp 3094  df-op 3095  df-uni 3247  df-int 3281  df-iun 3320  df-br 3397  df-opab 3450  df-tr 3465  df-eprel 3646  df-id 3650  df-po 3655  df-so 3669  df-fr 3689  df-we 3705  df-ord 3721  df-on 3722  df-lim 3723  df-suc 3724  df-om 4001  df-xp 4048  df-rel 4049  df-cnv 4050  df-co 4051  df-dm 4052  df-rn 4053  df-res 4054  df-ima 4055  df-fun 4056  df-fn 4057  df-f 4058  df-f1 4059  df-fo 4060  df-f1o 4061  df-fv 4062  df-iso 4063  df-ov 5034  df-oprab 5035  df-mpt 5196  df-mpt2 5197  df-1st 5333  df-2nd 5334  df-iota 5444  df-rdg 5535  df-1o 5572  df-oadd 5576  df-er 5710  df-map 5802  df-pm 5803  df-en 5869  df-dom 5870  df-sdom 5871  df-fin 5872  df-riota 6022  df-sup 6201  df-card 6455  df-pnf 7371  df-mnf 7372  df-xr 7373  df-ltxr 7374  df-le 7375  df-sub 7506  df-neg 7508  df-div 7734  df-n 7974  df-2 8020  df-3 8021  df-4 8022  df-5 8023  df-6 8024  df-7 8025  df-8 8026  df-9 8027  df-n0 8166  df-z 8217  df-uz 8411  df-q 8497  df-rp 8625  df-ioo 8660  df-ioc 8661  df-ico 8662  df-icc 8663  df-fz 8774  df-fl 8860  df-seq 8959  df-exp 9013  df-fac 9148  df-bc 9173  df-hash 9195  df-shft 9243  df-cj 9265  df-re 9266  df-im 9267  df-sqr 9361  df-abs 9362  df-limsup 9522  df-clim 9538  df-rlim 9539  df-sum 9673  df-ef 9843  df-sin 9845  df-cos 9846  df-pi 9848  df-topgen 10596  df-top 12043  df-bases 12045  df-cn 12278  df-cnp 12279  df-tx 12499  df-met 12761  df-bl 12762  df-opn 12763  df-cncf 13520
Copyright terms: Public domain