Theorem bcthlem16 8011

Description: Lemma for bcth 8029. A ball in sequence g is included in the complement of the closure of reference sequence M.

Hypotheses

Ref	Expression
bcthlem16.1	|- D e. CMet
bcthlem16.3	|- X = dom dom D
bcthlem16.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))})}
bcthlem16.8	|- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))

Assertion

Ref	Expression
bcthlem16	|- (((g:NN-->A /\ (((1st` (g` 1))( ball ` D)(2nd` (g` 1))) (_ (X \ ((cls` J)` (M` 1))) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) /\ m e. NN) -> ((1st` (g` m))( ball ` D)(2nd` (g` m))) (_ (X \ ((cls` J)` (M` m))))

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

Proof of Theorem bcthlem16

Step	Hyp	Ref	Expression
1		nnge1t 5945	. . . . . 6 |- (m e. NN -> 1 <_ m)
2		nnret 5931	. . . . . . 7 |- (m e. NN -> m e. RR)
3		1re 5447	. . . . . . . 8 |- 1 e. RR
4		leloet 5530	. . . . . . . 8 |- ((1 e. RR /\ m e. RR) -> (1 <_ m <-> (1 < m \/ 1 = m)))
5	3, 4	mpan 697	. . . . . . 7 |- (m e. RR -> (1 <_ m <-> (1 < m \/ 1 = m)))
6	2, 5	syl 10	. . . . . 6 |- (m e. NN -> (1 <_ m <-> (1 < m \/ 1 = m)))
7	1, 6	mpbid 195	. . . . 5 |- (m e. NN -> (1 < m \/ 1 = m))
8	7	adantr 391	. . . 4 |- ((m e. NN /\ g:NN-->A) -> (1 < m \/ 1 = m))
9		1nn 5936	. . . . . . . . . . 11 |- 1 e. NN
10		nnsubt 5959	. . . . . . . . . . 11 |- ((1 e. NN /\ m e. NN) -> (1 < m <-> (m - 1) e. NN))
11	9, 10	mpan 697	. . . . . . . . . 10 |- (m e. NN -> (1 < m <-> (m - 1) e. NN))
12	11	biimpa 418	. . . . . . . . 9 |- ((m e. NN /\ 1 < m) -> (m - 1) e. NN)
13		opreq1 3974	. . . . . . . . . . . 12 |- (k = (m - 1) -> (k + 1) = ((m - 1) + 1))
14	13	fveq2d 3734	. . . . . . . . . . 11 |- (k = (m - 1) -> (g` (k + 1)) = (g` ((m - 1) + 1)))
15		fveq2 3730	. . . . . . . . . . . 12 |- (k = (m - 1) -> (g` k) = (g` (m - 1)))
16	13, 15	opreq12d 3984	. . . . . . . . . . 11 |- (k = (m - 1) -> ((k + 1)F(g` k)) = (((m - 1) + 1)F(g` (m - 1))))
17	14, 16	eleq12d 1545	. . . . . . . . . 10 |- (k = (m - 1) -> ((g` (k + 1)) e. ((k + 1)F(g` k)) <-> (g` ((m - 1) + 1)) e. (((m - 1) + 1)F(g` (m - 1)))))
18	17	rcla4v 1876	. . . . . . . . 9 |- ((m - 1) e. NN -> (A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)) -> (g` ((m - 1) + 1)) e. (((m - 1) + 1)F(g` (m - 1)))))
19	12, 18	syl 10	. . . . . . . 8 |- ((m e. NN /\ 1 < m) -> (A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)) -> (g` ((m - 1) + 1)) e. (((m - 1) + 1)F(g` (m - 1)))))
20	19	adantlr 395	. . . . . . 7 |- (((m e. NN /\ g:NN-->A) /\ 1 < m) -> (A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)) -> (g` ((m - 1) + 1)) e. (((m - 1) + 1)F(g` (m - 1)))))
21		nncnt 5932	. . . . . . . . . 10 |- (m e. NN -> m e. CC)
22		ax1cn 5281	. . . . . . . . . . . . 13 |- 1 e. CC
23		npcant 5411	. . . . . . . . . . . . 13 |- ((m e. CC /\ 1 e. CC) -> ((m - 1) + 1) = m)
24	22, 23	mpan2 698	. . . . . . . . . . . 12 |- (m e. CC -> ((m - 1) + 1) = m)
25	24	fveq2d 3734	. . . . . . . . . . 11 |- (m e. CC -> (g` ((m - 1) + 1)) = (g` m))
26	24	opreq1d 3981	. . . . . . . . . . 11 |- (m e. CC -> (((m - 1) + 1)F(g` (m - 1))) = (mF(g` (m - 1))))
27	25, 26	eleq12d 1545	. . . . . . . . . 10 |- (m e. CC -> ((g` ((m - 1) + 1)) e. (((m - 1) + 1)F(g` (m - 1))) <-> (g` m) e. (mF(g` (m - 1)))))
28	21, 27	syl 10	. . . . . . . . 9 |- (m e. NN -> ((g` ((m - 1) + 1)) e. (((m - 1) + 1)F(g` (m - 1))) <-> (g` m) e. (mF(g` (m - 1)))))
29	28	ad2antrr 406	. . . . . . . 8 |- (((m e. NN /\ g:NN-->A) /\ 1 < m) -> ((g` ((m - 1) + 1)) e. (((m - 1) + 1)F(g` (m - 1))) <-> (g` m) e. (mF(g` (m - 1)))))
30		bcthlem16.1	. . . . . . . . . . . . . 14 |- D e. CMet
31		bcthlem16.3	. . . . . . . . . . . . . 14 |- X = dom dom D
32		bcthlem16.6	. . . . . . . . . . . . . 14 |- 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))})}
33		bcthlem16.8	. . . . . . . . . . . . . 14 |- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))
34	30, 31, 32, 33	bcthlem15 8010	. . . . . . . . . . . . 13 |- (((m e. NN /\ (g` (m - 1)) e. A) /\ (g` m) e. (mF(g` (m - 1)))) -> (((1st` (g` m)) e. X /\ ((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m)))) /\ ((2nd` (g` m)) < ((2nd` (g` (m - 1))) / 2) /\ ((1st` (g` m))( ball ` D)(2nd` (g` m))) (_ ((X \ ((cls` J)` (M` m))) i^i ((1st` (g` (m - 1)))( ball ` D)((2nd` (g` (m - 1))) / 2))))))
35	34	pm3.27d 325	. . . . . . . . . . . 12 |- (((m e. NN /\ (g` (m - 1)) e. A) /\ (g` m) e. (mF(g` (m - 1)))) -> ((2nd` (g` m)) < ((2nd` (g` (m - 1))) / 2) /\ ((1st` (g` m))( ball ` D)(2nd` (g` m))) (_ ((X \ ((cls` J)` (M` m))) i^i ((1st` (g` (m - 1)))( ball ` D)((2nd` (g` (m - 1))) / 2)))))
36	35	pm3.27d 325	. . . . . . . . . . 11 |- (((m e. NN /\ (g` (m - 1)) e. A) /\ (g` m) e. (mF(g` (m - 1)))) -> ((1st` (g` m))( ball ` D)(2nd` (g` m))) (_ ((X \ ((cls` J)` (M` m))) i^i ((1st` (g` (m - 1)))( ball ` D)((2nd` (g` (m - 1))) / 2))))
37		inss1 2233	. . . . . . . . . . . 12 |- ((X \ ((cls` J)` (M` m))) i^i ((1st` (g` (m - 1)))( ball ` D)((2nd` (g` (m - 1))) / 2))) (_ (X \ ((cls` J)` (M` m)))
38		sstr 2075	. . . . . . . . . . . 12 |- ((((1st` (g` m))( ball ` D)(2nd` (g` m))) (_ ((X \ ((cls` J)` (M` m))) i^i ((1st` (g` (m - 1)))( ball ` D)((2nd` (g` (m - 1))) / 2))) /\ ((X \ ((cls` J)` (M` m))) i^i ((1st` (g` (m - 1)))( ball ` D)((2nd` (g` (m - 1))) / 2))) (_ (X \ ((cls` J)` (M` m)))) -> ((1st`