Theorem sincos3rdpi 14802

Description: The sine and cosine of π / 3. (Contributed by Mario Carneiro, 21-May-2016.)

Assertion

Ref	Expression
sincos3rdpi	⊢ ((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π / 3)) = (1 / 2))

Proof of Theorem sincos3rdpi

Step	Hyp	Ref	Expression
1		picn 14746	. . . . . . 7 ⊢ π ∈ ℂ
2		2cn 9031	. . . . . . . 8 ⊢ 2 ∈ ℂ
3		2ap0 9053	. . . . . . . 8 ⊢ 2 # 0
4	2, 3	recclapi 8740	. . . . . . 7 ⊢ (1 / 2) ∈ ℂ
5		3cn 9035	. . . . . . . 8 ⊢ 3 ∈ ℂ
6		3ap0 9056	. . . . . . . 8 ⊢ 3 # 0
7	5, 6	recclapi 8740	. . . . . . 7 ⊢ (1 / 3) ∈ ℂ
8	1, 4, 7	subdii 8405	. . . . . 6 ⊢ (π · ((1 / 2) − (1 / 3))) = ((π · (1 / 2)) − (π · (1 / 3)))
9		halfthird 9567	. . . . . . 7 ⊢ ((1 / 2) − (1 / 3)) = (1 / 6)
10	9	oveq2i 5915	. . . . . 6 ⊢ (π · ((1 / 2) − (1 / 3))) = (π · (1 / 6))
11	8, 10	eqtr3i 2212	. . . . 5 ⊢ ((π · (1 / 2)) − (π · (1 / 3))) = (π · (1 / 6))
12	1, 2, 3	divrecapi 8755	. . . . . 6 ⊢ (π / 2) = (π · (1 / 2))
13	1, 5, 6	divrecapi 8755	. . . . . 6 ⊢ (π / 3) = (π · (1 / 3))
14	12, 13	oveq12i 5916	. . . . 5 ⊢ ((π / 2) − (π / 3)) = ((π · (1 / 2)) − (π · (1 / 3)))
15		6cn 9042	. . . . . 6 ⊢ 6 ∈ ℂ
16		6nn 9125	. . . . . . 7 ⊢ 6 ∈ ℕ
17	16	nnap0i 8991	. . . . . 6 ⊢ 6 # 0
18	1, 15, 17	divrecapi 8755	. . . . 5 ⊢ (π / 6) = (π · (1 / 6))
19	11, 14, 18	3eqtr4i 2220	. . . 4 ⊢ ((π / 2) − (π / 3)) = (π / 6)
20	19	fveq2i 5544	. . 3 ⊢ (cos‘((π / 2) − (π / 3))) = (cos‘(π / 6))
21	1, 5, 6	divclapi 8752	. . . 4 ⊢ (π / 3) ∈ ℂ
22		coshalfpim 14782	. . . 4 ⊢ ((π / 3) ∈ ℂ → (cos‘((π / 2) − (π / 3))) = (sin‘(π / 3)))
23	21, 22	ax-mp 5	. . 3 ⊢ (cos‘((π / 2) − (π / 3))) = (sin‘(π / 3))
24		sincos6thpi 14801	. . . 4 ⊢ ((sin‘(π / 6)) = (1 / 2) ∧ (cos‘(π / 6)) = ((√‘3) / 2))
25	24	simpri 113	. . 3 ⊢ (cos‘(π / 6)) = ((√‘3) / 2)
26	20, 23, 25	3eqtr3i 2218	. 2 ⊢ (sin‘(π / 3)) = ((√‘3) / 2)
27	19	fveq2i 5544	. . 3 ⊢ (sin‘((π / 2) − (π / 3))) = (sin‘(π / 6))
28		sinhalfpim 14780	. . . 4 ⊢ ((π / 3) ∈ ℂ → (sin‘((π / 2) − (π / 3))) = (cos‘(π / 3)))
29	21, 28	ax-mp 5	. . 3 ⊢ (sin‘((π / 2) − (π / 3))) = (cos‘(π / 3))
30	24	simpli 111	. . 3 ⊢ (sin‘(π / 6)) = (1 / 2)
31	27, 29, 30	3eqtr3i 2218	. 2 ⊢ (cos‘(π / 3)) = (1 / 2)
32	26, 31	pm3.2i 272	1 ⊢ ((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π / 3)) = (1 / 2))

