Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rrncmslem Structured version   Visualization version   GIF version

Theorem rrncmslem 36689
Description: Lemma for rrncms 36690. (Contributed by Jeff Madsen, 6-Jun-2014.) (Revised by Mario Carneiro, 13-Sep-2015.)
Hypotheses
Ref Expression
rrnval.1 𝑋 = (ℝ ↑m 𝐼)
rrndstprj1.1 𝑀 = ((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ))
rrncms.3 𝐽 = (MetOpenβ€˜(ℝnβ€˜πΌ))
rrncms.4 (πœ‘ β†’ 𝐼 ∈ Fin)
rrncms.5 (πœ‘ β†’ 𝐹 ∈ (Cauβ€˜(ℝnβ€˜πΌ)))
rrncms.6 (πœ‘ β†’ 𝐹:β„•βŸΆπ‘‹)
rrncms.7 𝑃 = (π‘š ∈ 𝐼 ↦ ( ⇝ β€˜(𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘š))))
Assertion
Ref Expression
rrncmslem (πœ‘ β†’ 𝐹 ∈ dom (β‡π‘‘β€˜π½))
Distinct variable groups:   π‘š,𝐼   𝑑,π‘š,𝐹
Allowed substitution hints:   πœ‘(𝑑,π‘š)   𝑃(𝑑,π‘š)   𝐼(𝑑)   𝐽(𝑑,π‘š)   𝑀(𝑑,π‘š)   𝑋(𝑑,π‘š)

