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

Theorem cos2pi 12683
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 12673 . . . 4
21recni 7093 . . 3
3 cos2t 9513 . . 3
42, 3ax-mp 8 . 2
5 cospi 12679 . . . . . . 7
65oveq1i 4932 . . . . . 6
7 ax-1cn 7061 . . . . . . 7
8 sqneg 8692 . . . . . . 7
97, 8ax-mp 8 . . . . . 6
10 sq1 8723 . . . . . 6
116, 9, 103eqtri 1953 . . . . 5
1211oveq2i 4933 . . . 4
13 2cn 7769 . . . . 5
1413mulid1i 7106 . . . 4
1512, 14eqtri 1949 . . 3
1615oveq1i 4932 . 2
17 1p1e2 7790 . . 3
1813, 7, 7, 17subaddrii 7267 . 2
194, 16, 183eqtri 1953 1
Colors of variables: wff set class
Syntax hints:   wceq 1425   wcel 1427  cfv 4003  (class class class)co 4924  cc 7004  c1 7007   cmul 7011   cmin 7229  cneg 7230  c2 7750  cexp 8636  ccos 9422  cpi 9424
This theorem is referenced by:  ef2pi 12684
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-13 1433  ax-14 1434  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-15 1803  ax-ext 1911  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3795  ax-inf2 6078  ax-resscn 7060  ax-1cn 7061  ax-icn 7062  ax-addcl 7063  ax-addrcl 7064  ax-mulcl 7065  ax-mulrcl 7066  ax-mulcom 7067  ax-addass 7068  ax-mulass 7069  ax-distr 7070  ax-i2m1 7071  ax-1ne0 7072  ax-1rid 7073  ax-rnegex 7074  ax-rrecex 7075  ax-cnre 7076  ax-pre-lttri 7077  ax-pre-lttrn 7078  ax-pre-ltadd 7079  ax-pre-mulgt0 7080  ax-pre-sup 7081
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3or 913  df-3an 914  df-tru 1320  df-ex 1347  df-sb 1602  df-eu 1829  df-mo 1830  df-clab 1917  df-cleq 1922  df-clel 1925  df-ne 2049  df-nel 2050  df-ral 2142  df-rex 2143  df-reu 2144  df-rab 2145  df-v 2337  df-sbc 2502  df-csb 2577  df-dif 2637  df-un 2639  df-in 2641  df-ss 2643  df-pss 2645  df-nul 2900  df-if 3005  df-pw 3063  df-sn 3080  df-pr 3081  df-tp 3082  df-op 3083  df-uni 3214  df-int 3248  df-iun 3286  df-br 3359  df-opab 3413  df-tr 3428  df-eprel 3608  df-id 3611  df-po 3616  df-so 3630  df-fr 3649  df-we 3665  df-ord 3681  df-on 3682  df-lim 3683  df-suc 3684  df-om 3958  df-xp 4005  df-rel 4006  df-cnv 4007  df-co 4008  df-dm 4009  df-rn 4010  df-res 4011  df-ima 4012  df-fun 4013  df-fn 4014  df-f 4015  df-f1 4016  df-fo 4017  df-f1o 4018  df-fv 4019  df-iso 4020  df-ov 4926  df-oprab 4927  df-mpt 5063  df-mpt2 5064  df-1st 5173  df-2nd 5174  df-iota 5277  df-rdg 5363  df-1o 5400  df-oadd 5404  df-er 5537  df-map 5625  df-pm 5626  df-en 5682  df-dom 5683  df-sdom 5684  df-fin 5685  df-riota 5825  df-sup 5999  df-card 6242  df-pnf 7119  df-mnf 7120  df-xr 7121  df-ltxr 7122  df-le 7123  df-sub 7248  df-neg 7250  df-div 7474  df-n 7713  df-2 7759  df-3 7760  df-4 7761  df-5 7762  df-6 7763  df-7 7764  df-8 7765  df-9 7766  df-n0 7883  df-z 7927  df-uz 8047  df-q 8129  df-rp 8254  df-ioo 8289  df-ioc 8290  df-ico 8291  df-icc 8292  df-fz 8399  df-fl 8492  df-seq 8585  df-exp 8637  df-fac 8770  df-bc 8795  df-hash 8816  df-shft 8849  df-cj 8871  df-re 8872  df-im 8873  df-sqr 8965  df-abs 8966  df-limsup 9120  df-clim 9136  df-rlim 9137  df-sum 9262  df-ef 9425  df-sin 9427  df-cos 9428  df-pi 9430  df-top 10891  df-bases 10893  df-topgen 10894  df-cn 11112  df-cnp 11113  df-tx 11184  df-met 11329  df-bl 11330  df-opn 11331  df-cncf 12062
Copyright terms: Public domain