ptolemy

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 , 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)

		Ref	Expression
	Assertion	ptolemy	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \sin A \sin B + \sin C \sin D = \sin (B + C) \sin (A + C)$

Proof

Step	Hyp	Ref	Expression
1		addcl	$⊢ (C \in ℂ \land D \in ℂ) \to C + D \in ℂ$
2	1	3ad2ant2	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to C + D \in ℂ$
3	2	coscld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (C + D) \in ℂ$
4	3	negnegd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to - (- \cos (C + D)) = \cos (C + D)$
5		addid2	$⊢ C + D \in ℂ \to 0 + C + D = C + D$
6	5	oveq1d	$⊢ C + D \in ℂ \to 0 + (C + D) - (A + B + C + D) = C + D - (A + B + C + D)$
7	2 6	syl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to 0 + (C + D) - (A + B + C + D) = C + D - (A + B + C + D)$
8		0cnd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to 0 \in ℂ$
9		addcl	$⊢ (A \in ℂ \land B \in ℂ) \to A + B \in ℂ$
10	9	adantr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A + B \in ℂ$
11	10	3adant3	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to A + B \in ℂ$
12	8 11 2	pnpcan2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to 0 + (C + D) - (A + B + C + D) = 0 - (A + B)$
13		simp3	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to A + B + C + D = π$
14	13	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to C + D - (A + B + C + D) = C + D - π$
15	7 12 14	3eqtr3rd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to C + D - π = 0 - (A + B)$
16		df-neg	$⊢ - (A + B) = 0 - (A + B)$
17	15 16	eqtr4di	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to C + D - π = - (A + B)$
18	17	fveq2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (C + D - π) = \cos (- (A + B))$
19		cosmpi	$⊢ C + D \in ℂ \to \cos (C + D - π) = - \cos (C + D)$
20	2 19	syl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (C + D - π) = - \cos (C + D)$
21		cosneg	$⊢ A + B \in ℂ \to \cos (- (A + B)) = \cos (A + B)$
22	11 21	syl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (- (A + B)) = \cos (A + B)$
23	18 20 22	3eqtr3d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to - \cos (C + D) = \cos (A + B)$
24	23	negeqd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to - (- \cos (C + D)) = - \cos (A + B)$
25	4 24	eqtr3d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (C + D) = - \cos (A + B)$
26	25	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (C - D) - \cos (C + D) = \cos (C - D) - (- \cos (A + B))$
27		subcl	$⊢ (C \in ℂ \land D \in ℂ) \to C - D \in ℂ$
28	27	adantl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to C - D \in ℂ$
29	28	coscld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to \cos (C - D) \in ℂ$
30	29	3adant3	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (C - D) \in ℂ$
31	11	coscld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (A + B) \in ℂ$
32	30 31	subnegd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (C - D) - (- \cos (A + B)) = \cos (C - D) + \cos (A + B)$
33	26 32	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (C - D) - \cos (C + D) = \cos (C - D) + \cos (A + B)$
34	33	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \frac{\cos (C - D) - \cos (C + D)}{2} = \frac{\cos (C - D) + \cos (A + B)}{2}$
35	34	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to (\frac{\cos (A - B) - \cos (A + B)}{2}) + (\frac{\cos (C - D) - \cos (C + D)}{2}) = (\frac{\cos (A - B) - \cos (A + B)}{2}) + (\frac{\cos (C - D) + \cos (A + B)}{2})$
36		subcl	$⊢ (A \in ℂ \land B \in ℂ) \to A - B \in ℂ$
37	36	3ad2ant1	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to A - B \in ℂ$
38	37	coscld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (A - B) \in ℂ$
39	38 31	subcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (A - B) - \cos (A + B) \in ℂ$
40	30 31	addcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (C - D) + \cos (A + B) \in ℂ$
41		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
42	41	a1i	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to (2 \in ℂ \land 2 \neq 0)$
43		divdir	$⊢ (\cos (A - B) - \cos (A + B) \in ℂ \land \cos (C - D) + \cos (A + B) \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{(\cos (A - B) - \cos (A + B)) + \cos (C - D) + \cos (A + B)}{2} = (\frac{\cos (A - B) - \cos (A + B)}{2}) + (\frac{\cos (C - D) + \cos (A + B)}{2})$
44	39 40 42 43	syl3anc	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \frac{(\cos (A - B) - \cos (A + B)) + \cos (C - D) + \cos (A + B)}{2} = (\frac{\cos (A - B) - \cos (A + B)}{2}) + (\frac{\cos (C - D) + \cos (A + B)}{2})$
45	38 31 30	nppcan3d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to (\cos (A - B) - \cos (A + B)) + \cos (C - D) + \cos (A + B) = \cos (A - B) + \cos (C - D)$
46	45	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \frac{(\cos (A - B) - \cos (A + B)) + \cos (C - D) + \cos (A + B)}{2} = \frac{\cos (A - B) + \cos (C - D)}{2}$
47	44 46	eqtr3d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to (\frac{\cos (A - B) - \cos (A + B)}{2}) + (\frac{\cos (C - D) + \cos (A + B)}{2}) = \frac{\cos (A - B) + \cos (C - D)}{2}$
48	35 47	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to (\frac{\cos (A - B) - \cos (A + B)}{2}) + (\frac{\cos (C - D) - \cos (C + D)}{2}) = \frac{\cos (A - B) + \cos (C - D)}{2}$
49		sinmul	$⊢ (A \in ℂ \land B \in ℂ) \to \sin A \sin B = \frac{\cos (A - B) - \cos (A + B)}{2}$
50	49	3ad2ant1	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \sin A \sin B = \frac{\cos (A - B) - \cos (A + B)}{2}$
51		sinmul	$⊢ (C \in ℂ \land D \in ℂ) \to \sin C \sin D = \frac{\cos (C - D) - \cos (C + D)}{2}$
52	51	3ad2ant2	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \sin C \sin D = \frac{\cos (C - D) - \cos (C + D)}{2}$
53	50 52	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \sin A \sin B + \sin C \sin D = (\frac{\cos (A - B) - \cos (A + B)}{2}) + (\frac{\cos (C - D) - \cos (C + D)}{2})$
54		simplr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B \in ℂ$
55		simpll	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A \in ℂ$
56		simprl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to C \in ℂ$
57	54 55 56	pnpcan2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B + C - (A + C) = B - A$
58	57	fveq2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to \cos (B + C - (A + C)) = \cos (B - A)$
59	58	3adant3	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (B + C - (A + C)) = \cos (B - A)$
60	1	adantl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to C + D \in ℂ$
61	10 60 28	3jca	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + B \in ℂ \land C + D \in ℂ \land C - D \in ℂ)$
62	61	3adant3	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to (A + B \in ℂ \land C + D \in ℂ \land C - D \in ℂ)$
63		addass	$⊢ (A + B \in ℂ \land C + D \in ℂ \land C - D \in ℂ) \to (A + B) + (C + D) + (C - D) = A + B + (C + D) + (C - D)$
64	62 63	syl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to (A + B) + (C + D) + (C - D) = A + B + (C + D) + (C - D)$
65		oveq1	$⊢ A + B + C + D = π \to (A + B) + (C + D) + (C - D) = π + C - D$
66	65	3ad2ant3	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to (A + B) + (C + D) + (C - D) = π + C - D$
67		simpl	$⊢ (C \in ℂ \land D \in ℂ) \to C \in ℂ$
68		simpr	$⊢ (C \in ℂ \land D \in ℂ) \to D \in ℂ$
69	67 68 67	3jca	$⊢ (C \in ℂ \land D \in ℂ) \to (C \in ℂ \land D \in ℂ \land C \in ℂ)$
70	69	3ad2ant2	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to (C \in ℂ \land D \in ℂ \land C \in ℂ)$
71		ppncan	$⊢ (C \in ℂ \land D \in ℂ \land C \in ℂ) \to C + D + (C - D) = C + C$
72	71	oveq2d	$⊢ (C \in ℂ \land D \in ℂ \land C \in ℂ) \to A + B + (C + D) + (C - D) = A + B + C + C$
73	70 72	syl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to A + B + (C + D) + (C - D) = A + B + C + C$
74		simp1	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to (A \in ℂ \land B \in ℂ)$
75	67 67	jca	$⊢ (C \in ℂ \land D \in ℂ) \to (C \in ℂ \land C \in ℂ)$
76	75	3ad2ant2	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to (C \in ℂ \land C \in ℂ)$
77		add4	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land C \in ℂ)) \to A + B + C + C = A + C + B + C$
78	74 76 77	syl2anc	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to A + B + C + C = A + C + B + C$
79		addcl	$⊢ (A \in ℂ \land C \in ℂ) \to A + C \in ℂ$
80	79	ad2ant2r	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A + C \in ℂ$
81		addcl	$⊢ (B \in ℂ \land C \in ℂ) \to B + C \in ℂ$
82	81	ad2ant2lr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B + C \in ℂ$
83	80 82	jca	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A + C \in ℂ \land B + C \in ℂ)$
84	83	3adant3	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to (A + C \in ℂ \land B + C \in ℂ)$
85		addcom	$⊢ (A + C \in ℂ \land B + C \in ℂ) \to A + C + B + C = B + C + A + C$
86	84 85	syl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to A + C + B + C = B + C + A + C$
87	73 78 86	3eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to A + B + (C + D) + (C - D) = B + C + A + C$
88	64 66 87	3eqtr3rd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to B + C + A + C = π + C - D$
89		picn	$⊢ π \in ℂ$
90		addcom	$⊢ (π \in ℂ \land C - D \in ℂ) \to π + C - D = C - D + π$
91	89 28 90	sylancr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to π + C - D = C - D + π$
92	91	3adant3	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to π + C - D = C - D + π$
93	88 92	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to B + C + A + C = C - D + π$
94	93	fveq2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (B + C + A + C) = \cos (C - D + π)$
95		cosppi	$⊢ C - D \in ℂ \to \cos (C - D + π) = - \cos (C - D)$
96	28 95	syl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to \cos (C - D + π) = - \cos (C - D)$
97	96	3adant3	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (C - D + π) = - \cos (C - D)$
98	94 97	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (B + C + A + C) = - \cos (C - D)$
99	59 98	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (B + C - (A + C)) - \cos (B + C + A + C) = \cos (B - A) - (- \cos (C - D))$
100		subcl	$⊢ (B \in ℂ \land A \in ℂ) \to B - A \in ℂ$
101	100	ancoms	$⊢ (A \in ℂ \land B \in ℂ) \to B - A \in ℂ$
102	101	adantr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B - A \in ℂ$
103	102	coscld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to \cos (B - A) \in ℂ$
104	103 29	subnegd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to \cos (B - A) - (- \cos (C - D)) = \cos (B - A) + \cos (C - D)$
105	104	3adant3	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (B - A) - (- \cos (C - D)) = \cos (B - A) + \cos (C - D)$
106	99 105	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (B + C - (A + C)) - \cos (B + C + A + C) = \cos (B - A) + \cos (C - D)$
107	106	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \frac{\cos (B + C - (A + C)) - \cos (B + C + A + C)}{2} = \frac{\cos (B - A) + \cos (C - D)}{2}$
108		sinmul	$⊢ (B + C \in ℂ \land A + C \in ℂ) \to \sin (B + C) \sin (A + C) = \frac{\cos (B + C - (A + C)) - \cos (B + C + A + C)}{2}$
109	82 80 108	syl2anc	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to \sin (B + C) \sin (A + C) = \frac{\cos (B + C - (A + C)) - \cos (B + C + A + C)}{2}$
110	109	3adant3	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \sin (B + C) \sin (A + C) = \frac{\cos (B + C - (A + C)) - \cos (B + C + A + C)}{2}$
111		cosneg	$⊢ A - B \in ℂ \to \cos (- (A - B)) = \cos (A - B)$
112	36 111	syl	$⊢ (A \in ℂ \land B \in ℂ) \to \cos (- (A - B)) = \cos (A - B)$
113		negsubdi2	$⊢ (A \in ℂ \land B \in ℂ) \to - (A - B) = B - A$
114	113	fveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to \cos (- (A - B)) = \cos (B - A)$
115	112 114	eqtr3d	$⊢ (A \in ℂ \land B \in ℂ) \to \cos (A - B) = \cos (B - A)$
116	115	3ad2ant1	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (A - B) = \cos (B - A)$
117	116	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \cos (A - B) + \cos (C - D) = \cos (B - A) + \cos (C - D)$
118	117	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \frac{\cos (A - B) + \cos (C - D)}{2} = \frac{\cos (B - A) + \cos (C - D)}{2}$
119	107 110 118	3eqtr4d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \sin (B + C) \sin (A + C) = \frac{\cos (A - B) + \cos (C - D)}{2}$
120	48 53 119	3eqtr4d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ) \land A + B + C + D = π) \to \sin A \sin B + \sin C \sin D = \sin (B + C) \sin (A + C)$

Metamath Proof Explorer

Theorem ptolemy

Proof