Theorem ioo2bl 7909

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 7908	. . . . 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 5284	. . . . . . 7 |- ((B e. RR /\ A e. RR) -> (B + A) e. RR)
4		rehalfclt 6036	. . . . . . 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 801	. . . . 5 |- ((B e. RR /\ A e. RR /\ A < B) -> ((B + A) / 2) e. RR)
7		resubclt 5450	. . . . . . 7 |- ((B e. RR /\ A e. RR) -> (B - A) e. RR)
8		rehalfclt 6036	. . . . . . 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 801	. . . . 5 |- ((B e. RR /\ A e. RR /\ A < B) -> ((B - A) / 2) e. RR)
11		posdift 5666	. . . . . . . 8 |- ((A e. RR /\ B e. RR) -> (A < B <-> 0 < (B - A)))
12	11	ancoms 438	. . . . . . 7 |- ((B e. RR /\ A e. RR) -> (A < B <-> 0 < (B - A)))
13		halfpos2t 6039	. . . . . . . 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 530	. . . . . 6 |- ((B e. RR /\ A e. RR) -> (A < B <-> 0 < ((B - A) / 2)))
16	15	biimp3a 921	. . . . 5 |- ((B e. RR /\ A e. RR /\ A < B) -> 0 < ((B - A) / 2))
17	2, 6, 10, 16	syl3anc 860	. . . 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 5492	. . . . . . . . . . 11 |- ((B e. CC /\ A e. CC /\ A e. CC) -> ((B + A) - (B - A)) = (A + A))
19	18	3anidm23 886	. . . . . . . . . 10 |- ((B e. CC /\ A e. CC) -> ((B + A) - (B - A)) = (A + A))
20		2timest 6006	. . . . . . . . . . 11 |- (A e. CC -> (2 x. A) = (A + A))
21	20	adantl 390	. . . . . . . . . 10 |- ((B e. CC /\ A e. CC) -> (2 x. A) = (A + A))
22	19, 21	eqtr4d 1513	. . . . . . . . 9 |- ((B e. CC /\ A e. CC) -> ((B + A) - (B - A)) = (2 x. A))
23	22	opreq1d 3981	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> (((B + A) - (B - A)) / 2) = ((2 x. A) / 2))
24		2cn 5982	. . . . . . . . . 10 |- 2 e. CC
25		2ne0 5992	. . . . . . . . . . 11 |- 2 =/= 0
26		divsubdirtOLD 5777	. . . . . . . . . . 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 698	. . . . . . . . . 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 907	. . . . . . . . 9 |- (((B + A) e. CC /\ (B - A) e. CC) -> (((B + A) - (B - A)) / 2) = (((B + A) / 2) - ((B - A) / 2)))
29		axaddcl 5283	. . . . . . . . 9 |- ((B e. CC /\ A e. CC) -> (B + A) e. CC)
30		subclt 5379	. . . . . . . . 9 |- ((B e. CC /\ A e. CC) -> (B - A) e. CC)
31	28, 29, 30	sylanc 473	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> (((B + A) - (B - A)) / 2) = (((B + A) / 2) - ((B - A) / 2)))
32		divcan3t 5763	. . . . . . . . . 10 |- ((A e. CC /\ 2 e. CC /\ 2 =/= 0) -> ((2 x. A) / 2) = A)
33	24, 25, 32	mp3an23 910	. . . . . . . . 9 |- (A e. CC -> ((2 x. A) / 2) = A)
34	33	adantl 390	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> ((2 x. A) / 2) = A)
35	23, 31, 34	3eqtr3d 1518	. . . . . . 7 |- ((B e. CC /\ A e. CC) -> (((B + A) / 2) - ((B - A) / 2)) = A)
36		ppncant 5493	. . . . . . . . . . 11 |- ((B e. CC /\ A e. CC /\ B e. CC) -> ((B + A) + (B - A)) = (B + B))
37	36	3anidm13 885	. . . . . . . . . 10 |- ((B e. CC /\ A e. CC) -> ((B + A) + (B - A)) = (B + B))
38		2timest 6006	. . . . . . . . . . 11 |- (B e. CC -> (2 x. B) = (B + B))
39	38	adantr 391	. . . . . . . . . 10 |- ((B e. CC /\ A e. CC) -> (2 x. B) = (B + B))
40	37, 39	eqtr4d 1513	. . . . . . . . 9 |- ((B e. CC /\ A e. CC) -> ((B + A) + (B - A)) = (2 x. B))
41	40	opreq1d 3981	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> (((B + A) + (B - A)) / 2) = ((2 x. B) / 2))
42	24, 25	pm3.2i 285	. . . . . . . . . 10 |- (2 e. CC /\ 2 =/= 0)
43		divdirt 5757	. . . . . . . . . 10 |- (((B + A) e. CC /\ (B - A) e. CC /\ (2 e. CC /\ 2 =/= 0)) -> (((B + A) + (B - A)) / 2) = (((B + A) / 2) + ((B - A) / 2)))
44	42, 43	mp3an3 907	. . . . . . . . 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 473	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> (((B + A) + (B - A)) / 2) = (((B + A) / 2) + ((B - A) / 2)))
46		divcan3t 5763	. . . . . . . . . 10 |- ((B e. CC /\ 2 e. CC /\ 2 =/= 0) -> ((2 x. B) / 2) = B)
47	24, 25, 46	mp3an23 910	. . . . . . . . 9 |- (B e. CC -> ((2 x. B) / 2) = B)
48	47	adantr 391	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> ((2 x. B) / 2) = B)
49	41, 45, 48	3eqtr3d 1518	. . . . . . 7 |- ((B e. CC /\ A e. CC) -> (((B + A) / 2) + ((B - A) / 2)) = B)
50	35, 49	opreq12d 3984	. . . . . 6 |- ((B e. CC /\ A e. CC) -> ((((B + A) / 2) - ((B - A) / 2))(,)(((B + A) / 2) + ((B - A) / 2))) = (A(,)B))
51		recnt 5325	. . . . . 6 |- (B e. RR -> B e. CC)
52		recnt 5325	. . . . . 6 |- (A e. RR -> A e. CC)
53	50, 51, 52	syl2an 456	. . . . 5 |- ((B e. RR /\ A e. RR) -> ((((B + A) / 2) - ((B - A) / 2))(,)(((B + A) / 2) + ((B - A) / 2))) = (A(,)B))
54	53	3adant3 801	. . . 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 1511	. . 3 |- ((B e. RR /\ A e. RR /\ A < B) -> (A(,)B) = (((B + A) / 2)( ball ` D)((B - A) / 2)))
56	55	3com12 839	. 2 |- ((A e. RR /\ B e. RR /\ A < B) -> (A(,)B) = (((B + A) / 2)( ball ` D)((B - A) / 2)))
57		axaddcom 5287	. . . . . 6 |- ((A e. CC /\ B e. CC) -> (A + B) = (B + A))
58	57, 52, 51	syl2an 456	. . . . 5 |- ((A e. RR /\