HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem 2wsms 10510
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 axaddass 5257 . . . . . . 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 1477 . . . . . 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 5698 . . . . . . . 8 |- ((2 e. CC /\ (abs` (A - B)) e. CC /\ 2 =/= 0) -> (2 x. ((abs` (A - B)) / 2)) = (abs` (A - B)))
4 2cn 5935 . . . . . . . . 9 |- 2 e. CC
54a1i 8 . . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> 2 e. CC)
6 3simpa 784 . . . . . . . . . 10 |- ((A e. RR /\ B e. RR /\ A < B) -> (A e. RR /\ B e. RR))
7 recnt 5293 . . . . . . . . . . 11 |- (A e. RR -> A e. CC)
8 recnt 5293 . . . . . . . . . . 11 |- (B e. RR -> B e. CC)
97, 8anim12i 333 . . . . . . . . . 10 |- ((A e. RR /\ B e. RR) -> (A e. CC /\ B e. CC))
10 subclt 5347 . . . . . . . . . 10 |- ((A e. CC /\ B e. CC) -> (A - B) e. CC)
116, 9, 103syl 20 . . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ A < B) -> (A - B) e. CC)
12 absclt 6776 . . . . . . . . 9 |- ((A - B) e. CC -> (abs` (A - B)) e. RR)
13 recnt 5293 . . . . . . . . 9 |- ((abs` (A - B)) e. RR -> (abs` (A - B)) e. CC)
1411, 12, 133syl 20 . . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (abs` (A - B)) e. CC)
15 2ne0 5945 . . . . . . . . 9 |- 2 =/= 0
1615a1i 8 . . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> 2 =/= 0)
173, 5, 14, 16syl3anc 857 . . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. ((abs` (A - B)) / 2)) = (abs` (A - B)))
18 resubclt 5418 . . . . . . . . 9 |- ((A e. RR /\ B e. RR) -> (A - B) e. RR)
19 recnt 5293 . . . . . . . . 9 |- ((A - B) e. RR -> (A - B) e. CC)
206, 18, 193syl 20 . . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (A - B) e. CC)
2120, 12, 133syl 20 . . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> (abs` (A - B)) e. CC)
2217, 21eqeltrd 1545 . . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. ((abs` (A - B)) / 2)) e. CC)
2373ad2ant1 799 . . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> A e. CC)
2483ad2ant2 800 . . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> B e. CC)
252, 22, 23, 24syl3anc 857 . . . . 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 5255 . . . . . 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 5251 . . . . . . 7 |- (((2 x. ((abs` (A - B)) / 2)) e. CC /\ A e. CC) -> ((2 x. ((abs` (A - B)) / 2)) + A) e. CC)
2827, 22, 23sylanc 471 . . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> ((2 x. ((abs` (A - B)) / 2)) + A) e. CC)
2926, 28, 24sylanc 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 788 . . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ A < B) -> B e. RR)
31 2timest 5959 . . . . . . . . 9 |- (B e. CC -> (2 x. B) = (B + B))
3230, 8, 313syl 20 . . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. B) = (B + B))
3332opreq1d 3966 . . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> ((2 x. B) - B) = ((B + B) - B))
348, 8jca 288 . . . . . . . 8 |- (B e. RR -> (B e. CC /\ B e. CC))
35 pncant 5377 . . . . . . . 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 abssuble0t 6842 . . . . . . . . . . 11 |- ((A e. RR /\ B e. RR /\ A <_ B) -> (abs` (A - B)) = (B - A))
38 ltlet 5501 . . . . . . . . . . . 12 |- ((A e. RR /\ B e. RR) -> (A < B -> A <_ B))
39383impia 829 . . . . . . . . . . 11 |- ((A e. RR /\ B e. RR /\ A < B) -> A <_ B)
4037, 39syl3dan3 869 . . . . . . . . . 10 |- ((A e. RR /\ B e. RR /\ A < B) -> (abs` (A - B)) = (B - A))
4117, 40eqtr2d 1505 . . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ A < B) -> (B - A) = (2 x. ((abs` (A - B)) / 2)))
42 subaddt 5355 . . . . . . . . . 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 857 . . . . . . . . 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 195 . . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (A + (2 x. ((abs` (A - B)) / 2))) = B)
45 axaddcom 5255 . . . . . . . . 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 471 . . . . . . . 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 1506 . . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> B = ((2 x. ((abs` (A - B)) / 2)) + A))
4833, 36, 473eqtrd 1508 . . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> ((2 x. B) - B) = ((2 x. ((abs` (A - B)) / 2)) + A))
49 subaddt 5355 . . . . . . 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 5253 . . . . . . . . 9 |- ((2 e. CC /\ B e. CC) -> (2 x. B) e. CC)
514, 50mpan 694 . . . . . . . 8 |- (B e. CC -> (2 x. B) e. CC)
5230, 8, 513syl 20 . . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. B) e. CC)
5349, 52, 24, 28syl3anc 857 . . . . . 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 195 . . . . 5 |- ((A e. RR /\ B e. RR /\ A < B) -> (B + ((2 x. ((abs` (A - B)) / 2)) + A)) = (2 x. B))
5525, 29, 543eqtrd 1508 . . . 4 |-