pythag

Description: Pythagorean theorem. Given three distinct points A, B, and C that form a right triangle (with the right angle at C), prove a relationship between their segment lengths. This theorem is expressed using the complex number plane as a plane, where F is the signed angle construct (as used in ang180 ), X is the distance of line segment BC, Y is the distance of line segment AC, Z is the distance of line segment AB (the hypotenuse), and O is the signed right angle m/__ BCA. We use the law of cosines lawcos to prove this, along with simple trigonometry facts like coshalfpi and cosneg . (Contributed by David A. Wheeler, 13-Jun-2015)

	Ref	Expression
Hypotheses	lawcos.1	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
	lawcos.2	$⊢ X = \|B - C\|$
	lawcos.3	$⊢ Y = \|A - C\|$
	lawcos.4	$⊢ Z = \|A - B\|$
	lawcos.5	$⊢ O = (B - C) F (A - C)$
Assertion	pythag	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to Z^{2} = X^{2} + Y^{2}$

Proof

Step	Hyp	Ref	Expression
1		lawcos.1	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
2		lawcos.2	$⊢ X = \|B - C\|$
3		lawcos.3	$⊢ Y = \|A - C\|$
4		lawcos.4	$⊢ Z = \|A - B\|$
5		lawcos.5	$⊢ O = (B - C) F (A - C)$
6	1 2 3 4 5	lawcos	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to Z^{2} = X^{2} + Y^{2} - 2 X Y \cos O$
7	6	3adant3	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to Z^{2} = X^{2} + Y^{2} - 2 X Y \cos O$
8		elpri	$⊢ O \in \{\frac{π}{2}, - \frac{π}{2}\} \to (O = \frac{π}{2} \lor O = - \frac{π}{2})$
9		fveq2	$⊢ O = \frac{π}{2} \to \cos O = \cos (\frac{π}{2})$
10		coshalfpi	$⊢ \cos (\frac{π}{2}) = 0$
11	9 10	eqtrdi	$⊢ O = \frac{π}{2} \to \cos O = 0$
12		fveq2	$⊢ O = - \frac{π}{2} \to \cos O = \cos (- \frac{π}{2})$
13		cosneghalfpi	$⊢ \cos (- \frac{π}{2}) = 0$
14	12 13	eqtrdi	$⊢ O = - \frac{π}{2} \to \cos O = 0$
15	11 14	jaoi	$⊢ (O = \frac{π}{2} \lor O = - \frac{π}{2}) \to \cos O = 0$
16	8 15	syl	$⊢ O \in \{\frac{π}{2}, - \frac{π}{2}\} \to \cos O = 0$
17	16	3ad2ant3	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to \cos O = 0$
18	17	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to X Y \cos O = X Y \cdot 0$
19		subcl	$⊢ (B \in ℂ \land C \in ℂ) \to B - C \in ℂ$
20	19	3adant1	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to B - C \in ℂ$
21	20	3ad2ant1	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to B - C \in ℂ$
22	21	abscld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to \|B - C\| \in ℝ$
23	22	recnd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to \|B - C\| \in ℂ$
24	2 23	eqeltrid	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to X \in ℂ$
25		subcl	$⊢ (A \in ℂ \land C \in ℂ) \to A - C \in ℂ$
26	25	3adant2	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A - C \in ℂ$
27	26	3ad2ant1	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to A - C \in ℂ$
28	27	abscld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to \|A - C\| \in ℝ$
29	28	recnd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to \|A - C\| \in ℂ$
30	3 29	eqeltrid	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to Y \in ℂ$
31	24 30	mulcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to X Y \in ℂ$
32	31	mul01d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to X Y \cdot 0 = 0$
33	18 32	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to X Y \cos O = 0$
34	33	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to 2 X Y \cos O = 2 \cdot 0$
35		2t0e0	$⊢ 2 \cdot 0 = 0$
36	34 35	eqtrdi	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to 2 X Y \cos O = 0$
37	36	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to X^{2} + Y^{2} - 2 X Y \cos O = X^{2} + Y^{2} - 0$
38	24	sqcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to X^{2} \in ℂ$
39	30	sqcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to Y^{2} \in ℂ$
40	38 39	addcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to X^{2} + Y^{2} \in ℂ$
41	40	subid1d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to X^{2} + Y^{2} - 0 = X^{2} + Y^{2}$
42	7 37 41	3eqtrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C) \land O \in \{\frac{π}{2}, - \frac{π}{2}\}) \to Z^{2} = X^{2} + Y^{2}$

Metamath Proof Explorer

Theorem pythag

Proof