ptolemy - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ptolemy		Structured version Unicode version

Theorem ptolemy 22619

Description: Ptolemy's Theorem. This theorem is named after the Greek astronomer and mathematician Ptolemy (Claudius Ptolemaeus). This particular version is expressed using the sine function. It is proved by expanding all the multiplication of sines to a product of cosines of differences using sinmul 13761, then using algebraic simplification to show that both sides are equal. This formalization is based on the proof in "Trigonometry" by Gelfand and Saul. This is Metamath 100 proof #95. (Contributed by David A. Wheeler, 31-May-2015.)

**Assertion**
Ref	Expression
ptolemy	$/\$ $/\$ $/\$ $/\$

**Proof of Theorem ptolemy**
Step	Hyp	Ref	Expression
1		addcl 9570	. . . . . . . . . . 11 $/\$
2	1	3ad2ant2 1018	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
3	2	coscld 13720	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
4	3	negnegd 9917	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
5		addid2 9758	. . . . . . . . . . . . . . 15
6	5	oveq1d 6297	. . . . . . . . . . . . . 14
7	2, 6	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
8		0cnd 9585	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
9		addcl 9570	. . . . . . . . . . . . . . . 16 $/\$
10	9	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
11	10	3adant3 1016	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
12	8, 11, 2	pnpcan2d 9964	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
13		simp3 998	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13	oveq2d 6298	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15	7, 12, 14	3eqtr3rd 2517	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
16		df-neg 9804	. . . . . . . . . . . 12
17	15, 16	syl6eqr 2526	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
18	17	fveq2d 5868	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
19		cosmpi 22611	. . . . . . . . . . 11
20	2, 19	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
21		cosneg 13736	. . . . . . . . . . 11
22	11, 21	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
23	18, 20, 22	3eqtr3d 2516	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
24	23	negeqd 9810	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
25	4, 24	eqtr3d 2510	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
26	25	oveq2d 6298	. . . . . 6 $/\$ $/\$ $/\$ $/\$
27		subcl 9815	. . . . . . . . . 10 $/\$
28	27	adantl 466	. . . . . . . . 9 $/\$ $/\$ $/\$
29	28	coscld 13720	. . . . . . . 8 $/\$ $/\$ $/\$
30	29	3adant3 1016	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
31	11	coscld 13720	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
32	30, 31	subnegd 9933	. . . . . 6 $/\$ $/\$ $/\$ $/\$
33	26, 32	eqtrd 2508	. . . . 5 $/\$ $/\$ $/\$ $/\$
34	33	oveq1d 6297	. . . 4 $/\$ $/\$ $/\$ $/\$
35	34	oveq2d 6298	. . 3 $/\$ $/\$ $/\$ $/\$
36		subcl 9815	. . . . . . . 8 $/\$
37	36	3ad2ant1 1017	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
38	37	coscld 13720	. . . . . 6 $/\$ $/\$ $/\$ $/\$
39	38, 31	subcld 9926	. . . . 5 $/\$ $/\$ $/\$ $/\$
40	30, 31	addcld 9611	. . . . 5 $/\$ $/\$ $/\$ $/\$
41		2cnne0 10746	. . . . . 6 $/\$
42	41	a1i 11	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
43		divdir 10226	. . . . 5 $/\$ $/\$ $/\$
44	39, 40, 42, 43	syl3anc 1228	. . . 4 $/\$ $/\$ $/\$ $/\$
45	38, 31, 30	nppcan3d 9953	. . . . 5 $/\$ $/\$ $/\$ $/\$
46	45	oveq1d 6297	. . . 4 $/\$ $/\$ $/\$ $/\$
47	44, 46	eqtr3d 2510	. . 3 $/\$ $/\$ $/\$ $/\$
48	35, 47	eqtrd 2508	. 2 $/\$ $/\$ $/\$ $/\$
49		sinmul 13761	. . . 4 $/\$
50	49	3ad2ant1 1017	. . 3 $/\$ $/\$ $/\$ $/\$
51		sinmul 13761	. . . 4 $/\$
52	51	3ad2ant2 1018	. . 3 $/\$ $/\$ $/\$ $/\$
53	50, 52	oveq12d 6300	. 2 $/\$ $/\$ $/\$ $/\$
54		simplr 754	. . . . . . . . 9 $/\$ $/\$ $/\$
55		simpll 753	. . . . . . . . 9 $/\$ $/\$ $/\$
56		simprl 755	. . . . . . . . 9 $/\$ $/\$ $/\$
57	54, 55, 56	pnpcan2d 9964	. . . . . . . 8 $/\$ $/\$ $/\$
58	57	fveq2d 5868	. . . . . . 7 $/\$ $/\$ $/\$
59	58	3adant3 1016	. . . . . 6 $/\$ $/\$ $/\$ $/\$
60	1	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
61	10, 60, 28	3jca 1176	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
62	61	3adant3 1016	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		addass 9575	. . . . . . . . . . 11 $/\$ $/\$
64	62, 63	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
65		oveq1 6289	. . . . . . . . . . 11
66	65	3ad2ant3 1019	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
67		simpl 457	. . . . . . . . . . . . . 14 $/\$
68		simpr 461	. . . . . . . . . . . . . 14 $/\$
69	67, 68, 67	3jca 1176	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
70	69	3ad2ant2 1018	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71		ppncan 9857	. . . . . . . . . . . . 13 $/\$ $/\$
72	71	oveq2d 6298	. . . . . . . . . . . 12 $/\$ $/\$
73	70, 72	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
74		simp1 996	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
75	67, 67	jca 532	. . . . . . . . . . . . 13 $/\$ $/\$
76	75	3ad2ant2 1018	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
77		add4 9791	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
78	74, 76, 77	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
79		addcl 9570	. . . . . . . . . . . . . . 15 $/\$
80	79	ad2ant2r 746	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
81		addcl 9570	. . . . . . . . . . . . . . 15 $/\$
82	81	ad2ant2lr 747	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
83	80, 82	jca 532	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
84	83	3adant3 1016	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
85		addcom 9761	. . . . . . . . . . . 12 $/\$
86	84, 85	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
87	73, 78, 86	3eqtrd 2512	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
88	64, 66, 87	3eqtr3rd 2517	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
89		picn 22583	. . . . . . . . . . 11
90		addcom 9761	. . . . . . . . . . 11 $/\$
91	89, 28, 90	sylancr 663	. . . . . . . . . 10 $/\$ $/\$ $/\$
92	91	3adant3 1016	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
93	88, 92	eqtrd 2508	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
94	93	fveq2d 5868	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
95		cosppi 22613	. . . . . . . . 9
96	28, 95	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$
97	96	3adant3 1016	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
98	94, 97	eqtrd 2508	. . . . . 6 $/\$ $/\$ $/\$ $/\$
99	59, 98	oveq12d 6300	. . . . 5 $/\$ $/\$ $/\$ $/\$
100		subcl 9815	. . . . . . . . . 10 $/\$
101	100	ancoms 453	. . . . . . . . 9 $/\$
102	101	adantr 465	. . . . . . . 8 $/\$ $/\$ $/\$
103	102	coscld 13720	. . . . . . 7 $/\$ $/\$ $/\$
104	103, 29	subnegd 9933	. . . . . 6 $/\$ $/\$ $/\$
105	104	3adant3 1016	. . . . 5 $/\$ $/\$ $/\$ $/\$
106	99, 105	eqtrd 2508	. . . 4 $/\$ $/\$ $/\$ $/\$
107	106	oveq1d 6297	. . 3 $/\$ $/\$ $/\$ $/\$
108		sinmul 13761	. . . . 5 $/\$
109	82, 80, 108	syl2anc 661	. . . 4 $/\$ $/\$ $/\$
110	109	3adant3 1016	. . 3 $/\$ $/\$ $/\$ $/\$
111		cosneg 13736	. . . . . . . 8
112	36, 111	syl 16	. . . . . . 7 $/\$
113		negsubdi2 9874	. . . . . . . 8 $/\$
114	113	fveq2d 5868	. . . . . . 7 $/\$
115	112, 114	eqtr3d 2510	. . . . . 6 $/\$
116	115	3ad2ant1 1017	. . . . 5 $/\$ $/\$ $/\$ $/\$
117	116	oveq1d 6297	. . . 4 $/\$ $/\$ $/\$ $/\$
118	117	oveq1d 6297	. . 3 $/\$ $/\$ $/\$ $/\$
119	107, 110, 118	3eqtr4d 2518	. 2 $/\$ $/\$ $/\$ $/\$
120	48, 53, 119	3eqtr4d 2518	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369 $/\$ w3a 973

