rrncmslem

	Ref	Expression
Hypotheses	rrnval.1	$⊢ X = ℝ^{I}$
	rrndstprj1.1	$⊢ M = {(abs \circ -) ↾}_{ℝ^{2}}$
	rrncms.3	$⊢ J = MetOpen (ℝ^{n} (I))$
	rrncms.4	$⊢ φ \to I \in Fin$
	rrncms.5	$⊢ φ \to F \in Cau (ℝ^{n} (I))$
	rrncms.6	$⊢ φ \to F : ℕ ⟶ X$
	rrncms.7	$⊢ P = (m \in I ⟼ ⇝ ((t \in ℕ ⟼ F (t) (m))))$
Assertion	rrncmslem	$⊢ φ \to F \in dom \underset{t}{⇝} (J)$

Proof

Step	Hyp	Ref	Expression
1		rrnval.1	$⊢ X = ℝ^{I}$
2		rrndstprj1.1	$⊢ M = {(abs \circ -) ↾}_{ℝ^{2}}$
3		rrncms.3	$⊢ J = MetOpen (ℝ^{n} (I))$
4		rrncms.4	$⊢ φ \to I \in Fin$
5		rrncms.5	$⊢ φ \to F \in Cau (ℝ^{n} (I))$
6		rrncms.6	$⊢ φ \to F : ℕ ⟶ X$
7		rrncms.7	$⊢ P = (m \in I ⟼ ⇝ ((t \in ℕ ⟼ F (t) (m))))$
8		lmrel	$⊢ Rel \underset{t}{⇝} (J)$
9		fvex	$⊢ ⇝ ((t \in ℕ ⟼ F (t) (m))) \in V$
10	9 7	fnmpti	$⊢ P Fn I$
11	10	a1i	$⊢ φ \to P Fn I$
12		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
13		1zzd	$⊢ (φ \land n \in I) \to 1 \in ℤ$
14		fveq2	$⊢ t = k \to F (t) = F (k)$
15	14	fveq1d	$⊢ t = k \to F (t) (n) = F (k) (n)$
16		eqid	$⊢ (t \in ℕ ⟼ F (t) (n)) = (t \in ℕ ⟼ F (t) (n))$
17		fvex	$⊢ F (k) (n) \in V$
18	15 16 17	fvmpt	$⊢ k \in ℕ \to (t \in ℕ ⟼ F (t) (n)) (k) = F (k) (n)$
19	18	adantl	$⊢ ((φ \land n \in I) \land k \in ℕ) \to (t \in ℕ ⟼ F (t) (n)) (k) = F (k) (n)$
20	6	ffvelrnda	$⊢ (φ \land k \in ℕ) \to F (k) \in X$
21	20 1	eleqtrdi	$⊢ (φ \land k \in ℕ) \to F (k) \in (ℝ^{I})$
22		elmapi	$⊢ F (k) \in (ℝ^{I}) \to F (k) : I ⟶ ℝ$
23	21 22	syl	$⊢ (φ \land k \in ℕ) \to F (k) : I ⟶ ℝ$
24	23	ffvelrnda	$⊢ ((φ \land k \in ℕ) \land n \in I) \to F (k) (n) \in ℝ$
25	24	an32s	$⊢ ((φ \land n \in I) \land k \in ℕ) \to F (k) (n) \in ℝ$
26	19 25	eqeltrd	$⊢ ((φ \land n \in I) \land k \in ℕ) \to (t \in ℕ ⟼ F (t) (n)) (k) \in ℝ$
27	26	recnd	$⊢ ((φ \land n \in I) \land k \in ℕ) \to (t \in ℕ ⟼ F (t) (n)) (k) \in ℂ$
28	1	rrnmet	$⊢ I \in Fin \to ℝ^{n} (I) \in Met (X)$
29	4 28	syl	$⊢ φ \to ℝ^{n} (I) \in Met (X)$
30		metxmet	$⊢ ℝ^{n} (I) \in Met (X) \to ℝ^{n} (I) \in ∞Met (X)$
31	29 30	syl	$⊢ φ \to ℝ^{n} (I) \in ∞Met (X)$
32		1zzd	$⊢ φ \to 1 \in ℤ$
33		eqidd	$⊢ (φ \land k \in ℕ) \to F (k) = F (k)$
34		eqidd	$⊢ (φ \land j \in ℕ) \to F (j) = F (j)$
35	12 31 32 33 34 6	iscauf	$⊢ φ \to (F \in Cau (ℝ^{n} (I)) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (j) ℝ^{n} (I) F (k) < x)$
36	5 35	mpbid	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (j) ℝ^{n} (I) F (k) < x$
37	36	adantr	$⊢ (φ \land n \in I) \to \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (j) ℝ^{n} (I) F (k) < x$
38	4	ad3antrrr	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to I \in Fin$
39		simpllr	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to n \in I$
40	6	ad3antrrr	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F : ℕ ⟶ X$
41		eluznn	$⊢ (j \in ℕ \land k \in ℤ_{\geq j}) \to k \in ℕ$
42	41	adantll	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to k \in ℕ$
43	40 42	ffvelrnd	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F (k) \in X$
44		simplr	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to j \in ℕ$
45	40 44	ffvelrnd	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F (j) \in X$
46	1 2	rrndstprj1	$⊢ ((I \in Fin \land n \in I) \land (F (k) \in X \land F (j) \in X)) \to F (k) (n) M F (j) (n) \leq F (k) ℝ^{n} (I) F (j)$
47	38 39 43 45 46	syl22anc	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F (k) (n) M F (j) (n) \leq F (k) ℝ^{n} (I) F (j)$
48	29	ad3antrrr	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to ℝ^{n} (I) \in Met (X)$
49		metsym	$⊢ (ℝ^{n} (I) \in Met (X) \land F (k) \in X \land F (j) \in X) \to F (k) ℝ^{n} (I) F (j) = F (j) ℝ^{n} (I) F (k)$
50	48 43 45 49	syl3anc	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F (k) ℝ^{n} (I) F (j) = F (j) ℝ^{n} (I) F (k)$
51	47 50	breqtrd	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F (k) (n) M F (j) (n) \leq F (j) ℝ^{n} (I) F (k)$
52	51	adantllr	$⊢ ((((φ \land n \in I) \land x \in ℝ^{+}) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F (k) (n) M F (j) (n) \leq F (j) ℝ^{n} (I) F (k)$
53	2	remet	$⊢ M \in Met (ℝ)$
54	53	a1i	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to M \in Met (ℝ)$
55		simpll	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to (φ \land n \in I)$
56	55 42 25	syl2anc	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F (k) (n) \in ℝ$
57	6	ffvelrnda	$⊢ (φ \land j \in ℕ) \to F (j) \in X$
58	57 1	eleqtrdi	$⊢ (φ \land j \in ℕ) \to F (j) \in (ℝ^{I})$
59		elmapi	$⊢ F (j) \in (ℝ^{I}) \to F (j) : I ⟶ ℝ$
60	58 59	syl	$⊢ (φ \land j \in ℕ) \to F (j) : I ⟶ ℝ$
61	60	ffvelrnda	$⊢ ((φ \land j \in ℕ) \land n \in I) \to F (j) (n) \in ℝ$
62	61	an32s	$⊢ ((φ \land n \in I) \land j \in ℕ) \to F (j) (n) \in ℝ$
63	62	adantr	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F (j) (n) \in ℝ$
64		metcl	$⊢ (M \in Met (ℝ) \land F (k) (n) \in ℝ \land F (j) (n) \in ℝ) \to F (k) (n) M F (j) (n) \in ℝ$
65	54 56 63 64	syl3anc	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F (k) (n) M F (j) (n) \in ℝ$
66	65	adantllr	$⊢ ((((φ \land n \in I) \land x \in ℝ^{+}) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F (k) (n) M F (j) (n) \in ℝ$
67		metcl	$⊢ (ℝ^{n} (I) \in Met (X) \land F (j) \in X \land F (k) \in X) \to F (j) ℝ^{n} (I) F (k) \in ℝ$
68	48 45 43 67	syl3anc	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F (j) ℝ^{n} (I) F (k) \in ℝ$
69	68	adantllr	$⊢ ((((φ \land n \in I) \land x \in ℝ^{+}) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F (j) ℝ^{n} (I) F (k) \in ℝ$
70		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
71	70	adantl	$⊢ ((φ \land n \in I) \land x \in ℝ^{+}) \to x \in ℝ$
72	71	ad2antrr	$⊢ ((((φ \land n \in I) \land x \in ℝ^{+}) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to x \in ℝ$
73		lelttr	$⊢ (F (k) (n) M F (j) (n) \in ℝ \land F (j) ℝ^{n} (I) F (k) \in ℝ \land x \in ℝ) \to ((F (k) (n) M F (j) (n) \leq F (j) ℝ^{n} (I) F (k) \land F (j) ℝ^{n} (I) F (k) < x) \to F (k) (n) M F (j) (n) < x)$
74	66 69 72 73	syl3anc	$⊢ ((((φ \land n \in I) \land x \in ℝ^{+}) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to ((F (k) (n) M F (j) (n) \leq F (j) ℝ^{n} (I) F (k) \land F (j) ℝ^{n} (I) F (k) < x) \to F (k) (n) M F (j) (n) < x)$
75	52 74	mpand	$⊢ ((((φ \land n \in I) \land x \in ℝ^{+}) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to (F (j) ℝ^{n} (I) F (k) < x \to F (k) (n) M F (j) (n) < x)$
76	75	ralimdva	$⊢ (((φ \land n \in I) \land x \in ℝ^{+}) \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} F (j) ℝ^{n} (I) F (k) < x \to \forall k \in ℤ_{\geq j} F (k) (n) M F (j) (n) < x)$
77	76	reximdva	$⊢ ((φ \land n \in I) \land x \in ℝ^{+}) \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} F (j) ℝ^{n} (I) F (k) < x \to \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) (n) M F (j) (n) < x)$
78	77	ralimdva	$⊢ (φ \land n \in I) \to (\forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (j) ℝ^{n} (I) F (k) < x \to \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) (n) M F (j) (n) < x)$
79	2	remetdval	$⊢ (F (k) (n) \in ℝ \land F (j) (n) \in ℝ) \to F (k) (n) M F (j) (n) = \|F (k) (n) - F (j) (n)\|$
80	56 63 79	syl2anc	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F (k) (n) M F (j) (n) = \|F (k) (n) - F (j) (n)\|$
81	42 18	syl	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to (t \in ℕ ⟼ F (t) (n)) (k) = F (k) (n)$
82		fveq2	$⊢ t = j \to F (t) = F (j)$
83	82	fveq1d	$⊢ t = j \to F (t) (n) = F (j) (n)$
84		fvex	$⊢ F (j) (n) \in V$
85	83 16 84	fvmpt	$⊢ j \in ℕ \to (t \in ℕ ⟼ F (t) (n)) (j) = F (j) (n)$
86	85	ad2antlr	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to (t \in ℕ ⟼ F (t) (n)) (j) = F (j) (n)$
87	81 86	oveq12d	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to (t \in ℕ ⟼ F (t) (n)) (k) - (t \in ℕ ⟼ F (t) (n)) (j) = F (k) (n) - F (j) (n)$
88	87	fveq2d	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to \|(t \in ℕ ⟼ F (t) (n)) (k) - (t \in ℕ ⟼ F (t) (n)) (j)\| = \|F (k) (n) - F (j) (n)\|$
89	80 88	eqtr4d	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to F (k) (n) M F (j) (n) = \|(t \in ℕ ⟼ F (t) (n)) (k) - (t \in ℕ ⟼ F (t) (n)) (j)\|$
90	89	breq1d	$⊢ (((φ \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to (F (k) (n) M F (j) (n) < x \leftrightarrow \|(t \in ℕ ⟼ F (t) (n)) (k) - (t \in ℕ ⟼ F (t) (n)) (j)\| < x)$
91	90	ralbidva	$⊢ ((φ \land n \in I) \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} F (k) (n) M F (j) (n) < x \leftrightarrow \forall k \in ℤ_{\geq j} \|(t \in ℕ ⟼ F (t) (n)) (k) - (t \in ℕ ⟼ F (t) (n)) (j)\| < x)$
92	91	rexbidva	$⊢ (φ \land n \in I) \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) (n) M F (j) (n) < x \leftrightarrow \exists j \in ℕ \forall k \in ℤ_{\geq j} \|(t \in ℕ ⟼ F (t) (n)) (k) - (t \in ℕ ⟼ F (t) (n)) (j)\| < x)$
93	92	ralbidv	$⊢ (φ \land n \in I) \to (\forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) (n) M F (j) (n) < x \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} \|(t \in ℕ ⟼ F (t) (n)) (k) - (t \in ℕ ⟼ F (t) (n)) (j)\| < x)$
94	78 93	sylibd	$⊢ (φ \land n \in I) \to (\forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (j) ℝ^{n} (I) F (k) < x \to \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} \|(t \in ℕ ⟼ F (t) (n)) (k) - (t \in ℕ ⟼ F (t) (n)) (j)\| < x)$
95	37 94	mpd	$⊢ (φ \land n \in I) \to \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} \|(t \in ℕ ⟼ F (t) (n)) (k) - (t \in ℕ ⟼ F (t) (n)) (j)\| < x$
96		nnex	$⊢ ℕ \in V$
97	96	mptex	$⊢ (t \in ℕ ⟼ F (t) (n)) \in V$
98	97	a1i	$⊢ (φ \land n \in I) \to (t \in ℕ ⟼ F (t) (n)) \in V$
99	12 27 95 98	caucvg	$⊢ (φ \land n \in I) \to (t \in ℕ ⟼ F (t) (n)) \in dom ⇝$
100		climdm	$⊢ (t \in ℕ ⟼ F (t) (n)) \in dom ⇝ \leftrightarrow (t \in ℕ ⟼ F (t) (n)) ⇝ ⇝ ((t \in ℕ ⟼ F (t) (n)))$
101	99 100	sylib	$⊢ (φ \land n \in I) \to (t \in ℕ ⟼ F (t) (n)) ⇝ ⇝ ((t \in ℕ ⟼ F (t) (n)))$
102		fveq2	$⊢ m = n \to F (t) (m) = F (t) (n)$
103	102	mpteq2dv	$⊢ m = n \to (t \in ℕ ⟼ F (t) (m)) = (t \in ℕ ⟼ F (t) (n))$
104	103	fveq2d	$⊢ m = n \to ⇝ ((t \in ℕ ⟼ F (t) (m))) = ⇝ ((t \in ℕ ⟼ F (t) (n)))$
105		fvex	$⊢ ⇝ ((t \in ℕ ⟼ F (t) (n))) \in V$
106	104 7 105	fvmpt	$⊢ n \in I \to P (n) = ⇝ ((t \in ℕ ⟼ F (t) (n)))$
107	106	adantl	$⊢ (φ \land n \in I) \to P (n) = ⇝ ((t \in ℕ ⟼ F (t) (n)))$
108	101 107	breqtrrd	$⊢ (φ \land n \in I) \to (t \in ℕ ⟼ F (t) (n)) ⇝ P (n)$
109	12 13 108 26	climrecl	$⊢ (φ \land n \in I) \to P (n) \in ℝ$
110	109	ralrimiva	$⊢ φ \to \forall n \in I P (n) \in ℝ$
111		ffnfv	$⊢ P : I ⟶ ℝ \leftrightarrow (P Fn I \land \forall n \in I P (n) \in ℝ)$
112	11 110 111	sylanbrc	$⊢ φ \to P : I ⟶ ℝ$
113		reex	$⊢ ℝ \in V$
114		elmapg	$⊢ (ℝ \in V \land I \in Fin) \to (P \in (ℝ^{I}) \leftrightarrow P : I ⟶ ℝ)$
115	113 4 114	sylancr	$⊢ φ \to (P \in (ℝ^{I}) \leftrightarrow P : I ⟶ ℝ)$
116	112 115	mpbird	$⊢ φ \to P \in (ℝ^{I})$
117	116 1	eleqtrrdi	$⊢ φ \to P \in X$
118		1nn	$⊢ 1 \in ℕ$
119	4	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land I = \emptyset)) \land k \in ℕ) \to I \in Fin$
120	20	adantlr	$⊢ ((φ \land (x \in ℝ^{+} \land I = \emptyset)) \land k \in ℕ) \to F (k) \in X$
121	117	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land I = \emptyset)) \land k \in ℕ) \to P \in X$
122	1	rrnmval	$⊢ (I \in Fin \land F (k) \in X \land P \in X) \to F (k) ℝ^{n} (I) P = \sqrt{\sum_{y \in I} {(F (k) (y) - P (y))}^{2}}$
123	119 120 121 122	syl3anc	$⊢ ((φ \land (x \in ℝ^{+} \land I = \emptyset)) \land k \in ℕ) \to F (k) ℝ^{n} (I) P = \sqrt{\sum_{y \in I} {(F (k) (y) - P (y))}^{2}}$
124		simplrr	$⊢ ((φ \land (x \in ℝ^{+} \land I = \emptyset)) \land k \in ℕ) \to I = \emptyset$
125	124	sumeq1d	$⊢ ((φ \land (x \in ℝ^{+} \land I = \emptyset)) \land k \in ℕ) \to \sum_{y \in I} {(F (k) (y) - P (y))}^{2} = \sum_{y \in \emptyset} {(F (k) (y) - P (y))}^{2}$
126		sum0	$⊢ \sum_{y \in \emptyset} {(F (k) (y) - P (y))}^{2} = 0$
127	125 126	eqtrdi	$⊢ ((φ \land (x \in ℝ^{+} \land I = \emptyset)) \land k \in ℕ) \to \sum_{y \in I} {(F (k) (y) - P (y))}^{2} = 0$
128	127	fveq2d	$⊢ ((φ \land (x \in ℝ^{+} \land I = \emptyset)) \land k \in ℕ) \to \sqrt{\sum_{y \in I} {(F (k) (y) - P (y))}^{2}} = \sqrt{0}$
129	123 128	eqtrd	$⊢ ((φ \land (x \in ℝ^{+} \land I = \emptyset)) \land k \in ℕ) \to F (k) ℝ^{n} (I) P = \sqrt{0}$
130		sqrt0	$⊢ \sqrt{0} = 0$
131	129 130	eqtrdi	$⊢ ((φ \land (x \in ℝ^{+} \land I = \emptyset)) \land k \in ℕ) \to F (k) ℝ^{n} (I) P = 0$
132		simplrl	$⊢ ((φ \land (x \in ℝ^{+} \land I = \emptyset)) \land k \in ℕ) \to x \in ℝ^{+}$
133	132	rpgt0d	$⊢ ((φ \land (x \in ℝ^{+} \land I = \emptyset)) \land k \in ℕ) \to 0 < x$
134	131 133	eqbrtrd	$⊢ ((φ \land (x \in ℝ^{+} \land I = \emptyset)) \land k \in ℕ) \to F (k) ℝ^{n} (I) P < x$
135	134	ralrimiva	$⊢ (φ \land (x \in ℝ^{+} \land I = \emptyset)) \to \forall k \in ℕ F (k) ℝ^{n} (I) P < x$
136		fveq2	$⊢ j = 1 \to ℤ_{\geq j} = ℤ_{\geq 1}$
137	136 12	eqtr4di	$⊢ j = 1 \to ℤ_{\geq j} = ℕ$
138	137	raleqdv	$⊢ j = 1 \to (\forall k \in ℤ_{\geq j} F (k) ℝ^{n} (I) P < x \leftrightarrow \forall k \in ℕ F (k) ℝ^{n} (I) P < x)$
139	138	rspcev	$⊢ (1 \in ℕ \land \forall k \in ℕ F (k) ℝ^{n} (I) P < x) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) ℝ^{n} (I) P < x$
140	118 135 139	sylancr	$⊢ (φ \land (x \in ℝ^{+} \land I = \emptyset)) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) ℝ^{n} (I) P < x$
141	140	expr	$⊢ (φ \land x \in ℝ^{+}) \to (I = \emptyset \to \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) ℝ^{n} (I) P < x)$
142		1zzd	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \to 1 \in ℤ$
143		simprl	$⊢ (φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \to x \in ℝ^{+}$
144		simprr	$⊢ (φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \to I \neq \emptyset$
145	4	adantr	$⊢ (φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \to I \in Fin$
146		hashnncl	$⊢ I \in Fin \to (\|I\| \in ℕ \leftrightarrow I \neq \emptyset)$
147	145 146	syl	$⊢ (φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \to (\|I\| \in ℕ \leftrightarrow I \neq \emptyset)$
148	144 147	mpbird	$⊢ (φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \to \|I\| \in ℕ$
149	148	nnrpd	$⊢ (φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \to \|I\| \in ℝ^{+}$
150	149	rpsqrtcld	$⊢ (φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \to \sqrt{\|I\|} \in ℝ^{+}$
151	143 150	rpdivcld	$⊢ (φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \to \frac{x}{\sqrt{\|I\|}} \in ℝ^{+}$
152	151	adantr	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \to \frac{x}{\sqrt{\|I\|}} \in ℝ^{+}$
153	18	adantl	$⊢ (((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \land k \in ℕ) \to (t \in ℕ ⟼ F (t) (n)) (k) = F (k) (n)$
154	108	adantlr	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \to (t \in ℕ ⟼ F (t) (n)) ⇝ P (n)$
155	12 142 152 153 154	climi2	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} \|F (k) (n) - P (n)\| < \frac{x}{\sqrt{\|I\|}}$
156		1z	$⊢ 1 \in ℤ$
157	12	rexuz3	$⊢ 1 \in ℤ \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}})$
158	156 157	ax-mp	$⊢ \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}}$
159	25	adantllr	$⊢ (((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \land k \in ℕ) \to F (k) (n) \in ℝ$
160	109	adantlr	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \to P (n) \in ℝ$
161	160	adantr	$⊢ (((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \land k \in ℕ) \to P (n) \in ℝ$
162	2	remetdval	$⊢ (F (k) (n) \in ℝ \land P (n) \in ℝ) \to F (k) (n) M P (n) = \|F (k) (n) - P (n)\|$
163	159 161 162	syl2anc	$⊢ (((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \land k \in ℕ) \to F (k) (n) M P (n) = \|F (k) (n) - P (n)\|$
164	163	breq1d	$⊢ (((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \land k \in ℕ) \to (F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \leftrightarrow \|F (k) (n) - P (n)\| < \frac{x}{\sqrt{\|I\|}})$
165	41 164	sylan2	$⊢ (((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to (F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \leftrightarrow \|F (k) (n) - P (n)\| < \frac{x}{\sqrt{\|I\|}})$
166	165	anassrs	$⊢ ((((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to (F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \leftrightarrow \|F (k) (n) - P (n)\| < \frac{x}{\sqrt{\|I\|}})$
167	166	ralbidva	$⊢ (((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \leftrightarrow \forall k \in ℤ_{\geq j} \|F (k) (n) - P (n)\| < \frac{x}{\sqrt{\|I\|}})$
168	167	rexbidva	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \leftrightarrow \exists j \in ℕ \forall k \in ℤ_{\geq j} \|F (k) (n) - P (n)\| < \frac{x}{\sqrt{\|I\|}})$
169	158 168	bitr3id	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \leftrightarrow \exists j \in ℕ \forall k \in ℤ_{\geq j} \|F (k) (n) - P (n)\| < \frac{x}{\sqrt{\|I\|}})$
170	155 169	mpbird	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land n \in I) \to \exists j \in ℤ \forall k \in ℤ_{\geq j} F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}}$
171	170	ralrimiva	$⊢ (φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \to \forall n \in I \exists j \in ℤ \forall k \in ℤ_{\geq j} F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}}$
172	12	rexuz3	$⊢ 1 \in ℤ \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} \forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}})$
173	156 172	ax-mp	$⊢ \exists j \in ℕ \forall k \in ℤ_{\geq j} \forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}}$
174		rexfiuz	$⊢ I \in Fin \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \leftrightarrow \forall n \in I \exists j \in ℤ \forall k \in ℤ_{\geq j} F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}})$
175	145 174	syl	$⊢ (φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} \forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \leftrightarrow \forall n \in I \exists j \in ℤ \forall k \in ℤ_{\geq j} F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}})$
176	173 175	syl5bb	$⊢ (φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} \forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \leftrightarrow \forall n \in I \exists j \in ℤ \forall k \in ℤ_{\geq j} F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}})$
177	171 176	mpbird	$⊢ (φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} \forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}}$
178	4	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land k \in ℕ) \to I \in Fin$
179		simplrr	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land k \in ℕ) \to I \neq \emptyset$
180		eldifsn	$⊢ I \in (Fin ∖ \{\emptyset\}) \leftrightarrow (I \in Fin \land I \neq \emptyset)$
181	178 179 180	sylanbrc	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land k \in ℕ) \to I \in (Fin ∖ \{\emptyset\})$
182	6	adantr	$⊢ (φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \to F : ℕ ⟶ X$
183	182	ffvelrnda	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land k \in ℕ) \to F (k) \in X$
184	117	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land k \in ℕ) \to P \in X$
185	151	adantr	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land k \in ℕ) \to \frac{x}{\sqrt{\|I\|}} \in ℝ^{+}$
186	1 2	rrndstprj2	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F (k) \in X \land P \in X) \land (\frac{x}{\sqrt{\|I\|}} \in ℝ^{+} \land \forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}})) \to F (k) ℝ^{n} (I) P < (\frac{x}{\sqrt{\|I\|}}) \sqrt{\|I\|}$
187	186	expr	$⊢ ((I \in (Fin ∖ \{\emptyset\}) \land F (k) \in X \land P \in X) \land \frac{x}{\sqrt{\|I\|}} \in ℝ^{+}) \to (\forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \to F (k) ℝ^{n} (I) P < (\frac{x}{\sqrt{\|I\|}}) \sqrt{\|I\|})$
188	181 183 184 185 187	syl31anc	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land k \in ℕ) \to (\forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \to F (k) ℝ^{n} (I) P < (\frac{x}{\sqrt{\|I\|}}) \sqrt{\|I\|})$
189		simplrl	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land k \in ℕ) \to x \in ℝ^{+}$
190	189	rpcnd	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land k \in ℕ) \to x \in ℂ$
191	150	adantr	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land k \in ℕ) \to \sqrt{\|I\|} \in ℝ^{+}$
192	191	rpcnd	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land k \in ℕ) \to \sqrt{\|I\|} \in ℂ$
193	191	rpne0d	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land k \in ℕ) \to \sqrt{\|I\|} \neq 0$
194	190 192 193	divcan1d	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land k \in ℕ) \to (\frac{x}{\sqrt{\|I\|}}) \sqrt{\|I\|} = x$
195	194	breq2d	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land k \in ℕ) \to (F (k) ℝ^{n} (I) P < (\frac{x}{\sqrt{\|I\|}}) \sqrt{\|I\|} \leftrightarrow F (k) ℝ^{n} (I) P < x)$
196	188 195	sylibd	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land k \in ℕ) \to (\forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \to F (k) ℝ^{n} (I) P < x)$
197	41 196	sylan2	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land (j \in ℕ \land k \in ℤ_{\geq j})) \to (\forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \to F (k) ℝ^{n} (I) P < x)$
198	197	anassrs	$⊢ (((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land j \in ℕ) \land k \in ℤ_{\geq j}) \to (\forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \to F (k) ℝ^{n} (I) P < x)$
199	198	ralimdva	$⊢ ((φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} \forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \to \forall k \in ℤ_{\geq j} F (k) ℝ^{n} (I) P < x)$
200	199	reximdva	$⊢ (φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} \forall n \in I F (k) (n) M P (n) < \frac{x}{\sqrt{\|I\|}} \to \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) ℝ^{n} (I) P < x)$
201	177 200	mpd	$⊢ (φ \land (x \in ℝ^{+} \land I \neq \emptyset)) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) ℝ^{n} (I) P < x$
202	201	expr	$⊢ (φ \land x \in ℝ^{+}) \to (I \neq \emptyset \to \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) ℝ^{n} (I) P < x)$
203	141 202	pm2.61dne	$⊢ (φ \land x \in ℝ^{+}) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) ℝ^{n} (I) P < x$
204	203	ralrimiva	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) ℝ^{n} (I) P < x$
205	3 31 12 32 33 6	lmmbrf	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (P \in X \land \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) ℝ^{n} (I) P < x))$
206	117 204 205	mpbir2and	$⊢ φ \to F \underset{t}{⇝} (J) P$
207		releldm	$⊢ (Rel \underset{t}{⇝} (J) \land F \underset{t}{⇝} (J) P) \to F \in dom \underset{t}{⇝} (J)$
208	8 206 207	sylancr	$⊢ φ \to F \in dom \underset{t}{⇝} (J)$

Metamath Proof Explorer

Theorem rrncmslem

Proof