Theorem dchrisumlem3 25180

Description: Lemma for dchrisum 25181. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.)

Hypotheses

Ref	Expression
rpvmasum.z	|- Z = (ℤ/nℤ ` N )
rpvmasum.l	|- L = ( ZRHom ` Z )
rpvmasum.a	|- ( ph -> N e. NN )
rpvmasum.g	|- G = (DChr ` N )
rpvmasum.d	|- D = ( Base ` G )
rpvmasum.1	|- .1. = ( 0g ` G )
dchrisum.b	|- ( ph -> X e. D )
dchrisum.n1	|- ( ph -> X =/= .1. )
dchrisum.2	|- ( n = x -> A = B )
dchrisum.3	|- ( ph -> M e. NN )
dchrisum.4	|- ( ( ph /\ n e. RR+ ) -> A e. RR )
dchrisum.5	|- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
dchrisum.6	|- ( ph -> ( n e. RR+ |-> A ) ~~> r 0 )
dchrisum.7	|- F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )
dchrisum.9	|- ( ph -> R e. RR )
dchrisum.10	|- ( ph -> A. u e. ( 0..^ N ) ( abs ` sum_ n e. ( 0..^ u ) ( X ` ( L ` n ) ) ) <_ R )

Assertion

Ref	Expression
dchrisumlem3	|- ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) )

Distinct variable groups:   u, n, x, c, t   .1. , c   t, n, .1. , x   u, c, F, n, t, x   A, c, t, x   N, c, n, t, u, x   ph, c, n, t, u, x   R, c, n, u, x   B, c, n   n, Z, x   D, c, n, t, x   L, c, n, t, u, x   M, c, n, u, x   X, c, n, t, u, x

Allowed substitution hints:   A( u, n)   B( x, u, t)   D( u)   R( t)   .1. ( u)   G( x, u, t, n, c)   M( t)   Z( u, t, c)

Proof of Theorem dchrisumlem3

