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 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 ( ⇝𝑡 ‘ 𝐽 ) )