Theorem bcthlem18 7966

Description: Lemma for bcth 7982. Sequence g represents a series of nested balls.

Hypotheses

Ref	Expression
bcthlem18.1	|- D e. CMet
bcthlem18.3	|- X = dom dom D
bcthlem18.6	|- F = {<.<.j, y>., z>. | ((j e. NN /\ y e. A) /\ z = {<.p, r>. | ((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O))})}
bcthlem18.7	|- A = (X X. {x e. RR | 0 < x})
bcthlem18.8	|- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))

Assertion

Ref	Expression
bcthlem18	|- (n e. NN -> (((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN) -> (m < n -> ((1st` (g` n))( ball ` D)(2nd` (g` n))) (_ ((1st` (g` m))( ball ` D)((2nd` (g` m)) / 2)))))

Distinct variable groups:   j,m,n,y,z,A   j,p,r,D,m,n,y,z   k,m,n,F   j,J,p,r,y,z   j,M,p,r,y,z   z,O   j,X,m,n,p,r,y,z   j,k,x,g,p,r,y,z,m,n

Proof of Theorem bcthlem18

Step	Hyp	Ref	Expression
1		leloet 5499	. . . . . . . . . 10 |- ((m e. RR /\ q e. RR) -> (m <_ q <-> (m < q \/ m = q)))
2		nnret 5885	. . . . . . . . . 10 |- (m e. NN -> m e. RR)
3		nnret 5885	. . . . . . . . . 10 |- (q e. NN -> q e. RR)
4	1, 2, 3	syl2an 454	. . . . . . . . 9 |- ((m e. NN /\ q e. NN) -> (m <_ q <-> (m < q \/ m = q)))
5		nnleltp1t 5909	. . . . . . . . 9 |- ((m e. NN /\ q e. NN) -> (m <_ q <-> m < (q + 1)))
6	4, 5	bitr3d 529	. . . . . . . 8 |- ((m e. NN /\ q e. NN) -> ((m < q \/ m = q) <-> m < (q + 1)))
7	6	ancoms 436	. . . . . . 7 |- ((q e. NN /\ m e. NN) -> ((m < q \/ m = q) <-> m < (q + 1)))
8	7	adantrl 394	. . . . . 6 |- ((q e. NN /\ ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN)) -> ((m < q \/ m = q) <-> m < (q + 1)))
9		bcthlem18.1	. . . . . . . . . . . . . . . 16 |- D e. CMet
10		bcthlem18.3	. . . . . . . . . . . . . . . 16 |- X = dom dom D
11		bcthlem18.6	. . . . . . . . . . . . . . . 16 |- F = {<.<.j, y>., z>. | ((j e. NN /\ y e. A) /\ z = {<.p, r>. | ((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O))})}
12		bcthlem18.8	. . . . . . . . . . . . . . . 16 |- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))
13	9, 10, 11, 12	bcthlem15 7963	. . . . . . . . . . . . . . 15 |- ((((q + 1) e. NN /\ (g` q) e. A) /\ (g` (q + 1)) e. ((q + 1)F(g` q))) -> (((1st` (g` (q + 1))) e. X /\ ((2nd` (g` (q + 1))) e. RR /\ 0 < (2nd` (g` (q + 1))))) /\ ((2nd` (g` (q + 1))) < ((2nd` (g` q)) / 2) /\ ((1st` (g` (q + 1)))( ball ` D)(2nd` (g` (q + 1)))) (_ ((X \ ((cls` J)` (M` (q + 1)))) i^i ((1st` (g` q))( ball ` D)((2nd` (g` q)) / 2))))))
14	13	pm3.27d 325	. . . . . . . . . . . . . 14 |- ((((q + 1) e. NN /\ (g` q) e. A) /\ (g` (q + 1)) e. ((q + 1)F(g` q))) -> ((2nd` (g` (q + 1))) < ((2nd` (g` q)) / 2) /\ ((1st` (g` (q + 1)))( ball ` D)(2nd` (g` (q + 1)))) (_ ((X \ ((cls` J)` (M` (q + 1)))) i^i ((1st` (g` q))( ball ` D)((2nd` (g` q)) / 2)))))
15	14	pm3.27d 325	. . . . . . . . . . . . 13 |- ((((q + 1) e. NN /\ (g` q) e. A) /\ (g` (q + 1)) e. ((q + 1)F(g` q))) -> ((1st` (g` (q + 1)))( ball ` D)(2nd` (g` (q + 1)))) (_ ((X \ ((cls` J)` (M` (q + 1)))) i^i ((1st` (g` q))( ball ` D)((2nd` (g` q)) / 2))))
16		peano2nn 5891	. . . . . . . . . . . . . . . 16 |- (q e. NN -> (q + 1) e. NN)
17	16	adantr 389	. . . . . . . . . . . . . . 15 |- ((q e. NN /\ g:NN-->A) -> (q + 1) e. NN)
18		ffvelrn 3805	. . . . . . . . . . . . . . . 16 |- ((g:NN-->A /\ q e. NN) -> (g` q) e. A)
19	18	ancoms 436	. . . . . . . . . . . . . . 15 |- ((q e. NN /\ g:NN-->A) -> (g` q) e. A)
20	17, 19	jca 288	. . . . . . . . . . . . . 14 |- ((q e. NN /\ g:NN-->A) -> ((q + 1) e. NN /\ (g` q) e. A))
21	20	adantrr 395	. . . . . . . . . . . . 13 |- ((q e. NN /\ (g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> ((q + 1) e. NN /\ (g` q) e. A))
22		opreq1 3959	. . . . . . . . . . . . . . . . 17 |- (k = q -> (k + 1) = (q + 1))
23	22	fveq2d 3719	. . . . . . . . . . . . . . . 16 |- (k = q -> (g` (k + 1)) = (g` (q + 1)))
24		fveq2 3715	. . . . . . . . . . . . . . . . 17 |- (k = q -> (g` k) = (g` q))
25	22, 24	opreq12d 3969	. . . . . . . . . . . . . . . 16 |- (k = q -> ((k + 1)F(g` k)) = ((q + 1)F(g` q)))
26	23, 25	eleq12d 1539	. . . . . . . . . . . . . . 15 |- (k = q -> ((g` (k + 1)) e. ((k + 1)F(g` k)) <-> (g` (q + 1)) e. ((q + 1)F(g` q))))
27	26	rcla4va 1871	. . . . . . . . . . . . . 14 |- ((q e. NN /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) -> (g` (q + 1)) e. ((q + 1)F(g` q)))
28	27	adantrl 394	. . . . . . . . . . . . 13 |- ((q e. NN /\ (g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> (g` (q + 1)) e. ((q + 1)F(g` q)))
29	15, 21, 28	sylanc 471	. . . . . . . . . . . 12 |- ((q e. NN /\ (g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> ((1st` (g` (q + 1)))( ball ` D)(2nd` (g` (q + 1)))) (_ ((X \ ((cls` J)` (M` (q + 1)))) i^i ((1st` (g` q))( ball ` D)((2nd` (g` q)) / 2))))
30		inss2 2227	. . . . . . . . . . . . . . 15 |- ((X \ ((cls` J)` (M` (q + 1)))) i^i ((1st` (g` q))( ball ` D)((2nd` (g` q)) / 2))) (_ ((1st` (g` q))( ball ` D)((2nd` (g` q)) / 2))
31	30	a1i 8	. . . . . . . . . . . . . 14 |- ((q e. NN /\ g:NN-->A) -> ((X \ ((cls` J)` (M` (q + 1)))) i^i ((1st` (g` q))( ball ` D)((2nd` (g` q)) / 2))) (_ ((1st` (g` q))( ball ` D)((2nd` (g` q)) / 2)))
32	10	ssbl 7807	. . . . . . . . . . . . . . . 16 |- ((((D e. Met /\ (1st` (g` q)) e. X) /\ (((2nd` (g` q)) / 2) e. RR /\ 0 < ((2nd` (g` q)) / 2)) /\ ((2nd` (g` q)) e. RR /\ 0 < (2nd` (g` q)))) /\ ((2nd` (g` q)) / 2) <_ (2nd` (g` q))) -> ((1st` (g` q))( ball ` D)((2nd` (g` q)) / 2)) (_ ((1st` (g` q))( ball ` D)(2nd` (g` q))))
33		bcthlem18.7	. . . . . . . . . . . . . . . . . . . 20 |- A = (X X. {x e. RR | 0 < x})
34	33	bcthlem4 7952	. . . . . . . . . . . . . . . . . . 19 |- ((g:NN-->A /\ q e. NN)