Theorem rrncmslem 26543

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

Hypotheses

Ref	Expression
rrnval.1	|- X = ( RR ^m I )
rrndstprj1.1	|- M = ( ( abs o. - ) |` ( RR X. RR ) )
rrncms.3	|- J = ( MetOpen ` ( Rn ` I ) )
rrncms.4	|- ( ph -> I e. Fin )
rrncms.5	|- ( ph -> F e. ( Cau ` ( Rn ` I ) ) )
rrncms.6	|- ( ph -> F : NN --> X )
rrncms.7	|- P = ( m e. I |-> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` m ) ) ) )

Assertion

Ref	Expression
rrncmslem	|- ( ph -> F e. dom ( ~~> t ` J ) )

Distinct variable groups:   m, I   t, m, F

Allowed substitution hints:   ph( t, m)   P( t, m)   I( t)   J( t, m)   M( t, m)   X( t, m)

Proof of Theorem rrncmslem

Dummy variables k n x y j are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lmrel 17296	. 2 |- Rel ( ~~> t ` J )
2		fvex 5744	. . . . . . . 8 |- ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` m ) ) ) e. _V
3		rrncms.7	. . . . . . . 8 |- P = ( m e. I |-> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` m ) ) ) )
4	2, 3	fnmpti 5575	. . . . . . 7 |- P Fn I
5	4	a1i 11	. . . . . 6 |- ( ph -> P Fn I )
6		nnuz 10523	. . . . . . . 8 |- NN = ( ZZ>= ` 1 )
7		1z 10313	. . . . . . . . 9 |- 1 e. ZZ
8	7	a1i 11	. . . . . . . 8 |- ( ( ph /\ n e. I ) -> 1 e. ZZ )
9		fveq2 5730	. . . . . . . . . . . . . . . 16 |- ( t = k -> ( F ` t ) = ( F ` k ) )
10	9	fveq1d 5732	. . . . . . . . . . . . . . 15 |- ( t = k -> ( ( F ` t ) ` n ) = ( ( F ` k ) ` n ) )
11		eqid 2438	. . . . . . . . . . . . . . 15 |- ( t e. NN |-> ( ( F ` t ) ` n ) ) = ( t e. NN |-> ( ( F ` t ) ` n ) )
12		fvex 5744	. . . . . . . . . . . . . . 15 |- ( ( F ` k ) ` n ) e. _V
13	10, 11, 12	fvmpt 5808	. . . . . . . . . . . . . 14 |- ( k e. NN -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) = ( ( F ` k ) ` n ) )
14	13	adantl 454	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. I ) /\ k e. NN ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) = ( ( F ` k ) ` n ) )
15		rrncms.6	. . . . . . . . . . . . . . . . . 18 |- ( ph -> F : NN --> X )
16	15	ffvelrnda 5872	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. X )
17		rrnval.1	. . . . . . . . . . . . . . . . 17 |- X = ( RR ^m I )
18	16, 17	syl6eleq 2528	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. ( RR ^m I ) )
19		elmapi 7040	. . . . . . . . . . . . . . . 16 |- ( ( F ` k ) e. ( RR ^m I ) -> ( F ` k ) : I --> RR )
20	18, 19	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( F ` k ) : I --> RR )
21	20	ffvelrnda 5872	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. NN ) /\ n e. I ) -> ( ( F ` k ) ` n ) e. RR )
22	21	an32s 781	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. I ) /\ k e. NN ) -> ( ( F ` k ) ` n ) e. RR )
23	14, 22	eqeltrd 2512	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. I ) /\ k e. NN ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) e. RR )
24	23	recnd 9116	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. I ) /\ k e. NN ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) e. CC )
25		rrncms.5	. . . . . . . . . . . . . 14 |- ( ph -> F e. ( Cau ` ( Rn ` I ) ) )
26		rrncms.4	. . . . . . . . . . . . . . . . 17 |- ( ph -> I e. Fin )
27	17	rrnmet 26540	. . . . . . . . . . . . . . . . 17 |- ( I e. Fin -> ( Rn ` I ) e. ( Met ` X ) )
28	26, 27	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Rn ` I ) e. ( Met ` X ) )
29		metxmet 18366	. . . . . . . . . . . . . . . 16 |- ( ( Rn ` I ) e. ( Met ` X ) -> ( Rn ` I ) e. ( * Met ` X ) )
30	28, 29	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> ( Rn ` I ) e. ( * Met ` X ) )
31	7	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. ZZ )
32		eqidd 2439	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( F ` k ) = ( F ` k ) )
33		eqidd 2439	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN ) -> ( F ` j ) = ( F ` j ) )
34	6, 30, 31, 32, 33, 15	iscauf 19235	. . . . . . . . . . . . . 14 |- ( ph -> ( F e. ( Cau ` ( Rn ` I ) ) <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x ) )
35	25, 34	mpbid 203	. . . . . . . . . . . . 13 |- ( ph -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x )
36	35	adantr 453	. . . . . . . . . . . 12 |- ( ( ph /\ n e. I ) -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x )
37	26	ad3antrrr 712	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> I e. Fin )
38		simpllr 737	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> n e. I )
39	15	ad3antrrr 712	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> F : NN --> X )
40	6	uztrn2 10505	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( j e. NN /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
41	40	adantll 696	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
42	39, 41	ffvelrnd 5873	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. X )
43		simplr 733	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> j e. NN )
44	39, 43	ffvelrnd 5873	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` j ) e. X )
45		rrndstprj1.1	. . . . . . . . . . . . . . . . . . . . 21 |- M = ( ( abs o. - ) |` ( RR X. RR ) )
46	17, 45	rrndstprj1 26541	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( I e. Fin /\ n e. I ) /\ ( ( F ` k ) e. X /\ ( F ` j ) e. X ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` k ) ( Rn ` I ) ( F ` j ) ) )
47	37, 38, 42, 44, 46	syl22anc 1186	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` k ) ( Rn ` I ) ( F ` j ) ) )
48	28	ad3antrrr 712	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( Rn ` I ) e. ( Met ` X ) )
49		metsym 18382	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( Rn ` I ) e. ( Met ` X ) /\ ( F ` k ) e. X /\ ( F ` j ) e. X ) -> ( ( F ` k ) ( Rn ` I ) ( F ` j ) ) = ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) )
50	48, 42, 44, 49	syl3anc 1185	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) ( Rn ` I ) ( F ` j ) ) = ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) )
51	47, 50	breqtrd 4238	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) )
52	51	adantllr 701	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) )
53	45	remet 18823	. . . . . . . . . . . . . . . . . . . . 21 |- M e. ( Met ` RR )
54	53	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> M e. ( Met ` RR ) )
55		simpll 732	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ph /\ n e. I ) )
56	55, 41, 22	syl2anc 644	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) ` n ) e. RR )
57	15	ffvelrnda 5872	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j e. NN ) -> ( F ` j ) e. X )
58	57, 17	syl6eleq 2528	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ j e. NN ) -> ( F ` j ) e. ( RR ^m I ) )
59		elmapi 7040	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F ` j ) e. ( RR ^m I ) -> ( F ` j ) : I --> RR )
60	58, 59	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ j e. NN ) -> ( F ` j ) : I --> RR )
61	60	ffvelrnda 5872	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ j e. NN ) /\ n e. I ) -> ( ( F ` j ) ` n ) e. RR )
62	61	an32s 781	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. I ) /\ j e. NN ) -> ( ( F ` j ) ` n ) e. RR )
63	62	adantr 453	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` j ) ` n ) e. RR )
64		metcl 18364	. . . . . . . . . . . . . . . . . . . 20 |- ( ( M e. ( Met ` RR ) /\ ( ( F ` k ) ` n ) e. RR /\ ( ( F ` j ) ` n ) e. RR ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) e. RR )
65	54, 56, 63, 64	syl3anc 1185	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) e. RR )
66	65	adantllr 701	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) e. RR )
67		metcl 18364	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( Rn ` I ) e. ( Met ` X ) /\ ( F ` j ) e. X /\ ( F ` k ) e. X ) -> ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) e. RR )
68	48, 44, 42, 67	syl3anc 1185	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) e. RR )
69	68	adantllr 701	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) e. RR )
70		rpre 10620	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. RR+ -> x e. RR )
71	70	adantl 454	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. I ) /\ x e. RR+ ) -> x e. RR )
72	71	ad2antrr 708	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> x e. RR )
73		lelttr 9167	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) e. RR /\ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) e. RR /\ x e. RR ) -> ( ( ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) /\ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) )
74	66, 69, 72, 73	syl3anc 1185	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) <_ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) /\ ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) )
75	52, 74	mpand 658	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) )
76	75	ralimdva 2786	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x -> A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) )
77	76	reximdva 2820	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. I ) /\ x e. RR+ ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) )
78	77	ralimdva 2786	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. I ) -> ( A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x ) )
79	45	remetdval 18822	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F ` k ) ` n ) e. RR /\ ( ( F ` j ) ` n ) e. RR ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) = ( abs ` ( ( ( F ` k ) ` n ) - ( ( F ` j ) ` n ) ) ) )
80	56, 63, 79	syl2anc 644	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) = ( abs ` ( ( ( F ` k ) ` n ) - ( ( F ` j ) ` n ) ) ) )
81	41, 13	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) = ( ( F ` k ) ` n ) )
82		fveq2 5730	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( t = j -> ( F ` t ) = ( F ` j ) )
83	82	fveq1d 5732	. . . . . . . . . . . . . . . . . . . . . 22 |- ( t = j -> ( ( F ` t ) ` n ) = ( ( F ` j ) ` n ) )
84		fvex 5744	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( F ` j ) ` n ) e. _V
85	83, 11, 84	fvmpt 5808	. . . . . . . . . . . . . . . . . . . . 21 |- ( j e. NN -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) = ( ( F ` j ) ` n ) )
86	85	ad2antlr 709	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) = ( ( F ` j ) ` n ) )
87	81, 86	oveq12d 6101	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) = ( ( ( F ` k ) ` n ) - ( ( F ` j ) ` n ) ) )
88	87	fveq2d 5734	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) = ( abs ` ( ( ( F ` k ) ` n ) - ( ( F ` j ) ` n ) ) ) )
89	80, 88	eqtr4d 2473	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) = ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) )
90	89	breq1d 4224	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x <-> ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) )
91	90	ralbidva 2723	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. I ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x <-> A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) )
92	91	rexbidva 2724	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. I ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x <-> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) )
93	92	ralbidv 2727	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. I ) -> ( A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) < x <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) )
94	78, 93	sylibd 207	. . . . . . . . . . . 12 |- ( ( ph /\ n e. I ) -> ( A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) < x -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x ) )
95	36, 94	mpd 15	. . . . . . . . . . 11 |- ( ( ph /\ n e. I ) -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) - ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) ) ) < x )
96		nnex 10008	. . . . . . . . . . . . 13 |- NN e. _V
97	96	mptex 5968	. . . . . . . . . . . 12 |- ( t e. NN |-> ( ( F ` t ) ` n ) ) e. _V
98	97	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) e. _V )
99	6, 24, 95, 98	caucvg 12474	. . . . . . . . . 10 |- ( ( ph /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) e. dom ~~> )
100		climdm 12350	. . . . . . . . . 10 |- ( ( t e. NN |-> ( ( F ` t ) ` n ) ) e. dom ~~> <-> ( t e. NN |-> ( ( F ` t ) ` n ) ) ~~> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) )
101	99, 100	sylib 190	. . . . . . . . 9 |- ( ( ph /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) ~~> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) )
102		fveq2 5730	. . . . . . . . . . . . 13 |- ( m = n -> ( ( F ` t ) ` m ) = ( ( F ` t ) ` n ) )
103	102	mpteq2dv 4298	. . . . . . . . . . . 12 |- ( m = n -> ( t e. NN |-> ( ( F ` t ) ` m ) ) = ( t e. NN |-> ( ( F ` t ) ` n ) ) )
104	103	fveq2d 5734	. . . . . . . . . . 11 |- ( m = n -> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` m ) ) ) = ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) )
105		fvex 5744	. . . . . . . . . . 11 |- ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) e. _V
106	104, 3, 105	fvmpt 5808	. . . . . . . . . 10 |- ( n e. I -> ( P ` n ) = ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) )
107	106	adantl 454	. . . . . . . . 9 |- ( ( ph /\ n e. I ) -> ( P ` n ) = ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) )
108	101, 107	breqtrrd 4240	. . . . . . . 8 |- ( ( ph /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) ~~> ( P ` n ) )
109	6, 8, 108, 23	climrecl 12379	. . . . . . 7 |- ( ( ph /\ n e. I ) -> ( P ` n ) e. RR )
110	109	ralrimiva 2791	. . . . . 6 |- ( ph -> A. n e. I ( P ` n ) e. RR )
111		ffnfv 5896	. . . . . 6 |- ( P : I --> RR <-> ( P Fn I /\ A. n e. I ( P ` n ) e. RR ) )
112	5, 110, 111	sylanbrc 647	. . . . 5 |- ( ph -> P : I --> RR )
113		reex 9083	. . . . . 6 |- RR e. _V
114		elmapg 7033	. . . . . 6 |- ( ( RR e. _V /\ I e. Fin ) -> ( P e. ( RR ^m I ) <-> P : I --> RR ) )
115	113, 26, 114	sylancr 646	. . . . 5 |- ( ph -> ( P e. ( RR ^m I ) <-> P : I --> RR ) )
116	112, 115	mpbird 225	. . . 4 |- ( ph -> P e. ( RR ^m I ) )
117	116, 17	syl6eleqr 2529	. . 3 |- ( ph -> P e. X )
118		1nn 10013	. . . . . . 7 |- 1 e. NN
119	26	ad2antrr 708	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> I e. Fin )
120	16	adantlr 697	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( F ` k ) e. X )
121	117	ad2antrr 708	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> P e. X )
122	17	rrnmval 26539	. . . . . . . . . . . 12 |- ( ( I e. Fin /\ ( F ` k ) e. X /\ P e. X ) -> ( ( F ` k ) ( Rn ` I ) P ) = ( sqr ` sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) ) )
123	119, 120, 121, 122	syl3anc 1185	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( ( F ` k ) ( Rn ` I ) P ) = ( sqr ` sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) ) )
124		simplrr 739	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> I = (/) )
125	124	sumeq1d 12497	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) = sum_ y e. (/) ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) )
126		sum0 12517	. . . . . . . . . . . . 13 |- sum_ y e. (/) ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) = 0
127	125, 126	syl6eq 2486	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) = 0 )
128	127	fveq2d 5734	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( sqr ` sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) ) = ( sqr ` 0 ) )
129	123, 128	eqtrd 2470	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( ( F ` k ) ( Rn ` I ) P ) = ( sqr ` 0 ) )
130		sqr0 12049	. . . . . . . . . 10 |- ( sqr ` 0 ) = 0
131	129, 130	syl6eq 2486	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( ( F ` k ) ( Rn ` I ) P ) = 0 )
132		simplrl 738	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> x e. RR+ )
133	132	rpgt0d 10653	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> 0 < x )
134	131, 133	eqbrtrd 4234	. . . . . . . 8 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( ( F ` k ) ( Rn ` I ) P ) < x )
135	134	ralrimiva 2791	. . . . . . 7 |- ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) -> A. k e. NN ( ( F ` k ) ( Rn ` I ) P ) < x )
136		fveq2 5730	. . . . . . . . . 10 |- ( j = 1 -> ( ZZ>= ` j ) = ( ZZ>= ` 1 ) )
137	136, 6	syl6eqr 2488	. . . . . . . . 9 |- ( j = 1 -> ( ZZ>= ` j ) = NN )
138	137	raleqdv 2912	. . . . . . . 8 |- ( j = 1 -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x <-> A. k e. NN ( ( F ` k ) ( Rn ` I ) P ) < x ) )
139	138	rspcev 3054	. . . . . . 7 |- ( ( 1 e. NN /\ A. k e. NN ( ( F ` k ) ( Rn ` I ) P ) < x ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x )
140	118, 135, 139	sylancr 646	. . . . . 6 |- ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x )
141	140	expr 600	. . . . 5 |- ( ( ph /\ x e. RR+ ) -> ( I = (/) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) )
142	7	a1i 11	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> 1 e. ZZ )
143		simprl 734	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> x e. RR+ )
144		simprr 735	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> I =/= (/) )
145	26	adantr 453	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> I e. Fin )
146		hashnncl 11647	. . . . . . . . . . . . . . . . 17 |- ( I e. Fin -> ( ( # ` I ) e. NN <-> I =/= (/) ) )
147	145, 146	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( ( # ` I ) e. NN <-> I =/= (/) ) )
148	144, 147	mpbird 225	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( # ` I ) e. NN )
149	148	nnrpd 10649	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( # ` I ) e. RR+ )
150	149	rpsqrcld 12216	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( sqr ` ( # ` I ) ) e. RR+ )
151	143, 150	rpdivcld 10667	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( x / ( sqr ` ( # ` I ) ) ) e. RR+ )
152	151	adantr 453	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( x / ( sqr ` ( # ` I ) ) ) e. RR+ )
153	13	adantl 454	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) = ( ( F ` k ) ` n ) )
154	108	adantlr 697	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) ~~> ( P ` n ) )
155	6, 142, 152, 153, 154	climi2 12307	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqr ` ( # ` I ) ) ) )
156	6	rexuz3 12154	. . . . . . . . . . . 12 |- ( 1 e. ZZ -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) ) )
157	7, 156	ax-mp 8	. . . . . . . . . . 11 |- ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) )
158	22	adantllr 701	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( ( F ` k ) ` n ) e. RR )
159	109	adantlr 697	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( P ` n ) e. RR )
160	159	adantr 453	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( P ` n ) e. RR )
161	45	remetdval 18822	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( F ` k ) ` n ) e. RR /\ ( P ` n ) e. RR ) -> ( ( ( F ` k ) ` n ) M ( P ` n ) ) = ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) )
162	158, 160, 161	syl2anc 644	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( ( ( F ` k ) ` n ) M ( P ` n ) ) = ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) )
163	162	breq1d 4224	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) <-> ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqr ` ( # ` I ) ) ) ) )
164	40, 163	sylan2 462	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ ( j e. NN /\ k e. ( ZZ>= ` j ) ) ) -> ( ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) <-> ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqr ` ( # ` I ) ) ) ) )
165	164	anassrs 631	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) <-> ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqr ` ( # ` I ) ) ) ) )
166	165	ralbidva 2723	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) <-> A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqr ` ( # ` I ) ) ) ) )
167	166	rexbidva 2724	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) <-> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqr ` ( # ` I ) ) ) ) )
168	157, 167	syl5bbr 252	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) <-> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` n ) - ( P ` n ) ) ) < ( x / ( sqr ` ( # ` I ) ) ) ) )
169	155, 168	mpbird 225	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) )
170	169	ralrimiva 2791	. . . . . . . 8 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> A. n e. I E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) )
171	6	rexuz3 12154	. . . . . . . . . 10 |- ( 1 e. ZZ -> ( E. j e. NN A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) ) )
172	7, 171	ax-mp 8	. . . . . . . . 9 |- ( E. j e. NN A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) )
173		rexfiuz 12153	. . . . . . . . . 10 |- ( I e. Fin -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) <-> A. n e. I E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) ) )
174	145, 173	syl 16	. . . . . . . . 9 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) <-> A. n e. I E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) ) )
175	172, 174	syl5bb 250	. . . . . . . 8 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) <-> A. n e. I E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) ) )
176	170, 175	mpbird 225	. . . . . . 7 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) )
177	26	ad2antrr 708	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> I e. Fin )
178		simplrr 739	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> I =/= (/) )
179		eldifsn 3929	. . . . . . . . . . . . . 14 |- ( I e. ( Fin \ { (/) } ) <-> ( I e. Fin /\ I =/= (/) ) )
180	177, 178, 179	sylanbrc 647	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> I e. ( Fin \ { (/) } ) )
181	15	adantr 453	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> F : NN --> X )
182	181	ffvelrnda 5872	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( F ` k ) e. X )
183	117	ad2antrr 708	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> P e. X )
184	151	adantr 453	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( x / ( sqr ` ( # ` I ) ) ) e. RR+ )
185	17, 45	rrndstprj2 26542	. . . . . . . . . . . . . 14 |- ( ( ( I e. ( Fin \ { (/) } ) /\ ( F ` k ) e. X /\ P e. X ) /\ ( ( x / ( sqr ` ( # ` I ) ) ) e. RR+ /\ A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < ( ( x / ( sqr ` ( # ` I ) ) ) x. ( sqr ` ( # ` I ) ) ) )
186	185	expr 600	. . . . . . . . . . . . 13 |- ( ( ( I e. ( Fin \ { (/) } ) /\ ( F ` k ) e. X /\ P e. X ) /\ ( x / ( sqr ` ( # ` I ) ) ) e. RR+ ) -> ( A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < ( ( x / ( sqr ` ( # ` I ) ) ) x. ( sqr ` ( # ` I ) ) ) ) )
187	180, 182, 183, 184, 186	syl31anc 1188	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < ( ( x / ( sqr ` ( # ` I ) ) ) x. ( sqr ` ( # ` I ) ) ) ) )
188		simplrl 738	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> x e. RR+ )
189	188	rpcnd 10652	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> x e. CC )
190	150	adantr 453	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( sqr ` ( # ` I ) ) e. RR+ )
191	190	rpcnd 10652	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( sqr ` ( # ` I ) ) e. CC )
192	190	rpne0d 10655	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( sqr ` ( # ` I ) ) =/= 0 )
193	189, 191, 192	divcan1d 9793	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( ( x / ( sqr ` ( # ` I ) ) ) x. ( sqr ` ( # ` I ) ) ) = x )
194	193	breq2d 4226	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( ( ( F ` k ) ( Rn ` I ) P ) < ( ( x / ( sqr ` ( # ` I ) ) ) x. ( sqr ` ( # ` I ) ) ) <-> ( ( F ` k ) ( Rn ` I ) P ) < x ) )
195	187, 194	sylibd 207	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < x ) )
196	40, 195	sylan2 462	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ ( j e. NN /\ k e. ( ZZ>= ` j ) ) ) -> ( A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < x ) )
197	196	anassrs 631	. . . . . . . . 9 |- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) -> ( ( F ` k ) ( Rn ` I ) P ) < x ) )
198	197	ralimdva 2786	. . . . . . . 8 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) -> A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) )
199	198	reximdva 2820	. . . . . . 7 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) A. n e. I ( ( ( F ` k ) ` n ) M ( P ` n ) ) < ( x / ( sqr ` ( # ` I ) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) )
200	176, 199	mpd 15	. . . . . 6 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x )
201	200	expr 600	. . . . 5 |- ( ( ph /\ x e. RR+ ) -> ( I =/= (/) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) )
202	141, 201	pm2.61dne 2683	. . . 4 |- ( ( ph /\ x e. RR+ ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x )
203	202	ralrimiva 2791	. . 3 |- ( ph -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x )
204		rrncms.3	. . . 4 |- J = ( MetOpen ` ( Rn ` I ) )
205	204, 30, 6, 31, 32, 15	lmmbrf 19217	. . 3 |- ( ph -> ( F ( ~~> t ` J ) P <-> ( P e. X /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x ) ) )
206	117, 203, 205	mpbir2and 890	. 2 |- ( ph -> F ( ~~> t ` J ) P )
207		releldm 5104	. 2 |- ( ( Rel ( ~~> t ` J ) /\ F ( ~~> t ` J ) P ) -> F e. dom ( ~~> t ` J ) )
208	1, 206, 207	sylancr 646	1 |- ( ph -> F e. dom ( ~~> t ` J ) )

Syntax hints:   -> wi 4   <-> wb 178   /\ wa 360   /\ w3a 937   = wceq 1653   e. wcel 1726   =/= wne 2601   A.wral 2707   E.wrex 2708   _Vcvv 2958   \ cdif 3319   (/)c0 3630   {csn 3816   class class class wbr 4214   e. cmpt 4268   X. cxp 4878   dom cdm 4880   |` cres 4882   o. ccom 4884   Rel wrel 4885   Fn wfn 5451   -->wf 5452   ` cfv 5456  (class class class)co 6083   ^m cmap 7020   Fincfn 7111   RRcr 8991   0cc0 8992   1c1 8993   x. cmul 8997   < clt 9122   <_ cle 9123   - cmin 9293   / cdiv 9679   NNcn 10002   2c2 10051   ZZcz 10284   ZZ>=cuz 10490   RR+crp 10614   ^cexp 11384   #chash 11620   sqrcsqr 12040   abscabs 12041   ~~> cli 12280   sum_csu 12481   * Metcxmt 16688   Metcme 16689   MetOpencmopn 16693   ~~> tclm 17292   Caucca 19208   Rncrrn 26536

This theorem is referenced by:  rrncms  26544

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4322  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-inf2 7598  ax-cnex 9048  ax-resscn 9049  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-addrcl 9053  ax-mulcl 9054  ax-mulrcl 9055  ax-mulcom 9056  ax-addass 9057  ax-mulass 9058  ax-distr 9059  ax-i2m1 9060  ax-1ne0 9061  ax-1rid 9062  ax-rnegex 9063  ax-rrecex 9064  ax-cnre 9065  ax-pre-lttri 9066  ax-pre-lttrn 9067  ax-pre-ltadd 9068  ax-pre-mulgt0 9069  ax-pre-sup 9070  ax-addf 9071  ax-mulf 9072

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-br 4215  df-opab 4269  df-mpt 4270  df-tr 4305  df-eprel 4496  df-id 4500  df-po 4505  df-so 4506  df-fr 4543  df-se 4544  df-we 4545  df-ord 4586  df-on 4587  df-lim 4588  df-suc 4589  df-om 4848  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-isom 5465  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-1st 6351  df-2nd 6352  df-riota 6551  df-recs 6635  df-rdg 6670  df-1o 6726  df-oadd 6730  df-er 6907  df-map 7022  df-pm 7023  df-en 7112  df-dom 7113  df-sdom 7114  df-fin 7115  df-sup 7448  df-oi 7481  df-card 7828  df-pnf 9124  df-mnf 9125  df-xr 9126  df-ltxr 9127  df-le 9128  df-sub 9295  df-neg 9296  df-div 9680  df-nn 10003  df-2 10060  df-3 10061  df-4 10062  df-n0 10224  df-z 10285  df-uz 10491  df-q 10577  df-rp 10615  df-xneg 10712  df-xadd 10713  df-xmul 10714  df-ico 10924  df-fz 11046  df-fzo 11138  df-fl 11204  df-seq 11326  df-exp 11385  df-hash 11621  df-cj 11906  df-re 11907  df-im 11908  df-sqr 12042  df-abs 12043  df-limsup 12267  df-clim 12284  df-rlim 12285  df-sum 12482  df-topgen 13669  df-psmet 16696  df-xmet 16697  df-met 16698  df-bl 16699  df-mopn 16700  df-top 16965  df-bases 16967  df-topon 16968  df-lm 17295  df-cau 19211  df-rrn 26537