Metamath Proof Explorer


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 ffvelrnda ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹𝑘 ) ∈ 𝑋 )
21 20 1 eleqtrdi ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹𝑘 ) ∈ ( ℝ ↑m 𝐼 ) )
22 elmapi ( ( 𝐹𝑘 ) ∈ ( ℝ ↑m 𝐼 ) → ( 𝐹𝑘 ) : 𝐼 ⟶ ℝ )
23 21 22 syl ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹𝑘 ) : 𝐼 ⟶ ℝ )
24 23 ffvelrnda ( ( ( 𝜑𝑘 ∈ ℕ ) ∧ 𝑛𝐼 ) → ( ( 𝐹𝑘 ) ‘ 𝑛 ) ∈ ℝ )
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 ffvelrnd ( ( ( ( 𝜑𝑛𝐼 ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( 𝐹𝑘 ) ∈ 𝑋 )
44 simplr ( ( ( ( 𝜑𝑛𝐼 ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → 𝑗 ∈ ℕ )
45 40 44 ffvelrnd ( ( ( ( 𝜑𝑛𝐼 ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( 𝐹𝑗 ) ∈ 𝑋 )
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 ffvelrnda ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐹𝑗 ) ∈ 𝑋 )
58 57 1 eleqtrdi ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐹𝑗 ) ∈ ( ℝ ↑m 𝐼 ) )
59 elmapi ( ( 𝐹𝑗 ) ∈ ( ℝ ↑m 𝐼 ) → ( 𝐹𝑗 ) : 𝐼 ⟶ ℝ )
60 58 59 syl ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐹𝑗 ) : 𝐼 ⟶ ℝ )
61 60 ffvelrnda ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑛𝐼 ) → ( ( 𝐹𝑗 ) ‘ 𝑛 ) ∈ ℝ )
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 syl5bb ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝐼 ≠ ∅ ) ) → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ𝑗 ) ∀ 𝑛𝐼 ( ( ( 𝐹𝑘 ) ‘ 𝑛 ) 𝑀 ( 𝑃𝑛 ) ) < ( 𝑥 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ↔ ∀ 𝑛𝐼𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( ( 𝐹𝑘 ) ‘ 𝑛 ) 𝑀 ( 𝑃𝑛 ) ) < ( 𝑥 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
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 ffvelrnda ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝐼 ≠ ∅ ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹𝑘 ) ∈ 𝑋 )
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 ( ⇝𝑡𝐽 ) )