Syntax hints:   ∧ wa 104   = wceq 1364   ∈ wcel 2160  ‘cfv 5242  (class class class)co 5904  ℂcc 7849  1c1 7852   · cmul 7856   − cmin 8169   / cdiv 8670  2c2 9011  3c3 9012  6c6 9015  √csqrt 11052  sincsin 11699  cosccos 11700  πcpi 11702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4140  ax-sep 4143  ax-nul 4151  ax-pow 4199  ax-pr 4234  ax-un 4458  ax-setind 4561  ax-iinf 4612  ax-cnex 7942  ax-resscn 7943  ax-1cn 7944  ax-1re 7945  ax-icn 7946  ax-addcl 7947  ax-addrcl 7948  ax-mulcl 7949  ax-mulrcl 7950  ax-addcom 7951  ax-mulcom 7952  ax-addass 7953  ax-mulass 7954  ax-distr 7955  ax-i2m1 7956  ax-0lt1 7957  ax-1rid 7958  ax-0id 7959  ax-rnegex 7960  ax-precex 7961  ax-cnre 7962  ax-pre-ltirr 7963  ax-pre-ltwlin 7964  ax-pre-lttrn 7965  ax-pre-apti 7966  ax-pre-ltadd 7967  ax-pre-mulgt0 7968  ax-pre-mulext 7969  ax-arch 7970  ax-caucvg 7971  ax-pre-suploc 7972  ax-addf 7973  ax-mulf 7974

This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2758  df-sbc 2982  df-csb 3077  df-dif 3150  df-un 3152  df-in 3154  df-ss 3161  df-nul 3442  df-if 3554  df-pw 3599  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3832  df-int 3867  df-iun 3910  df-disj 4003  df-br 4026  df-opab 4087  df-mpt 4088  df-tr 4124  df-id 4318  df-po 4321  df-iso 4322  df-iord 4391  df-on 4393  df-ilim 4394  df-suc 4396  df-iom 4615  df-xp 4657  df-rel 4658  df-cnv 4659  df-co 4660  df-dm 4661  df-rn 4662  df-res 4663  df-ima 4664  df-iota 5203  df-fun 5244  df-fn 5245  df-f 5246  df-f1 5247  df-fo 5248  df-f1o 5249  df-fv 5250  df-isom 5251  df-riota 5859  df-ov 5907  df-oprab 5908  df-mpo 5909  df-of 6114  df-1st 6173  df-2nd 6174  df-recs 6338  df-irdg 6403  df-frec 6424  df-1o 6449  df-oadd 6453  df-er 6567  df-map 6684  df-pm 6685  df-en 6775  df-dom 6776  df-fin 6777  df-sup 7022  df-inf 7023  df-pnf 8035  df-mnf 8036  df-xr 8037  df-ltxr 8038  df-le 8039  df-sub 8171  df-neg 8172  df-reap 8573  df-ap 8580  df-div 8671  df-inn 8961  df-2 9019  df-3 9020  df-4 9021  df-5 9022  df-6 9023  df-7 9024  df-8 9025  df-9 9026  df-n0 9218  df-z 9295  df-uz 9570  df-q 9662  df-rp 9696  df-xneg 9814  df-xadd 9815  df-ioo 9934  df-ioc 9935  df-ico 9936  df-icc 9937  df-fz 10051  df-fzo 10185  df-seqfrec 10491  df-exp 10566  df-fac 10753  df-bc 10775  df-ihash 10803  df-shft 10871  df-cj 10898  df-re 10899  df-im 10900  df-rsqrt 11054  df-abs 11055  df-clim 11334  df-sumdc 11409  df-ef 11703  df-sin 11705  df-cos 11706  df-pi 11708  df-rest 12763  df-topgen 12782  df-psmet 13902  df-xmet 13903  df-met 13904  df-bl 13905  df-mopn 13906  df-top 14019  df-topon 14032  df-bases 14064  df-ntr 14117  df-cn 14209  df-cnp 14210  df-tx 14274  df-cncf 14579  df-limced 14663  df-dvap 14664

This theorem is referenced by: (None)