Theorem rrncmslem 26431

Description: Lemma for rrncms 26432. (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 17248	. 2 |- Rel ( ~~> t ` J )
2		fvex 5701	. . . . . . . 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 5532	. . . . . . 7 |- P Fn I
5	4	a1i 11	. . . . . 6 |- ( ph -> P Fn I )
6		nnuz 10477	. . . . . . . 8 |- NN = ( ZZ>= ` 1 )
7		1z 10267	. . . . . . . . 9 |- 1 e. ZZ
8	7	a1i 11	. . . . . . . 8 |- ( ( ph /\ n e. I ) -> 1 e. ZZ )
9		fveq2 5687	. . . . . . . . . . . . . . . 16 |- ( t = k -> ( F ` t ) = ( F ` k ) )
10	9	fveq1d 5689	. . . . . . . . . . . . . . 15 |- ( t = k -> ( ( F ` t ) ` n ) = ( ( F ` k ) ` n ) )
11		eqid 2404	. . . . . . . . . . . . . . 15 |- ( t e. NN |-> ( ( F ` t ) ` n ) ) = ( t e. NN |-> ( ( F ` t ) ` n ) )
12		fvex 5701	. . . . . . . . . . . . . . 15 |- ( ( F ` k ) ` n ) e. _V
13	10, 11, 12	fvmpt 5765	. . . . . . . . . . . . . 14 |- ( k e. NN -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) = ( ( F ` k ) ` n ) )
14	13	adantl 453	. . . . . . . . . . . . 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 5829	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. X )
17		rrnval.1	. . . . . . . . . . . . . . . . 17 |- X = ( RR ^m I )
18	16, 17	syl6eleq 2494	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. NN ) -> ( F ` k ) e. ( RR ^m I ) )
19		elmapi 6997	. . . . . . . . . . . . . . . 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 5829	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. NN ) /\ n e. I ) -> ( ( F ` k ) ` n ) e. RR )
22	21	an32s 780	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. I ) /\ k e. NN ) -> ( ( F ` k ) ` n ) e. RR )
23	14, 22	eqeltrd 2478	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. I ) /\ k e. NN ) -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` k ) e. RR )
24	23	recnd 9070	. . . . . . . . . . 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 26428	. . . . . . . . . . . . . . . . 17 |- ( I e. Fin -> ( Rn ` I ) e. ( Met ` X ) )
28	26, 27	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Rn ` I ) e. ( Met ` X ) )
29		metxmet 18317	. . . . . . . . . . . . . . . 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 2405	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> ( F ` k ) = ( F ` k ) )
33		eqidd 2405	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN ) -> ( F ` j ) = ( F ` j ) )
34	6, 30, 31, 32, 33, 15	iscauf 19186	. . . . . . . . . . . . . 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 202	. . . . . . . . . . . . 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 452	. . . . . . . . . . . 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 711	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> I e. Fin )
38		simpllr 736	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> n e. I )
39	15	ad3antrrr 711	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> F : NN --> X )
40	6	uztrn2 10459	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( j e. NN /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
41	40	adantll 695	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
42	39, 41	ffvelrnd 5830	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. X )
43		simplr 732	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> j e. NN )
44	39, 43	ffvelrnd 5830	. . . . . . . . . . . . . . . . . . . 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 26429	. . . . . . . . . . . . . . . . . . . 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 1185	. . . . . . . . . . . . . . . . . . 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 711	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( Rn ` I ) e. ( Met ` X ) )
49		metsym 18333	. . . . . . . . . . . . . . . . . . . 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 1184	. . . . . . . . . . . . . . . . . . 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 4196	. . . . . . . . . . . . . . . . . 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 700	. . . . . . . . . . . . . . . . 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 18774	. . . . . . . . . . . . . . . . . . . . 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 731	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ph /\ n e. I ) )
56	55, 41, 22	syl2anc 643	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) ` n ) e. RR )
57	15	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j e. NN ) -> ( F ` j ) e. X )
58	57, 17	syl6eleq 2494	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ j e. NN ) -> ( F ` j ) e. ( RR ^m I ) )
59		elmapi 6997	. . . . . . . . . . . . . . . . . . . . . . . 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 5829	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ j e. NN ) /\ n e. I ) -> ( ( F ` j ) ` n ) e. RR )
62	61	an32s 780	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. I ) /\ j e. NN ) -> ( ( F ` j ) ` n ) e. RR )
63	62	adantr 452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` j ) ` n ) e. RR )
64		metcl 18315	. . . . . . . . . . . . . . . . . . . 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 1184	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) ` n ) M ( ( F ` j ) ` n ) ) e. RR )
66	65	adantllr 700	. . . . . . . . . . . . . . . . . 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 18315	. . . . . . . . . . . . . . . . . . . 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 1184	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ n e. I ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` j ) ( Rn ` I ) ( F ` k ) ) e. RR )
69	68	adantllr 700	. . . . . . . . . . . . . . . . . 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 10574	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. RR+ -> x e. RR )
71	70	adantl 453	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. I ) /\ x e. RR+ ) -> x e. RR )
72	71	ad2antrr 707	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ n e. I ) /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> x e. RR )
73		lelttr 9121	. . . . . . . . . . . . . . . . . 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 1184	. . . . . . . . . . . . . . . . 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 657	. . . . . . . . . . . . . . . 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 2744	. . . . . . . . . . . . . . 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 2778	. . . . . . . . . . . . . 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 2744	. . . . . . . . . . . . 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 18773	. . . . . . . . . . . . . . . . . . 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 643	. . . . . . . . . . . . . . . . . 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 5687	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( t = j -> ( F ` t ) = ( F ` j ) )
83	82	fveq1d 5689	. . . . . . . . . . . . . . . . . . . . . 22 |- ( t = j -> ( ( F ` t ) ` n ) = ( ( F ` j ) ` n ) )
84		fvex 5701	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( F ` j ) ` n ) e. _V
85	83, 11, 84	fvmpt 5765	. . . . . . . . . . . . . . . . . . . . 21 |- ( j e. NN -> ( ( t e. NN |-> ( ( F ` t ) ` n ) ) ` j ) = ( ( F ` j ) ` n ) )
86	85	ad2antlr 708	. . . . . . . . . . . . . . . . . . . 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 6058	. . . . . . . . . . . . . . . . . . 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 5691	. . . . . . . . . . . . . . . . . 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 2439	. . . . . . . . . . . . . . . . 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 4182	. . . . . . . . . . . . . . . 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 2682	. . . . . . . . . . . . . . 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 2683	. . . . . . . . . . . . . 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 2686	. . . . . . . . . . . . 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 206	. . . . . . . . . . . 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 9962	. . . . . . . . . . . . 13 |- NN e. _V
97	96	mptex 5925	. . . . . . . . . . . 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 12427	. . . . . . . . . 10 |- ( ( ph /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) e. dom ~~> )
100		climdm 12303	. . . . . . . . . 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 189	. . . . . . . . 9 |- ( ( ph /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) ~~> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) )
102		fveq2 5687	. . . . . . . . . . . . 13 |- ( m = n -> ( ( F ` t ) ` m ) = ( ( F ` t ) ` n ) )
103	102	mpteq2dv 4256	. . . . . . . . . . . 12 |- ( m = n -> ( t e. NN |-> ( ( F ` t ) ` m ) ) = ( t e. NN |-> ( ( F ` t ) ` n ) ) )
104	103	fveq2d 5691	. . . . . . . . . . 11 |- ( m = n -> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` m ) ) ) = ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) )
105		fvex 5701	. . . . . . . . . . 11 |- ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) e. _V
106	104, 3, 105	fvmpt 5765	. . . . . . . . . 10 |- ( n e. I -> ( P ` n ) = ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) )
107	106	adantl 453	. . . . . . . . 9 |- ( ( ph /\ n e. I ) -> ( P ` n ) = ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` n ) ) ) )
108	101, 107	breqtrrd 4198	. . . . . . . 8 |- ( ( ph /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) ~~> ( P ` n ) )
109	6, 8, 108, 23	climrecl 12332	. . . . . . 7 |- ( ( ph /\ n e. I ) -> ( P ` n ) e. RR )
110	109	ralrimiva 2749	. . . . . 6 |- ( ph -> A. n e. I ( P ` n ) e. RR )
111		ffnfv 5853	. . . . . 6 |- ( P : I --> RR <-> ( P Fn I /\ A. n e. I ( P ` n ) e. RR ) )
112	5, 110, 111	sylanbrc 646	. . . . 5 |- ( ph -> P : I --> RR )
113		reex 9037	. . . . . 6 |- RR e. _V
114		elmapg 6990	. . . . . 6 |- ( ( RR e. _V /\ I e. Fin ) -> ( P e. ( RR ^m I ) <-> P : I --> RR ) )
115	113, 26, 114	sylancr 645	. . . . 5 |- ( ph -> ( P e. ( RR ^m I ) <-> P : I --> RR ) )
116	112, 115	mpbird 224	. . . 4 |- ( ph -> P e. ( RR ^m I ) )
117	116, 17	syl6eleqr 2495	. . 3 |- ( ph -> P e. X )
118		1nn 9967	. . . . . . 7 |- 1 e. NN
119	26	ad2antrr 707	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> I e. Fin )
120	16	adantlr 696	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( F ` k ) e. X )
121	117	ad2antrr 707	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> P e. X )
122	17	rrnmval 26427	. . . . . . . . . . . 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 1184	. . . . . . . . . . 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 738	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> I = (/) )
125	124	sumeq1d 12450	. . . . . . . . . . . . 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 12470	. . . . . . . . . . . . 13 |- sum_ y e. (/) ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) = 0
127	125, 126	syl6eq 2452	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> sum_ y e. I ( ( ( ( F ` k ) ` y ) - ( P ` y ) ) ^ 2 ) = 0 )
128	127	fveq2d 5691	. . . . . . . . . . 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 2436	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( ( F ` k ) ( Rn ` I ) P ) = ( sqr ` 0 ) )
130		sqr0 12002	. . . . . . . . . 10 |- ( sqr ` 0 ) = 0
131	129, 130	syl6eq 2452	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( ( F ` k ) ( Rn ` I ) P ) = 0 )
132		simplrl 737	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> x e. RR+ )
133	132	rpgt0d 10607	. . . . . . . . 9 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> 0 < x )
134	131, 133	eqbrtrd 4192	. . . . . . . 8 |- ( ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) /\ k e. NN ) -> ( ( F ` k ) ( Rn ` I ) P ) < x )
135	134	ralrimiva 2749	. . . . . . 7 |- ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) -> A. k e. NN ( ( F ` k ) ( Rn ` I ) P ) < x )
136		fveq2 5687	. . . . . . . . . 10 |- ( j = 1 -> ( ZZ>= ` j ) = ( ZZ>= ` 1 ) )
137	136, 6	syl6eqr 2454	. . . . . . . . 9 |- ( j = 1 -> ( ZZ>= ` j ) = NN )
138	137	raleqdv 2870	. . . . . . . 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 3012	. . . . . . 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 645	. . . . . 6 |- ( ( ph /\ ( x e. RR+ /\ I = (/) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x )
141	140	expr 599	. . . . 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 733	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> x e. RR+ )
144		simprr 734	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> I =/= (/) )
145	26	adantr 452	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> I e. Fin )
146		hashnncl 11600	. . . . . . . . . . . . . . . . 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 224	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( # ` I ) e. NN )
149	148	nnrpd 10603	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( # ` I ) e. RR+ )
150	149	rpsqrcld 12169	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( sqr ` ( # ` I ) ) e. RR+ )
151	143, 150	rpdivcld 10621	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> ( x / ( sqr ` ( # ` I ) ) ) e. RR+ )
152	151	adantr 452	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( x / ( sqr ` ( # ` I ) ) ) e. RR+ )
153	13	adantl 453	. . . . . . . . . . 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 696	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( t e. NN |-> ( ( F ` t ) ` n ) ) ~~> ( P ` n ) )
155	6, 142, 152, 153, 154	climi2 12260	. . . . . . . . . 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 12107	. . . . . . . . . . . 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 700	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( ( F ` k ) ` n ) e. RR )
159	109	adantlr 696	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) -> ( P ` n ) e. RR )
160	159	adantr 452	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ n e. I ) /\ k e. NN ) -> ( P ` n ) e. RR )
161	45	remetdval 18773	. . . . . . . . . . . . . . . . 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 643	. . . . . . . . . . . . . . . 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 4182	. . . . . . . . . . . . . . 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 461	. . . . . . . . . . . . . 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 630	. . . . . . . . . . . . 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 2682	. . . . . . . . . . . 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 2683	. . . . . . . . . . 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 251	. . . . . . . . . 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 224	. . . . . . . . 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 2749	. . . . . . . 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 12107	. . . . . . . . . 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 12106	. . . . . . . . . 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 249	. . . . . . . 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 224	. . . . . . 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 707	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> I e. Fin )
178		simplrr 738	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> I =/= (/) )
179		eldifsn 3887	. . . . . . . . . . . . . 14 |- ( I e. ( Fin \ { (/) } ) <-> ( I e. Fin /\ I =/= (/) ) )
180	177, 178, 179	sylanbrc 646	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> I e. ( Fin \ { (/) } ) )
181	15	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) -> F : NN --> X )
182	181	ffvelrnda 5829	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( F ` k ) e. X )
183	117	ad2antrr 707	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> P e. X )
184	151	adantr 452	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( x / ( sqr ` ( # ` I ) ) ) e. RR+ )
185	17, 45	rrndstprj2 26430	. . . . . . . . . . . . . 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 599	. . . . . . . . . . . . 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 1187	. . . . . . . . . . . 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 737	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> x e. RR+ )
189	188	rpcnd 10606	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> x e. CC )
190	150	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( sqr ` ( # ` I ) ) e. RR+ )
191	190	rpcnd 10606	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( sqr ` ( # ` I ) ) e. CC )
192	190	rpne0d 10609	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( sqr ` ( # ` I ) ) =/= 0 )
193	189, 191, 192	divcan1d 9747	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. RR+ /\ I =/= (/) ) ) /\ k e. NN ) -> ( ( x / ( sqr ` ( # ` I ) ) ) x. ( sqr ` ( # ` I ) ) ) = x )
194	193	breq2d 4184	. . . . . . . . . . . 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 206	. . . . . . . . . . 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 461	. . . . . . . . . 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 630	. . . . . . . . 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 2744	. . . . . . . 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 2778	. . . . . . 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 599	. . . . 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 2644	. . . 4 |- ( ( ph /\ x e. RR+ ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) ( Rn ` I ) P ) < x )
203	202	ralrimiva 2749	. . 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 19168	. . 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 889	. 2 |- ( ph -> F ( ~~> t ` J ) P )
207		releldm 5061	. 2 |- ( ( Rel ( ~~> t ` J ) /\ F ( ~~> t ` J ) P ) -> F e. dom ( ~~> t ` J ) )
208	1, 206, 207	sylancr 645	1 |- ( ph -> F e. dom ( ~~> t ` J ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916   \ cdif 3277   (/)c0 3588   {csn 3774   class class class wbr 4172   e. cmpt 4226   X. cxp 4835   dom cdm 4837   |` cres 4839   o. ccom 4841   Rel wrel 4842   Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040   ^m cmap 6977   Fincfn 7068   RRcr 8945   0cc0 8946   1c1 8947   x. cmul 8951   < clt 9076   <_ cle 9077   - cmin 9247   / cdiv 9633   NNcn 9956   2c2 10005   ZZcz 10238   ZZ>=cuz 10444   RR+crp 10568   ^cexp 11337   #chash 11573   sqrcsqr 11993   abscabs 11994   ~~> cli 12233   sum_csu 12434   * Metcxmt 16641   Metcme 16642   MetOpencmopn 16646   ~~> tclm 17244   Caucca 19159   Rncrrn 26424

This theorem is referenced by:  rrncms  26432

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025  ax-mulf 9026

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-n0 10178  df-z 10239  df-uz 10445  df-q 10531  df-rp 10569  df-xneg 10666  df-xadd 10667  df-xmul 10668  df-ico 10878  df-fz 11000  df-fzo 11091  df-fl 11157  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-limsup 12220  df-clim 12237  df-rlim 12238  df-sum 12435  df-topgen 13622  df-psmet 16649  df-xmet 16650  df-met 16651  df-bl 16652  df-mopn 16653  df-top 16918  df-bases 16920  df-topon 16921  df-lm 17247  df-cau 19162  df-rrn 26425