Theorem rrncmslem

Description: Lemma for rrncms . (Contributed by Jeff Madsen, 6-Jun-2014) (Revised by Mario Carneiro, 13-Sep-2015)

	Ref	Expression
Hypotheses	rrnval.1	⊢ 𝑋 = ( ℝ ↑m 𝐼 )
	rrndstprj1.1	⊢ 𝑀 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
	rrncms.3	⊢ 𝐽 = ( MetOpen ‘ ( ℝn ‘ 𝐼 ) )
	rrncms.4	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	rrncms.5	⊢ ( 𝜑 → 𝐹 ∈ ( Cau ‘ ( ℝn ‘ 𝐼 ) ) )
	rrncms.6	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑋 )
	rrncms.7	⊢ 𝑃 = ( 𝑚 ∈ 𝐼 ↦ ( ⇝ ‘ ( 𝑡 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑡 ) ‘ 𝑚 ) ) ) )
Assertion	rrncmslem	⊢ ( 𝜑 → 𝐹 ∈ dom ( ⇝𝑡 ‘ 𝐽 ) )

Proof

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