Dummy variables k m i j e are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnuz 11723	. . . 4 |- NN = ( ZZ>= ` 1 )
2		1zzd 11408	. . . . . 6 |- ( ph -> 1 e. ZZ )
3		simpr 477	. . . . . . . 8 |- ( ( ph /\ i e. NN ) -> i e. NN )
4		rpvmasum.g	. . . . . . . . . 10 |- G = (DChr ` N )
5		rpvmasum.z	. . . . . . . . . 10 |- Z = (ℤ/nℤ ` N )
6		rpvmasum.d	. . . . . . . . . 10 |- D = ( Base ` G )
7		rpvmasum.l	. . . . . . . . . 10 |- L = ( ZRHom ` Z )
8		dchrisum.b	. . . . . . . . . . 11 |- ( ph -> X e. D )
9	8	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> X e. D )
10	3	nnzd 11481	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> i e. ZZ )
11	4, 5, 6, 7, 9, 10	dchrzrhcl 24970	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> ( X ` ( L ` i ) ) e. CC )
12		dchrisum.4	. . . . . . . . . . . 12 |- ( ( ph /\ n e. RR+ ) -> A e. RR )
13	12	ralrimiva 2966	. . . . . . . . . . 11 |- ( ph -> A. n e. RR+ A e. RR )
14		nnrp 11842	. . . . . . . . . . 11 |- ( i e. NN -> i e. RR+ )
15		nfcsb1v 3549	. . . . . . . . . . . . . 14 |- F/_ n [_ i / n ]_ A
16	15	nfel1 2779	. . . . . . . . . . . . 13 |- F/ n [_ i / n ]_ A e. RR
17		csbeq1a 3542	. . . . . . . . . . . . . 14 |- ( n = i -> A = [_ i / n ]_ A )
18	17	eleq1d 2686	. . . . . . . . . . . . 13 |- ( n = i -> ( A e. RR <-> [_ i / n ]_ A e. RR ) )
19	16, 18	rspc 3303	. . . . . . . . . . . 12 |- ( i e. RR+ -> ( A. n e. RR+ A e. RR -> [_ i / n ]_ A e. RR ) )
20	19	impcom 446	. . . . . . . . . . 11 |- ( ( A. n e. RR+ A e. RR /\ i e. RR+ ) -> [_ i / n ]_ A e. RR )
21	13, 14, 20	syl2an 494	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> [_ i / n ]_ A e. RR )
22	21	recnd 10068	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> [_ i / n ]_ A e. CC )
23	11, 22	mulcld 10060	. . . . . . . 8 |- ( ( ph /\ i e. NN ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
24		nfcv 2764	. . . . . . . . 9 |- F/_ n i
25		nfcv 2764	. . . . . . . . . 10 |- F/_ n ( X ` ( L ` i ) )
26		nfcv 2764	. . . . . . . . . 10 |- F/_ n x.
27	25, 26, 15	nfov 6676	. . . . . . . . 9 |- F/_ n ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A )
28		fveq2 6191	. . . . . . . . . . 11 |- ( n = i -> ( L ` n ) = ( L ` i ) )
29	28	fveq2d 6195	. . . . . . . . . 10 |- ( n = i -> ( X ` ( L ` n ) ) = ( X ` ( L ` i ) ) )
30	29, 17	oveq12d 6668	. . . . . . . . 9 |- ( n = i -> ( ( X ` ( L ` n ) ) x. A ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
31		dchrisum.7	. . . . . . . . 9 |- F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )
32	24, 27, 30, 31	fvmptf 6301	. . . . . . . 8 |- ( ( i e. NN /\ ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
33	3, 23, 32	syl2anc 693	. . . . . . 7 |- ( ( ph /\ i e. NN ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
34	33, 23	eqeltrd 2701	. . . . . 6 |- ( ( ph /\ i e. NN ) -> ( F ` i ) e. CC )
35	1, 2, 34	serf 12829	. . . . 5 |- ( ph -> seq 1 ( + , F ) : NN --> CC )
36	35	ffvelrnda 6359	. . . 4 |- ( ( ph /\ k e. NN ) -> ( seq 1 ( + , F ) ` k ) e. CC )
37	12	recnd 10068	. . . . . . . . 9 |- ( ( ph /\ n e. RR+ ) -> A e. CC )
38	37	ralrimiva 2966	. . . . . . . 8 |- ( ph -> A. n e. RR+ A e. CC )
39	38	adantr 481	. . . . . . 7 |- ( ( ph /\ e e. RR+ ) -> A. n e. RR+ A e. CC )
40		id 22	. . . . . . . 8 |- ( e e. RR+ -> e e. RR+ )
41		2re 11090	. . . . . . . . . 10 |- 2 e. RR
42		dchrisum.9	. . . . . . . . . 10 |- ( ph -> R e. RR )
43		remulcl 10021	. . . . . . . . . 10 |- ( ( 2 e. RR /\ R e. RR ) -> ( 2 x. R ) e. RR )
44	41, 42, 43	sylancr 695	. . . . . . . . 9 |- ( ph -> ( 2 x. R ) e. RR )
45		rpvmasum.a	. . . . . . . . . . . 12 |- ( ph -> N e. NN )
46		lbfzo0 12507	. . . . . . . . . . . 12 |- ( 0 e. ( 0..^ N ) <-> N e. NN )
47	45, 46	sylibr 224	. . . . . . . . . . 11 |- ( ph -> 0 e. ( 0..^ N ) )
48		dchrisum.10	. . . . . . . . . . 11 |- ( ph -> A. u e. ( 0..^ N ) ( abs ` sum_ n e. ( 0..^ u ) ( X ` ( L ` n ) ) ) <_ R )
49		oveq2 6658	. . . . . . . . . . . . . . . . 17 |- ( u = 0 -> ( 0..^ u ) = ( 0..^ 0 ) )
50		fzo0 12492	. . . . . . . . . . . . . . . . 17 |- ( 0..^ 0 ) = (/)
51	49, 50	syl6eq 2672	. . . . . . . . . . . . . . . 16 |- ( u = 0 -> ( 0..^ u ) = (/) )
52	51	sumeq1d 14431	. . . . . . . . . . . . . . 15 |- ( u = 0 -> sum_ n e. ( 0..^ u ) ( X ` ( L ` n ) ) = sum_ n e. (/) ( X ` ( L ` n ) ) )
53		sum0 14452	. . . . . . . . . . . . . . 15 |- sum_ n e. (/) ( X ` ( L ` n ) ) = 0
54	52, 53	syl6eq 2672	. . . . . . . . . . . . . 14 |- ( u = 0 -> sum_ n e. ( 0..^ u ) ( X ` ( L ` n ) ) = 0 )
55	54	abs00bd 14031	. . . . . . . . . . . . 13 |- ( u = 0 -> ( abs ` sum_ n e. ( 0..^ u ) ( X ` ( L ` n ) ) ) = 0 )
56	55	breq1d 4663	. . . . . . . . . . . 12 |- ( u = 0 -> ( ( abs ` sum_ n e. ( 0..^ u ) ( X ` ( L ` n ) ) ) <_ R <-> 0 <_ R ) )
57	56	rspcv 3305	. . . . . . . . . . 11 |- ( 0 e. ( 0..^ N ) -> ( A. u e. ( 0..^ N ) ( abs ` sum_ n e. ( 0..^ u ) ( X ` ( L ` n ) ) ) <_ R -> 0 <_ R ) )
58	47, 48, 57	sylc 65	. . . . . . . . . 10 |- ( ph -> 0 <_ R )
59		0le2 11111	. . . . . . . . . . 11 |- 0 <_ 2
60		mulge0 10546	. . . . . . . . . . 11 |- ( ( ( 2 e. RR /\ 0 <_ 2 ) /\ ( R e. RR /\ 0 <_ R ) ) -> 0 <_ ( 2 x. R ) )
61	41, 59, 60	mpanl12 718	. . . . . . . . . 10 |- ( ( R e. RR /\ 0 <_ R ) -> 0 <_ ( 2 x. R ) )
62	42, 58, 61	syl2anc 693	. . . . . . . . 9 |- ( ph -> 0 <_ ( 2 x. R ) )
63	44, 62	ge0p1rpd 11902	. . . . . . . 8 |- ( ph -> ( ( 2 x. R ) + 1 ) e. RR+ )
64		rpdivcl 11856	. . . . . . . 8 |- ( ( e e. RR+ /\ ( ( 2 x. R ) + 1 ) e. RR+ ) -> ( e / ( ( 2 x. R ) + 1 ) ) e. RR+ )
65	40, 63, 64	syl2anr 495	. . . . . . 7 |- ( ( ph /\ e e. RR+ ) -> ( e / ( ( 2 x. R ) + 1 ) ) e. RR+ )
66		dchrisum.6	. . . . . . . 8 |- ( ph -> ( n e. RR+ |-> A ) ~~> r 0 )
67	66	adantr 481	. . . . . . 7 |- ( ( ph /\ e e. RR+ ) -> ( n e. RR+ |-> A ) ~~> r 0 )
68	39, 65, 67	rlimi 14244	. . . . . 6 |- ( ( ph /\ e e. RR+ ) -> E. m e. RR A. n e. RR+ ( m <_ n -> ( abs ` ( A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) )
69		simpr 477	. . . . . . . . . . . 12 |- ( ( ph /\ m e. RR ) -> m e. RR )
70		dchrisum.3	. . . . . . . . . . . . . 14 |- ( ph -> M e. NN )
71	70	nnred 11035	. . . . . . . . . . . . 13 |- ( ph -> M e. RR )
72	71	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ m e. RR ) -> M e. RR )
73	69, 72	ifcld 4131	. . . . . . . . . . 11 |- ( ( ph /\ m e. RR ) -> if ( M <_ m , m , M ) e. RR )
74		0red 10041	. . . . . . . . . . . 12 |- ( ( ph /\ m e. RR ) -> 0 e. RR )
75	70	nngt0d 11064	. . . . . . . . . . . . 13 |- ( ph -> 0 < M )
76	75	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ m e. RR ) -> 0 < M )
77		max1 12016	. . . . . . . . . . . . 13 |- ( ( M e. RR /\ m e. RR ) -> M <_ if ( M <_ m , m , M ) )
78	71, 77	sylan 488	. . . . . . . . . . . 12 |- ( ( ph /\ m e. RR ) -> M <_ if ( M <_ m , m , M ) )
79	74, 72, 73, 76, 78	ltletrd 10197	. . . . . . . . . . 11 |- ( ( ph /\ m e. RR ) -> 0 < if ( M <_ m , m , M ) )
80	73, 79	elrpd 11869	. . . . . . . . . 10 |- ( ( ph /\ m e. RR ) -> if ( M <_ m , m , M ) e. RR+ )
81	80	adantlr 751	. . . . . . . . 9 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> if ( M <_ m , m , M ) e. RR+ )
82		nfv 1843	. . . . . . . . . . 11 |- F/ n m <_ if ( M <_ m , m , M )
83		nfcv 2764	. . . . . . . . . . . . 13 |- F/_ n abs
84		nfcsb1v 3549	. . . . . . . . . . . . . 14 |- F/_ n [_ if ( M <_ m , m , M ) / n ]_ A
85		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ n -
86		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ n 0
87	84, 85, 86	nfov 6676	. . . . . . . . . . . . 13 |- F/_ n ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 )
88	83, 87	nffv 6198	. . . . . . . . . . . 12 |- F/_ n ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) )
89		nfcv 2764	. . . . . . . . . . . 12 |- F/_ n <
90		nfcv 2764	. . . . . . . . . . . 12 |- F/_ n ( e / ( ( 2 x. R ) + 1 ) )
91	88, 89, 90	nfbr 4699	. . . . . . . . . . 11 |- F/ n ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) )
92	82, 91	nfim 1825	. . . . . . . . . 10 |- F/ n ( m <_ if ( M <_ m , m , M ) -> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) )
93		breq2 4657	. . . . . . . . . . 11 |- ( n = if ( M <_ m , m , M ) -> ( m <_ n <-> m <_ if ( M <_ m , m , M ) ) )
94		csbeq1a 3542	. . . . . . . . . . . . . 14 |- ( n = if ( M <_ m , m , M ) -> A = [_ if ( M <_ m , m , M ) / n ]_ A )
95	94	oveq1d 6665	. . . . . . . . . . . . 13 |- ( n = if ( M <_ m , m , M ) -> ( A - 0 ) = ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) )
96	95	fveq2d 6195	. . . . . . . . . . . 12 |- ( n = if ( M <_ m , m , M ) -> ( abs ` ( A - 0 ) ) = ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) )
97	96	breq1d 4663	. . . . . . . . . . 11 |- ( n = if ( M <_ m , m , M ) -> ( ( abs ` ( A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) <-> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) )
98	93, 97	imbi12d 334	. . . . . . . . . 10 |- ( n = if ( M <_ m , m , M ) -> ( ( m <_ n -> ( abs ` ( A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) <-> ( m <_ if ( M <_ m , m , M ) -> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) ) )
99	92, 98	rspc 3303	. . . . . . . . 9 |- ( if ( M <_ m , m , M ) e. RR+ -> ( A. n e. RR+ ( m <_ n -> ( abs ` ( A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) -> ( m <_ if ( M <_ m , m , M ) -> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) ) )
100	81, 99	syl 17	. . . . . . . 8 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( A. n e. RR+ ( m <_ n -> ( abs ` ( A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) -> ( m <_ if ( M <_ m , m , M ) -> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) ) )
101	71	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> M e. RR )
102		max2 12018	. . . . . . . . . 10 |- ( ( M e. RR /\ m e. RR ) -> m <_ if ( M <_ m , m , M ) )
103	101, 102	sylancom 701	. . . . . . . . 9 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> m <_ if ( M <_ m , m , M ) )
104	13	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> A. n e. RR+ A e. RR )
105	84	nfel1 2779	. . . . . . . . . . . . . . . . . . 19 |- F/ n [_ if ( M <_ m , m , M ) / n ]_ A e. RR
106	94	eleq1d 2686	. . . . . . . . . . . . . . . . . . 19 |- ( n = if ( M <_ m , m , M ) -> ( A e. RR <-> [_ if ( M <_ m , m , M ) / n ]_ A e. RR ) )
107	105, 106	rspc 3303	. . . . . . . . . . . . . . . . . 18 |- ( if ( M <_ m , m , M ) e. RR+ -> ( A. n e. RR+ A e. RR -> [_ if ( M <_ m , m , M ) / n ]_ A e. RR ) )
108	81, 104, 107	sylc 65	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> [_ if ( M <_ m , m , M ) / n ]_ A e. RR )
109	108	recnd 10068	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> [_ if ( M <_ m , m , M ) / n ]_ A e. CC )
110	109	subid1d 10381	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) = [_ if ( M <_ m , m , M ) / n ]_ A )
111	110	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) = ( abs ` [_ if ( M <_ m , m , M ) / n ]_ A ) )
112	73	adantlr 751	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> if ( M <_ m , m , M ) e. RR )
113	101, 77	sylancom 701	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> M <_ if ( M <_ m , m , M ) )
114		elicopnf 12269	. . . . . . . . . . . . . . . . . 18 |- ( M e. RR -> ( if ( M <_ m , m , M ) e. ( M [,) +oo ) <-> ( if ( M <_ m , m , M ) e. RR /\ M <_ if ( M <_ m , m , M ) ) ) )
115	101, 114	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( if ( M <_ m , m , M ) e. ( M [,) +oo ) <-> ( if ( M <_ m , m , M ) e. RR /\ M <_ if ( M <_ m , m , M ) ) ) )
116	112, 113, 115	mpbir2and 957	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> if ( M <_ m , m , M ) e. ( M [,) +oo ) )
117	45	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> N e. NN )
118		rpvmasum.1	. . . . . . . . . . . . . . . . . 18 |- .1. = ( 0g ` G )
119	8	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> X e. D )
120		dchrisum.n1	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> X =/= .1. )
121	120	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> X =/= .1. )
122		dchrisum.2	. . . . . . . . . . . . . . . . . 18 |- ( n = x -> A = B )
123	70	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> M e. NN )
124	104	r19.21bi 2932	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ n e. RR+ ) -> A e. RR )
125		simpll 790	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ph )
126		dchrisum.5	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
127	125, 126	syl3an1 1359	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
128	66	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( n e. RR+ |-> A ) ~~> r 0 )
129	5, 7, 117, 4, 6, 118, 119, 121, 122, 123, 124, 127, 128, 31	dchrisumlema 25177	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( if ( M <_ m , m , M ) e. RR+ -> [_ if ( M <_ m , m , M ) / n ]_ A e. RR ) /\ ( if ( M <_ m , m , M ) e. ( M [,) +oo ) -> 0 <_ [_ if ( M <_ m , m , M ) / n ]_ A ) ) )
130	129	simprd 479	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( if ( M <_ m , m , M ) e. ( M [,) +oo ) -> 0 <_ [_ if ( M <_ m , m , M ) / n ]_ A ) )
131	116, 130	mpd 15	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> 0 <_ [_ if ( M <_ m , m , M ) / n ]_ A )
132	108, 131	absidd 14161	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( abs ` [_ if ( M <_ m , m , M ) / n ]_ A ) = [_ if ( M <_ m , m , M ) / n ]_ A )
133	111, 132	eqtrd 2656	. . . . . . . . . . . . 13 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) = [_ if ( M <_ m , m , M ) / n ]_ A )
134	133	breq1d 4663	. . . . . . . . . . . 12 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) <-> [_ if ( M <_ m , m , M ) / n ]_ A < ( e / ( ( 2 x. R ) + 1 ) ) ) )
135		rpre 11839	. . . . . . . . . . . . . 14 |- ( e e. RR+ -> e e. RR )
136	135	ad2antlr 763	. . . . . . . . . . . . 13 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> e e. RR )
137	63	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( 2 x. R ) + 1 ) e. RR+ )
138	108, 136, 137	ltmuldiv2d 11920	. . . . . . . . . . . 12 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e <-> [_ if ( M <_ m , m , M ) / n ]_ A < ( e / ( ( 2 x. R ) + 1 ) ) ) )
139	134, 138	bitr4d 271	. . . . . . . . . . 11 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) <-> ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) )
140	44	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( 2 x. R ) e. RR )
141	137	rpred 11872	. . . . . . . . . . . . 13 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( 2 x. R ) + 1 ) e. RR )
142	140	lep1d 10955	. . . . . . . . . . . . 13 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( 2 x. R ) <_ ( ( 2 x. R ) + 1 ) )
143	140, 141, 108, 131, 142	lemul1ad 10963	. . . . . . . . . . . 12 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) <_ ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) )
144	140, 108	remulcld 10070	. . . . . . . . . . . . 13 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) e. RR )
145	141, 108	remulcld 10070	. . . . . . . . . . . . 13 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) e. RR )
146		lelttr 10128	. . . . . . . . . . . . 13 |- ( ( ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) e. RR /\ ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) e. RR /\ e e. RR ) -> ( ( ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) <_ ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) /\ ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) -> ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) )
147	144, 145, 136, 146	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) <_ ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) /\ ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) -> ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) )
148	143, 147	mpand 711	. . . . . . . . . . 11 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( ( ( 2 x. R ) + 1 ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e -> ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) )
149	139, 148	sylbid 230	. . . . . . . . . 10 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) -> ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) )
150		1red 10055	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. RR ) -> 1 e. RR )
151	70	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ m e. RR ) -> M e. NN )
152	151	nnge1d 11063	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. RR ) -> 1 <_ M )
153	150, 72, 73, 152, 78	letrd 10194	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. RR ) -> 1 <_ if ( M <_ m , m , M ) )
154		flge1nn 12622	. . . . . . . . . . . . 13 |- ( ( if ( M <_ m , m , M ) e. RR /\ 1 <_ if ( M <_ m , m , M ) ) -> ( |_ ` if ( M <_ m , m , M ) ) e. NN )
155	73, 153, 154	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ph /\ m e. RR ) -> ( |_ ` if ( M <_ m , m , M ) ) e. NN )
156	155	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( |_ ` if ( M <_ m , m , M ) ) e. NN )
157	45	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> N e. NN )
158	8	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> X e. D )
159	120	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> X =/= .1. )
160	70	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> M e. NN )
161	12	adantlr 751	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. RR ) /\ n e. RR+ ) -> A e. RR )
162	161	adantlr 751	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) /\ n e. RR+ ) -> A e. RR )
163	126	3adant1r 1319	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. RR ) /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
164	163	3adant1r 1319	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
165	66	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( n e. RR+ |-> A ) ~~> r 0 )
166	42	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> R e. RR )
167	48	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> A. u e. ( 0..^ N ) ( abs ` sum_ n e. ( 0..^ u ) ( X ` ( L ` n ) ) ) <_ R )
168	80	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> if ( M <_ m , m , M ) e. RR+ )
169	78	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> M <_ if ( M <_ m , m , M ) )
170	73	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> if ( M <_ m , m , M ) e. RR )
171		fllep1 12602	. . . . . . . . . . . . . . . 16 |- ( if ( M <_ m , m , M ) e. RR -> if ( M <_ m , m , M ) <_ ( ( |_ ` if ( M <_ m , m , M ) ) + 1 ) )
172	170, 171	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> if ( M <_ m , m , M ) <_ ( ( |_ ` if ( M <_ m , m , M ) ) + 1 ) )
173	155	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( |_ ` if ( M <_ m , m , M ) ) e. NN )
174		simpr 477	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) )
175	5, 7, 157, 4, 6, 118, 158, 159, 122, 160, 162, 164, 165, 31, 166, 167, 168, 169, 172, 173, 174	dchrisumlem2 25179	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) <_ ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) )
176	175	adantllr 755	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) <_ ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) )
177	35	ad3antrrr 766	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> seq 1 ( + , F ) : NN --> CC )
178		eluznn 11758	. . . . . . . . . . . . . . . . . 18 |- ( ( ( |_ ` if ( M <_ m , m , M ) ) e. NN /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> k e. NN )
179	156, 178	sylan 488	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> k e. NN )
180	177, 179	ffvelrnd 6360	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( seq 1 ( + , F ) ` k ) e. CC )
181	156	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( |_ ` if ( M <_ m , m , M ) ) e. NN )
182	177, 181	ffvelrnd 6360	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) e. CC )
183	180, 182	subcld 10392	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) e. CC )
184	183	abscld 14175	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) e. RR )
185	144	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) e. RR )
186	136	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> e e. RR )
187		lelttr 10128	. . . . . . . . . . . . . 14 |- ( ( ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) e. RR /\ ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) e. RR /\ e e. RR ) -> ( ( ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) <_ ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) /\ ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) -> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) < e ) )
188	184, 185, 186, 187	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( ( ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) <_ ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) /\ ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e ) -> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) < e ) )
189	176, 188	mpand 711	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) /\ k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ) -> ( ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e -> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) < e ) )
190	189	ralrimdva 2969	. . . . . . . . . . 11 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e -> A. k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) < e ) )
191		fveq2 6191	. . . . . . . . . . . . 13 |- ( j = ( |_ ` if ( M <_ m , m , M ) ) -> ( ZZ>= ` j ) = ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) )
192		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( j = ( |_ ` if ( M <_ m , m , M ) ) -> ( seq 1 ( + , F ) ` j ) = ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) )
193	192	oveq2d 6666	. . . . . . . . . . . . . . 15 |- ( j = ( |_ ` if ( M <_ m , m , M ) ) -> ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) = ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) )
194	193	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( j = ( |_ ` if ( M <_ m , m , M ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) = ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) )
195	194	breq1d 4663	. . . . . . . . . . . . 13 |- ( j = ( |_ ` if ( M <_ m , m , M ) ) -> ( ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e <-> ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) < e ) )
196	191, 195	raleqbidv 3152	. . . . . . . . . . . 12 |- ( j = ( |_ ` if ( M <_ m , m , M ) ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e <-> A. k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) < e ) )
197	196	rspcev 3309	. . . . . . . . . . 11 |- ( ( ( |_ ` if ( M <_ m , m , M ) ) e. NN /\ A. k e. ( ZZ>= ` ( |_ ` if ( M <_ m , m , M ) ) ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` ( |_ ` if ( M <_ m , m , M ) ) ) ) ) < e ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e )
198	156, 190, 197	syl6an 568	. . . . . . . . . 10 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( ( 2 x. R ) x. [_ if ( M <_ m , m , M ) / n ]_ A ) < e -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e ) )
199	149, 198	syld 47	. . . . . . . . 9 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e ) )
200	103, 199	embantd 59	. . . . . . . 8 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( ( m <_ if ( M <_ m , m , M ) -> ( abs ` ( [_ if ( M <_ m , m , M ) / n ]_ A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e ) )
201	100, 200	syld 47	. . . . . . 7 |- ( ( ( ph /\ e e. RR+ ) /\ m e. RR ) -> ( A. n e. RR+ ( m <_ n -> ( abs ` ( A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e ) )
202	201	rexlimdva 3031	. . . . . 6 |- ( ( ph /\ e e. RR+ ) -> ( E. m e. RR A. n e. RR+ ( m <_ n -> ( abs ` ( A - 0 ) ) < ( e / ( ( 2 x. R ) + 1 ) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e ) )
203	68, 202	mpd 15	. . . . 5 |- ( ( ph /\ e e. RR+ ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e )
204	203	ralrimiva 2966	. . . 4 |- ( ph -> A. e e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( abs ` ( ( seq 1 ( + , F ) ` k ) - ( seq 1 ( + , F ) ` j ) ) ) < e )
205		seqex 12803	. . . . 5 |- seq 1 ( + , F ) e. _V
206	205	a1i 11	. . . 4 |- ( ph -> seq 1 ( + , F ) e. _V )
207	1, 36, 204, 206	caucvg 14409	. . 3 |- ( ph -> seq 1 ( + , F ) e. dom ~~> )
208	205	eldm 5321	. . 3 |- ( seq 1 ( + , F ) e. dom ~~> <-> E. t seq 1 ( + , F ) ~~> t )
209	207, 208	sylib 208	. 2 |- ( ph -> E. t seq 1 ( + , F ) ~~> t )
210		simpr 477	. . . . 5 |- ( ( ph /\ seq 1 ( + , F ) ~~> t ) -> seq 1 ( + , F ) ~~> t )
211		elrege0 12278	. . . . . . . 8 |- ( ( 2 x. R ) e. ( 0 [,) +oo ) <-> ( ( 2 x. R ) e. RR /\ 0 <_ ( 2 x. R ) ) )
212	44, 62, 211	sylanbrc 698	. . . . . . 7 |- ( ph -> ( 2 x. R ) e. ( 0 [,) +oo ) )
213	212	adantr 481	. . . . . 6 |- ( ( ph /\ seq 1 ( + , F ) ~~> t ) -> ( 2 x. R ) e. ( 0 [,) +oo ) )
214		eqid 2622	. . . . . . . 8 |- ( ZZ>= ` ( |_ ` m ) ) = ( ZZ>= ` ( |_ ` m ) )
215		pnfxr 10092	. . . . . . . . . . . 12 |- +oo e. RR*
216		icossre 12254	. . . . . . . . . . . 12 |- ( ( M e. RR /\ +oo e. RR* ) -> ( M [,) +oo ) C_ RR )
217	71, 215, 216	sylancl 694	. . . . . . . . . . 11 |- ( ph -> ( M [,) +oo ) C_ RR )
218	217	sselda 3603	. . . . . . . . . 10 |- ( ( ph /\ m e. ( M [,) +oo ) ) -> m e. RR )
219	218	adantlr 751	. . . . . . . . 9 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> m e. RR )
220	219	flcld 12599	. . . . . . . 8 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( |_ ` m ) e. ZZ )
221		simplr 792	. . . . . . . . . 10 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> seq 1 ( + , F ) ~~> t )
222	35	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> seq 1 ( + , F ) : NN --> CC )
223		1red 10055	. . . . . . . . . . . . 13 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> 1 e. RR )
224	71	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> M e. RR )
225	70	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> M e. NN )
226	225	nnge1d 11063	. . . . . . . . . . . . 13 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> 1 <_ M )
227		elicopnf 12269	. . . . . . . . . . . . . . . 16 |- ( M e. RR -> ( m e. ( M [,) +oo ) <-> ( m e. RR /\ M <_ m ) ) )
228	71, 227	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> ( m e. ( M [,) +oo ) <-> ( m e. RR /\ M <_ m ) ) )
229	228	simplbda 654	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( M [,) +oo ) ) -> M <_ m )
230	229	adantlr 751	. . . . . . . . . . . . 13 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> M <_ m )
231	223, 224, 219, 226, 230	letrd 10194	. . . . . . . . . . . 12 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> 1 <_ m )
232		flge1nn 12622	. . . . . . . . . . . 12 |- ( ( m e. RR /\ 1 <_ m ) -> ( |_ ` m ) e. NN )
233	219, 231, 232	syl2anc 693	. . . . . . . . . . 11 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( |_ ` m ) e. NN )
234	222, 233	ffvelrnd 6360	. . . . . . . . . 10 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( seq 1 ( + , F ) ` ( |_ ` m ) ) e. CC )
235		nnex 11026	. . . . . . . . . . . 12 |- NN e. _V
236	235	mptex 6486	. . . . . . . . . . 11 |- ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) e. _V
237	236	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) e. _V )
238	222	adantr 481	. . . . . . . . . . 11 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> seq 1 ( + , F ) : NN --> CC )
239		eluznn 11758	. . . . . . . . . . . 12 |- ( ( ( |_ ` m ) e. NN /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> i e. NN )
240	233, 239	sylan 488	. . . . . . . . . . 11 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> i e. NN )
241	238, 240	ffvelrnd 6360	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( seq 1 ( + , F ) ` i ) e. CC )
242		fveq2 6191	. . . . . . . . . . . . 13 |- ( k = i -> ( seq 1 ( + , F ) ` k ) = ( seq 1 ( + , F ) ` i ) )
243	242	oveq2d 6666	. . . . . . . . . . . 12 |- ( k = i -> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) = ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) )
244		eqid 2622	. . . . . . . . . . . 12 |- ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) = ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) )
245		ovex 6678	. . . . . . . . . . . 12 |- ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) e. _V
246	243, 244, 245	fvmpt3i 6287	. . . . . . . . . . 11 |- ( i e. NN -> ( ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ` i ) = ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) )
247	240, 246	syl 17	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ` i ) = ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) )
248	214, 220, 221, 234, 237, 241, 247	climsubc2 14369	. . . . . . . . 9 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ~~> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) )
249	235	mptex 6486	. . . . . . . . . 10 |- ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) e. _V
250	249	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) e. _V )
251		fvex 6201	. . . . . . . . . . . . . 14 |- ( seq 1 ( + , F ) ` ( |_ ` m ) ) e. _V
252	251	fvconst2 6469	. . . . . . . . . . . . 13 |- ( i e. NN -> ( ( NN X. { ( seq 1 ( + , F ) ` ( |_ ` m ) ) } ) ` i ) = ( seq 1 ( + , F ) ` ( |_ ` m ) ) )
253	240, 252	syl 17	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( NN X. { ( seq 1 ( + , F ) ` ( |_ ` m ) ) } ) ` i ) = ( seq 1 ( + , F ) ` ( |_ ` m ) ) )
254	253	oveq1d 6665	. . . . . . . . . . 11 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( ( NN X. { ( seq 1 ( + , F ) ` ( |_ ` m ) ) } ) ` i ) - ( seq 1 ( + , F ) ` i ) ) = ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) )
255	247, 254	eqtr4d 2659	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ` i ) = ( ( ( NN X. { ( seq 1 ( + , F ) ` ( |_ ` m ) ) } ) ` i ) - ( seq 1 ( + , F ) ` i ) ) )
256	234	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( seq 1 ( + , F ) ` ( |_ ` m ) ) e. CC )
257	253, 256	eqeltrd 2701	. . . . . . . . . . 11 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( NN X. { ( seq 1 ( + , F ) ` ( |_ ` m ) ) } ) ` i ) e. CC )
258	257, 241	subcld 10392	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( ( NN X. { ( seq 1 ( + , F ) ` ( |_ ` m ) ) } ) ` i ) - ( seq 1 ( + , F ) ` i ) ) e. CC )
259	255, 258	eqeltrd 2701	. . . . . . . . 9 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ` i ) e. CC )
260	243	fveq2d 6195	. . . . . . . . . . . 12 |- ( k = i -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) ) )
261		eqid 2622	. . . . . . . . . . . 12 |- ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) = ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) )
262		fvex 6201	. . . . . . . . . . . 12 |- ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) e. _V
263	260, 261, 262	fvmpt3i 6287	. . . . . . . . . . 11 |- ( i e. NN -> ( ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) ` i ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) ) )
264	240, 263	syl 17	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) ` i ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) ) )
265	247	fveq2d 6195	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( abs ` ( ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ` i ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) ) )
266	264, 265	eqtr4d 2659	. . . . . . . . 9 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) ` i ) = ( abs ` ( ( k e. NN |-> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ` i ) ) )
267	214, 248, 250, 220, 259, 266	climabs 14334	. . . . . . . 8 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) ~~> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) )
268	44	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( 2 x. R ) e. RR )
269		0red 10041	. . . . . . . . . . . . . . 15 |- ( ( ph /\ m e. ( M [,) +oo ) ) -> 0 e. RR )
270	71	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ m e. ( M [,) +oo ) ) -> M e. RR )
271	75	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ m e. ( M [,) +oo ) ) -> 0 < M )
272	269, 270, 218, 271, 229	ltletrd 10197	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( M [,) +oo ) ) -> 0 < m )
273	218, 272	elrpd 11869	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. ( M [,) +oo ) ) -> m e. RR+ )
274		nfcsb1v 3549	. . . . . . . . . . . . . . . 16 |- F/_ n [_ m / n ]_ A
275	274	nfel1 2779	. . . . . . . . . . . . . . 15 |- F/ n [_ m / n ]_ A e. RR
276		csbeq1a 3542	. . . . . . . . . . . . . . . 16 |- ( n = m -> A = [_ m / n ]_ A )
277	276	eleq1d 2686	. . . . . . . . . . . . . . 15 |- ( n = m -> ( A e. RR <-> [_ m / n ]_ A e. RR ) )
278	275, 277	rspc 3303	. . . . . . . . . . . . . 14 |- ( m e. RR+ -> ( A. n e. RR+ A e. RR -> [_ m / n ]_ A e. RR ) )
279	13, 278	mpan9 486	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. RR+ ) -> [_ m / n ]_ A e. RR )
280	273, 279	syldan 487	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( M [,) +oo ) ) -> [_ m / n ]_ A e. RR )
281	280	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> [_ m / n ]_ A e. RR )
282	268, 281	remulcld 10070	. . . . . . . . . 10 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( ( 2 x. R ) x. [_ m / n ]_ A ) e. RR )
283	282	recnd 10068	. . . . . . . . 9 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( ( 2 x. R ) x. [_ m / n ]_ A ) e. CC )
284		1z 11407	. . . . . . . . 9 |- 1 e. ZZ
285	1	eqimss2i 3660	. . . . . . . . . 10 |- ( ZZ>= ` 1 ) C_ NN
286	285, 235	climconst2 14279	. . . . . . . . 9 |- ( ( ( ( 2 x. R ) x. [_ m / n ]_ A ) e. CC /\ 1 e. ZZ ) -> ( NN X. { ( ( 2 x. R ) x. [_ m / n ]_ A ) } ) ~~> ( ( 2 x. R ) x. [_ m / n ]_ A ) )
287	283, 284, 286	sylancl 694	. . . . . . . 8 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( NN X. { ( ( 2 x. R ) x. [_ m / n ]_ A ) } ) ~~> ( ( 2 x. R ) x. [_ m / n ]_ A ) )
288	256, 241	subcld 10392	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) e. CC )
289	288	abscld 14175	. . . . . . . . 9 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) ) e. RR )
290	264, 289	eqeltrd 2701	. . . . . . . 8 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) ` i ) e. RR )
291		ovex 6678	. . . . . . . . . . 11 |- ( ( 2 x. R ) x. [_ m / n ]_ A ) e. _V
292	291	fvconst2 6469	. . . . . . . . . 10 |- ( i e. NN -> ( ( NN X. { ( ( 2 x. R ) x. [_ m / n ]_ A ) } ) ` i ) = ( ( 2 x. R ) x. [_ m / n ]_ A ) )
293	240, 292	syl 17	. . . . . . . . 9 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( NN X. { ( ( 2 x. R ) x. [_ m / n ]_ A ) } ) ` i ) = ( ( 2 x. R ) x. [_ m / n ]_ A ) )
294	282	adantr 481	. . . . . . . . 9 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( 2 x. R ) x. [_ m / n ]_ A ) e. RR )
295	293, 294	eqeltrd 2701	. . . . . . . 8 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( NN X. { ( ( 2 x. R ) x. [_ m / n ]_ A ) } ) ` i ) e. RR )
296		simplll 798	. . . . . . . . . . 11 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ph )
297	296, 45	syl 17	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> N e. NN )
298	296, 8	syl 17	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> X e. D )
299	296, 120	syl 17	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> X =/= .1. )
300	225	adantr 481	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> M e. NN )
301	296, 12	sylan 488	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) /\ n e. RR+ ) -> A e. RR )
302	296, 126	syl3an1 1359	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
303	296, 66	syl 17	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( n e. RR+ |-> A ) ~~> r 0 )
304	296, 42	syl 17	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> R e. RR )
305	296, 48	syl 17	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> A. u e. ( 0..^ N ) ( abs ` sum_ n e. ( 0..^ u ) ( X ` ( L ` n ) ) ) <_ R )
306	273	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> m e. RR+ )
307	306	adantr 481	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> m e. RR+ )
308	230	adantr 481	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> M <_ m )
309	219	adantr 481	. . . . . . . . . . 11 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> m e. RR )
310		reflcl 12597	. . . . . . . . . . . 12 |- ( m e. RR -> ( |_ ` m ) e. RR )
311		peano2re 10209	. . . . . . . . . . . 12 |- ( ( |_ ` m ) e. RR -> ( ( |_ ` m ) + 1 ) e. RR )
312	309, 310, 311	3syl 18	. . . . . . . . . . 11 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( |_ ` m ) + 1 ) e. RR )
313		flltp1 12601	. . . . . . . . . . . 12 |- ( m e. RR -> m < ( ( |_ ` m ) + 1 ) )
314	309, 313	syl 17	. . . . . . . . . . 11 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> m < ( ( |_ ` m ) + 1 ) )
315	309, 312, 314	ltled 10185	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> m <_ ( ( |_ ` m ) + 1 ) )
316	233	adantr 481	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( |_ ` m ) e. NN )
317		simpr 477	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> i e. ( ZZ>= ` ( |_ ` m ) ) )
318	5, 7, 297, 4, 6, 118, 298, 299, 122, 300, 301, 302, 303, 31, 304, 305, 307, 308, 315, 316, 317	dchrisumlem2 25179	. . . . . . . . 9 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` i ) - ( seq 1 ( + , F ) ` ( |_ ` m ) ) ) ) <_ ( ( 2 x. R ) x. [_ m / n ]_ A ) )
319	256, 241	abssubd 14192	. . . . . . . . . 10 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` i ) ) ) = ( abs ` ( ( seq 1 ( + , F ) ` i ) - ( seq 1 ( + , F ) ` ( |_ ` m ) ) ) ) )
320	264, 319	eqtrd 2656	. . . . . . . . 9 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) ` i ) = ( abs ` ( ( seq 1 ( + , F ) ` i ) - ( seq 1 ( + , F ) ` ( |_ ` m ) ) ) ) )
321	318, 320, 293	3brtr4d 4685	. . . . . . . 8 |- ( ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( |_ ` m ) ) ) -> ( ( k e. NN |-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - ( seq 1 ( + , F ) ` k ) ) ) ) ` i ) <_ ( ( NN X. { ( ( 2 x. R ) x. [_ m / n ]_ A ) } ) ` i ) )
322	214, 220, 267, 287, 290, 295, 321	climle 14370	. . . . . . 7 |- ( ( ( ph /\ seq 1 ( + , F ) ~~> t ) /\ m e. ( M [,) +oo ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) <_ ( ( 2 x. R ) x. [_ m / n ]_ A ) )
323	322	ralrimiva 2966	. . . . . 6 |- ( ( ph /\ seq 1 ( + , F ) ~~> t ) -> A. m e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) <_ ( ( 2 x. R ) x. [_ m / n ]_ A ) )
324		oveq1 6657	. . . . . . . . . 10 |- ( c = ( 2 x. R ) -> ( c x. B ) = ( ( 2 x. R ) x. B ) )
325	324	breq2d 4665	. . . . . . . . 9 |- ( c = ( 2 x. R ) -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) <-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( ( 2 x. R ) x. B ) ) )
326	325	ralbidv 2986	. . . . . . . 8 |- ( c = ( 2 x. R ) -> ( A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) <-> A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( ( 2 x. R ) x. B ) ) )
327		fveq2 6191	. . . . . . . . . . . . 13 |- ( m = x -> ( |_ ` m ) = ( |_ ` x ) )
328	327	fveq2d 6195	. . . . . . . . . . . 12 |- ( m = x -> ( seq 1 ( + , F ) ` ( |_ ` m ) ) = ( seq 1 ( + , F ) ` ( |_ ` x ) ) )
329	328	oveq1d 6665	. . . . . . . . . . 11 |- ( m = x -> ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) = ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) )
330	329	fveq2d 6195	. . . . . . . . . 10 |- ( m = x -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) )
331		vex 3203	. . . . . . . . . . . . 13 |- m e. _V
332	331	a1i 11	. . . . . . . . . . . 12 |- ( m = x -> m e. _V )
333		equequ2 1953	. . . . . . . . . . . . . 14 |- ( m = x -> ( n = m <-> n = x ) )
334	333	biimpa 501	. . . . . . . . . . . . 13 |- ( ( m = x /\ n = m ) -> n = x )
335	334, 122	syl 17	. . . . . . . . . . . 12 |- ( ( m = x /\ n = m ) -> A = B )
336	332, 335	csbied 3560	. . . . . . . . . . 11 |- ( m = x -> [_ m / n ]_ A = B )
337	336	oveq2d 6666	. . . . . . . . . 10 |- ( m = x -> ( ( 2 x. R ) x. [_ m / n ]_ A ) = ( ( 2 x. R ) x. B ) )
338	330, 337	breq12d 4666	. . . . . . . . 9 |- ( m = x -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) <_ ( ( 2 x. R ) x. [_ m / n ]_ A ) <-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( ( 2 x. R ) x. B ) ) )
339	338	cbvralv 3171	. . . . . . . 8 |- ( A. m e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) <_ ( ( 2 x. R ) x. [_ m / n ]_ A ) <-> A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( ( 2 x. R ) x. B ) )
340	326, 339	syl6bbr 278	. . . . . . 7 |- ( c = ( 2 x. R ) -> ( A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) <-> A. m e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) <_ ( ( 2 x. R ) x. [_ m / n ]_ A ) ) )
341	340	rspcev 3309	. . . . . 6 |- ( ( ( 2 x. R ) e. ( 0 [,) +oo ) /\ A. m e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` m ) ) - t ) ) <_ ( ( 2 x. R ) x. [_ m / n ]_ A ) ) -> E. c e. ( 0 [,) +oo ) A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) )
342	213, 323, 341	syl2anc 693	. . . . 5 |- ( ( ph /\ seq 1 ( + , F ) ~~> t ) -> E. c e. ( 0 [,) +oo ) A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) )
343		r19.42v 3092	. . . . 5 |- ( E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) <-> ( seq 1 ( + , F ) ~~> t /\ E. c e. ( 0 [,) +oo ) A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) )
344	210, 342, 343	sylanbrc 698	. . . 4 |- ( ( ph /\ seq 1 ( + , F ) ~~> t ) -> E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) )
345	344	ex 450	. . 3 |- ( ph -> ( seq 1 ( + , F ) ~~> t -> E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) ) )
346	345	eximdv 1846	. 2 |- ( ph -> ( E. t seq 1 ( + , F ) ~~> t -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) ) )
347	209, 346	mpd 15	1 |- ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   [_csb 3533   C_ wss 3574   (/)c0 3915   ifcif 4086   {csn 4177   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   dom cdm 5114   -->wf 5884   ` cfv 5888  (class class class)co 6650   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   +oocpnf 10071   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   / cdiv 10684   NNcn 11020   2c2 11070   ZZcz 11377   ZZ>=cuz 11687   RR+crp 11832   [,)cico 12177  ..^cfzo 12465   |_cfl 12591   seqcseq 12801   abscabs 13974   ~~> cli 14215   ~~> r crli 14216   sum_csu 14416   Basecbs 15857   0gc0g 16100   ZRHomczrh 19848  ℤ/nℤczn 19851  DChrcdchr 24957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-tpos 7352  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-ec 7744  df-qs 7748  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-xnn0 11364  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-ico 12181  df-fz 12327  df-fzo 12466  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-limsup 14202  df-clim 14219  df-rlim 14220  df-sum 14417  df-dvds 14984  df-gcd 15217  df-phi 15471  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-0g 16102  df-imas 16168  df-qus 16169  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-subg 17591  df-nsg 17592  df-eqg 17593  df-ghm 17658  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-ring 18549  df-cring 18550  df-oppr 18623  df-dvdsr 18641  df-unit 18642  df-invr 18672  df-rnghom 18715  df-subrg 18778  df-lmod 18865  df-lss 18933  df-lsp 18972  df-sra 19172  df-rgmod 19173  df-lidl 19174  df-rsp 19175  df-2idl 19232  df-cnfld 19747  df-zring 19819  df-zrh 19852  df-zn 19855  df-dchr 24958

This theorem is referenced by:  dchrisum  25181