wceq 1379

wcel 1767

wne 2662

cfv 5586 (class class class)co 6282

cc 9486

cc0 9488

caddc 9491

cmul 9493

cmin 9801

cneg 9802

cdiv 10202

c2 10581

csin 13654

ccos 13655

cpi 13657

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-inf2 8054 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566 ax-addf 9567 ax-mulf 9568

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-iin 4328 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-of 6522 df-om 6679 df-1st 6781 df-2nd 6782 df-supp 6899 df-recs 7039 df-rdg 7073 df-1o 7127 df-2o 7128 df-oadd 7131 df-er 7308 df-map 7419 df-pm 7420 df-ixp 7467 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-fsupp 7826 df-fi 7867 df-sup 7897 df-oi 7931 df-card 8316 df-cda 8544 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-4 10592 df-5 10593 df-6 10594 df-7 10595 df-8 10596 df-9 10597 df-10 10598 df-n0 10792 df-z 10861 df-dec 10973 df-uz 11079 df-q 11179 df-rp 11217 df-xneg 11314 df-xadd 11315 df-xmul 11316 df-ioo 11529 df-ioc 11530 df-ico 11531 df-icc 11532 df-fz 11669 df-fzo 11789 df-fl 11893 df-seq 12071 df-exp 12130 df-fac 12316 df-bc 12343 df-hash 12368 df-shft 12857 df-cj 12889 df-re 12890 df-im 12891 df-sqrt 13025 df-abs 13026 df-limsup 13250 df-clim 13267 df-rlim 13268 df-sum 13465 df-ef 13658 df-sin 13660 df-cos 13661 df-pi 13663 df-struct 14485 df-ndx 14486 df-slot 14487 df-base 14488 df-sets 14489 df-ress 14490 df-plusg 14561 df-mulr 14562 df-starv 14563 df-sca 14564 df-vsca 14565 df-ip 14566 df-tset 14567 df-ple 14568 df-ds 14570 df-unif 14571 df-hom 14572 df-cco 14573 df-rest 14671 df-topn 14672 df-0g 14690 df-gsum 14691 df-topgen 14692 df-pt 14693 df-prds 14696 df-xrs 14750 df-qtop 14755 df-imas 14756 df-xps 14758 df-mre 14834 df-mrc 14835 df-acs 14837 df-mnd 15725 df-submnd 15775 df-mulg 15858 df-cntz 16147 df-cmn 16593 df-psmet 18179 df-xmet 18180 df-met 18181 df-bl 18182 df-mopn 18183 df-fbas 18184 df-fg 18185 df-cnfld 18189 df-top 19163 df-bases 19165 df-topon 19166 df-topsp 19167 df-cld 19283 df-ntr 19284 df-cls 19285 df-nei 19362 df-lp 19400 df-perf 19401 df-cn 19491 df-cnp 19492 df-haus 19579 df-tx 19795 df-hmeo 19988 df-fil 20079 df-fm 20171 df-flim 20172 df-flf 20173 df-xms 20555 df-ms 20556 df-tms 20557 df-cncf 21114 df-limc 22002 df-dv 22003

This theorem is referenced by: (None)

W3C validator