Theorem 2wsms 10712

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		addass 5372	. . . . . . 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 1527	. . . . . 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		divcan2 5789	. . . . . . . 8 |- (((abs` (A - B)) e. CC /\ 2 e. CC /\ 2 =/= 0) -> (2 x. ((abs` (A - B)) / 2)) = (abs` (A - B)))
4		3simpa 797	. . . . . . . . . 10 |- ((A e. RR /\ B e. RR /\ A < B) -> (A e. RR /\ B e. RR))
5		recn 5378	. . . . . . . . . . 11 |- (A e. RR -> A e. CC)
6		recn 5378	. . . . . . . . . . 11 |- (B e. RR -> B e. CC)
7	5, 6	anim12i 340	. . . . . . . . . 10 |- ((A e. RR /\ B e. RR) -> (A e. CC /\ B e. CC))
8		subcl 5432	. . . . . . . . . 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		abscl 6923	. . . . . . . . 9 |- ((A - B) e. CC -> (abs` (A - B)) e. RR)
11		recn 5378	. . . . . . . . 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 6041	. . . . . . . . 9 |- 2 e. CC
14	13	a1i 8	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> 2 e. CC)
15		2ne0 6051	. . . . . . . . 9 |- 2 =/= 0
16	15	a1i 8	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> 2 =/= 0)
17	3, 12, 14, 16	syl3anc 870	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. ((abs` (A - B)) / 2)) = (abs` (A - B)))
18		resubcl 5503	. . . . . . . . 9 |- ((A e. RR /\ B e. RR) -> (A - B) e. RR)
19		recn 5378	. . . . . . . . 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 1595	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. ((abs` (A - B)) / 2)) e. CC)
23	5	3ad2ant1 812	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> A e. CC)
24	6	3ad2ant2 813	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> B e. CC)
25	2, 22, 23, 24	syl3anc 870	. . . . 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		addcom 5370	. . . . . 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		addcl 5366	. . . . . . 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 482	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> ((2 x. ((abs` (A - B)) / 2)) + A) e. CC)
29	26, 28, 24	sylanc 482	. . . . 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 801	. . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ A < B) -> B e. RR)
31		2times 6065	. . . . . . . . 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 4033	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> ((2 x. B) - B) = ((B + B) - B))
34	6, 6	jca 295	. . . . . . . 8 |- (B e. RR -> (B e. CC /\ B e. CC))
35		pncan 5462	. . . . . . . 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		abssuble0 6986	. . . . . . . . . . 11 |- ((A e. RR /\ B e. RR /\ A <_ B) -> (abs` (A - B)) = (B - A))
38		ltle 5585	. . . . . . . . . . . 12 |- ((A e. RR /\ B e. RR) -> (A < B -> A <_ B))
39	38	3impia 842	. . . . . . . . . . 11 |- ((A e. RR /\ B e. RR /\ A < B) -> A <_ B)
40	37, 39	syld3an3 882	. . . . . . . . . 10 |- ((A e. RR /\ B e. RR /\ A < B) -> (abs` (A - B)) = (B - A))
41	17, 40	eqtr2d 1555	. . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ A < B) -> (B - A) = (2 x. ((abs` (A - B)) / 2)))
42		subadd 5440	. . . . . . . . . 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 870	. . . . . . . . 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 202	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (A + (2 x. ((abs` (A - B)) / 2))) = B)
45		addcom 5370	. . . . . . . . 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 482	. . . . . . . 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 1556	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> B = ((2 x. ((abs` (A - B)) / 2)) + A))
48	33, 36, 47	3eqtrd 1558	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> ((2 x. B) - B) = ((2 x. ((abs` (A - B)) / 2)) + A))
49		subadd 5440	. . . . . . 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		mulcl 5368	. . . . . . . . 9 |- ((2 e. CC /\ B e. CC) -> (2 x. B) e. CC)
51	13, 50	mpan 707	. . . . . . . 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 870	. . . . . 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 202	. . . . 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 1558	. . . 4 |- (