Theorem 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 e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
	lawcos.2	|- X = ( abs ` ( B - C ) )
	lawcos.3	|- Y = ( abs ` ( A - C ) )
	lawcos.4	|- Z = ( abs ` ( A - B ) )
	lawcos.5	|- O = ( ( B - C ) F ( A - C ) )
Assertion	pythag	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( Z ^ 2 ) = ( ( X ^ 2 ) + ( Y ^ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lawcos.1	|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2		lawcos.2	|- X = ( abs ` ( B - C ) )
3		lawcos.3	|- Y = ( abs ` ( A - C ) )
4		lawcos.4	|- Z = ( abs ` ( A - B ) )
5		lawcos.5	|- O = ( ( B - C ) F ( A - C ) )
6	1 2 3 4 5	lawcos	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( Z ^ 2 ) = ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) - ( 2 x. ( ( X x. Y ) x. ( cos ` O ) ) ) ) )
7	6	3adant3	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( Z ^ 2 ) = ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) - ( 2 x. ( ( X x. Y ) x. ( cos ` O ) ) ) ) )
8		elpri	|- ( O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } -> ( O = ( _pi / 2 ) \/ O = -u ( _pi / 2 ) ) )
9		fveq2	|- ( O = ( _pi / 2 ) -> ( cos ` O ) = ( cos ` ( _pi / 2 ) ) )
10		coshalfpi	|- ( cos ` ( _pi / 2 ) ) = 0
11	9 10	eqtrdi	|- ( O = ( _pi / 2 ) -> ( cos ` O ) = 0 )
12		fveq2	|- ( O = -u ( _pi / 2 ) -> ( cos ` O ) = ( cos ` -u ( _pi / 2 ) ) )
13		cosneghalfpi	|- ( cos ` -u ( _pi / 2 ) ) = 0
14	12 13	eqtrdi	|- ( O = -u ( _pi / 2 ) -> ( cos ` O ) = 0 )
15	11 14	jaoi	|- ( ( O = ( _pi / 2 ) \/ O = -u ( _pi / 2 ) ) -> ( cos ` O ) = 0 )
16	8 15	syl	|- ( O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } -> ( cos ` O ) = 0 )
17	16	3ad2ant3	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( cos ` O ) = 0 )
18	17	oveq2d	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( ( X x. Y ) x. ( cos ` O ) ) = ( ( X x. Y ) x. 0 ) )
19		subcl	|- ( ( B e. CC /\ C e. CC ) -> ( B - C ) e. CC )
20	19	3adant1	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B - C ) e. CC )
21	20	3ad2ant1	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( B - C ) e. CC )
22	21	abscld	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( abs ` ( B - C ) ) e. RR )
23	22	recnd	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( abs ` ( B - C ) ) e. CC )
24	2 23	eqeltrid	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> X e. CC )
25		subcl	|- ( ( A e. CC /\ C e. CC ) -> ( A - C ) e. CC )
26	25	3adant2	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - C ) e. CC )
27	26	3ad2ant1	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( A - C ) e. CC )
28	27	abscld	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( abs ` ( A - C ) ) e. RR )
29	28	recnd	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( abs ` ( A - C ) ) e. CC )
30	3 29	eqeltrid	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> Y e. CC )
31	24 30	mulcld	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( X x. Y ) e. CC )
32	31	mul01d	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( ( X x. Y ) x. 0 ) = 0 )
33	18 32	eqtrd	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( ( X x. Y ) x. ( cos ` O ) ) = 0 )
34	33	oveq2d	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( 2 x. ( ( X x. Y ) x. ( cos ` O ) ) ) = ( 2 x. 0 ) )
35		2t0e0	|- ( 2 x. 0 ) = 0
36	34 35	eqtrdi	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( 2 x. ( ( X x. Y ) x. ( cos ` O ) ) ) = 0 )
37	36	oveq2d	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) - ( 2 x. ( ( X x. Y ) x. ( cos ` O ) ) ) ) = ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) - 0 ) )
38	24	sqcld	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( X ^ 2 ) e. CC )
39	30	sqcld	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( Y ^ 2 ) e. CC )
40	38 39	addcld	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( ( X ^ 2 ) + ( Y ^ 2 ) ) e. CC )
41	40	subid1d	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) - 0 ) = ( ( X ^ 2 ) + ( Y ^ 2 ) ) )
42	7 37 41	3eqtrd	|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( _pi / 2 ) , -u ( _pi / 2 ) } ) -> ( Z ^ 2 ) = ( ( X ^ 2 ) + ( Y ^ 2 ) ) )