Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem ioo2bl 7851

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

Hypothesis

Ref	Expression
remet.1

Assertion

Ref	Expression
ioo2bl	(,) ball

---

Proof of Theorem ioo2bl

Step	Hyp	Ref	Expression
1		remet.1	. . . . . 6
2	1	bl2ioo 7850	. . . . 5 ball (,)
3		axaddrcl 5244	. . . . . . 7
4		rehalfclt 5981	. . . . . . 7
5	3, 4	syl 10	. . . . . 6
6	5	3adant3 797	. . . . 5
7		resubclt 5410	. . . . . . 7
8		rehalfclt 5981	. . . . . . 7
9	7, 8	syl 10	. . . . . 6
10	9	3adant3 797	. . . . 5
11		posdift 5627	. . . . . . . 8
12	11	ancoms 436	. . . . . . 7
13		halfpos2t 5984	. . . . . . . 8
14	7, 13	syl 10	. . . . . . 7
15	12, 14	bitrd 526	. . . . . 6
16	15	biimp3a 916	. . . . 5
17	2, 6, 10, 16	syl3anc 856	. . . 4 ball (,)
18		pnncant 5452	. . . . . . . . . . 11
19	18	3anidm23 881	. . . . . . . . . 10
20		2timest 5951	. . . . . . . . . . 11
21	20	adantl 388	. . . . . . . . . 10
22	19, 21	eqtr4d 1502	. . . . . . . . 9
23	22	opreq1d 3960	. . . . . . . 8
24		2cn 5927	. . . . . . . . . 10
25		2ne0 5937	. . . . . . . . . . 11
26		divsubdirt 5731	. . . . . . . . . . 11
27	25, 26	mpan2 694	. . . . . . . . . 10
28	24, 27	mp3an3 902	. . . . . . . . 9
29		axaddcl 5243	. . . . . . . . 9
30		subclt 5339	. . . . . . . . 9
31	28, 29, 30	sylanc 471	. . . . . . . 8
32		divcan3t 5718	. . . . . . . . . 10
33	24, 25, 32	mp3an13 904	. . . . . . . . 9
34	33	adantl 388	. . . . . . . 8
35	23, 31, 34	3eqtr3d 1507	. . . . . . 7
36		ppncant 5453	. . . . . . . . . . 11
37	36	3anidm13 880	. . . . . . . . . 10
38		2timest 5951	. . . . . . . . . . 11
39	38	adantr 389	. . . . . . . . . 10
40	37, 39	eqtr4d 1502	. . . . . . . . 9
41	40	opreq1d 3960	. . . . . . . 8
42		divdirt 5713	. . . . . . . . . . 11
43	25, 42	mpan2 694	. . . . . . . . . 10
44	24, 43	mp3an3 902	. . . . . . . . 9
45	44, 29, 30	sylanc 471	. . . . . . . 8
46		divcan3t 5718	. . . . . . . . . 10
47	24, 25, 46	mp3an13 904	. . . . . . . . 9
48	47	adantr 389	. . . . . . . 8
49	41, 45, 48	3eqtr3d 1507	. . . . . . 7
50	35, 49	opreq12d 3963	. . . . . 6 (,) (,)
51		recnt 5285	. . . . . 6
52		recnt 5285	. . . . . 6
53	50, 51, 52	syl2an 454	. . . . 5 (,) (,)
54	53	3adant3 797	. . . 4 (,) (,)
55	17, 54	eqtr2d 1500	. . 3 (,) ball
56	55	3com12 835	. 2 (,) ball