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

Theorem cos2pi 15284
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 15274 . . . 4
21recni 7995 . . 3
3 cos2t 10604 . . 3
42, 3ax-mp 8 . 2
5 cospi 15280 . . . . . . 7
65oveq1i 5214 . . . . . 6
7 ax-1cn 7963 . . . . . . 7
8 sqneg 9725 . . . . . . 7
97, 8ax-mp 8 . . . . . 6
10 sq1 9756 . . . . . 6
116, 9, 103eqtri 2054 . . . . 5
1211oveq2i 5215 . . . 4
13 2cn 8681 . . . . 5
1413mulid1i 8009 . . . 4
1512, 14eqtri 2050 . . 3
1615oveq1i 5214 . 2
17 1p1e2 8702 . . 3
1813, 7, 7, 17subaddrii 8176 . 2
194, 16, 183eqtri 2054 1
Colors of variables: wff set class
Syntax hints:   wceq 1526   wcel 1528  cfv 4184  (class class class)co 5206  cc 7906  c1 7909   cmul 7913   cmin 8138  cneg 8139  c2 8662  cexp 9666  ccos 10500  cpi 10502
This theorem is referenced by:  ef2pi 15285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-13 1534  ax-14 1535  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-15 1904  ax-ext 2012  ax-rep 3616  ax-sep 3626  ax-nul 3635  ax-pow 3671  ax-pr 3695  ax-un 3973  ax-inf2 6607  ax-resscn 7962  ax-1cn 7963  ax-icn 7964  ax-addcl 7965  ax-addrcl 7966  ax-mulcl 7967  ax-mulrcl 7968  ax-mulcom 7969  ax-addass 7970  ax-mulass 7971  ax-distr 7972  ax-i2m1 7973  ax-1ne0 7974  ax-1rid 7975  ax-rnegex 7976  ax-rrecex 7977  ax-cnre 7978  ax-pre-lttri 7979  ax-pre-lttrn 7980  ax-pre-ltadd 7981  ax-pre-mulgt0 7982  ax-pre-sup 7983  ax-addf 7984  ax-mulf 7985
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1261  df-ex 1448  df-sb 1703  df-eu 1930  df-mo 1931  df-clab 2018  df-cleq 2023  df-clel 2026  df-ne 2149  df-nel 2150  df-ral 2243  df-rex 2244  df-reu 2245  df-rab 2246  df-v 2442  df-sbc 2609  df-csb 2691  df-dif 2753  df-un 2755  df-in 2757  df-ss 2761  df-pss 2763  df-nul 3026  df-if 3135  df-pw 3196  df-sn 3214  df-pr 3215  df-tp 3216  df-op 3217  df-uni 3375  df-int 3409  df-iun 3451  df-iin 3452  df-br 3532  df-opab 3585  df-tr 3600  df-eprel 3783  df-id 3787  df-po 3792  df-so 3806  df-fr 3826  df-we 3842  df-ord 3858  df-on 3859  df-lim 3860  df-suc 3861  df-om 4139  df-xp 4186  df-rel 4187  df-cnv 4188  df-co 4189  df-dm 4190  df-rn 4191  df-res 4192  df-ima 4193  df-fun 4194  df-fn 4195  df-f 4196  df-f1 4197  df-fo 4198  df-f1o 4199  df-fv 4200  df-iso 4201  df-ov 5208  df-oprab 5209  df-mpt 5371  df-mpt2 5372  df-of 5477  df-1st 5521  df-2nd 5522  df-iota 5647  df-recs 5722  df-rdg 5750  df-1o 5798  df-oadd 5802  df-er 5952  df-map 6044  df-pm 6045  df-en 6121  df-dom 6122  df-sdom 6123  df-fin 6124  df-riota 6281  df-sup 6474  df-card 6824  df-pnf 8022  df-mnf 8023  df-xr 8024  df-ltxr 8025  df-le 8026  df-sub 8157  df-neg 8159  df-div 8385  df-n 8625  df-2 8671  df-3 8672  df-4 8673  df-5 8674  df-6 8675  df-7 8676  df-8 8677  df-9 8678  df-n0 8817  df-z 8868  df-uz 9062  df-q 9148  df-rp 9277  df-ioo 9312  df-ioc 9313  df-ico 9314  df-icc 9315  df-fz 9426  df-fl 9512  df-seq 9612  df-exp 9667  df-fac 9804  df-bc 9830  df-hash 9852  df-shft 9901  df-cj 9923  df-re 9924  df-im 9925  df-sqr 10021  df-abs 10022  df-limsup 10180  df-clim 10196  df-rlim 10197  df-sum 10331  df-ef 10503  df-sin 10505  df-cos 10506  df-pi 10508  df-topgen 11262  df-top 13228  df-bases 13230  df-cld 13326  df-ntr 13327  df-cls 13328  df-rest 13424  df-cn 13466  df-cnp 13467  df-lm 13468  df-tx 13687  df-met 13978  df-bl 13979  df-opn 13980  df-cncf 14336  df-dv 14778
Copyright terms: Public domain