Theorem tgioolem 7853

Description: Lemma for tgioo 7854. An open interval includes a ball around any of its points. Warning: The HTML proof page is 0.6MB in size.

Hypothesis

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

Assertion

Ref	Expression
tgioolem	|- ((t e. RR* /\ s e. RR*) -> (v e. (t(,)s) -> E.u e. RR (0 < u /\ (v( ball ` D)u) (_ (t(,)s))))

Distinct variable group:   t,s,u,v,D

Proof of Theorem tgioolem

Step	Hyp	Ref	Expression
1		elioo2t 6316	. 2 |- ((t e. RR* /\ s e. RR*) -> (v e. (t(,)s) <-> (v e. RR /\ t < v /\ v < s)))
2		resubclt 5410	. . . . . . . . . 10 |- ((v e. RR /\ t e. RR) -> (v - t) e. RR)
3	2	ancoms 436	. . . . . . . . 9 |- ((t e. RR /\ v e. RR) -> (v - t) e. RR)
4	3	ad2ant2r 409	. . . . . . . 8 |- (((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v)) -> (v - t) e. RR)
5	4	3adantr3 806	. . . . . . 7 |- (((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v /\ v < s)) -> (v - t) e. RR)
6		resubclt 5410	. . . . . . . . 9 |- ((s e. RR /\ v e. RR) -> (s - v) e. RR)
7	6	ad2ant2lr 410	. . . . . . . 8 |- (((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v)) -> (s - v) e. RR)
8	7	3adantr3 806	. . . . . . 7 |- (((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v /\ v < s)) -> (s - v) e. RR)
9		breq2 2613	. . . . . . . . . 10 |- (u = (v - t) -> (0 < u <-> 0 < (v - t)))
10		opreq2 3954	. . . . . . . . . . 11 |- (u = (v - t) -> (v( ball ` D)u) = (v( ball ` D)(v - t)))
11	10	sseq1d 2078	. . . . . . . . . 10 |- (u = (v - t) -> ((v( ball ` D)u) (_ (t(,)s) <-> (v( ball ` D)(v - t)) (_ (t(,)s)))
12	9, 11	anbi12d 626	. . . . . . . . 9 |- (u = (v - t) -> ((0 < u /\ (v( ball ` D)u) (_ (t(,)s)) <-> (0 < (v - t) /\ (v( ball ` D)(v - t)) (_ (t(,)s))))
13	12	rcla4ev 1868	. . . . . . . 8 |- (((v - t) e. RR /\ (0 < (v - t) /\ (v( ball ` D)(v - t)) (_ (t(,)s))) -> E.u e. RR (0 < u /\ (v( ball ` D)u) (_ (t(,)s)))
14	5	adantr 389	. . . . . . . 8 |- ((((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v /\ v < s)) /\ (v - t) <_ (s - v)) -> (v - t) e. RR)
15		posdift 5627	. . . . . . . . . . . . . 14 |- ((t e. RR /\ v e. RR) -> (t < v <-> 0 < (v - t)))
16	15	biimp3a 916	. . . . . . . . . . . . 13 |- ((t e. RR /\ v e. RR /\ t < v) -> 0 < (v - t))
17	16	3expb 832	. . . . . . . . . . . 12 |- ((t e. RR /\ (v e. RR /\ t < v)) -> 0 < (v - t))
18	17	adantlr 393	. . . . . . . . . . 11 |- (((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v)) -> 0 < (v - t))
19	18	3adantr3 806	. . . . . . . . . 10 |- (((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v /\ v < s)) -> 0 < (v - t))
20	19	adantr 389	. . . . . . . . 9 |- ((((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v /\ v < s)) /\ (v - t) <_ (s - v)) -> 0 < (v - t))
21		remet.1	. . . . . . . . . . . . . . . . 17 |- D = ((abs o. - ) |` (RR X. RR))
22	21	bl2ioo 7850	. . . . . . . . . . . . . . . 16 |- ((v e. RR /\ (v - t) e. RR /\ 0 < (v - t)) -> (v( ball ` D)(v - t)) = ((v - (v - t))(,)(v + (v - t))))
23		3simp2 787	. . . . . . . . . . . . . . . 16 |- ((t e. RR /\ v e. RR /\ t < v) -> v e. RR)
24	3	3adant3 797	. . . . . . . . . . . . . . . 16 |- ((t e. RR /\ v e. RR /\ t < v) -> (v - t) e. RR)
25	22, 23, 24, 16	syl3anc 856	. . . . . . . . . . . . . . 15 |- ((t e. RR /\ v e. RR /\ t < v) -> (v( ball ` D)(v - t)) = ((v - (v - t))(,)(v + (v - t))))
26		nncant 5441	. . . . . . . . . . . . . . . . . . 19 |- ((v e. CC /\ t e. CC) -> (v - (v - t)) = t)
27		recnt 5285	. . . . . . . . . . . . . . . . . . 19 |- (v e. RR -> v e. CC)
28		recnt 5285	. . . . . . . . . . . . . . . . . . 19 |- (t e. RR -> t e. CC)
29	26, 27, 28	syl2an 454	. . . . . . . . . . . . . . . . . 18 |- ((v e. RR /\ t e. RR) -> (v - (v - t)) = t)
30	29	ancoms 436	. . . . . . . . . . . . . . . . 17 |- ((t e. RR /\ v e. RR) -> (v - (v - t)) = t)
31	30	3adant3 797	. . . . . . . . . . . . . . . 16 |- ((t e. RR /\ v e. RR /\ t < v) -> (v - (v - t)) = t)
32	31	opreq1d 3960	. . . . . . . . . . . . . . 15 |- ((t e. RR /\ v e. RR /\ t < v) -> ((v - (v - t))(,)(v + (v - t))) = (t(,)(v + (v - t))))
33	25, 32	eqtrd 1499	. . . . . . . . . . . . . 14 |- ((t e. RR /\ v e. RR /\ t < v) -> (v( ball ` D)(v - t)) = (t(,)(v + (v - t))))
34	33	3expb 832	. . . . . . . . . . . . 13 |- ((t e. RR /\ (v e. RR /\ t < v)) -> (v( ball ` D)(v - t)) = (t(,)(v + (v - t))))
35	34	adantlr 393	. . . . . . . . . . . 12 |- (((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v)) -> (v( ball ` D)(v - t)) = (t(,)(v + (v - t))))
36	35	3adantr3 806	. . . . . . . . . . 11 |- (((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v /\ v < s)) -> (v( ball ` D)(v - t)) = (t(,)(v + (v - t))))
37	36	adantr 389	. . . . . . . . . 10 |- ((((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v /\ v < s)) /\ (v - t) <_ (s - v)) -> (v( ball ` D)(v - t)) = (t(,)(v + (v - t))))
38		iooss2 6311	. . . . . . . . . . . . 13 |- (((t e. RR* /\ (v + (v - t)) e. RR* /\ s e. RR*) /\ (v + (v - t)) <_ s) -> (t(,)(v + (v - t))) (_ (t(,)s))
39	38	ex 373	. . . . . . . . . . . 12 |- ((t e. RR* /\ (v + (v - t)) e. RR* /\ s e. RR*) -> ((v + (v - t)) <_ s -> (t(,)(v + (v - t))) (_ (t(,)s)))
40		rexrt 5471	. . . . . . . . . . . 12 |- (t e. RR -> t e. RR*)
41		rexrt 5471	. . . . . . . . . . . 12 |- ((v + (v - t)) e. RR -> (v + (v - t)) e. RR*)
42		rexrt 5471	. . . . . . . . . . . 12 |- (s e. RR -> s e. RR*)
43	39, 40, 41, 42	syl3an 866	. . . . . . . . . . 11 |- ((t e. RR /\ (v + (v - t)) e. RR /\ s e. RR) -> ((v + (v - t)) <_ s -> (t(,)(v + (v - t))) (_ (t(,)s)))
44		pm3.26 319	. . . . . . . . . . . . 13 |- ((t e. RR /\ s e. RR) -> t e. RR)
45	44	ad2antrr 404	. . . . . . . . . . . 12 |- ((((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v /\ v < s)) /\ (v - t) <_ (s - v)) -> t e. RR)
46		axaddrcl 5244	. . . . . . . . . . . . . . . 16 |- ((v e. RR /\ (v - t) e. RR) -> (v + (v - t)) e. RR)
47		pm3.27 323	. . . . . . . . . . . . . . . 16 |- ((t e. RR /\ v e. RR) -> v e. RR)
48	46, 47, 3	sylanc 471	. . . . . . . . . . . . . . 15 |- ((t e. RR /\ v e. RR) -> (v + (v - t)) e. RR)
49	48	ad2ant2r 409	. . . . . . . . . . . . . 14 |- (((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v)) -> (v + (v - t)) e. RR)
50	49	3adantr3 806	. . . . . . . . . . . . 13 |- (((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v /\ v < s)) -> (v + (v - t)) e. RR)
51	50	adantr 389	. . . . . . . . . . . 12 |- ((((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v /\ v < s)) /\ (v - t) <_ (s - v)) -> (v + (v - t)) e. RR)
52		pm3.27 323	. . . . . . . . . . . . 13 |- ((t e. RR /\ s e. RR) -> s e. RR)
53	52	ad2antrr 404	. . . . . . . . . . . 12 |- ((((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v /\ v < s)) /\ (v - t) <_ (s - v)) -> s e. RR)
54	45, 51, 53	3jca 817	. . . . . . . . . . 11 |- ((((t e. RR /\ s e. RR) /\ (v e. RR /\ t < v /\ v < s)) /\ (v - t) <_ (s - v)) -> (t e. RR /\ (v + (v - t)) e. RR /\ s e. RR))
55		leaddsub2t 5608	. . . . . . . . . . . . . 14 |- ((v e. RR /\ (v - t) e. RR /\ s e. RR) -> ((v + (v - t)) <_ s <-> (v - t) <_ (s - v)))
56		pm3.27 323	. . . . . . . . . . . . . 14 |- (((t e. RR /\ s e. RR) /\ v e. RR) -> v e. <