Theorem ioo2bl 7997

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 7996	. . . . 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		readdcl 5367	. . . . . . 7 |- ((B e. RR /\ A e. RR) -> (B + A) e. RR)
4		rehalfcl 6095	. . . . . . 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 811	. . . . 5 |- ((B e. RR /\ A e. RR /\ A < B) -> ((B + A) / 2) e. RR)
7		resubcl 5503	. . . . . . 7 |- ((B e. RR /\ A e. RR) -> (B - A) e. RR)
8		rehalfcl 6095	. . . . . . 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 811	. . . . 5 |- ((B e. RR /\ A e. RR /\ A < B) -> ((B - A) / 2) e. RR)
11		posdif 5719	. . . . . . . 8 |- ((A e. RR /\ B e. RR) -> (A < B <-> 0 < (B - A)))
12	11	ancoms 447	. . . . . . 7 |- ((B e. RR /\ A e. RR) -> (A < B <-> 0 < (B - A)))
13		halfpos2 6098	. . . . . . . 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 539	. . . . . 6 |- ((B e. RR /\ A e. RR) -> (A < B <-> 0 < ((B - A) / 2)))
16	15	biimp3a 931	. . . . 5 |- ((B e. RR /\ A e. RR /\ A < B) -> 0 < ((B - A) / 2))
17	2, 6, 10, 16	syl3anc 870	. . . 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		pnncan 5545	. . . . . . . . . . 11 |- ((B e. CC /\ A e. CC /\ A e. CC) -> ((B + A) - (B - A)) = (A + A))
19	18	3anidm23 896	. . . . . . . . . 10 |- ((B e. CC /\ A e. CC) -> ((B + A) - (B - A)) = (A + A))
20		2times 6065	. . . . . . . . . . 11 |- (A e. CC -> (2 x. A) = (A + A))
21	20	adantl 397	. . . . . . . . . 10 |- ((B e. CC /\ A e. CC) -> (2 x. A) = (A + A))
22	19, 21	eqtr4d 1557	. . . . . . . . 9 |- ((B e. CC /\ A e. CC) -> ((B + A) - (B - A)) = (2 x. A))
23	22	opreq1d 4033	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> (((B + A) - (B - A)) / 2) = ((2 x. A) / 2))
24		2cn 6041	. . . . . . . . . 10 |- 2 e. CC
25		2ne0 6051	. . . . . . . . . . 11 |- 2 =/= 0
26		divsubdirOLD 5833	. . . . . . . . . . 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 708	. . . . . . . . . 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 917	. . . . . . . . 9 |- (((B + A) e. CC /\ (B - A) e. CC) -> (((B + A) - (B - A)) / 2) = (((B + A) / 2) - ((B - A) / 2)))
29		addcl 5366	. . . . . . . . 9 |- ((B e. CC /\ A e. CC) -> (B + A) e. CC)
30		subcl 5432	. . . . . . . . 9 |- ((B e. CC /\ A e. CC) -> (B - A) e. CC)
31	28, 29, 30	sylanc 482	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> (((B + A) - (B - A)) / 2) = (((B + A) / 2) - ((B - A) / 2)))
32		divcan3 5819	. . . . . . . . . 10 |- ((A e. CC /\ 2 e. CC /\ 2 =/= 0) -> ((2 x. A) / 2) = A)
33	24, 25, 32	mp3an23 920	. . . . . . . . 9 |- (A e. CC -> ((2 x. A) / 2) = A)
34	33	adantl 397	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> ((2 x. A) / 2) = A)
35	23, 31, 34	3eqtr3d 1562	. . . . . . 7 |- ((B e. CC /\ A e. CC) -> (((B + A) / 2) - ((B - A) / 2)) = A)
36		ppncan 5546	. . . . . . . . . . 11 |- ((B e. CC /\ A e. CC /\ B e. CC) -> ((B + A) + (B - A)) = (B + B))
37	36	3anidm13 895	. . . . . . . . . 10 |- ((B e. CC /\ A e. CC) -> ((B + A) + (B - A)) = (B + B))
38		2times 6065	. . . . . . . . . . 11 |- (B e. CC -> (2 x. B) = (B + B))
39	38	adantr 398	. . . . . . . . . 10 |- ((B e. CC /\ A e. CC) -> (2 x. B) = (B + B))
40	37, 39	eqtr4d 1557	. . . . . . . . 9 |- ((B e. CC /\ A e. CC) -> ((B + A) + (B - A)) = (2 x. B))
41	40	opreq1d 4033	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> (((B + A) + (B - A)) / 2) = ((2 x. B) / 2))
42	24, 25	pm3.2i 292	. . . . . . . . . 10 |- (2 e. CC /\ 2 =/= 0)
43		divdir 5813	. . . . . . . . . 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 917	. . . . . . . . 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 482	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> (((B + A) + (B - A)) / 2) = (((B + A) / 2) + ((B - A) / 2)))
46		divcan3 5819	. . . . . . . . . 10 |- ((B e. CC /\ 2 e. CC /\ 2 =/= 0) -> ((2 x. B) / 2) = B)
47	24, 25, 46	mp3an23 920	. . . . . . . . 9 |- (B e. CC -> ((2 x. B) / 2) = B)
48	47	adantr 398	. . . . . . . 8 |- ((B e. CC /\ A e. CC) -> ((2 x. B) / 2) = B)
49	41, 45, 48	3eqtr3d 1562	. . . . . . 7 |- ((B e. CC /\ A e. CC) -> (((B + A) / 2) + ((B - A) / 2)) = B)
50	35, 49	opreq12d 4036	. . . . . 6 |- ((B e. CC /\ A e. CC) -> ((((B + A) / 2) - ((B - A) / 2))(,)(((B + A) / 2) + ((B - A) / 2))) = (A(,)B))
51		recn 5378	. . . . . 6 |- (B e. RR -> B e. CC)
52		recn 5378	. . . . . 6 |- (A e. RR -> A e. CC)
53	50, 51, 52	syl2an 465	. . . . 5 |- ((B e. RR /\ A e. RR) -> ((((B + A) / 2) - ((B - A) / 2))(,)(((B + A) / 2) + ((B - A) / 2))) = (A(,)B))
54	53	3adant3 811	. . . 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 1555	. . 3 |- ((B e. RR /\ A e. RR /\ A < B) -> (A(,)B) = (((B + A) / 2)( ball ` D)((B - A) / 2)))
56	55	3com12 849	. 2 |- ((A e. RR /\ B e. RR /\ A < B) -> (A(,)B) = (((B + A) / 2)( ball ` D)((B - A) / 2)))
57		addcom 5370	. . . . . 6 |- ((A e. CC /\ B e. CC) -> (A + B) = (B + A))
58	57, 52, 51	syl2an 465	. . . . 5 |- ((A e. RR /\ B e. RR