Table of ContentsTable of Contents User Sandbox < Previous   Next >
Related theorems
Unicode version

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
StepHypRef 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)))
21eqcomd 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)
75, 6anim12i 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)
94, 7, 83syl 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)
129, 10, 113syl 20 . . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (abs` (A - B)) e. CC)
13 2cn 6041 . . . . . . . . 9 |- 2 e. CC
1413a1i 8 . . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> 2 e. CC)
15 2ne0 6051 . . . . . . . . 9 |- 2 =/= 0
1615a1i 8 . . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> 2 =/= 0)
173, 12, 14, 16syl3anc 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)
204, 18, 193syl 20 . . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (A - B) e. CC)
2120, 10, 113syl 20 . . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> (abs` (A - B)) e. CC)
2217, 21eqeltrd 1595 . . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. ((abs`
(A - B)) / 2)) e. CC)
2353ad2ant1 812 . . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> A e. CC)
2463ad2ant2 813 . . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> B e. CC)
252, 22, 23, 24syl3anc 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)
2827, 22, 23sylanc 482 . . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> ((2 x. ((abs` (A - B)) / 2)) + A) e. CC)
2926, 28, 24sylanc 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))
3230, 6, 313syl 20 . . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. B) = (B + B))
3332opreq1d 4033 . . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> ((2 x. B) - B) = ((B + B) - B))
346, 6jca 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)
3630, 34, 353syl 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))
39383impia 842 . . . . . . . . . . 11 |- ((A e. RR /\ B e. RR /\ A < B) -> A <_ B)
4037, 39syld3an3 882 . . . . . . . . . 10 |- ((A e. RR /\ B e. RR /\ A < B) -> (abs` (A - B)) = (B - A))
4117, 40eqtr2d 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))
4342, 24, 23, 22syl3anc 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))
4441, 43mpbid 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))
4645, 23, 22sylanc 482 . . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (A + (2 x. ((abs` (A - B)) / 2))) = ((2 x. ((abs` (A - B)) / 2)) + A))
4744, 46eqtr3d 1556 . . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> B = ((2 x. ((abs` (A - B)) / 2)) + A))
4833, 36, 473eqtrd 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)
5113, 50mpan 707 . . . . . . . 8 |- (B e. CC -> (2 x. B) e. CC)
5230, 6, 513syl 20 . . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. B) e. CC)
5349, 52, 24, 28syl3anc 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)))
5448, 53mpbid 202 . . . . 5 |- ((A e. RR /\ B e. RR /\ A < B) -> (B + ((2 x. ((abs`
(A - B)) / 2)) + A)) = (2 x. B))
5525, 29, 543eqtrd 1558 . . . 4 |- (