caubl

Description: Sufficient condition to ensure a sequence of nested balls is Cauchy. (Contributed by Mario Carneiro, 18-Jan-2014) (Revised by Mario Carneiro, 1-May-2014)

	Ref	Expression
Hypotheses	caubl.2	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
	caubl.3	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( 𝑋 × ℝ⁺ ) )
	caubl.4	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) )
	caubl.5	⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑛 ∈ ℕ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 )
Assertion	caubl	⊢ ( 𝜑 → ( 1^st ∘ 𝐹 ) ∈ ( Cau ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		caubl.2	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
2		caubl.3	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( 𝑋 × ℝ⁺ ) )
3		caubl.4	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) )
4		caubl.5	⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑛 ∈ ℕ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 )
5		2fveq3	⊢ ( 𝑟 = 𝑛 → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑟 ) ) = ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) )
6	5	sseq1d	⊢ ( 𝑟 = 𝑛 → ( ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑟 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
7	6	imbi2d	⊢ ( 𝑟 = 𝑛 → ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑟 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
8		2fveq3	⊢ ( 𝑟 = 𝑘 → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑟 ) ) = ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) )
9	8	sseq1d	⊢ ( 𝑟 = 𝑘 → ( ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑟 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
10	9	imbi2d	⊢ ( 𝑟 = 𝑘 → ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑟 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
11		2fveq3	⊢ ( 𝑟 = ( 𝑘 + 1 ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑟 ) ) = ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
12	11	sseq1d	⊢ ( 𝑟 = ( 𝑘 + 1 ) → ( ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑟 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
13	12	imbi2d	⊢ ( 𝑟 = ( 𝑘 + 1 ) → ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑟 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
14		ssid	⊢ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) )
15	14	2a1i	⊢ ( 𝑛 ∈ ℤ → ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
16		eluznn	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → 𝑘 ∈ ℕ )
17		fvoveq1	⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
18	17	fveq2d	⊢ ( 𝑛 = 𝑘 → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
19		2fveq3	⊢ ( 𝑛 = 𝑘 → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) )
20	18 19	sseq12d	⊢ ( 𝑛 = 𝑘 → ( ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
21	20	rspccva	⊢ ( ( ∀ 𝑛 ∈ ℕ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) )
22	3 16 21	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) )
23	22	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) )
24		sstr2	⊢ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) → ( ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
25	23 24	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
26	25	expcom	⊢ ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) → ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
27	26	a2d	⊢ ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) → ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) → ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
28	7 10 13 10 15 27	uzind4	⊢ ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) → ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
29	28	com12	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
30	29	ad2ant2r	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) → ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
31		relxp	⊢ Rel ( 𝑋 × ℝ⁺ )
32	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → 𝐹 : ℕ ⟶ ( 𝑋 × ℝ⁺ ) )
33		simplrl	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → 𝑛 ∈ ℕ )
34	32 33	ffvelrnd	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ( 𝑋 × ℝ⁺ ) )
35		1st2nd	⊢ ( ( Rel ( 𝑋 × ℝ⁺ ) ∧ ( 𝐹 ‘ 𝑛 ) ∈ ( 𝑋 × ℝ⁺ ) ) → ( 𝐹 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
36	31 34 35	sylancr	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑛 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
37	36	fveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ) )
38		df-ov	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
39	37 38	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
40	1	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
41		xp1st	⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( 𝑋 × ℝ⁺ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ 𝑋 )
42	34 41	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ 𝑋 )
43		xp2nd	⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( 𝑋 × ℝ⁺ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ⁺ )
44	34 43	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ⁺ )
45	44	rpxrd	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ^* )
46		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → 𝑟 ∈ ℝ⁺ )
47	46	rpxrd	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → 𝑟 ∈ ℝ^* )
48		simplrr	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 )
49		rpre	⊢ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ⁺ → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
50		rpre	⊢ ( 𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ )
51		ltle	⊢ ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑟 ) )
52	49 50 51	syl2an	⊢ ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ⁺ ∧ 𝑟 ∈ ℝ⁺ ) → ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑟 ) )
53	44 46 52	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑟 ) )
54	48 53	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑟 )
55		ssbl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ 𝑋 ) ∧ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ^* ∧ 𝑟 ∈ ℝ^* ) ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑟 ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ( ball ‘ 𝐷 ) 𝑟 ) )
56	40 42 45 47 54 55	syl221anc	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ( ball ‘ 𝐷 ) 𝑟 ) )
57	39 56	eqsstrd	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ⊆ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ( ball ‘ 𝐷 ) 𝑟 ) )
58		sstr2	⊢ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) → ( ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ⊆ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ( ball ‘ 𝐷 ) 𝑟 ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ( ball ‘ 𝐷 ) 𝑟 ) ) )
59	57 58	syl5com	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ( ball ‘ 𝐷 ) 𝑟 ) ) )
60		simprl	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) → 𝑛 ∈ ℕ )
61	60 16	sylan	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → 𝑘 ∈ ℕ )
62	32 61	ffvelrnd	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑋 × ℝ⁺ ) )
63		xp1st	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑋 × ℝ⁺ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝑋 )
64	62 63	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝑋 )
65		xp2nd	⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑋 × ℝ⁺ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ⁺ )
66	62 65	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ⁺ )
67		blcntr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝑋 ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ⁺ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
68	40 64 66 67	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
69		1st2nd	⊢ ( ( Rel ( 𝑋 × ℝ⁺ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑋 × ℝ⁺ ) ) → ( 𝐹 ‘ 𝑘 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ )
70	31 62 69	sylancr	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑘 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ )
71	70	fveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ ) )
72		df-ov	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ⟩ )
73	71 72	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ( ball ‘ 𝐷 ) ( 2^nd ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
74	68 73	eleqtrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) )
75		ssel	⊢ ( ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ( ball ‘ 𝐷 ) 𝑟 ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ( ball ‘ 𝐷 ) 𝑟 ) ) )
76	59 74 75	syl6ci	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) → ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ( ball ‘ 𝐷 ) 𝑟 ) ) )
77		elbl2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑟 ∈ ℝ^* ) ∧ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ 𝑋 ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ 𝑋 ) ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ( ball ‘ 𝐷 ) 𝑟 ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) 𝐷 ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑟 ) )
78	40 47 42 64 77	syl22anc	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ( ball ‘ 𝐷 ) 𝑟 ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) 𝐷 ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑟 ) )
79	76 78	sylibd	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) ∧ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ) → ( ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) 𝐷 ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑟 ) )
80	79	ex	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) → ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) → ( ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑘 ) ) ⊆ ( ( ball ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑛 ) ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) 𝐷 ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑟 ) ) )
81	30 80	mpdd	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) → ( 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) 𝐷 ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑟 ) )
82	81	ralrimiv	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑛 ∈ ℕ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 ) ) → ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) 𝐷 ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑟 )
83	82	expr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑛 ∈ ℕ ) → ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 → ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) 𝐷 ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑟 ) )
84	83	reximdva	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) → ( ∃ 𝑛 ∈ ℕ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 → ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) 𝐷 ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑟 ) )
85	84	ralimdva	⊢ ( 𝜑 → ( ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑛 ∈ ℕ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑟 → ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) 𝐷 ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑟 ) )
86	4 85	mpd	⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) 𝐷 ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑟 )
87		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
88		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
89		fvco3	⊢ ( ( 𝐹 : ℕ ⟶ ( 𝑋 × ℝ⁺ ) ∧ 𝑘 ∈ ℕ ) → ( ( 1^st ∘ 𝐹 ) ‘ 𝑘 ) = ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) )
90	2 89	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 1^st ∘ 𝐹 ) ‘ 𝑘 ) = ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) )
91		fvco3	⊢ ( ( 𝐹 : ℕ ⟶ ( 𝑋 × ℝ⁺ ) ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ∘ 𝐹 ) ‘ 𝑛 ) = ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) )
92	2 91	sylan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ∘ 𝐹 ) ‘ 𝑛 ) = ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) )
93		1stcof	⊢ ( 𝐹 : ℕ ⟶ ( 𝑋 × ℝ⁺ ) → ( 1^st ∘ 𝐹 ) : ℕ ⟶ 𝑋 )
94	2 93	syl	⊢ ( 𝜑 → ( 1^st ∘ 𝐹 ) : ℕ ⟶ 𝑋 )
95	87 1 88 90 92 94	iscauf	⊢ ( 𝜑 → ( ( 1^st ∘ 𝐹 ) ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ_≥ ‘ 𝑛 ) ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) 𝐷 ( 1^st ‘ ( 𝐹 ‘ 𝑘 ) ) ) < 𝑟 ) )
96	86 95	mpbird	⊢ ( 𝜑 → ( 1^st ∘ 𝐹 ) ∈ ( Cau ‘ 𝐷 ) )

Metamath Proof Explorer

Theorem caubl

Proof