Theorem 2wsms 10630

Description: Two ways to state the midpoint of a segment.

Assertion

Ref	Expression
2wsms	|- ((A e. RR /\ B e. RR /\ A < B) -> ((A + B) / 2) = (B - ((abs` (A - B)) / 2)))

Proof of Theorem 2wsms

Step	Hyp	Ref	Expression
1		axaddass 5277	. . . . . . 7 |- (((2 x. ((abs` (A - B)) / 2)) e. CC /\ A e. CC /\ B e. CC) -> (((2 x. ((abs` (A - B)) / 2)) + A) + B) = ((2 x. ((abs` (A - B)) / 2)) + (A + B)))
2	1	eqcomd 1480	. . . . . 6 |- (((2 x. ((abs` (A - B)) / 2)) e. CC /\ A e. CC /\ B e. CC) -> ((2 x. ((abs` (A - B)) / 2)) + (A + B)) = (((2 x. ((abs` (A - B)) / 2)) + A) + B))
3		divcan2t 5726	. . . . . . . 8 |- (((abs` (A - B)) e. CC /\ 2 e. CC /\ 2 =/= 0) -> (2 x. ((abs` (A - B)) / 2)) = (abs` (A - B)))
4		3simpa 785	. . . . . . . . . 10 |- ((A e. RR /\ B e. RR /\ A < B) -> (A e. RR /\ B e. RR))
5		recnt 5313	. . . . . . . . . . 11 |- (A e. RR -> A e. CC)
6		recnt 5313	. . . . . . . . . . 11 |- (B e. RR -> B e. CC)
7	5, 6	anim12i 333	. . . . . . . . . 10 |- ((A e. RR /\ B e. RR) -> (A e. CC /\ B e. CC))
8		subclt 5367	. . . . . . . . . 10 |- ((A e. CC /\ B e. CC) -> (A - B) e. CC)
9	4, 7, 8	3syl 20	. . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ A < B) -> (A - B) e. CC)
10		absclt 6833	. . . . . . . . 9 |- ((A - B) e. CC -> (abs` (A - B)) e. RR)
11		recnt 5313	. . . . . . . . 9 |- ((abs` (A - B)) e. RR -> (abs` (A - B)) e. CC)
12	9, 10, 11	3syl 20	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (abs` (A - B)) e. CC)
13		2cn 5980	. . . . . . . . 9 |- 2 e. CC
14	13	a1i 8	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> 2 e. CC)
15		2ne0 5990	. . . . . . . . 9 |- 2 =/= 0
16	15	a1i 8	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> 2 =/= 0)
17	3, 12, 14, 16	syl3anc 858	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. ((abs` (A - B)) / 2)) = (abs` (A - B)))
18		resubclt 5438	. . . . . . . . 9 |- ((A e. RR /\ B e. RR) -> (A - B) e. RR)
19		recnt 5313	. . . . . . . . 9 |- ((A - B) e. RR -> (A - B) e. CC)
20	4, 18, 19	3syl 20	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (A - B) e. CC)
21	20, 10, 11	3syl 20	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> (abs` (A - B)) e. CC)
22	17, 21	eqeltrd 1548	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. ((abs` (A - B)) / 2)) e. CC)
23	5	3ad2ant1 800	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> A e. CC)
24	6	3ad2ant2 801	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> B e. CC)
25	2, 22, 23, 24	syl3anc 858	. . . . 5 |- ((A e. RR /\ B e. RR /\ A < B) -> ((2 x. ((abs` (A - B)) / 2)) + (A + B)) = (((2 x. ((abs` (A - B)) / 2)) + A) + B))
26		axaddcom 5275	. . . . . 6 |- ((((2 x. ((abs` (A - B)) / 2)) + A) e. CC /\ B e. CC) -> (((2 x. ((abs` (A - B)) / 2)) + A) + B) = (B + ((2 x. ((abs` (A - B)) / 2)) + A)))
27		axaddcl 5271	. . . . . . 7 |- (((2 x. ((abs` (A - B)) / 2)) e. CC /\ A e. CC) -> ((2 x. ((abs` (A - B)) / 2)) + A) e. CC)
28	27, 22, 23	sylanc 471	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> ((2 x. ((abs` (A - B)) / 2)) + A) e. CC)
29	26, 28, 24	sylanc 471	. . . . 5 |- ((A e. RR /\ B e. RR /\ A < B) -> (((2 x. ((abs` (A - B)) / 2)) + A) + B) = (B + ((2 x. ((abs` (A - B)) / 2)) + A)))
30		3simp2 789	. . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ A < B) -> B e. RR)
31		2timest 6004	. . . . . . . . 9 |- (B e. CC -> (2 x. B) = (B + B))
32	30, 6, 31	3syl 20	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. B) = (B + B))
33	32	opreq1d 3975	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> ((2 x. B) - B) = ((B + B) - B))
34	6, 6	jca 288	. . . . . . . 8 |- (B e. RR -> (B e. CC /\ B e. CC))
35		pncant 5397	. . . . . . . 8 |- ((B e. CC /\ B e. CC) -> ((B + B) - B) = B)
36	30, 34, 35	3syl 20	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> ((B + B) - B) = B)
37		abssuble0t 6896	. . . . . . . . . . 11 |- ((A e. RR /\ B e. RR /\ A <_ B) -> (abs` (A - B)) = (B - A))
38		ltlet 5520	. . . . . . . . . . . 12 |- ((A e. RR /\ B e. RR) -> (A < B -> A <_ B))
39	38	3impia 830	. . . . . . . . . . 11 |- ((A e. RR /\ B e. RR /\ A < B) -> A <_ B)
40	37, 39	syld3an3 870	. . . . . . . . . 10 |- ((A e. RR /\ B e. RR /\ A < B) -> (abs` (A - B)) = (B - A))
41	17, 40	eqtr2d 1508	. . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ A < B) -> (B - A) = (2 x. ((abs` (A - B)) / 2)))
42		subaddt 5375	. . . . . . . . . 10 |- ((B e. CC /\ A e. CC /\ (2 x. ((abs` (A - B)) / 2)) e. CC) -> ((B - A) = (2 x. ((abs` (A - B)) / 2)) <-> (A + (2 x. ((abs` (A - B)) / 2))) = B))
43	42, 24, 23, 22	syl3anc 858	. . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ A < B) -> ((B - A) = (2 x. ((abs` (A - B)) / 2)) <-> (A + (2 x. ((abs` (A - B)) / 2))) = B))
44	41, 43	mpbid 195	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (A + (2 x. ((abs` (A - B)) / 2))) = B)
45		axaddcom 5275	. . . . . . . . 9 |- ((A e. CC /\ (2 x. ((abs` (A - B)) / 2)) e. CC) -> (A + (2 x. ((abs` (A - B)) / 2))) = ((2 x. ((abs` (A - B)) / 2)) + A))
46	45, 23, 22	sylanc 471	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (A + (2 x. ((abs` (A - B)) / 2))) = ((2 x. ((abs` (A - B)) / 2)) + A))
47	44, 46	eqtr3d 1509	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> B = ((2 x. ((abs` (A - B)) / 2)) + A))
48	33, 36, 47	3eqtrd 1511	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> ((2 x. B) - B) = ((2 x. ((abs` (A - B)) / 2)) + A))
49		subaddt 5375	. . . . . . 7 |- (((2 x. B) e. CC /\ B e. CC /\ ((2 x. ((abs` (A - B)) / 2)) + A) e. CC) -> (((2 x. B) - B) = ((2 x. ((abs` (A - B)) / 2)) + A) <-> (B + ((2 x. ((abs` (A - B)) / 2)) + A)) = (2 x. B)))
50		axmulcl 5273	. . . . . . . . 9 |- ((2 e. CC /\ B e. CC) -> (2 x. B) e. CC)
51	13, 50	mpan 695	. . . . . . . 8 |- (B e. CC -> (2 x. B) e. CC)
52	30, 6, 51	3syl 20	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. B) e. CC)
53	49, 52, 24, 28	syl3anc 858	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> (((2 x. B) - B) = ((2 x. ((abs` (A - B)) / 2)) + A) <-> (B + ((2 x. ((abs` (A - B)) / 2)) + A)) = (2 x. B)))
54	48, 53	mpbid 195	. . . . 5 |- ((A e. RR /\ B e. RR /\ A < B) -> (B + ((2 x. ((abs` (A - B)) / 2)) + A)) = (2 x. B))
55	25, 29, 54	3eqtrd 1511	. . . 4