Theorem ioo2bl 7864

Description: An open interval of reals in terms of a ball.

Hypothesis

Ref	Expression
remet.1	|- D = ((abs o. - ) |` (RR X. RR))

Assertion

Ref	Expression
ioo2bl	|- ((A e. RR /\ B e. RR /\ A < B) -> (A(,)B) = (((A + B) / 2)( ball ` D)((B - A) / 2)))

Proof of Theorem ioo2bl

Step	Hyp	Ref	Expression
1		remet.1	. . . . . 6 |- D = ((abs o. - ) |` (RR X. RR))
2	1	bl2ioo 7863	. . . . 5 |- ((((B + A) / 2) e. RR /\ ((B - A) / 2) e. RR /\ 0 < ((B - A) / 2)) -> (((B + A) / 2)( ball ` D)((B - A) / 2)) = ((((B + A) / 2) - ((B - A) / 2))(,)(((B + A) / 2) + ((B - A) / 2))))
3		axaddrcl 5252	. . . . . . 7 |- ((B e. RR /\ A e. RR) -> (B + A) e. RR)
4		rehalfclt 5989	. . . . . . 7 |- ((B + A) e. RR -> ((B + A) / 2) e. RR)
5	3, 4	syl 10	. . . . . 6 |- ((B e. RR /\ A e. RR) -> ((B + A) / 2) e. RR)
6	5	3adant3 798	. . . . 5 |- ((B e. RR /\ A e. RR /\ A < B) -> ((B + A) / 2) e. RR)
7		resubclt 5418	. . . . . . 7 |- ((B e. RR /\ A e. RR) -> (B - A) e. RR)
8		rehalfclt 5989	. . . . . . 7 |- ((B - A) e. RR -> ((B - A) / 2) e. RR)
9	7, 8	syl 10	. . . . . 6 |- ((B e. RR /\ A e. RR) -> ((B - A) / 2) e. RR)
10	9	3adant3 798	. . . . 5 |- ((B e. RR /\ A e. RR /\ A < B) -> ((B - A) / 2) e. RR)
11		posdift 5635	. . . . . . . 8 |- ((A e. RR /\ B e. RR) -> (A < B <-> 0 < (B - A)))
12	11	ancoms 436	. . . . . . 7 |- ((B e. RR /\ A e. RR) -> (A < B <-> 0 < (B - A)))
13		halfpos2t 5992	. . . . . . . 8 |- ((B - A) e. RR -> (0 < (B - A) <-> 0 < ((B - A) / 2)))
14	7, 13	syl 10	. . . . . . 7 |- ((B e. RR /\ A e. RR) -> (0 < (B - A) <-> 0 < ((B - A) / 2)))
15	12, 14	bitrd 527	. . . . . 6 |- ((B e. RR /\ A e. RR) -> (A < B <-> 0 < ((B - A) / 2)))
16	15	biimp3a 917	. . . . 5 |- ((B e. RR /\ A e. RR /\ A < B) -> 0 < ((B - A) / 2))
17	2, 6, 10, 16	syl3anc 857	. . . 4 |- ((B e. RR /\ A e. RR /\ A < B) -> (((B + A) / 2)( ball ` D)((B - A) / 2)) = ((((B + A) / 2) - ((B - A) / 2))(,)(((B + A) / 2) + ((B - A) / 2))))
18		pnncant 5460	. . . . . . . . . . 11 |- ((B e. CC /\ A e. CC /\ A e. CC) -> ((B + A) - (B - A)) = (A + A))
19	18	3anidm23 882	. . . . . . . . . 10 |- ((B e. CC /\ A e. CC) -> ((B + A) - (B - A)) = (A + A))
20		2timest 5959	. . . . . . . . . . 11 |- (A e. CC -> (2 x. A) = (A + A))
21	20	adantl 388	. . . . . . . . . 10 |- ((B e. CC /\ A e. CC) -> (2 x. A) = (A + A))
22	19, 21	eqtr4d 1507	. . . . . . . . 9 |- ((B e. CC /\ A e. CC) -> ((B + A) - (B - A)) = (2 x. A))
23	22	opreq1d 3966	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> (((B + A) - (B - A)) / 2) = ((2 x. A) / 2))
24		2cn 5935	. . . . . . . . . 10 |- 2 e. CC
25		2ne0 5945	. . . . . . . . . . 11 |- 2 =/= 0
26		divsubdirt 5739	. . . . . . . . . . 11 |- ((((B + A) e. CC /\ (B - A) e. CC /\ 2 e. CC) /\ 2 =/= 0) -> (((B + A) - (B - A)) / 2) = (((B + A) / 2) - ((B - A) / 2)))
27	25, 26	mpan2 695	. . . . . . . . . 10 |- (((B + A) e. CC /\ (B - A) e. CC /\ 2 e. CC) -> (((B + A) - (B - A)) / 2) = (((B + A) / 2) - ((B - A) / 2)))
28	24, 27	mp3an3 903	. . . . . . . . 9 |- (((B + A) e. CC /\ (B - A) e. CC) -> (((B + A) - (B - A)) / 2) = (((B + A) / 2) - ((B - A) / 2)))
29		axaddcl 5251	. . . . . . . . 9 |- ((B e. CC /\ A e. CC) -> (B + A) e. CC)
30		subclt 5347	. . . . . . . . 9 |- ((B e. CC /\ A e. CC) -> (B - A) e. CC)
31	28, 29, 30	sylanc 471	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> (((B + A) - (B - A)) / 2) = (((B + A) / 2) - ((B - A) / 2)))
32		divcan3t 5726	. . . . . . . . . 10 |- ((2 e. CC /\ A e. CC /\ 2 =/= 0) -> ((2 x. A) / 2) = A)
33	24, 25, 32	mp3an13 905	. . . . . . . . 9 |- (A e. CC -> ((2 x. A) / 2) = A)
34	33	adantl 388	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> ((2 x. A) / 2) = A)
35	23, 31, 34	3eqtr3d 1512	. . . . . . 7 |- ((B e. CC /\ A e. CC) -> (((B + A) / 2) - ((B - A) / 2)) = A)
36		ppncant 5461	. . . . . . . . . . 11 |- ((B e. CC /\ A e. CC /\ B e. CC) -> ((B + A) + (B - A)) = (B + B))
37	36	3anidm13 881	. . . . . . . . . 10 |- ((B e. CC /\ A e. CC) -> ((B + A) + (B - A)) = (B + B))
38		2timest 5959	. . . . . . . . . . 11 |- (B e. CC -> (2 x. B) = (B + B))
39	38	adantr 389	. . . . . . . . . 10 |- ((B e. CC /\ A e. CC) -> (2 x. B) = (B + B))
40	37, 39	eqtr4d 1507	. . . . . . . . 9 |- ((B e. CC /\ A e. CC) -> ((B + A) + (B - A)) = (2 x. B))
41	40	opreq1d 3966	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> (((B + A) + (B - A)) / 2) = ((2 x. B) / 2))
42		divdirt 5721	. . . . . . . . . . 11 |- ((((B + A) e. CC /\ (B - A) e. CC /\ 2 e. CC) /\ 2 =/= 0) -> (((B + A) + (B - A)) / 2) = (((B + A) / 2) + ((B - A) / 2)))
43	25, 42	mpan2 695	. . . . . . . . . 10 |- (((B + A) e. CC /\ (B - A) e. CC /\ 2 e. CC) -> (((B + A) + (B - A)) / 2) = (((B + A) / 2) + ((B - A) / 2)))
44	24, 43	mp3an3 903	. . . . . . . . 9 |- (((B + A) e. CC /\ (B - A) e. CC) -> (((B + A) + (B - A)) / 2) = (((B + A) / 2) + ((B - A) / 2)))
45	44, 29, 30	sylanc 471	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> (((B + A) + (B - A)) / 2) = (((B + A) / 2) + ((B - A) / 2)))
46		divcan3t 5726	. . . . . . . . . 10 |- ((2 e. CC /\ B e. CC /\ 2 =/= 0) -> ((2 x. B) / 2) = B)
47	24, 25, 46	mp3an13 905	. . . . . . . . 9 |- (B e. CC -> ((2 x. B) / 2) = B)
48	47	adantr 389	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> ((2 x. B) / 2) = B)
49	41, 45, 48	3eqtr3d 1512	. . . . . . 7 |- ((B e. CC /\ A e. CC) -> (((B + A) / 2) + ((B - A) / 2)) = B)
50	35, 49	opreq12d 3969	. . . . . 6 |- ((B e. CC /\ A e. CC) -> ((((B + A) / 2) - ((B - A) / 2))(,)(((B + A) / 2) + ((B - A) / 2))) = (A(,)B))
51		recnt 5293	. . . . . 6 |- (B e. RR -> B e. CC)
52		recnt 5293	. . . . . 6 |- (A e. RR -> A e. CC)
53	50, 51, 52	syl2an 454	. . . . 5 |- ((B e. RR /\ A e. RR) -> ((((B + A) / 2) - ((B - A) / 2))(,)(((B + A) / 2) + ((B - A) / 2))) = (A(,)B))
54	53	3adant3 798	. . . 4 |- ((B e. RR /\ A e. RR /\ A < B) -> ((((B + A) / 2) - ((B - A) / 2))(,)(((B + A) / 2) + ((B - A) / 2))) = (A(,)B))
55	17, 54	eqtr2d 1505	. . 3 |- ((B e. RR /\ A e. RR /\ A < B) -> (A(,)B) = (((B + A) / 2)( ball ` D)((B - A) / 2)))
56	55	3com12 836	. 2 |- ((A e. RR /\ B e. RR /\ A < B) -> (A(,)B) = (((B + A) / 2)( ball `