Theorem summo 12466

Description: A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)

Hypotheses

Ref	Expression
summo.1	|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
summo.2	|- ( ( ph /\ k e. A ) -> B e. CC )
summo.3	|- G = ( n e. NN |-> [_ ( f ` n ) / k ]_ B )

Assertion

Ref	Expression
summo	|- ( ph -> E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) )

Distinct variable groups:   f, k, m, n, x, A   f, F, k, m, n, x   k, G, m, n, x   ph, k, m, n   B, f, m, n, x   ph, x, f

Allowed substitution hints:   B( k)   G( f)

Proof of Theorem summo

Dummy variables g j y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5687	. . . . . . . . . 10 |- ( m = n -> ( ZZ>= ` m ) = ( ZZ>= ` n ) )
2	1	sseq2d 3336	. . . . . . . . 9 |- ( m = n -> ( A C_ ( ZZ>= ` m ) <-> A C_ ( ZZ>= ` n ) ) )
3		seqeq1 11281	. . . . . . . . . 10 |- ( m = n -> seq m ( + , F ) = seq n ( + , F ) )
4	3	breq1d 4182	. . . . . . . . 9 |- ( m = n -> ( seq m ( + , F ) ~~> y <-> seq n ( + , F ) ~~> y ) )
5	2, 4	anbi12d 692	. . . . . . . 8 |- ( m = n -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) <-> ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) )
6	5	cbvrexv 2893	. . . . . . 7 |- ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) <-> E. n e. ZZ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) )
7		reeanv 2835	. . . . . . . . 9 |- ( E. m e. ZZ E. n e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) <-> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ E. n e. ZZ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) )
8		simprlr 740	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> seq m ( + , F ) ~~> x )
9		summo.1	. . . . . . . . . . . . . 14 |- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
10		simpll 731	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> ph )
11		summo.2	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. A ) -> B e. CC )
12	10, 11	sylan 458	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) /\ k e. A ) -> B e. CC )
13		simplrl 737	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> m e. ZZ )
14		simplrr 738	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> n e. ZZ )
15		simprll 739	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> A C_ ( ZZ>= ` m ) )
16		simprrl 741	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> A C_ ( ZZ>= ` n ) )
17	9, 12, 13, 14, 15, 16	sumrb 12462	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> ( seq m ( + , F ) ~~> x <-> seq n ( + , F ) ~~> x ) )
18	8, 17	mpbid 202	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> seq n ( + , F ) ~~> x )
19		simprrr 742	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> seq n ( + , F ) ~~> y )
20		climuni 12301	. . . . . . . . . . . 12 |- ( ( seq n ( + , F ) ~~> x /\ seq n ( + , F ) ~~> y ) -> x = y )
21	18, 19, 20	syl2anc 643	. . . . . . . . . . 11 |- ( ( ( ph /\ ( m e. ZZ /\ n e. ZZ ) ) /\ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) ) -> x = y )
22	21	exp31 588	. . . . . . . . . 10 |- ( ph -> ( ( m e. ZZ /\ n e. ZZ ) -> ( ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) -> x = y ) ) )
23	22	rexlimdvv 2796	. . . . . . . . 9 |- ( ph -> ( E. m e. ZZ E. n e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) -> x = y ) )
24	7, 23	syl5bir 210	. . . . . . . 8 |- ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) /\ E. n e. ZZ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) ) -> x = y ) )
25	24	expdimp 427	. . . . . . 7 |- ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) ) -> ( E. n e. ZZ ( A C_ ( ZZ>= ` n ) /\ seq n ( + , F ) ~~> y ) -> x = y ) )
26	6, 25	syl5bi 209	. . . . . 6 |- ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) ) -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) -> x = y ) )
27		summo.3	. . . . . . 7 |- G = ( n e. NN |-> [_ ( f ` n ) / k ]_ B )
28	9, 11, 27	summolem2 12465	. . . . . 6 |- ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) -> x = y ) )
29	26, 28	jaod 370	. . . . 5 |- ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) ) -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) -> x = y ) )
30	9, 11, 27	summolem2 12465	. . . . . . . 8 |- ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) -> y = x ) )
31		equcom 1688	. . . . . . . 8 |- ( y = x <-> x = y )
32	30, 31	syl6ib 218	. . . . . . 7 |- ( ( ph /\ E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) -> x = y ) )
33	32	impancom 428	. . . . . 6 |- ( ( ph /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) -> x = y ) )
34		oveq2 6048	. . . . . . . . . . . 12 |- ( m = n -> ( 1 ... m ) = ( 1 ... n ) )
35		f1oeq2 5625	. . . . . . . . . . . 12 |- ( ( 1 ... m ) = ( 1 ... n ) -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... n ) -1-1-onto-> A ) )
36	34, 35	syl 16	. . . . . . . . . . 11 |- ( m = n -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... n ) -1-1-onto-> A ) )
37		fveq2 5687	. . . . . . . . . . . 12 |- ( m = n -> ( seq 1 ( + , G ) ` m ) = ( seq 1 ( + , G ) ` n ) )
38	37	eqeq2d 2415	. . . . . . . . . . 11 |- ( m = n -> ( y = ( seq 1 ( + , G ) ` m ) <-> y = ( seq 1 ( + , G ) ` n ) ) )
39	36, 38	anbi12d 692	. . . . . . . . . 10 |- ( m = n -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) <-> ( f : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` n ) ) ) )
40	39	exbidv 1633	. . . . . . . . 9 |- ( m = n -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) <-> E. f ( f : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` n ) ) ) )
41		f1oeq1 5624	. . . . . . . . . . 11 |- ( f = g -> ( f : ( 1 ... n ) -1-1-onto-> A <-> g : ( 1 ... n ) -1-1-onto-> A ) )
42		fveq1 5686	. . . . . . . . . . . . . . . . 17 |- ( f = g -> ( f ` n ) = ( g ` n ) )
43	42	csbeq1d 3217	. . . . . . . . . . . . . . . 16 |- ( f = g -> [_ ( f ` n ) / k ]_ B = [_ ( g ` n ) / k ]_ B )
44	43	mpteq2dv 4256	. . . . . . . . . . . . . . 15 |- ( f = g -> ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) )
45	27, 44	syl5eq 2448	. . . . . . . . . . . . . 14 |- ( f = g -> G = ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) )
46	45	seqeq3d 11286	. . . . . . . . . . . . 13 |- ( f = g -> seq 1 ( + , G ) = seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) )
47	46	fveq1d 5689	. . . . . . . . . . . 12 |- ( f = g -> ( seq 1 ( + , G ) ` n ) = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) )
48	47	eqeq2d 2415	. . . . . . . . . . 11 |- ( f = g -> ( y = ( seq 1 ( + , G ) ` n ) <-> y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) )
49	41, 48	anbi12d 692	. . . . . . . . . 10 |- ( f = g -> ( ( f : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` n ) ) <-> ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) )
50	49	cbvexv 2053	. . . . . . . . 9 |- ( E. f ( f : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` n ) ) <-> E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) )
51	40, 50	syl6bb 253	. . . . . . . 8 |- ( m = n -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) <-> E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) )
52	51	cbvrexv 2893	. . . . . . 7 |- ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) <-> E. n e. NN E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) )
53		reeanv 2835	. . . . . . . . 9 |- ( E. m e. NN E. n e. NN ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) <-> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ E. n e. NN E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) )
54		eeanv 1933	. . . . . . . . . . 11 |- ( E. f E. g ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) <-> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) )
55		an4 798	. . . . . . . . . . . . 13 |- ( ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) <-> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) /\ ( x = ( seq 1 ( + , G ) ` m ) /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) )
56		simpll 731	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( m e. NN /\ n e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) ) -> ph )
57	56, 11	sylan 458	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( m e. NN /\ n e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) ) /\ k e. A ) -> B e. CC )
58		fveq2 5687	. . . . . . . . . . . . . . . . . . 19 |- ( n = j -> ( f ` n ) = ( f ` j ) )
59	58	csbeq1d 3217	. . . . . . . . . . . . . . . . . 18 |- ( n = j -> [_ ( f ` n ) / k ]_ B = [_ ( f ` j ) / k ]_ B )
60	59	cbvmptv 4260	. . . . . . . . . . . . . . . . 17 |- ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( j e. NN |-> [_ ( f ` j ) / k ]_ B )
61	27, 60	eqtri 2424	. . . . . . . . . . . . . . . 16 |- G = ( j e. NN |-> [_ ( f ` j ) / k ]_ B )
62		fveq2 5687	. . . . . . . . . . . . . . . . . 18 |- ( n = j -> ( g ` n ) = ( g ` j ) )
63	62	csbeq1d 3217	. . . . . . . . . . . . . . . . 17 |- ( n = j -> [_ ( g ` n ) / k ]_ B = [_ ( g ` j ) / k ]_ B )
64	63	cbvmptv 4260	. . . . . . . . . . . . . . . 16 |- ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) = ( j e. NN |-> [_ ( g ` j ) / k ]_ B )
65		simplr 732	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( m e. NN /\ n e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) ) -> ( m e. NN /\ n e. NN ) )
66		simprl 733	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( m e. NN /\ n e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) ) -> f : ( 1 ... m ) -1-1-onto-> A )
67		simprr 734	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( m e. NN /\ n e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) ) -> g : ( 1 ... n ) -1-1-onto-> A )
68	9, 57, 61, 64, 65, 66, 67	summolem3 12463	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( m e. NN /\ n e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) ) -> ( seq 1 ( + , G ) ` m ) = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) )
69		eqeq12 2416	. . . . . . . . . . . . . . 15 |- ( ( x = ( seq 1 ( + , G ) ` m ) /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) -> ( x = y <-> ( seq 1 ( + , G ) ` m ) = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) )
70	68, 69	syl5ibrcom 214	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( m e. NN /\ n e. NN ) ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) ) -> ( ( x = ( seq 1 ( + , G ) ` m ) /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) -> x = y ) )
71	70	expimpd 587	. . . . . . . . . . . . 13 |- ( ( ph /\ ( m e. NN /\ n e. NN ) ) -> ( ( ( f : ( 1 ... m ) -1-1-onto-> A /\ g : ( 1 ... n ) -1-1-onto-> A ) /\ ( x = ( seq 1 ( + , G ) ` m ) /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) -> x = y ) )
72	55, 71	syl5bi 209	. . . . . . . . . . . 12 |- ( ( ph /\ ( m e. NN /\ n e. NN ) ) -> ( ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) -> x = y ) )
73	72	exlimdvv 1644	. . . . . . . . . . 11 |- ( ( ph /\ ( m e. NN /\ n e. NN ) ) -> ( E. f E. g ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) -> x = y ) )
74	54, 73	syl5bir 210	. . . . . . . . . 10 |- ( ( ph /\ ( m e. NN /\ n e. NN ) ) -> ( ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) -> x = y ) )
75	74	rexlimdvva 2797	. . . . . . . . 9 |- ( ph -> ( E. m e. NN E. n e. NN ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) -> x = y ) )
76	53, 75	syl5bir 210	. . . . . . . 8 |- ( ph -> ( ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) /\ E. n e. NN E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) ) -> x = y ) )
77	76	expdimp 427	. . . . . . 7 |- ( ( ph /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) -> ( E. n e. NN E. g ( g : ( 1 ... n ) -1-1-onto-> A /\ y = ( seq 1 ( + , ( n e. NN |-> [_ ( g ` n ) / k ]_ B ) ) ` n ) ) -> x = y ) )
78	52, 77	syl5bi 209	. . . . . 6 |- ( ( ph /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) -> x = y ) )
79	33, 78	jaod 370	. . . . 5 |- ( ( ph /\ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) -> x = y ) )
80	29, 79	jaodan 761	. . . 4 |- ( ( ph /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) ) -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) -> x = y ) )
81	80	expimpd 587	. . 3 |- ( ph -> ( ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) ) -> x = y ) )
82	81	alrimivv 1639	. 2 |- ( ph -> A. x A. y ( ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) ) -> x = y ) )
83		breq2 4176	. . . . . 6 |- ( x = y -> ( seq m ( + , F ) ~~> x <-> seq m ( + , F ) ~~> y ) )
84	83	anbi2d 685	. . . . 5 |- ( x = y -> ( ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) <-> ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) ) )
85	84	rexbidv 2687	. . . 4 |- ( x = y -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) <-> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) ) )
86		eqeq1 2410	. . . . . . 7 |- ( x = y -> ( x = ( seq 1 ( + , G ) ` m ) <-> y = ( seq 1 ( + , G ) ` m ) ) )
87	86	anbi2d 685	. . . . . 6 |- ( x = y -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) )
88	87	exbidv 1633	. . . . 5 |- ( x = y -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) )
89	88	rexbidv 2687	. . . 4 |- ( x = y -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) <-> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) )
90	85, 89	orbi12d 691	. . 3 |- ( x = y -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) <-> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) ) )
91	90	mo4 2287	. 2 |- ( E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) <-> A. x A. y ( ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> y ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ y = ( seq 1 ( + , G ) ` m ) ) ) ) -> x = y ) )
92	82, 91	sylibr 204	1 |- ( ph -> E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , F ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , G ) ` m ) ) ) )

Syntax hints:   -> wi 4   <-> wb 177   \/ wo 358   /\ wa 359   A.wal 1546   E.wex 1547   = wceq 1649   e. wcel 1721   E*wmo 2255   E.wrex 2667   [_csb 3211   C_ wss 3280   ifcif 3699   class class class wbr 4172   e. cmpt 4226   -1-1-onto->wf1o 5412   ` cfv 5413  (class class class)co 6040   CCcc 8944   0cc0 8946   1c1 8947   + caddc 8949   NNcn 9956   ZZcz 10238   ZZ>=cuz 10444   ...cfz 10999   seq cseq 11278   ~~> cli 12233

This theorem is referenced by:  fsum  12469

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

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-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-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-fz 11000  df-fzo 11091  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-clim 12237