Proof of Theorem rrncmslem
Dummy variables π‘˜ 𝑛 π‘₯ 𝑦 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lmrel 22726 . 2 Rel (β‡π‘‘β€˜π½)
2 fvex 6902 . . . . . . . 8 ( ⇝ β€˜(𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘š))) ∈ V
3 rrncms.7 . . . . . . . 8 𝑃 = (π‘š ∈ 𝐼 ↦ ( ⇝ β€˜(𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘š))))
42, 3fnmpti 6691 . . . . . . 7 𝑃 Fn 𝐼
54a1i 11 . . . . . 6 (πœ‘ β†’ 𝑃 Fn 𝐼)
6 nnuz 12862 . . . . . . . 8 β„• = (β„€β‰₯β€˜1)
7 1zzd 12590 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ 𝐼) β†’ 1 ∈ β„€)
8 fveq2 6889 . . . . . . . . . . . . . . . 16 (𝑑 = π‘˜ β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘˜))
98fveq1d 6891 . . . . . . . . . . . . . . 15 (𝑑 = π‘˜ β†’ ((πΉβ€˜π‘‘)β€˜π‘›) = ((πΉβ€˜π‘˜)β€˜π‘›))
10 eqid 2733 . . . . . . . . . . . . . . 15 (𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›)) = (𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))
11 fvex 6902 . . . . . . . . . . . . . . 15 ((πΉβ€˜π‘˜)β€˜π‘›) ∈ V
129, 10, 11fvmpt 6996 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„• β†’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘˜) = ((πΉβ€˜π‘˜)β€˜π‘›))
1312adantl 483 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ π‘˜ ∈ β„•) β†’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘˜) = ((πΉβ€˜π‘˜)β€˜π‘›))
14 rrncms.6 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐹:β„•βŸΆπ‘‹)
1514ffvelcdmda 7084 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜) ∈ 𝑋)
16 rrnval.1 . . . . . . . . . . . . . . . . 17 𝑋 = (ℝ ↑m 𝐼)
1715, 16eleqtrdi 2844 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜) ∈ (ℝ ↑m 𝐼))
18 elmapi 8840 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘˜) ∈ (ℝ ↑m 𝐼) β†’ (πΉβ€˜π‘˜):πΌβŸΆβ„)
1917, 18syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜):πΌβŸΆβ„)
2019ffvelcdmda 7084 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ 𝑛 ∈ 𝐼) β†’ ((πΉβ€˜π‘˜)β€˜π‘›) ∈ ℝ)
2120an32s 651 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜π‘˜)β€˜π‘›) ∈ ℝ)
2213, 21eqeltrd 2834 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ π‘˜ ∈ β„•) β†’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘˜) ∈ ℝ)
2322recnd 11239 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ π‘˜ ∈ β„•) β†’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘˜) ∈ β„‚)
24 rrncms.5 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐹 ∈ (Cauβ€˜(ℝnβ€˜πΌ)))
25 rrncms.4 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐼 ∈ Fin)
2616rrnmet 36686 . . . . . . . . . . . . . . . . 17 (𝐼 ∈ Fin β†’ (ℝnβ€˜πΌ) ∈ (Metβ€˜π‘‹))
2725, 26syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (ℝnβ€˜πΌ) ∈ (Metβ€˜π‘‹))
28 metxmet 23832 . . . . . . . . . . . . . . . 16 ((ℝnβ€˜πΌ) ∈ (Metβ€˜π‘‹) β†’ (ℝnβ€˜πΌ) ∈ (∞Metβ€˜π‘‹))
2927, 28syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (ℝnβ€˜πΌ) ∈ (∞Metβ€˜π‘‹))
30 1zzd 12590 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 1 ∈ β„€)
31 eqidd 2734 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜) = (πΉβ€˜π‘˜))
32 eqidd 2734 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) = (πΉβ€˜π‘—))
336, 29, 30, 31, 32, 14iscauf 24789 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐹 ∈ (Cauβ€˜(ℝnβ€˜πΌ)) ↔ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) < π‘₯))
3424, 33mpbid 231 . . . . . . . . . . . . 13 (πœ‘ β†’ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) < π‘₯)
3534adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ 𝐼) β†’ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) < π‘₯)
3625ad3antrrr 729 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ 𝐼 ∈ Fin)
37 simpllr 775 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ 𝑛 ∈ 𝐼)
3814ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ 𝐹:β„•βŸΆπ‘‹)
39 eluznn 12899 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑗 ∈ β„• ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ π‘˜ ∈ β„•)
4039adantll 713 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ π‘˜ ∈ β„•)
4138, 40ffvelcdmd 7085 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (πΉβ€˜π‘˜) ∈ 𝑋)
42 simplr 768 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ 𝑗 ∈ β„•)
4338, 42ffvelcdmd 7085 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (πΉβ€˜π‘—) ∈ 𝑋)
44 rrndstprj1.1 . . . . . . . . . . . . . . . . . . . . 21 𝑀 = ((abs ∘ βˆ’ ) β†Ύ (ℝ Γ— ℝ))
4516, 44rrndstprj1 36687 . . . . . . . . . . . . . . . . . . . 20 (((𝐼 ∈ Fin ∧ 𝑛 ∈ 𝐼) ∧ ((πΉβ€˜π‘˜) ∈ 𝑋 ∧ (πΉβ€˜π‘—) ∈ 𝑋)) β†’ (((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) ≀ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)(πΉβ€˜π‘—)))
4636, 37, 41, 43, 45syl22anc 838 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) ≀ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)(πΉβ€˜π‘—)))
4727ad3antrrr 729 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (ℝnβ€˜πΌ) ∈ (Metβ€˜π‘‹))
48 metsym 23848 . . . . . . . . . . . . . . . . . . . 20 (((ℝnβ€˜πΌ) ∈ (Metβ€˜π‘‹) ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ (πΉβ€˜π‘—) ∈ 𝑋) β†’ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)(πΉβ€˜π‘—)) = ((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)))
4947, 41, 43, 48syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)(πΉβ€˜π‘—)) = ((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)))
5046, 49breqtrd 5174 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) ≀ ((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)))
5150adantllr 718 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) ≀ ((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)))
5244remet 24298 . . . . . . . . . . . . . . . . . . . . 21 𝑀 ∈ (Metβ€˜β„)
5352a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ 𝑀 ∈ (Metβ€˜β„))
54 simpll 766 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (πœ‘ ∧ 𝑛 ∈ 𝐼))
5554, 40, 21syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ ((πΉβ€˜π‘˜)β€˜π‘›) ∈ ℝ)
5614ffvelcdmda 7084 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) ∈ 𝑋)
5756, 16eleqtrdi 2844 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) ∈ (ℝ ↑m 𝐼))
58 elmapi 8840 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πΉβ€˜π‘—) ∈ (ℝ ↑m 𝐼) β†’ (πΉβ€˜π‘—):πΌβŸΆβ„)
5957, 58syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—):πΌβŸΆβ„)
6059ffvelcdmda 7084 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ 𝑛 ∈ 𝐼) β†’ ((πΉβ€˜π‘—)β€˜π‘›) ∈ ℝ)
6160an32s 651 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) β†’ ((πΉβ€˜π‘—)β€˜π‘›) ∈ ℝ)
6261adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ ((πΉβ€˜π‘—)β€˜π‘›) ∈ ℝ)
63 metcl 23830 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 ∈ (Metβ€˜β„) ∧ ((πΉβ€˜π‘˜)β€˜π‘›) ∈ ℝ ∧ ((πΉβ€˜π‘—)β€˜π‘›) ∈ ℝ) β†’ (((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) ∈ ℝ)
6453, 55, 62, 63syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) ∈ ℝ)
6564adantllr 718 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) ∈ ℝ)
66 metcl 23830 . . . . . . . . . . . . . . . . . . . 20 (((ℝnβ€˜πΌ) ∈ (Metβ€˜π‘‹) ∧ (πΉβ€˜π‘—) ∈ 𝑋 ∧ (πΉβ€˜π‘˜) ∈ 𝑋) β†’ ((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) ∈ ℝ)
6747, 43, 41, 66syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ ((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) ∈ ℝ)
6867adantllr 718 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ ((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) ∈ ℝ)
69 rpre 12979 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ ℝ+ β†’ π‘₯ ∈ ℝ)
7069adantl 483 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ π‘₯ ∈ ℝ+) β†’ π‘₯ ∈ ℝ)
7170ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ π‘₯ ∈ ℝ)
72 lelttr 11301 . . . . . . . . . . . . . . . . . 18 (((((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) ∈ ℝ ∧ ((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) ∈ ℝ ∧ π‘₯ ∈ ℝ) β†’ (((((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) ≀ ((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) ∧ ((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) < π‘₯) β†’ (((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) < π‘₯))
7365, 68, 71, 72syl3anc 1372 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (((((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) ≀ ((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) ∧ ((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) < π‘₯) β†’ (((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) < π‘₯))
7451, 73mpand 694 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) < π‘₯ β†’ (((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) < π‘₯))
7574ralimdva 3168 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ π‘₯ ∈ ℝ+) ∧ 𝑗 ∈ β„•) β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) < π‘₯ β†’ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) < π‘₯))
7675reximdva 3169 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ π‘₯ ∈ ℝ+) β†’ (βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) < π‘₯ β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) < π‘₯))
7776ralimdva 3168 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ 𝐼) β†’ (βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) < π‘₯ β†’ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) < π‘₯))
7844remetdval 24297 . . . . . . . . . . . . . . . . . . 19 ((((πΉβ€˜π‘˜)β€˜π‘›) ∈ ℝ ∧ ((πΉβ€˜π‘—)β€˜π‘›) ∈ ℝ) β†’ (((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) = (absβ€˜(((πΉβ€˜π‘˜)β€˜π‘›) βˆ’ ((πΉβ€˜π‘—)β€˜π‘›))))
7955, 62, 78syl2anc 585 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) = (absβ€˜(((πΉβ€˜π‘˜)β€˜π‘›) βˆ’ ((πΉβ€˜π‘—)β€˜π‘›))))
8040, 12syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘˜) = ((πΉβ€˜π‘˜)β€˜π‘›))
81 fveq2 6889 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = 𝑗 β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘—))
8281fveq1d 6891 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 = 𝑗 β†’ ((πΉβ€˜π‘‘)β€˜π‘›) = ((πΉβ€˜π‘—)β€˜π‘›))
83 fvex 6902 . . . . . . . . . . . . . . . . . . . . . 22 ((πΉβ€˜π‘—)β€˜π‘›) ∈ V
8482, 10, 83fvmpt 6996 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ β„• β†’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘—) = ((πΉβ€˜π‘—)β€˜π‘›))
8584ad2antlr 726 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘—) = ((πΉβ€˜π‘—)β€˜π‘›))
8680, 85oveq12d 7424 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘˜) βˆ’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘—)) = (((πΉβ€˜π‘˜)β€˜π‘›) βˆ’ ((πΉβ€˜π‘—)β€˜π‘›)))
8786fveq2d 6893 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (absβ€˜(((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘˜) βˆ’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘—))) = (absβ€˜(((πΉβ€˜π‘˜)β€˜π‘›) βˆ’ ((πΉβ€˜π‘—)β€˜π‘›))))
8879, 87eqtr4d 2776 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) = (absβ€˜(((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘˜) βˆ’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘—))))
8988breq1d 5158 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ ((((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) < π‘₯ ↔ (absβ€˜(((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘˜) βˆ’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘—))) < π‘₯))
9089ralbidva 3176 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) < π‘₯ ↔ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘˜) βˆ’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘—))) < π‘₯))
9190rexbidva 3177 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ 𝐼) β†’ (βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) < π‘₯ ↔ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘˜) βˆ’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘—))) < π‘₯))
9291ralbidv 3178 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ 𝐼) β†’ (βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀((πΉβ€˜π‘—)β€˜π‘›)) < π‘₯ ↔ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘˜) βˆ’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘—))) < π‘₯))
9377, 92sylibd 238 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ 𝐼) β†’ (βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘—)(ℝnβ€˜πΌ)(πΉβ€˜π‘˜)) < π‘₯ β†’ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘˜) βˆ’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘—))) < π‘₯))
9435, 93mpd 15 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ 𝐼) β†’ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘˜) βˆ’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘—))) < π‘₯)
95 nnex 12215 . . . . . . . . . . . . 13 β„• ∈ V
9695mptex 7222 . . . . . . . . . . . 12 (𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›)) ∈ V
9796a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ 𝐼) β†’ (𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›)) ∈ V)
986, 23, 94, 97caucvg 15622 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ 𝐼) β†’ (𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›)) ∈ dom ⇝ )
99 climdm 15495 . . . . . . . . . 10 ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›)) ∈ dom ⇝ ↔ (𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›)) ⇝ ( ⇝ β€˜(𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))))
10098, 99sylib 217 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ 𝐼) β†’ (𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›)) ⇝ ( ⇝ β€˜(𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))))
101 fveq2 6889 . . . . . . . . . . . . 13 (π‘š = 𝑛 β†’ ((πΉβ€˜π‘‘)β€˜π‘š) = ((πΉβ€˜π‘‘)β€˜π‘›))
102101mpteq2dv 5250 . . . . . . . . . . . 12 (π‘š = 𝑛 β†’ (𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘š)) = (𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›)))
103102fveq2d 6893 . . . . . . . . . . 11 (π‘š = 𝑛 β†’ ( ⇝ β€˜(𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘š))) = ( ⇝ β€˜(𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))))
104 fvex 6902 . . . . . . . . . . 11 ( ⇝ β€˜(𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))) ∈ V
105103, 3, 104fvmpt 6996 . . . . . . . . . 10 (𝑛 ∈ 𝐼 β†’ (π‘ƒβ€˜π‘›) = ( ⇝ β€˜(𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))))
106105adantl 483 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ 𝐼) β†’ (π‘ƒβ€˜π‘›) = ( ⇝ β€˜(𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))))
107100, 106breqtrrd 5176 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ 𝐼) β†’ (𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›)) ⇝ (π‘ƒβ€˜π‘›))
1086, 7, 107, 22climrecl 15524 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ 𝐼) β†’ (π‘ƒβ€˜π‘›) ∈ ℝ)
109108ralrimiva 3147 . . . . . 6 (πœ‘ β†’ βˆ€π‘› ∈ 𝐼 (π‘ƒβ€˜π‘›) ∈ ℝ)
110 ffnfv 7115 . . . . . 6 (𝑃:πΌβŸΆβ„ ↔ (𝑃 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘ƒβ€˜π‘›) ∈ ℝ))
1115, 109, 110sylanbrc 584 . . . . 5 (πœ‘ β†’ 𝑃:πΌβŸΆβ„)
112 reex 11198 . . . . . 6 ℝ ∈ V
113 elmapg 8830 . . . . . 6 ((ℝ ∈ V ∧ 𝐼 ∈ Fin) β†’ (𝑃 ∈ (ℝ ↑m 𝐼) ↔ 𝑃:πΌβŸΆβ„))
114112, 25, 113sylancr 588 . . . . 5 (πœ‘ β†’ (𝑃 ∈ (ℝ ↑m 𝐼) ↔ 𝑃:πΌβŸΆβ„))
115111, 114mpbird 257 . . . 4 (πœ‘ β†’ 𝑃 ∈ (ℝ ↑m 𝐼))
116115, 16eleqtrrdi 2845 . . 3 (πœ‘ β†’ 𝑃 ∈ 𝑋)
117 1nn 12220 . . . . . . 7 1 ∈ β„•
11825ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 = βˆ…)) ∧ π‘˜ ∈ β„•) β†’ 𝐼 ∈ Fin)
11915adantlr 714 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 = βˆ…)) ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜) ∈ 𝑋)
120116ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 = βˆ…)) ∧ π‘˜ ∈ β„•) β†’ 𝑃 ∈ 𝑋)
12116rrnmval 36685 . . . . . . . . . . . 12 ((𝐼 ∈ Fin ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) β†’ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) = (βˆšβ€˜Ξ£π‘¦ ∈ 𝐼 ((((πΉβ€˜π‘˜)β€˜π‘¦) βˆ’ (π‘ƒβ€˜π‘¦))↑2)))
122118, 119, 120, 121syl3anc 1372 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 = βˆ…)) ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) = (βˆšβ€˜Ξ£π‘¦ ∈ 𝐼 ((((πΉβ€˜π‘˜)β€˜π‘¦) βˆ’ (π‘ƒβ€˜π‘¦))↑2)))
123 simplrr 777 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 = βˆ…)) ∧ π‘˜ ∈ β„•) β†’ 𝐼 = βˆ…)
124123sumeq1d 15644 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 = βˆ…)) ∧ π‘˜ ∈ β„•) β†’ Σ𝑦 ∈ 𝐼 ((((πΉβ€˜π‘˜)β€˜π‘¦) βˆ’ (π‘ƒβ€˜π‘¦))↑2) = Σ𝑦 ∈ βˆ… ((((πΉβ€˜π‘˜)β€˜π‘¦) βˆ’ (π‘ƒβ€˜π‘¦))↑2))
125 sum0 15664 . . . . . . . . . . . . 13 Σ𝑦 ∈ βˆ… ((((πΉβ€˜π‘˜)β€˜π‘¦) βˆ’ (π‘ƒβ€˜π‘¦))↑2) = 0
126124, 125eqtrdi 2789 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 = βˆ…)) ∧ π‘˜ ∈ β„•) β†’ Σ𝑦 ∈ 𝐼 ((((πΉβ€˜π‘˜)β€˜π‘¦) βˆ’ (π‘ƒβ€˜π‘¦))↑2) = 0)
127126fveq2d 6893 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 = βˆ…)) ∧ π‘˜ ∈ β„•) β†’ (βˆšβ€˜Ξ£π‘¦ ∈ 𝐼 ((((πΉβ€˜π‘˜)β€˜π‘¦) βˆ’ (π‘ƒβ€˜π‘¦))↑2)) = (βˆšβ€˜0))
128122, 127eqtrd 2773 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 = βˆ…)) ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) = (βˆšβ€˜0))
129 sqrt0 15185 . . . . . . . . . 10 (βˆšβ€˜0) = 0
130128, 129eqtrdi 2789 . . . . . . . . 9 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 = βˆ…)) ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) = 0)
131 simplrl 776 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 = βˆ…)) ∧ π‘˜ ∈ β„•) β†’ π‘₯ ∈ ℝ+)
132131rpgt0d 13016 . . . . . . . . 9 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 = βˆ…)) ∧ π‘˜ ∈ β„•) β†’ 0 < π‘₯)
133130, 132eqbrtrd 5170 . . . . . . . 8 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 = βˆ…)) ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯)
134133ralrimiva 3147 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 = βˆ…)) β†’ βˆ€π‘˜ ∈ β„• ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯)
135 fveq2 6889 . . . . . . . . . 10 (𝑗 = 1 β†’ (β„€β‰₯β€˜π‘—) = (β„€β‰₯β€˜1))
136135, 6eqtr4di 2791 . . . . . . . . 9 (𝑗 = 1 β†’ (β„€β‰₯β€˜π‘—) = β„•)
137136raleqdv 3326 . . . . . . . 8 (𝑗 = 1 β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯ ↔ βˆ€π‘˜ ∈ β„• ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯))
138137rspcev 3613 . . . . . . 7 ((1 ∈ β„• ∧ βˆ€π‘˜ ∈ β„• ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯)
139117, 134, 138sylancr 588 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 = βˆ…)) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯)
140139expr 458 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (𝐼 = βˆ… β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯))
141 1zzd 12590 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) β†’ 1 ∈ β„€)
142 simprl 770 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) β†’ π‘₯ ∈ ℝ+)
143 simprr 772 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) β†’ 𝐼 β‰  βˆ…)
14425adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) β†’ 𝐼 ∈ Fin)
145 hashnncl 14323 . . . . . . . . . . . . . . . . 17 (𝐼 ∈ Fin β†’ ((β™―β€˜πΌ) ∈ β„• ↔ 𝐼 β‰  βˆ…))
146144, 145syl 17 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) β†’ ((β™―β€˜πΌ) ∈ β„• ↔ 𝐼 β‰  βˆ…))
147143, 146mpbird 257 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) β†’ (β™―β€˜πΌ) ∈ β„•)
148147nnrpd 13011 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) β†’ (β™―β€˜πΌ) ∈ ℝ+)
149148rpsqrtcld 15355 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) β†’ (βˆšβ€˜(β™―β€˜πΌ)) ∈ ℝ+)
150142, 149rpdivcld 13030 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) β†’ (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ∈ ℝ+)
151150adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) β†’ (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ∈ ℝ+)
15212adantl 483 . . . . . . . . . . 11 ((((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) ∧ π‘˜ ∈ β„•) β†’ ((𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›))β€˜π‘˜) = ((πΉβ€˜π‘˜)β€˜π‘›))
153107adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) β†’ (𝑑 ∈ β„• ↦ ((πΉβ€˜π‘‘)β€˜π‘›)) ⇝ (π‘ƒβ€˜π‘›))
1546, 141, 151, 152, 153climi2 15452 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(((πΉβ€˜π‘˜)β€˜π‘›) βˆ’ (π‘ƒβ€˜π‘›))) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))))
155 1z 12589 . . . . . . . . . . . 12 1 ∈ β„€
1566rexuz3 15292 . . . . . . . . . . . 12 (1 ∈ β„€ β†’ (βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ↔ βˆƒπ‘— ∈ β„€ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ)))))
157155, 156ax-mp 5 . . . . . . . . . . 11 (βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ↔ βˆƒπ‘— ∈ β„€ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))))
15821adantllr 718 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜π‘˜)β€˜π‘›) ∈ ℝ)
159108adantlr 714 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) β†’ (π‘ƒβ€˜π‘›) ∈ ℝ)
160159adantr 482 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) ∧ π‘˜ ∈ β„•) β†’ (π‘ƒβ€˜π‘›) ∈ ℝ)
16144remetdval 24297 . . . . . . . . . . . . . . . . 17 ((((πΉβ€˜π‘˜)β€˜π‘›) ∈ ℝ ∧ (π‘ƒβ€˜π‘›) ∈ ℝ) β†’ (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) = (absβ€˜(((πΉβ€˜π‘˜)β€˜π‘›) βˆ’ (π‘ƒβ€˜π‘›))))
162158, 160, 161syl2anc 585 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) ∧ π‘˜ ∈ β„•) β†’ (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) = (absβ€˜(((πΉβ€˜π‘˜)β€˜π‘›) βˆ’ (π‘ƒβ€˜π‘›))))
163162breq1d 5158 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) ∧ π‘˜ ∈ β„•) β†’ ((((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ↔ (absβ€˜(((πΉβ€˜π‘˜)β€˜π‘›) βˆ’ (π‘ƒβ€˜π‘›))) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ)))))
16439, 163sylan2 594 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) ∧ (𝑗 ∈ β„• ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—))) β†’ ((((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ↔ (absβ€˜(((πΉβ€˜π‘˜)β€˜π‘›) βˆ’ (π‘ƒβ€˜π‘›))) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ)))))
165164anassrs 469 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ ((((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ↔ (absβ€˜(((πΉβ€˜π‘˜)β€˜π‘›) βˆ’ (π‘ƒβ€˜π‘›))) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ)))))
166165ralbidva 3176 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ β„•) β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ↔ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(((πΉβ€˜π‘˜)β€˜π‘›) βˆ’ (π‘ƒβ€˜π‘›))) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ)))))
167166rexbidva 3177 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) β†’ (βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ↔ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(((πΉβ€˜π‘˜)β€˜π‘›) βˆ’ (π‘ƒβ€˜π‘›))) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ)))))
168157, 167bitr3id 285 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) β†’ (βˆƒπ‘— ∈ β„€ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ↔ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(((πΉβ€˜π‘˜)β€˜π‘›) βˆ’ (π‘ƒβ€˜π‘›))) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ)))))
169154, 168mpbird 257 . . . . . . . . 9 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑛 ∈ 𝐼) β†’ βˆƒπ‘— ∈ β„€ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))))
170169ralrimiva 3147 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) β†’ βˆ€π‘› ∈ 𝐼 βˆƒπ‘— ∈ β„€ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))))
1716rexuz3 15292 . . . . . . . . . 10 (1 ∈ β„€ β†’ (βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ↔ βˆƒπ‘— ∈ β„€ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ)))))
172155, 171ax-mp 5 . . . . . . . . 9 (βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ↔ βˆƒπ‘— ∈ β„€ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))))
173 rexfiuz 15291 . . . . . . . . . 10 (𝐼 ∈ Fin β†’ (βˆƒπ‘— ∈ β„€ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ↔ βˆ€π‘› ∈ 𝐼 βˆƒπ‘— ∈ β„€ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ)))))
174144, 173syl 17 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) β†’ (βˆƒπ‘— ∈ β„€ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ↔ βˆ€π‘› ∈ 𝐼 βˆƒπ‘— ∈ β„€ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ)))))
175172, 174bitrid 283 . . . . . . . 8 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) β†’ (βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ↔ βˆ€π‘› ∈ 𝐼 βˆƒπ‘— ∈ β„€ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ)))))
176170, 175mpbird 257 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))))
17725ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ π‘˜ ∈ β„•) β†’ 𝐼 ∈ Fin)
178 simplrr 777 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ π‘˜ ∈ β„•) β†’ 𝐼 β‰  βˆ…)
179 eldifsn 4790 . . . . . . . . . . . . . 14 (𝐼 ∈ (Fin βˆ– {βˆ…}) ↔ (𝐼 ∈ Fin ∧ 𝐼 β‰  βˆ…))
180177, 178, 179sylanbrc 584 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ π‘˜ ∈ β„•) β†’ 𝐼 ∈ (Fin βˆ– {βˆ…}))
18114adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) β†’ 𝐹:β„•βŸΆπ‘‹)
182181ffvelcdmda 7084 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘˜) ∈ 𝑋)
183116ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ π‘˜ ∈ β„•) β†’ 𝑃 ∈ 𝑋)
184150adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ π‘˜ ∈ β„•) β†’ (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ∈ ℝ+)
18516, 44rrndstprj2 36688 . . . . . . . . . . . . . 14 (((𝐼 ∈ (Fin βˆ– {βˆ…}) ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) ∧ ((π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ∈ ℝ+ ∧ βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))))) β†’ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < ((π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) Β· (βˆšβ€˜(β™―β€˜πΌ))))
186185expr 458 . . . . . . . . . . . . 13 (((𝐼 ∈ (Fin βˆ– {βˆ…}) ∧ (πΉβ€˜π‘˜) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) ∧ (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) ∈ ℝ+) β†’ (βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) β†’ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < ((π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) Β· (βˆšβ€˜(β™―β€˜πΌ)))))
187180, 182, 183, 184, 186syl31anc 1374 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ π‘˜ ∈ β„•) β†’ (βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) β†’ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < ((π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) Β· (βˆšβ€˜(β™―β€˜πΌ)))))
188 simplrl 776 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ π‘˜ ∈ β„•) β†’ π‘₯ ∈ ℝ+)
189188rpcnd 13015 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ π‘˜ ∈ β„•) β†’ π‘₯ ∈ β„‚)
190149adantr 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ π‘˜ ∈ β„•) β†’ (βˆšβ€˜(β™―β€˜πΌ)) ∈ ℝ+)
191190rpcnd 13015 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ π‘˜ ∈ β„•) β†’ (βˆšβ€˜(β™―β€˜πΌ)) ∈ β„‚)
192190rpne0d 13018 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ π‘˜ ∈ β„•) β†’ (βˆšβ€˜(β™―β€˜πΌ)) β‰  0)
193189, 191, 192divcan1d 11988 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ π‘˜ ∈ β„•) β†’ ((π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) Β· (βˆšβ€˜(β™―β€˜πΌ))) = π‘₯)
194193breq2d 5160 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ π‘˜ ∈ β„•) β†’ (((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < ((π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) Β· (βˆšβ€˜(β™―β€˜πΌ))) ↔ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯))
195187, 194sylibd 238 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ π‘˜ ∈ β„•) β†’ (βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) β†’ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯))
19639, 195sylan2 594 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ (𝑗 ∈ β„• ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—))) β†’ (βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) β†’ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯))
197196anassrs 469 . . . . . . . . 9 ((((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑗 ∈ β„•) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ (βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) β†’ ((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯))
198197ralimdva 3168 . . . . . . . 8 (((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) ∧ 𝑗 ∈ β„•) β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) β†’ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯))
199198reximdva 3169 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) β†’ (βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘› ∈ 𝐼 (((πΉβ€˜π‘˜)β€˜π‘›)𝑀(π‘ƒβ€˜π‘›)) < (π‘₯ / (βˆšβ€˜(β™―β€˜πΌ))) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯))
200176, 199mpd 15 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ ℝ+ ∧ 𝐼 β‰  βˆ…)) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯)
201200expr 458 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ (𝐼 β‰  βˆ… β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯))
202140, 201pm2.61dne 3029 . . . 4 ((πœ‘ ∧ π‘₯ ∈ ℝ+) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯)
203202ralrimiva 3147 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯)
204 rrncms.3 . . . 4 𝐽 = (MetOpenβ€˜(ℝnβ€˜πΌ))
205204, 29, 6, 30, 31, 14lmmbrf 24771 . . 3 (πœ‘ β†’ (𝐹(β‡π‘‘β€˜π½)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ βˆ€π‘₯ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)((πΉβ€˜π‘˜)(ℝnβ€˜πΌ)𝑃) < π‘₯)))
206116, 203, 205mpbir2and 712 . 2 (πœ‘ β†’ 𝐹(β‡π‘‘β€˜π½)𝑃)
207 releldm 5942 . 2 ((Rel (β‡π‘‘β€˜π½) ∧ 𝐹(β‡π‘‘β€˜π½)𝑃) β†’ 𝐹 ∈ dom (β‡π‘‘β€˜π½))
2081, 206, 207sylancr 588 1 (πœ‘ β†’ 𝐹 ∈ dom (β‡π‘‘β€˜π½))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   βˆ– cdif 3945  βˆ…c0 4322  {csn 4628   class class class wbr 5148   ↦ cmpt 5231   Γ— cxp 5674  dom cdm 5676   β†Ύ cres 5678   ∘ ccom 5680  Rel wrel 5681   Fn wfn 6536  βŸΆwf 6537  β€˜cfv 6541  (class class class)co 7406   ↑m cmap 8817  Fincfn 8936  β„cr 11106  0cc0 11107  1c1 11108   Β· cmul 11112   < clt 11245   ≀ cle 11246   βˆ’ cmin 11441   / cdiv 11868  β„•cn 12209  2c2 12264  β„€cz 12555  β„€β‰₯cuz 12819  β„+crp 12971  β†‘cexp 14024  β™―chash 14287  βˆšcsqrt 15177  abscabs 15178   ⇝ cli 15425  Ξ£csu 15629  βˆžMetcxmet 20922  Metcmet 20923  MetOpencmopn 20927  β‡π‘‘clm 22722  Cauccau 24762  β„ncrrn 36682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-map 8819  df-pm 8820  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-sup 9434  df-inf 9435  df-oi 9502  df-card 9931  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-n0 12470  df-z 12556  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ico 13327  df-fz 13482  df-fzo 13625  df-fl 13754  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-limsup 15412  df-clim 15429  df-rlim 15430  df-sum 15630  df-topgen 17386  df-psmet 20929  df-xmet 20930  df-met 20931  df-bl 20932  df-mopn 20933  df-top 22388  df-topon 22405  df-bases 22441  df-lm 22725  df-cau 24765  df-rrn 36683
This theorem is referenced by:  rrncms  36690
  Copyright terms: Public domain W3C validator