Theorem heiborlem36 12046

Description: Lemma for heibor 12053. Combine the two bounds in heiborlem34 12044 and heiborlem35 12045 to get a ball in H lying completely within a ball of arbitrary radius about Y.

Hypotheses

Ref	Expression
heibor.1	|- J = (Open` M)
heibor.2	|- X = dom dom M
heibor.9	|- M e. CMet
heibor.10	|- M e. TotBnd
heibor.11	|- U (_ J
heibor.12	|- X = U.U
heibor.13	|- D = {s e. P~X | -. E.v e. (P~U i^i Fin)s (_ U.v}
heibor.14	|- B = {<.x, r>. | ((x e. X /\ r e. RR+) /\ (x( ball ` M)r) e. D)}
heibor.15	|- G = {<.<.n, a>., h>. | ((n e. NN /\ a e. B) /\ h = {<.x, r>. | ((x e. X /\ r = (1 / (2^n))) /\ ((x( ball ` M)r) e. D /\ ((x( ball ` M)r) i^i (( ball ` M)` a)) =/= (/)))})}

Assertion

Ref	Expression
heiborlem36	|- (((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g)) /\ (1st o. H)(~~>m` M)Y) /\ (Y e. X /\ R e. RR+)) -> E.p e. NN (( ball ` M)` (H` p)) (_ (Y( ball ` M)R))

Distinct variable groups:   n,M,r,s,v,x   n,J,s,v,x   n,X,r,s,v,x   x,U   B,n   Y,r,x   U,p,s,v   Y,a,h,n,p,s,v   D,a,h,n,r,x   X,a,g,h,p   H,a,g,h,n,p,r,s,v,x   B,a,g,h,p   M,a,g,h,p   g,G,p   R,a,h,n,p,r,s,v,x

Proof of Theorem heiborlem36

Step	Hyp	Ref	Expression
1		heibor.1	. . . . 5 |- J = (Open` M)
2		heibor.2	. . . . 5 |- X = dom dom M
3		heibor.9	. . . . 5 |- M e. CMet
4		heibor.10	. . . . 5 |- M e. TotBnd
5		heibor.11	. . . . 5 |- U (_ J
6		heibor.12	. . . . 5 |- X = U.U
7		heibor.13	. . . . 5 |- D = {s e. P~X | -. E.v e. (P~U i^i Fin)s (_ U.v}
8		heibor.14	. . . . 5 |- B = {<.x, r>. | ((x e. X /\ r e. RR+) /\ (x( ball ` M)r) e. D)}
9		heibor.15	. . . . 5 |- G = {<.<.n, a>., h>. | ((n e. NN /\ a e. B) /\ h = {<.x, r>. | ((x e. X /\ r = (1 / (2^n))) /\ ((x( ball ` M)r) e. D /\ ((x( ball ` M)r) i^i (( ball ` M)` a)) =/= (/)))})}
10	1, 2, 3, 4, 5, 6, 7, 8, 9	heiborlem34 12044	. . . 4 |- (((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g)) /\ (1st o. H)(~~>m` M)Y) /\ (Y e. X /\ (R / 2) e. RR+)) -> E.j e. NN A.m e. NN (j <_ m -> ((1st` (H` m))MY) < (R / 2)))
11	1, 2, 3, 4, 5, 6, 7, 8, 9	heiborlem35 12045	. . . 4 |- (((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g)) /\ (1st o. H)(~~>m` M)Y) /\ (Y e. X /\ (R / 2) e. RR+)) -> E.l e. NN A.m e. NN (l <_ m -> A.y e. (( ball ` M)` (H` m))((1st` (H` m))My) < (R / 2)))
12	10, 11	jca 286	. . 3 |- (((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g)) /\ (1st o. H)(~~>m` M)Y) /\ (Y e. X /\ (R / 2) e. RR+)) -> (E.j e. NN A.m e. NN (j <_ m -> ((1st` (H` m))MY) < (R / 2)) /\ E.l e. NN A.m e. NN (l <_ m -> A.y e. (( ball ` M)` (H` m))((1st` (H` m))My) < (R / 2))))
13		2re 6125	. . . . 5 |- 2 e. RR
14		2pos 6135	. . . . 5 |- 0 < 2
15	13, 14	elrpii 6193	. . . 4 |- 2 e. RR+
16		rpdivcl 6208	. . . 4 |- ((R e. RR+ /\ 2 e. RR+) -> (R / 2) e. RR+)
17	15, 16	mpan2 700	. . 3 |- (R e. RR+ -> (R / 2) e. RR+)
18	12, 17	sylanr2 465	. 2 |- (((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g)) /\ (1st o. H)(~~>m` M)Y) /\ (Y e. X /\ R e. RR+)) -> (E.j e. NN A.m e. NN (j <_ m -> ((1st` (H` m))MY) < (R / 2)) /\ E.l e. NN A.m e. NN (l <_ m -> A.y e. (( ball ` M)` (H` m))((1st` (H` m))My) < (R / 2))))
19		prth 559	. . . . . . . . . . . . . . . . 17 |- (((j <_ p -> ((1st` (H` p))MY) < (R / 2)) /\ (l <_ p -> A.y e. (( ball ` M)` (H` p))((1st` (H` p))My) < (R / 2))) -> ((j <_ p /\ l <_ p) -> (((1st` (H` p))MY) < (R / 2) /\ A.y e. (( ball ` M)` (H` p))((1st` (H` p))My) < (R / 2))))
20		ffvelrn 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((H:NN-->B /\ p e. NN) -> (H` p) e. B)
21	1, 2, 3, 4, 5, 6, 7, 8	heiborlem24 12034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((H` p) e. B <-> ((H` p) e. (X X. RR+) /\ (( ball ` M)` (H` p)) e. D))
22	21	pm3.26bi 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((H` p) e. B -> (H` p) e. (X X. RR+))
23		elxp6 4161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((H` p) e. (X X. RR+) <-> ((H` p) = <.(1st` (H` p)), (2nd` (H` p))>. /\ ((1st` (H` p)) e. X /\ (2nd` (H` p)) e. RR+)))
24	23	pm3.26bi 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((H` p) e. (X X. RR+) -> (H` p) = <.(1st` (H` p)), (2nd` (H` p))>.)
25	22, 24	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((H` p) e. B -> (H` p) = <.(1st` (H` p)), (2nd` (H` p))>.)
26	25	fveq2d 3839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((H` p) e. B -> (( ball ` M)` (H` p)) = (( ball ` M)` <.(1st` (H` p)), (2nd` (H` p))>.))
27		df-opr 4023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((1st` (H` p))( ball ` M)(2nd` (H` p))) = (( ball ` M)` <.(1st` (H` p)), (2nd` (H` p))>.)
28	26, 27	syl6eqr 1568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((H` p) e. B -> (( ball ` M)` (H` p)) = ((1st` (H` p))( ball ` M)(2nd` (H` p))))
29	20, 28	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((H:NN-->B /\ p e. NN) -> (( ball ` M)` (H` p)) = ((1st` (H` p))( ball ` M)(2nd` (H` p))))
30	29	adantlr 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) -> (( ball ` M)` (H` p)) = ((1st` (H` p))( ball ` M)(2nd` (H` p))))
31	30	adantllr 397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) -> (( ball ` M)` (H` p)) = ((1st` (H` p))( ball ` M)(2nd` (H` p))))
32	31	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) /\ ((1st` (H` p))My) < (R / 2)) -> (( ball ` M)` (H` p)) = ((1st` (H` p))( ball ` M)(2nd` (H` p))))
33	32	eleq2d 1584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) /\ ((1st` (H` p))My) < (R / 2)) -> (y e. (( ball ` M)` (H` p)) <-> y e. ((1st` (H` p))( ball ` M)(2nd` (H` p)))))
34	23	pm3.27bi 324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((H` p) e. (X X. RR+) -> ((1st` (H` p)) e. X /\ (2nd` (H` p)) e. RR+))
35	2	elbl 8048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((M e. Met /\ (1st` (H` p)) e. X) /\ ((2nd` (H` p)) e. RR /\ 0 < (2nd` (H` p)))) -> (y e. ((1st` (H` p))( ball ` M)(2nd` (H` p))) <-> (y e. X /\ ((1st` (H` p))My) < (2nd` (H` p)))))
36	3	cmsmeti 8173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- M e. Met
37	36	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((1st` (H` p)) e. X /\ (2nd` (H` p)) e. RR+) -> M e. Met)
38		pm3.26 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((1st` (H` p)) e. X /\ (2nd` (H` p)) e. RR+) -> (1st` (H` p)) e. X)
39		rpre 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((2nd` (H` p)) e. RR+ -> (2nd` (H` p)) e. RR)
40	39	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((1st` (H` p)) e. X /\ (2nd` (H` p)) e. RR+) -> (2nd` (H` p)) e. RR)
41		rpgt0 6199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((2nd` (H` p)) e. RR+ -> 0 < (2nd` (H` p)))
42	41	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((1st` (H` p)) e. X /\ (2nd` (H` p)) e. RR+) -> 0 < (2nd` (H` p)))
43	35, 37, 38, 40, 42	syl2anc 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((1st` (H` p)) e. X /\ (2nd` (H` p)) e. RR+) -> (y e. ((1st` (H` p))( ball ` M)(2nd` (H` p))) <-> (y e. X /\ ((1st` (H` p))My) < (2nd` (H` p)))))
44	34, 43	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((H` p) e. (X X. RR+) -> (y e. ((1st` (H` p))( ball ` M)(2nd` (H` p))) <-> (y e. X /\ ((1st` (H` p))My) < (2nd` (H` p)))))
45	20, 22, 44	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((H:NN-->B /\ p e. NN) -> (y e. ((1st` (H` p))( ball ` M)(2nd` (H` p))) <-> (y e. X /\ ((1st` (H` p))My) < (2nd` (H` p)))))
46	45	adantlr 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ p e. NN) -> (y e. ((1st` (H` p))( ball ` M)(2nd` (H` p))) <-> (y e. X /\ ((1st` (H` p))My) < (2nd` (H` p)))))
47	46	adantlr 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) -> (y e. ((1st` (H` p))( ball ` M)(2nd` (H` p))) <-> (y e. X /\ ((1st` (H` p))My) < (2nd` (H` p)))))
48	47	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) /\ ((1st` (H` p))My) < (R / 2)) -> (y e. ((1st` (H` p))( ball ` M)(2nd` (H` p))) <-> (y e. X /\ ((1st` (H` p))My) < (2nd` (H` p)))))
49	33, 48	bitrd 531	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) /\ ((1st` (H` p))My) < (R / 2)) -> (y e. (( ball ` M)` (H` p)) <-> (y e. X /\ ((1st` (H` p))My) < (2nd` (H` p)))))
50	49	pm3.26bda 420	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) /\ ((1st` (H` p))My) < (R / 2)) /\ y e. (( ball ` M)` (H` p))) -> y e. X)
51		pm3.27 321	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) /\ ((1st` (H` p))My) < (R / 2)) /\ y e. X) -> y e. X)
52		lt2add 5797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((1st` (H` p))MY) e. RR /\ ((1st` (H` p))My) e. RR) /\ ((R / 2) e. RR /\ (R / 2) e. RR)) -> ((((1st` (H` p))MY) < (R / 2) /\ ((1st` (H` p))My) < (R / 2)) -> (((1st` (H` p))MY) + ((1st` (H` p))My)) < ((R / 2) + (R / 2))))
53	2	metcl 8021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((M e. Met /\ (1st` (H` p)) e. X /\ Y e. X) -> ((1st` (H` p))MY) e. RR)
54	36	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((H:NN-->B /\ Y e. X) /\ p e. NN) -> M e. Met)
55		xp1st 11796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((H` p) e. (X X. RR+) -> (1st` (H` p)) e. X)
56	20, 22, 55	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((H:NN-->B /\ p e. NN) -> (1st` (H` p)) e. X)
57	56	adantlr 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((H:NN-->B /\ Y e. X) /\ p e. NN) -> (1st` (H` p)) e. X)
58		simplr 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((H:NN-->B /\ Y e. X) /\ p e. NN) -> Y e. X)
59	53, 54, 57, 58	syl3anc 864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((H:NN-->B /\ Y e. X) /\ p e. NN) -> ((1st` (H` p))MY) e. RR)
60	59	adantlrr 399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) -> ((1st` (H` p))MY) e. RR)
61	60	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> ((1st` (H` p))MY) e. RR)
62	2	metcl 8021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((M e. Met /\ (1st` (H` p)) e. X /\ y e. X) -> ((1st` (H` p))My) e. RR)
63	36	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((H:NN-->B /\ p e. NN) /\ y e. X) -> M e. Met)
64	56	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((H:NN-->B /\ p e. NN) /\ y e. X) -> (1st` (H` p)) e. X)
65		pm3.27 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((H:NN-->B /\ p e. NN) /\ y e. X) -> y e. X)
66	62, 63, 64, 65	syl3anc 864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((H:NN-->B /\ p e. NN) /\ y e. X) -> ((1st` (H` p))My) e. RR)
67	66	adantllr 397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> ((1st` (H` p))My) e. RR)
68		rpre 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((R / 2) e. RR+ -> (R / 2) e. RR)
69	17, 68	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (R e. RR+ -> (R / 2) e. RR)
70	69	ad2antll 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((H:NN-->B /\ (Y e. X /\ R e. RR+)) -> (R / 2) e. RR)
71	70	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> (R / 2) e. RR)
72	52, 61, 67, 71, 71	syl2anc 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> ((((1st` (H` p))MY) < (R / 2) /\ ((1st` (H` p))My) < (R / 2)) -> (((1st` (H` p))MY) + ((1st` (H` p))My)) < ((R / 2) + (R / 2))))
73	2	mettri4 8024	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((M e. Met /\ Y e. X) /\ (y e. X /\ (1st` (H` p)) e. X)) -> (YMy) <_ (((1st` (H` p))MY) + ((1st` (H` p))My)))
74	36	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> M e. Met)
75		simprl 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((H:NN-->B /\ (Y e. X /\ R e. RR+)) -> Y e. X)
76	75	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> Y e. X)
77		pm3.27 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> y e. X)
78	64	adantllr 397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> (1st` (H` p)) e. X)
79	73, 74, 76, 77, 78	syl2anc 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> (YMy) <_ (((1st` (H` p))MY) + ((1st` (H` p))My)))
80		lelttr 5677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((YMy) e. RR /\ (((1st` (H` p))MY) + ((1st` (H` p))My)) e. RR /\ ((R / 2) + (R / 2)) e. RR) -> (((YMy) <_ (((1st` (H` p))MY) + ((1st` (H` p))My)) /\ (((1st` (H` p))MY) + ((1st` (H` p))My)) < ((R / 2) + (R / 2))) -> (YMy) < ((R / 2) + (R / 2))))
81	2	metcl 8021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((M e. Met /\ Y e. X /\ y e. X) -> (YMy) e. RR)
82	36, 81	mp3an1 909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((Y e. X /\ y e. X) -> (YMy) e. RR)
83	82	adantlr 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((Y e. X /\ R e. RR+) /\ y e. X) -> (YMy) e. RR)
84	83	adantll 392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ y e. X) -> (YMy) e. RR)
85	84	adantlr 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> (YMy) e. RR)
86		readdcl 5456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((((1st` (H` p))MY) e. RR /\ ((1st` (H` p))My) e. RR) -> (((1st` (H` p))MY) + ((1st` (H` p))My)) e. RR)
87	86, 61, 67	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> (((1st` (H` p))MY) + ((1st` (H` p))My)) e. RR)
88		readdcl 5456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (((R / 2) e. RR /\ (R / 2) e. RR) -> ((R / 2) + (R / 2)) e. RR)
89	88	anidms 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((R / 2) e. RR -> ((R / 2) + (R / 2)) e. RR)
90	17, 68, 89	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (R e. RR+ -> ((R / 2) + (R / 2)) e. RR)
91	90	ad2antll 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((H:NN-->B /\ (Y e. X /\ R e. RR+)) -> ((R / 2) + (R / 2)) e. RR)
92	91	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> ((R / 2) + (R / 2)) e. RR)
93	80, 85, 87, 92	syl3anc 864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> (((YMy) <_ (((1st` (H` p))MY) + ((1st` (H` p))My)) /\ (((1st` (H` p))MY) + ((1st` (H` p))My)) < ((R / 2) + (R / 2))) -> (YMy) < ((R / 2) + (R / 2))))
94	79, 93	mpand 705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> ((((1st` (H` p))MY) + ((1st` (H` p))My)) < ((R / 2) + (R / 2)) -> (YMy) < ((R / 2) + (R / 2))))
95	94	imp 348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) /\ (((1st` (H` p))MY) + ((1st` (H` p))My)) < ((R / 2) + (R / 2))) -> (YMy) < ((R / 2) + (R / 2)))
96		rpcn 6196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (R e. RR+ -> R e. CC)
97		2halves 6185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (R e. CC -> ((R / 2) + (R / 2)) = R)
98	96, 97	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (R e. RR+ -> ((R / 2) + (R / 2)) = R)
99	98	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((Y e. X /\ R e. RR+) -> ((R / 2) + (R / 2)) = R)
100	99	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) -> ((R / 2) + (R / 2)) = R)
101	100	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) /\ (((1st` (H` p))MY) + ((1st` (H` p))My)) < ((R / 2) + (R / 2))) -> ((R / 2) + (R / 2)) = R)
102	95, 101	breqtrd 2712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) /\ (((1st` (H` p))MY) + ((1st` (H` p))My)) < ((R / 2) + (R / 2))) -> (YMy) < R)
103	102	ex 371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> ((((1st` (H` p))MY) + ((1st` (H` p))My)) < ((R / 2) + (R / 2)) -> (YMy) < R))
104	72, 103	syld 27	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ y e. X) -> ((((1st` (H` p))MY) < (R / 2) /\ ((1st` (H` p))My) < (R / 2)) -> (YMy) < R))
105	104	ex 371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) -> (y e. X -> ((((1st` (H` p))MY) < (R / 2) /\ ((1st` (H` p))My) < (R / 2)) -> (YMy) < R)))
106	105	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((H:NN-->B /\ (Y e. X /\ R e. RR+)) /\ p e. NN) -> ((((1st` (H` p))MY) < (R / 2) /\ ((1st` (H` p))My) < (R / 2)) -> (y e. X -> (YMy) < R)))
107	106	adantllr 397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) -> ((((1st` (H` p))MY) < (R / 2) /\ ((1st` (H` p))My) < (R / 2)) -> (y e. X -> (YMy) < R)))
108	107	imp 348	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ (((1st` (H` p))MY) < (R / 2) /\ ((1st` (H` p))My) < (R / 2))) -> (y e. X -> (YMy) < R))
109	108	anassrs 443	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) /\ ((1st` (H` p))My) < (R / 2)) -> (y e. X -> (YMy) < R))
110	109	imp 348	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) /\ ((1st` (H` p))My) < (R / 2)) /\ y e. X) -> (YMy) < R)
111	51, 110	jca 286	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) /\ ((1st` (H` p))My) < (R / 2)) /\ y e. X) -> (y e. X /\ (YMy) < R))
112	50, 111	syldan 469	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) /\ ((1st` (H` p))My) < (R / 2)) /\ y e. (( ball ` M)` (H` p))) -> (y e. X /\ (YMy) < R))
113	112	an1rs 492	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) /\ y e. (( ball ` M)` (H` p))) /\ ((1st` (H` p))My) < (R / 2)) -> (y e. X /\ (YMy) < R))
114	2	elbl 8048	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((M e. Met /\ Y e. X) /\ (R e. RR /\ 0 < R)) -> (y e. (Y( ball ` M)R) <-> (y e. X /\ (YMy) < R)))
115	36	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((Y e. X /\ R e. RR+) -> M e. Met)
116		pm3.26 317	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((Y e. X /\ R e. RR+) -> Y e. X)
117		rpre 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (R e. RR+ -> R e. RR)
118	117	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((Y e. X /\ R e. RR+) -> R e. RR)
119		rpgt0 6199	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (R e. RR+ -> 0 < R)
120	119	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((Y e. X /\ R e. RR+) -> 0 < R)
121	114, 115, 116, 118, 120	syl2anc 475	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((Y e. X /\ R e. RR+) -> (y e. (Y( ball ` M)R) <-> (y e. X /\ (YMy) < R)))
122	121	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) -> (y e. (Y( ball ` M)R) <-> (y e. X /\ (YMy) < R)))
123	122	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) -> (y e. (Y( ball ` M)R) <-> (y e. X /\ (YMy) < R)))
124	123	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) /\ y e. (( ball ` M)` (H` p))) /\ ((1st` (H` p))My) < (R / 2)) -> (y e. (Y( ball ` M)R) <-> (y e. X /\ (YMy) < R)))
125	113, 124	mpbird 194	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) /\ y e. (( ball ` M)` (H` p))) /\ ((1st` (H` p))My) < (R / 2)) -> y e. (Y( ball ` M)R))
126	125	ex 371	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) /\ y e. (( ball ` M)` (H` p))) -> (((1st` (H` p))My) < (R / 2) -> y e. (Y( ball ` M)R)))
127	126	r19.20dva 1755	. . . . . . . . . . . . . . . . . . . 20 |- (((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((1st` (H` p))MY) < (R / 2)) -> (A.y e. (( ball ` M)` (H` p))((1st` (H` p))My) < (R / 2) -> A.y e. (( ball ` M)` (H` p))y e. (Y( ball ` M)R)))
128	127	impr 11359	. . . . . . . . . . . . . . . . . . 19 |- (((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ (((1st` (H` p))MY) < (R / 2) /\ A.y e. (( ball ` M)` (H` p))((1st` (H` p))My) < (R / 2))) -> A.y e. (( ball ` M)` (H` p))y e. (Y( ball ` M)R))
129		dfss3 2111	. . . . . . . . . . . . . . . . . . 19 |- ((( ball ` M)` (H` p)) (_ (Y( ball ` M)R) <-> A.y e. (( ball ` M)` (H` p))y e. (Y( ball ` M)R))
130	128, 129	sylibr 198	. . . . . . . . . . . . . . . . . 18 |- (((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ (((1st` (H` p))MY) < (R / 2) /\ A.y e. (( ball ` M)` (H` p))((1st` (H` p))My) < (R / 2))) -> (( ball ` M)` (H` p)) (_ (Y( ball ` M)R))
131	130	ex 371	. . . . . . . . . . . . . . . . 17 |- ((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) -> ((((1st` (H` p))MY) < (R / 2) /\ A.y e. (( ball ` M)` (H` p))((1st` (H` p))My) < (R / 2)) -> (( ball ` M)` (H` p)) (_ (Y( ball ` M)R)))
132	19, 131	sylan9r 471	. . . . . . . . . . . . . . . 16 |- (((((H:NN-->B /\ A.g e. NN (H` (g + 1)) e. ((g + 1)G(H` g))) /\ (Y e. X /\ R e. RR+)) /\ p e. NN) /\ ((j <_ p -> ((1st` (H` p))MY) < (R / 2)) /\ (l <_ p -> A.y e. (( ball ` M)` (H` p))((1st` (H` p))My) < (R / 2)))) -> ((j <_ p /\ l <_ p) -> (( ball ` M)` (H` p)) (_ (Y( ball ` M