Theorem chordthmlem4

Description: If P is on the segment AB and M is the midpoint of AB, then PA x. PB = BM² - PM². If all lengths are reexpressed as fractions of AB, this reduces to the identity X x. ( 1 - X ) = ( 1 / 2 )² - ( ( 1 / 2 ) - X )². (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	chordthmlem4.A	|- ( ph -> A e. CC )
	chordthmlem4.B	|- ( ph -> B e. CC )
	chordthmlem4.X	|- ( ph -> X e. ( 0 [,] 1 ) )
	chordthmlem4.M	|- ( ph -> M = ( ( A + B ) / 2 ) )
	chordthmlem4.P	|- ( ph -> P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) )
Assertion	chordthmlem4	|- ( ph -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( ( abs ` ( B - M ) ) ^ 2 ) - ( ( abs ` ( P - M ) ) ^ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		chordthmlem4.A	|- ( ph -> A e. CC )
2		chordthmlem4.B	|- ( ph -> B e. CC )
3		chordthmlem4.X	|- ( ph -> X e. ( 0 [,] 1 ) )
4		chordthmlem4.M	|- ( ph -> M = ( ( A + B ) / 2 ) )
5		chordthmlem4.P	|- ( ph -> P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) )
6		1red	|- ( ph -> 1 e. RR )
7		unitssre	|- ( 0 [,] 1 ) C_ RR
8	7 3	sseldi	|- ( ph -> X e. RR )
9	6 8	resubcld	|- ( ph -> ( 1 - X ) e. RR )
10	9	recnd	|- ( ph -> ( 1 - X ) e. CC )
11	10	abscld	|- ( ph -> ( abs ` ( 1 - X ) ) e. RR )
12	11	recnd	|- ( ph -> ( abs ` ( 1 - X ) ) e. CC )
13	2 1	subcld	|- ( ph -> ( B - A ) e. CC )
14	13	abscld	|- ( ph -> ( abs ` ( B - A ) ) e. RR )
15	14	recnd	|- ( ph -> ( abs ` ( B - A ) ) e. CC )
16	8	recnd	|- ( ph -> X e. CC )
17	16	abscld	|- ( ph -> ( abs ` X ) e. RR )
18	17	recnd	|- ( ph -> ( abs ` X ) e. CC )
19	12 15 18 15	mul4d	|- ( ph -> ( ( ( abs ` ( 1 - X ) ) x. ( abs ` ( B - A ) ) ) x. ( ( abs ` X ) x. ( abs ` ( B - A ) ) ) ) = ( ( ( abs ` ( 1 - X ) ) x. ( abs ` X ) ) x. ( ( abs ` ( B - A ) ) x. ( abs ` ( B - A ) ) ) ) )
20	16 1	mulcld	|- ( ph -> ( X x. A ) e. CC )
21	10 2	mulcld	|- ( ph -> ( ( 1 - X ) x. B ) e. CC )
22	20 21	addcld	|- ( ph -> ( ( X x. A ) + ( ( 1 - X ) x. B ) ) e. CC )
23	5 22	eqeltrd	|- ( ph -> P e. CC )
24	1 23 2 16	affineequiv2	|- ( ph -> ( P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) <-> ( P - A ) = ( ( 1 - X ) x. ( B - A ) ) ) )
25	5 24	mpbid	|- ( ph -> ( P - A ) = ( ( 1 - X ) x. ( B - A ) ) )
26	25	fveq2d	|- ( ph -> ( abs ` ( P - A ) ) = ( abs ` ( ( 1 - X ) x. ( B - A ) ) ) )
27	10 13	absmuld	|- ( ph -> ( abs ` ( ( 1 - X ) x. ( B - A ) ) ) = ( ( abs ` ( 1 - X ) ) x. ( abs ` ( B - A ) ) ) )
28	26 27	eqtrd	|- ( ph -> ( abs ` ( P - A ) ) = ( ( abs ` ( 1 - X ) ) x. ( abs ` ( B - A ) ) ) )
29	23 2	abssubd	|- ( ph -> ( abs ` ( P - B ) ) = ( abs ` ( B - P ) ) )
30	1 23 2 16	affineequiv	|- ( ph -> ( P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) <-> ( B - P ) = ( X x. ( B - A ) ) ) )
31	5 30	mpbid	|- ( ph -> ( B - P ) = ( X x. ( B - A ) ) )
32	31	fveq2d	|- ( ph -> ( abs ` ( B - P ) ) = ( abs ` ( X x. ( B - A ) ) ) )
33	16 13	absmuld	|- ( ph -> ( abs ` ( X x. ( B - A ) ) ) = ( ( abs ` X ) x. ( abs ` ( B - A ) ) ) )
34	29 32 33	3eqtrd	|- ( ph -> ( abs ` ( P - B ) ) = ( ( abs ` X ) x. ( abs ` ( B - A ) ) ) )
35	28 34	oveq12d	|- ( ph -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( ( abs ` ( 1 - X ) ) x. ( abs ` ( B - A ) ) ) x. ( ( abs ` X ) x. ( abs ` ( B - A ) ) ) ) )
36	15	sqvald	|- ( ph -> ( ( abs ` ( B - A ) ) ^ 2 ) = ( ( abs ` ( B - A ) ) x. ( abs ` ( B - A ) ) ) )
37	36	oveq2d	|- ( ph -> ( ( ( abs ` ( 1 - X ) ) x. ( abs ` X ) ) x. ( ( abs ` ( B - A ) ) ^ 2 ) ) = ( ( ( abs ` ( 1 - X ) ) x. ( abs ` X ) ) x. ( ( abs ` ( B - A ) ) x. ( abs ` ( B - A ) ) ) ) )
38	19 35 37	3eqtr4d	|- ( ph -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( ( abs ` ( 1 - X ) ) x. ( abs ` X ) ) x. ( ( abs ` ( B - A ) ) ^ 2 ) ) )
39	6	recnd	|- ( ph -> 1 e. CC )
40	39	halfcld	|- ( ph -> ( 1 / 2 ) e. CC )
41	40	sqcld	|- ( ph -> ( ( 1 / 2 ) ^ 2 ) e. CC )
42	6	rehalfcld	|- ( ph -> ( 1 / 2 ) e. RR )
43	42 8	resubcld	|- ( ph -> ( ( 1 / 2 ) - X ) e. RR )
44	43	recnd	|- ( ph -> ( ( 1 / 2 ) - X ) e. CC )
45	44	abscld	|- ( ph -> ( abs ` ( ( 1 / 2 ) - X ) ) e. RR )
46	45	recnd	|- ( ph -> ( abs ` ( ( 1 / 2 ) - X ) ) e. CC )
47	46	sqcld	|- ( ph -> ( ( abs ` ( ( 1 / 2 ) - X ) ) ^ 2 ) e. CC )
48	15	sqcld	|- ( ph -> ( ( abs ` ( B - A ) ) ^ 2 ) e. CC )
49	41 47 48	subdird	|- ( ph -> ( ( ( ( 1 / 2 ) ^ 2 ) - ( ( abs ` ( ( 1 / 2 ) - X ) ) ^ 2 ) ) x. ( ( abs ` ( B - A ) ) ^ 2 ) ) = ( ( ( ( 1 / 2 ) ^ 2 ) x. ( ( abs ` ( B - A ) ) ^ 2 ) ) - ( ( ( abs ` ( ( 1 / 2 ) - X ) ) ^ 2 ) x. ( ( abs ` ( B - A ) ) ^ 2 ) ) ) )
50		subsq	|- ( ( ( 1 / 2 ) e. CC /\ ( ( 1 / 2 ) - X ) e. CC ) -> ( ( ( 1 / 2 ) ^ 2 ) - ( ( ( 1 / 2 ) - X ) ^ 2 ) ) = ( ( ( 1 / 2 ) + ( ( 1 / 2 ) - X ) ) x. ( ( 1 / 2 ) - ( ( 1 / 2 ) - X ) ) ) )
51	40 44 50	syl2anc	|- ( ph -> ( ( ( 1 / 2 ) ^ 2 ) - ( ( ( 1 / 2 ) - X ) ^ 2 ) ) = ( ( ( 1 / 2 ) + ( ( 1 / 2 ) - X ) ) x. ( ( 1 / 2 ) - ( ( 1 / 2 ) - X ) ) ) )
52	40 40 16	addsubassd	|- ( ph -> ( ( ( 1 / 2 ) + ( 1 / 2 ) ) - X ) = ( ( 1 / 2 ) + ( ( 1 / 2 ) - X ) ) )
53	39	2halvesd	|- ( ph -> ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
54	53	oveq1d	|- ( ph -> ( ( ( 1 / 2 ) + ( 1 / 2 ) ) - X ) = ( 1 - X ) )
55	52 54	eqtr3d	|- ( ph -> ( ( 1 / 2 ) + ( ( 1 / 2 ) - X ) ) = ( 1 - X ) )
56	40 16	nncand	|- ( ph -> ( ( 1 / 2 ) - ( ( 1 / 2 ) - X ) ) = X )
57	55 56	oveq12d	|- ( ph -> ( ( ( 1 / 2 ) + ( ( 1 / 2 ) - X ) ) x. ( ( 1 / 2 ) - ( ( 1 / 2 ) - X ) ) ) = ( ( 1 - X ) x. X ) )
58	51 57	eqtr2d	|- ( ph -> ( ( 1 - X ) x. X ) = ( ( ( 1 / 2 ) ^ 2 ) - ( ( ( 1 / 2 ) - X ) ^ 2 ) ) )
59		elicc01	|- ( X e. ( 0 [,] 1 ) <-> ( X e. RR /\ 0 <_ X /\ X <_ 1 ) )
60	3 59	sylib	|- ( ph -> ( X e. RR /\ 0 <_ X /\ X <_ 1 ) )
61	60	simp3d	|- ( ph -> X <_ 1 )
62	8 6 61	abssubge0d	|- ( ph -> ( abs ` ( 1 - X ) ) = ( 1 - X ) )
63	60	simp2d	|- ( ph -> 0 <_ X )
64	8 63	absidd	|- ( ph -> ( abs ` X ) = X )
65	62 64	oveq12d	|- ( ph -> ( ( abs ` ( 1 - X ) ) x. ( abs ` X ) ) = ( ( 1 - X ) x. X ) )
66		absresq	|- ( ( ( 1 / 2 ) - X ) e. RR -> ( ( abs ` ( ( 1 / 2 ) - X ) ) ^ 2 ) = ( ( ( 1 / 2 ) - X ) ^ 2 ) )
67	43 66	syl	|- ( ph -> ( ( abs ` ( ( 1 / 2 ) - X ) ) ^ 2 ) = ( ( ( 1 / 2 ) - X ) ^ 2 ) )
68	67	oveq2d	|- ( ph -> ( ( ( 1 / 2 ) ^ 2 ) - ( ( abs ` ( ( 1 / 2 ) - X ) ) ^ 2 ) ) = ( ( ( 1 / 2 ) ^ 2 ) - ( ( ( 1 / 2 ) - X ) ^ 2 ) ) )
69	58 65 68	3eqtr4d	|- ( ph -> ( ( abs ` ( 1 - X ) ) x. ( abs ` X ) ) = ( ( ( 1 / 2 ) ^ 2 ) - ( ( abs ` ( ( 1 / 2 ) - X ) ) ^ 2 ) ) )
70	69	oveq1d	|- ( ph -> ( ( ( abs ` ( 1 - X ) ) x. ( abs ` X ) ) x. ( ( abs ` ( B - A ) ) ^ 2 ) ) = ( ( ( ( 1 / 2 ) ^ 2 ) - ( ( abs ` ( ( 1 / 2 ) - X ) ) ^ 2 ) ) x. ( ( abs ` ( B - A ) ) ^ 2 ) ) )
71		2cnd	|- ( ph -> 2 e. CC )
72		2ne0	|- 2 =/= 0
73	72	a1i	|- ( ph -> 2 =/= 0 )
74	2 71 73	divcan4d	|- ( ph -> ( ( B x. 2 ) / 2 ) = B )
75	2	times2d	|- ( ph -> ( B x. 2 ) = ( B + B ) )
76	75	oveq1d	|- ( ph -> ( ( B x. 2 ) / 2 ) = ( ( B + B ) / 2 ) )
77	74 76	eqtr3d	|- ( ph -> B = ( ( B + B ) / 2 ) )
78	77 4	oveq12d	|- ( ph -> ( B - M ) = ( ( ( B + B ) / 2 ) - ( ( A + B ) / 2 ) ) )
79	2 2	addcld	|- ( ph -> ( B + B ) e. CC )
80	1 2	addcld	|- ( ph -> ( A + B ) e. CC )
81	79 80 71 73	divsubdird	|- ( ph -> ( ( ( B + B ) - ( A + B ) ) / 2 ) = ( ( ( B + B ) / 2 ) - ( ( A + B ) / 2 ) ) )
82	2 1 2	pnpcan2d	|- ( ph -> ( ( B + B ) - ( A + B ) ) = ( B - A ) )
83	82	oveq1d	|- ( ph -> ( ( ( B + B ) - ( A + B ) ) / 2 ) = ( ( B - A ) / 2 ) )
84	78 81 83	3eqtr2d	|- ( ph -> ( B - M ) = ( ( B - A ) / 2 ) )
85	13 71 73	divrec2d	|- ( ph -> ( ( B - A ) / 2 ) = ( ( 1 / 2 ) x. ( B - A ) ) )
86	84 85	eqtrd	|- ( ph -> ( B - M ) = ( ( 1 / 2 ) x. ( B - A ) ) )
87	86	fveq2d	|- ( ph -> ( abs ` ( B - M ) ) = ( abs ` ( ( 1 / 2 ) x. ( B - A ) ) ) )
88	40 13	absmuld	|- ( ph -> ( abs ` ( ( 1 / 2 ) x. ( B - A ) ) ) = ( ( abs ` ( 1 / 2 ) ) x. ( abs ` ( B - A ) ) ) )
89		0red	|- ( ph -> 0 e. RR )
90		halfgt0	|- 0 < ( 1 / 2 )
91	90	a1i	|- ( ph -> 0 < ( 1 / 2 ) )
92	89 42 91	ltled	|- ( ph -> 0 <_ ( 1 / 2 ) )
93	42 92	absidd	|- ( ph -> ( abs ` ( 1 / 2 ) ) = ( 1 / 2 ) )
94	93	oveq1d	|- ( ph -> ( ( abs ` ( 1 / 2 ) ) x. ( abs ` ( B - A ) ) ) = ( ( 1 / 2 ) x. ( abs ` ( B - A ) ) ) )
95	87 88 94	3eqtrd	|- ( ph -> ( abs ` ( B - M ) ) = ( ( 1 / 2 ) x. ( abs ` ( B - A ) ) ) )
96	95	oveq1d	|- ( ph -> ( ( abs ` ( B - M ) ) ^ 2 ) = ( ( ( 1 / 2 ) x. ( abs ` ( B - A ) ) ) ^ 2 ) )
97	40 15	sqmuld	|- ( ph -> ( ( ( 1 / 2 ) x. ( abs ` ( B - A ) ) ) ^ 2 ) = ( ( ( 1 / 2 ) ^ 2 ) x. ( ( abs ` ( B - A ) ) ^ 2 ) ) )
98	96 97	eqtrd	|- ( ph -> ( ( abs ` ( B - M ) ) ^ 2 ) = ( ( ( 1 / 2 ) ^ 2 ) x. ( ( abs ` ( B - A ) ) ^ 2 ) ) )
99	40 16 13	subdird	|- ( ph -> ( ( ( 1 / 2 ) - X ) x. ( B - A ) ) = ( ( ( 1 / 2 ) x. ( B - A ) ) - ( X x. ( B - A ) ) ) )
100	86 31	oveq12d	|- ( ph -> ( ( B - M ) - ( B - P ) ) = ( ( ( 1 / 2 ) x. ( B - A ) ) - ( X x. ( B - A ) ) ) )
101	80	halfcld	|- ( ph -> ( ( A + B ) / 2 ) e. CC )
102	4 101	eqeltrd	|- ( ph -> M e. CC )
103	2 102 23	nnncan1d	|- ( ph -> ( ( B - M ) - ( B - P ) ) = ( P - M ) )
104	99 100 103	3eqtr2rd	|- ( ph -> ( P - M ) = ( ( ( 1 / 2 ) - X ) x. ( B - A ) ) )
105	104	fveq2d	|- ( ph -> ( abs ` ( P - M ) ) = ( abs ` ( ( ( 1 / 2 ) - X ) x. ( B - A ) ) ) )
106	44 13	absmuld	|- ( ph -> ( abs ` ( ( ( 1 / 2 ) - X ) x. ( B - A ) ) ) = ( ( abs ` ( ( 1 / 2 ) - X ) ) x. ( abs ` ( B - A ) ) ) )
107	105 106	eqtrd	|- ( ph -> ( abs ` ( P - M ) ) = ( ( abs ` ( ( 1 / 2 ) - X ) ) x. ( abs ` ( B - A ) ) ) )
108	107	oveq1d	|- ( ph -> ( ( abs ` ( P - M ) ) ^ 2 ) = ( ( ( abs ` ( ( 1 / 2 ) - X ) ) x. ( abs ` ( B - A ) ) ) ^ 2 ) )
109	46 15	sqmuld	|- ( ph -> ( ( ( abs ` ( ( 1 / 2 ) - X ) ) x. ( abs ` ( B - A ) ) ) ^ 2 ) = ( ( ( abs ` ( ( 1 / 2 ) - X ) ) ^ 2 ) x. ( ( abs ` ( B - A ) ) ^ 2 ) ) )
110	108 109	eqtrd	|- ( ph -> ( ( abs ` ( P - M ) ) ^ 2 ) = ( ( ( abs ` ( ( 1 / 2 ) - X ) ) ^ 2 ) x. ( ( abs ` ( B - A ) ) ^ 2 ) ) )
111	98 110	oveq12d	|- ( ph -> ( ( ( abs ` ( B - M ) ) ^ 2 ) - ( ( abs ` ( P - M ) ) ^ 2 ) ) = ( ( ( ( 1 / 2 ) ^ 2 ) x. ( ( abs ` ( B - A ) ) ^ 2 ) ) - ( ( ( abs ` ( ( 1 / 2 ) - X ) ) ^ 2 ) x. ( ( abs ` ( B - A ) ) ^ 2 ) ) ) )
112	49 70 111	3eqtr4rd	|- ( ph -> ( ( ( abs ` ( B - M ) ) ^ 2 ) - ( ( abs ` ( P - M ) ) ^ 2 ) ) = ( ( ( abs ` ( 1 - X ) ) x. ( abs ` X ) ) x. ( ( abs ` ( B - A ) ) ^ 2 ) ) )
113	38 112	eqtr4d	|- ( ph -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( ( abs ` ( B - M ) ) ^ 2 ) - ( ( abs ` ( P - M ) ) ^ 2 ) ) )