Theorem mslb1 10509

Description: The midpoint of a segment AB of the real line is on the "left" of B.

Assertion

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

Proof of Theorem mslb1

Step	Hyp	Ref	Expression
1		axdistr 5259	. . . . 5 |- ((2 e. CC /\ A e. CC /\ ((abs` (B - A)) / 2) e. CC) -> (2 x. (A + ((abs` (B - A)) / 2))) = ((2 x. A) + (2 x. ((abs` (B - A)) / 2))))
2		2cn 5935	. . . . . 6 |- 2 e. CC
3	2	a1i 8	. . . . 5 |- ((A e. RR /\ B e. RR /\ A < B) -> 2 e. CC)
4		recnt 5293	. . . . . 6 |- (A e. RR -> A e. CC)
5	4	3ad2ant1 799	. . . . 5 |- ((A e. RR /\ B e. RR /\ A < B) -> A e. CC)
6		3simpa 784	. . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ A < B) -> (A e. RR /\ B e. RR))
7		recnt 5293	. . . . . . . . . . 11 |- (B e. RR -> B e. CC)
8	7, 4	anim12i 333	. . . . . . . . . 10 |- ((B e. RR /\ A e. RR) -> (B e. CC /\ A e. CC))
9	8	ancoms 436	. . . . . . . . 9 |- ((A e. RR /\ B e. RR) -> (B e. CC /\ A e. CC))
10		abssubt 6840	. . . . . . . . 9 |- ((B e. CC /\ A e. CC) -> (abs` (B - A)) = (abs` (A - B)))
11	6, 9, 10	3syl 20	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (abs` (B - A)) = (abs` (A - B)))
12	11	opreq1d 3966	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> ((abs` (B - A)) / 2) = ((abs` (A - B)) / 2))
13		dmse2 10504	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> ((abs` (A - B)) / 2) e. RR+)
14	12, 13	eqeltrd 1545	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> ((abs` (B - A)) / 2) e. RR+)
15		rpret 6230	. . . . . 6 |- (((abs` (B - A)) / 2) e. RR+ -> ((abs` (B - A)) / 2) e. RR)
16		recnt 5293	. . . . . 6 |- (((abs` (B - A)) / 2) e. RR -> ((abs` (B - A)) / 2) e. CC)
17	14, 15, 16	3syl 20	. . . . 5 |- ((A e. RR /\ B e. RR /\ A < B) -> ((abs` (B - A)) / 2) e. CC)
18	1, 3, 5, 17	syl3anc 857	. . . 4 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. (A + ((abs` (B - A)) / 2))) = ((2 x. A) + (2 x. ((abs` (B - A)) / 2))))
19		divcan2t 5698	. . . . . . 7 |- ((2 e. CC /\ (abs` (B - A)) e. CC /\ 2 =/= 0) -> (2 x. ((abs` (B - A)) / 2)) = (abs` (B - A)))
20		subclt 5347	. . . . . . . . 9 |- ((B e. CC /\ A e. CC) -> (B - A) e. CC)
21	6, 9, 20	3syl 20	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (B - A) e. CC)
22		absclt 6776	. . . . . . . 8 |- ((B - A) e. CC -> (abs` (B - A)) e. RR)
23		recnt 5293	. . . . . . . 8 |- ((abs` (B - A)) e. RR -> (abs` (B - A)) e. CC)
24	21, 22, 23	3syl 20	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> (abs` (B - A)) e. CC)
25		2ne0 5945	. . . . . . . 8 |- 2 =/= 0
26	25	a1i 8	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> 2 =/= 0)
27	19, 3, 24, 26	syl3anc 857	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. ((abs` (B - A)) / 2)) = (abs` (B - A)))
28		absidt 6805	. . . . . . 7 |- (((B - A) e. RR /\ 0 <_ (B - A)) -> (abs` (B - A)) = (B - A))
29		resubclt 5418	. . . . . . . . 9 |- ((B e. RR /\ A e. RR) -> (B - A) e. RR)
30	29	ancoms 436	. . . . . . . 8 |- ((A e. RR /\ B e. RR) -> (B - A) e. RR)
31	30	3adant3 798	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> (B - A) e. RR)
32		ltlet 5501	. . . . . . . . 9 |- ((A e. RR /\ B e. RR) -> (A < B -> A <_ B))
33	32	3impia 829	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> A <_ B)
34		pm3.22 438	. . . . . . . . 9 |- ((A e. RR /\ B e. RR) -> (B e. RR /\ A e. RR))
35		subge0t 5655	. . . . . . . . 9 |- ((B e. RR /\ A e. RR) -> (0 <_ (B - A) <-> A <_ B))
36	6, 34, 35	3syl 20	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (0 <_ (B - A) <-> A <_ B))
37	33, 36	mpbird 196	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> 0 <_ (B - A))
38	28, 31, 37	sylanc 471	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> (abs` (B - A)) = (B - A))
39	27, 38	eqtrd 1504	. . . . 5 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. ((abs` (B - A)) / 2)) = (B - A))
40	39	opreq2d 3967	. . . 4 |- ((A e. RR /\ B e. RR /\ A < B) -> ((2 x. A) + (2 x. ((abs` (B - A)) / 2))) = ((2 x. A) + (B - A)))
41	18, 40	eqtrd 1504	. . 3 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. (A + ((abs` (B - A)) / 2))) = ((2 x. A) + (B - A)))
42		axaddcl 5251	. . . . . . 7 |- (((2 x. A) e. CC /\ (B - A) e. CC) -> ((2 x. A) + (B - A)) e. CC)
43		3simp1 787	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> A e. RR)
44		axmulcl 5253	. . . . . . . . 9 |- ((2 e. CC /\ A e. CC) -> (2 x. A) e. CC)
45	2, 44	mpan 694	. . . . . . . 8 |- (A e. CC -> (2 x. A) e. CC)
46	43, 4, 45	3syl 20	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. A) e. CC)
47	42, 46, 21	sylanc 471	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> ((2 x. A) + (B - A)) e. CC)
48		msr4 10506	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> (A + ((abs` (B - A)) / 2)) e. RR)
49		recnt 5293	. . . . . . 7 |- ((A + ((abs` (B - A)) / 2)) e. RR -> (A + ((abs` (B - A)) / 2)) e. CC)
50	6, 48, 49	3syl 20	. . . . . 6 |- ((A e. RR /\ B e. RR /\ A < B) -> (A + ((abs` (B - A)) / 2)) e. CC)
51	47, 3, 50	3jca 818	. . . . 5 |- ((A e. RR /\ B e. RR /\ A < B) -> (((2 x. A) + (B - A)) e. CC /\ 2 e. CC /\ (A + ((abs` (B - A)) / 2)) e. CC))
52	51, 25	jctir 293	. . . 4 |- ((A e. RR /\ B e. RR /\ A < B) -> ((((2 x. A) + (B - A)) e. CC /\ 2 e. CC /\ (A + ((abs` (B - A)) / 2)) e. CC) /\ 2 =/= 0))
53		divmult 5684	. . . 4 |- (((((2 x. A) + (B - A)) e. CC /\ 2 e. CC /\ (A + ((abs` (B - A)) / 2)) e. CC) /\ 2 =/= 0) -> ((((2 x. A) + (B - A)) / 2) = (A + ((abs` (B - A)) / 2)) <-> (2 x. (A + ((abs` (B - A)) / 2))) = ((2 x. A) + (B - A))))
54	52, 53	syl 10	. . 3 |- ((A e. RR /\ B e. RR /\ A < B) -> ((((2 x. A) + (B - A)) / 2) = (A + ((abs` (B - A)) / 2)) <-> (2 x. (A + ((abs` (B - A)) / 2))) = ((2 x. A) + (B - A))))
55	41, 54	mpbird 196	. 2 |- ((A e. RR /\ B e. RR /\ A < B) -> (((2 x. A) + (B - A)) / 2) = (A + ((abs` (B - A)) / 2)))
56		3simp3 789	. . . . 5 |- ((A e. RR /\ B e. RR /\ A < B) -> A < B)
57		2timest 5959	. . . . . . . . 9 |- (A e. CC -> (2 x. A) = (A + A))
58	43, 4, 57	3syl 20	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A < B) -> (2 x. A) = (A + A))
59	58	adantr 389	. . . . . . 7 |- (((A e. RR /\ B e. RR /\ A < B) /\ A < B) -> (2 x. A) = (A + A))
60	59	opreq1d 3966	. . . . . 6 |- (((A e. RR /\ B e. RR /\ A < B) /\ A < B) -> ((