Theorem fprodseq 11524

Description: The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017.) (Revised by Jim Kingdon, 15-Jul-2024.)

Hypotheses

Ref	Expression
fprod.1	|- ( k = ( F ` n ) -> B = C )
fprod.2	|- ( ph -> M e. NN )
fprod.3	|- ( ph -> F : ( 1 ... M ) -1-1-onto-> A )
fprod.4	|- ( ( ph /\ k e. A ) -> B e. CC )
fprod.5	|- ( ( ph /\ n e. ( 1 ... M ) ) -> ( G ` n ) = C )

Assertion

Ref	Expression
fprodseq	|- ( ph -> prod_ k e. A B = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) )

Distinct variable groups:   A, k, n   B, n   C, k   k, F, n   k, G, n   k, M, n   ph, k, n

Allowed substitution hints:   B( k)   C( n)

Proof of Theorem fprodseq

Dummy variables f i j m x p q u y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-proddc 11492	. 2 |- prod_ k e. A B = ( iota x ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) )
2		nnuz 9501	. . . . 5 |- NN = ( ZZ>= ` 1 )
3		1zzd 9218	. . . . 5 |- ( ph -> 1 e. ZZ )
4		eqid 2165	. . . . . . 7 |- ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) = ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) )
5		breq1 3985	. . . . . . . 8 |- ( n = p -> ( n <_ M <-> p <_ M ) )
6		fveq2 5486	. . . . . . . 8 |- ( n = p -> ( G ` n ) = ( G ` p ) )
7	5, 6	ifbieq1d 3542	. . . . . . 7 |- ( n = p -> if ( n <_ M , ( G ` n ) , 1 ) = if ( p <_ M , ( G ` p ) , 1 ) )
8		simpr 109	. . . . . . 7 |- ( ( ph /\ p e. NN ) -> p e. NN )
9		simpll 519	. . . . . . . . 9 |- ( ( ( ph /\ p e. NN ) /\ p <_ M ) -> ph )
10	8	anim1i 338	. . . . . . . . . 10 |- ( ( ( ph /\ p e. NN ) /\ p <_ M ) -> ( p e. NN /\ p <_ M ) )
11		fprod.2	. . . . . . . . . . . . 13 |- ( ph -> M e. NN )
12	11	nnzd 9312	. . . . . . . . . . . 12 |- ( ph -> M e. ZZ )
13		fznn 10024	. . . . . . . . . . . 12 |- ( M e. ZZ -> ( p e. ( 1 ... M ) <-> ( p e. NN /\ p <_ M ) ) )
14	12, 13	syl 14	. . . . . . . . . . 11 |- ( ph -> ( p e. ( 1 ... M ) <-> ( p e. NN /\ p <_ M ) ) )
15	14	ad2antrr 480	. . . . . . . . . 10 |- ( ( ( ph /\ p e. NN ) /\ p <_ M ) -> ( p e. ( 1 ... M ) <-> ( p e. NN /\ p <_ M ) ) )
16	10, 15	mpbird 166	. . . . . . . . 9 |- ( ( ( ph /\ p e. NN ) /\ p <_ M ) -> p e. ( 1 ... M ) )
17	6	eleq1d 2235	. . . . . . . . . 10 |- ( n = p -> ( ( G ` n ) e. CC <-> ( G ` p ) e. CC ) )
18		fprod.1	. . . . . . . . . . . 12 |- ( k = ( F ` n ) -> B = C )
19		fprod.3	. . . . . . . . . . . 12 |- ( ph -> F : ( 1 ... M ) -1-1-onto-> A )
20		fprod.4	. . . . . . . . . . . 12 |- ( ( ph /\ k e. A ) -> B e. CC )
21		fprod.5	. . . . . . . . . . . 12 |- ( ( ph /\ n e. ( 1 ... M ) ) -> ( G ` n ) = C )
22	18, 11, 19, 20, 21	fsumgcl 11327	. . . . . . . . . . 11 |- ( ph -> A. n e. ( 1 ... M ) ( G ` n ) e. CC )
23	22	adantr 274	. . . . . . . . . 10 |- ( ( ph /\ p e. ( 1 ... M ) ) -> A. n e. ( 1 ... M ) ( G ` n ) e. CC )
24		simpr 109	. . . . . . . . . 10 |- ( ( ph /\ p e. ( 1 ... M ) ) -> p e. ( 1 ... M ) )
25	17, 23, 24	rspcdva 2835	. . . . . . . . 9 |- ( ( ph /\ p e. ( 1 ... M ) ) -> ( G ` p ) e. CC )
26	9, 16, 25	syl2anc 409	. . . . . . . 8 |- ( ( ( ph /\ p e. NN ) /\ p <_ M ) -> ( G ` p ) e. CC )
27		1cnd 7915	. . . . . . . 8 |- ( ( ( ph /\ p e. NN ) /\ -. p <_ M ) -> 1 e. CC )
28	8	nnzd 9312	. . . . . . . . 9 |- ( ( ph /\ p e. NN ) -> p e. ZZ )
29	12	adantr 274	. . . . . . . . 9 |- ( ( ph /\ p e. NN ) -> M e. ZZ )
30		zdcle 9267	. . . . . . . . 9 |- ( ( p e. ZZ /\ M e. ZZ ) -> DECID p <_ M )
31	28, 29, 30	syl2anc 409	. . . . . . . 8 |- ( ( ph /\ p e. NN ) -> DECID p <_ M )
32	26, 27, 31	ifcldadc 3549	. . . . . . 7 |- ( ( ph /\ p e. NN ) -> if ( p <_ M , ( G ` p ) , 1 ) e. CC )
33	4, 7, 8, 32	fvmptd3 5579	. . . . . 6 |- ( ( ph /\ p e. NN ) -> ( ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ` p ) = if ( p <_ M , ( G ` p ) , 1 ) )
34	33, 32	eqeltrd 2243	. . . . 5 |- ( ( ph /\ p e. NN ) -> ( ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ` p ) e. CC )
35	2, 3, 34	prodf 11479	. . . 4 |- ( ph -> seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) : NN --> CC )
36	35, 11	ffvelrnd 5621	. . 3 |- ( ph -> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) e. CC )
37		eleq1w 2227	. . . . . . . . . . . . 13 |- ( i = j -> ( i e. A <-> j e. A ) )
38	37	dcbid 828	. . . . . . . . . . . 12 |- ( i = j -> (DECID i e. A <-> DECID j e. A ) )
39	38	cbvralv 2692	. . . . . . . . . . 11 |- ( A. i e. ( ZZ>= ` m )DECID i e. A <-> A. j e. ( ZZ>= ` m )DECID j e. A )
40	39	anbi2i 453	. . . . . . . . . 10 |- ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) <-> ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) )
41	40	anbi1i 454	. . . . . . . . 9 |- ( ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) <-> ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) )
42	41	rexbii 2473	. . . . . . . 8 |- ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) <-> E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) )
43		nnnn0 9121	. . . . . . . . . . . . . . . . . . . . 21 |- ( m e. NN -> m e. NN0 )
44		hashfz1 10696	. . . . . . . . . . . . . . . . . . . . 21 |- ( m e. NN0 -> (♯ ` ( 1 ... m ) ) = m )
45	43, 44	syl 14	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. NN -> (♯ ` ( 1 ... m ) ) = m )
46	45	adantr 274	. . . . . . . . . . . . . . . . . . 19 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> (♯ ` ( 1 ... m ) ) = m )
47		1zzd 9218	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> 1 e. ZZ )
48		nnz 9210	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m e. NN -> m e. ZZ )
49	48	adantr 274	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> m e. ZZ )
50	47, 49	fzfigd 10366	. . . . . . . . . . . . . . . . . . . 20 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( 1 ... m ) e. Fin )
51		simpr 109	. . . . . . . . . . . . . . . . . . . 20 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> f : ( 1 ... m ) -1-1-onto-> A )
52	50, 51	fihasheqf1od 10703	. . . . . . . . . . . . . . . . . . 19 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> (♯ ` ( 1 ... m ) ) = (♯ ` A ) )
53	46, 52	eqtr3d 2200	. . . . . . . . . . . . . . . . . 18 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> m = (♯ ` A ) )
54	53	breq2d 3994	. . . . . . . . . . . . . . . . 17 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( n <_ m <-> n <_ (♯ ` A ) ) )
55	54	ifbid 3541	. . . . . . . . . . . . . . . 16 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) = if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) )
56	55	mpteq2dv 4073	. . . . . . . . . . . . . . 15 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) = ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) )
57	56	seqeq3d 10388	. . . . . . . . . . . . . 14 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) = seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) )
58	57	fveq1d 5488	. . . . . . . . . . . . 13 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) )
59	58	eqeq2d 2177	. . . . . . . . . . . 12 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) <-> x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) )
60	59	pm5.32da 448	. . . . . . . . . . 11 |- ( m e. NN -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) )
61	60	exbidv 1813	. . . . . . . . . 10 |- ( m e. NN -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) )
62	61	rexbiia 2481	. . . . . . . . 9 |- ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) <-> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) )
63	62	bicomi 131	. . . . . . . 8 |- ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) <-> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) )
64	42, 63	orbi12i 754	. . . . . . 7 |- ( ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) <-> ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) )
65		f1of 5432	. . . . . . . . . . . . 13 |- ( F : ( 1 ... M ) -1-1-onto-> A -> F : ( 1 ... M ) --> A )
66	19, 65	syl 14	. . . . . . . . . . . 12 |- ( ph -> F : ( 1 ... M ) --> A )
67	3, 12	fzfigd 10366	. . . . . . . . . . . 12 |- ( ph -> ( 1 ... M ) e. Fin )
68		fex 5714	. . . . . . . . . . . 12 |- ( ( F : ( 1 ... M ) --> A /\ ( 1 ... M ) e. Fin ) -> F e. _V )
69	66, 67, 68	syl2anc 409	. . . . . . . . . . 11 |- ( ph -> F e. _V )
70	11, 2	eleqtrdi 2259	. . . . . . . . . . . . 13 |- ( ph -> M e. ( ZZ>= ` 1 ) )
71		fveq2 5486	. . . . . . . . . . . . . . . . 17 |- ( n = u -> ( F ` n ) = ( F ` u ) )
72	71	csbeq1d 3052	. . . . . . . . . . . . . . . 16 |- ( n = u -> [_ ( F ` n ) / k ]_ B = [_ ( F ` u ) / k ]_ B )
73		fveq2 5486	. . . . . . . . . . . . . . . 16 |- ( n = u -> ( G ` n ) = ( G ` u ) )
74	72, 73	eqeq12d 2180	. . . . . . . . . . . . . . 15 |- ( n = u -> ( [_ ( F ` n ) / k ]_ B = ( G ` n ) <-> [_ ( F ` u ) / k ]_ B = ( G ` u ) ) )
75	66	ffvelrnda 5620	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n e. ( 1 ... M ) ) -> ( F ` n ) e. A )
76	18	adantl 275	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. ( 1 ... M ) ) /\ k = ( F ` n ) ) -> B = C )
77	75, 76	csbied 3091	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. ( 1 ... M ) ) -> [_ ( F ` n ) / k ]_ B = C )
78	77, 21	eqtr4d 2201	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. ( 1 ... M ) ) -> [_ ( F ` n ) / k ]_ B = ( G ` n ) )
79	78	ralrimiva 2539	. . . . . . . . . . . . . . . 16 |- ( ph -> A. n e. ( 1 ... M ) [_ ( F ` n ) / k ]_ B = ( G ` n ) )
80	79	adantr 274	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( 1 ... M ) ) -> A. n e. ( 1 ... M ) [_ ( F ` n ) / k ]_ B = ( G ` n ) )
81		simpr 109	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u e. ( 1 ... M ) )
82	74, 80, 81	rspcdva 2835	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( 1 ... M ) ) -> [_ ( F ` u ) / k ]_ B = ( G ` u ) )
83		eqid 2165	. . . . . . . . . . . . . . . 16 |- ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) = ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) )
84		breq1 3985	. . . . . . . . . . . . . . . . 17 |- ( n = u -> ( n <_ (♯ ` A ) <-> u <_ (♯ ` A ) ) )
85	84, 72	ifbieq1d 3542	. . . . . . . . . . . . . . . 16 |- ( n = u -> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) = if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) )
86		elfznn 9989	. . . . . . . . . . . . . . . . 17 |- ( u e. ( 1 ... M ) -> u e. NN )
87	86	adantl 275	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u e. NN )
88		elfzle2 9963	. . . . . . . . . . . . . . . . . . . . 21 |- ( u e. ( 1 ... M ) -> u <_ M )
89	88	adantl 275	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u <_ M )
90	11	nnnn0d 9167	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> M e. NN0 )
91		hashfz1 10696	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( M e. NN0 -> (♯ ` ( 1 ... M ) ) = M )
92	90, 91	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> (♯ ` ( 1 ... M ) ) = M )
93	67, 19	fihasheqf1od 10703	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> (♯ ` ( 1 ... M ) ) = (♯ ` A ) )
94	92, 93	eqtr3d 2200	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> M = (♯ ` A ) )
95	94	adantr 274	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( 1 ... M ) ) -> M = (♯ ` A ) )
96	89, 95	breqtrd 4008	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u <_ (♯ ` A ) )
97	96	iftrued 3527	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) = [_ ( F ` u ) / k ]_ B )
98	97, 82	eqtrd 2198	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) = ( G ` u ) )
99	73	eleq1d 2235	. . . . . . . . . . . . . . . . . 18 |- ( n = u -> ( ( G ` n ) e. CC <-> ( G ` u ) e. CC ) )
100	22	adantr 274	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( 1 ... M ) ) -> A. n e. ( 1 ... M ) ( G ` n ) e. CC )
101	99, 100, 81	rspcdva 2835	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( G ` u ) e. CC )
102	98, 101	eqeltrd 2243	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) e. CC )
103	83, 85, 87, 102	fvmptd3 5579	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ` u ) = if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) )
104	103, 97	eqtrd 2198	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ` u ) = [_ ( F ` u ) / k ]_ B )
105		breq1 3985	. . . . . . . . . . . . . . . . 17 |- ( n = u -> ( n <_ M <-> u <_ M ) )
106	105, 73	ifbieq1d 3542	. . . . . . . . . . . . . . . 16 |- ( n = u -> if ( n <_ M , ( G ` n ) , 1 ) = if ( u <_ M , ( G ` u ) , 1 ) )
107	89	iftrued 3527	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ M , ( G ` u ) , 1 ) = ( G ` u ) )
108	107, 101	eqeltrd 2243	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ M , ( G ` u ) , 1 ) e. CC )
109	4, 106, 87, 108	fvmptd3 5579	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ` u ) = if ( u <_ M , ( G ` u ) , 1 ) )
110	109, 107	eqtrd 2198	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ` u ) = ( G ` u ) )
111	82, 104, 110	3eqtr4rd 2209	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ` u ) = ( ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ` u ) )
112		elnnuz 9502	. . . . . . . . . . . . . 14 |- ( p e. NN <-> p e. ( ZZ>= ` 1 ) )
113	112, 34	sylan2br 286	. . . . . . . . . . . . 13 |- ( ( ph /\ p e. ( ZZ>= ` 1 ) ) -> ( ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ` p ) e. CC )
114		breq1 3985	. . . . . . . . . . . . . . . . 17 |- ( n = p -> ( n <_ (♯ ` A ) <-> p <_ (♯ ` A ) ) )
115		fveq2 5486	. . . . . . . . . . . . . . . . . 18 |- ( n = p -> ( F ` n ) = ( F ` p ) )
116	115	csbeq1d 3052	. . . . . . . . . . . . . . . . 17 |- ( n = p -> [_ ( F ` n ) / k ]_ B = [_ ( F ` p ) / k ]_ B )
117	114, 116	ifbieq1d 3542	. . . . . . . . . . . . . . . 16 |- ( n = p -> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) = if ( p <_ (♯ ` A ) , [_ ( F ` p ) / k ]_ B , 1 ) )
118		simpll 519	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ p e. NN ) /\ p <_ (♯ ` A ) ) -> ph )
119		simpr 109	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ p e. NN ) /\ p <_ (♯ ` A ) ) -> p <_ (♯ ` A ) )
120	94	breq2d 3994	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( p <_ M <-> p <_ (♯ ` A ) ) )
121	120	ad2antrr 480	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ p e. NN ) /\ p <_ (♯ ` A ) ) -> ( p <_ M <-> p <_ (♯ ` A ) ) )
122	119, 121	mpbird 166	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ p e. NN ) /\ p <_ (♯ ` A ) ) -> p <_ M )
123	122, 16	syldan 280	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ p e. NN ) /\ p <_ (♯ ` A ) ) -> p e. ( 1 ... M ) )
124	66	ffvelrnda 5620	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( 1 ... M ) ) -> ( F ` p ) e. A )
125	20	ralrimiva 2539	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> A. k e. A B e. CC )
126	125	adantr 274	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( 1 ... M ) ) -> A. k e. A B e. CC )
127		nfcsb1v 3078	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ k [_ ( F ` p ) / k ]_ B
128	127	nfel1 2319	. . . . . . . . . . . . . . . . . . . 20 |- F/ k [_ ( F ` p ) / k ]_ B e. CC
129		csbeq1a 3054	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = ( F ` p ) -> B = [_ ( F ` p ) / k ]_ B )
130	129	eleq1d 2235	. . . . . . . . . . . . . . . . . . . 20 |- ( k = ( F ` p ) -> ( B e. CC <-> [_ ( F ` p ) / k ]_ B e. CC ) )
131	128, 130	rspc 2824	. . . . . . . . . . . . . . . . . . 19 |- ( ( F ` p ) e. A -> ( A. k e. A B e. CC -> [_ ( F ` p ) / k ]_ B e. CC ) )
132	124, 126, 131	sylc 62	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ p e. ( 1 ... M ) ) -> [_ ( F ` p ) / k ]_ B e. CC )
133	118, 123, 132	syl2anc 409	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ p e. NN ) /\ p <_ (♯ ` A ) ) -> [_ ( F ` p ) / k ]_ B e. CC )
134		1cnd 7915	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ p e. NN ) /\ -. p <_ (♯ ` A ) ) -> 1 e. CC )
135	94, 12	eqeltrrd 2244	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> (♯ ` A ) e. ZZ )
136	135	adantr 274	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ p e. NN ) -> (♯ ` A ) e. ZZ )
137		zdcle 9267	. . . . . . . . . . . . . . . . . 18 |- ( ( p e. ZZ /\ (♯ ` A ) e. ZZ ) -> DECID p <_ (♯ ` A ) )
138	28, 136, 137	syl2anc 409	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. NN ) -> DECID p <_ (♯ ` A ) )
139	133, 134, 138	ifcldadc 3549	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ p e. NN ) -> if ( p <_ (♯ ` A ) , [_ ( F ` p ) / k ]_ B , 1 ) e. CC )
140	83, 117, 8, 139	fvmptd3 5579	. . . . . . . . . . . . . . 15 |- ( ( ph /\ p e. NN ) -> ( ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ` p ) = if ( p <_ (♯ ` A ) , [_ ( F ` p ) / k ]_ B , 1 ) )
141	140, 139	eqeltrd 2243	. . . . . . . . . . . . . 14 |- ( ( ph /\ p e. NN ) -> ( ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ` p ) e. CC )
142	112, 141	sylan2br 286	. . . . . . . . . . . . 13 |- ( ( ph /\ p e. ( ZZ>= ` 1 ) ) -> ( ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ` p ) e. CC )
143		mulcl 7880	. . . . . . . . . . . . . 14 |- ( ( p e. CC /\ q e. CC ) -> ( p x. q ) e. CC )
144	143	adantl 275	. . . . . . . . . . . . 13 |- ( ( ph /\ ( p e. CC /\ q e. CC ) ) -> ( p x. q ) e. CC )
145	70, 111, 113, 142, 144	seq3fveq 10406	. . . . . . . . . . . 12 |- ( ph -> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ) ` M ) )
146	19, 145	jca 304	. . . . . . . . . . 11 |- ( ph -> ( F : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ) ` M ) ) )
147		f1oeq1 5421	. . . . . . . . . . . 12 |- ( f = F -> ( f : ( 1 ... M ) -1-1-onto-> A <-> F : ( 1 ... M ) -1-1-onto-> A ) )
148		fveq1 5485	. . . . . . . . . . . . . . . . . 18 |- ( f = F -> ( f ` n ) = ( F ` n ) )
149	148	csbeq1d 3052	. . . . . . . . . . . . . . . . 17 |- ( f = F -> [_ ( f ` n ) / k ]_ B = [_ ( F ` n ) / k ]_ B )
150	149	ifeq1d 3537	. . . . . . . . . . . . . . . 16 |- ( f = F -> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) = if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) )
151	150	mpteq2dv 4073	. . . . . . . . . . . . . . 15 |- ( f = F -> ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) = ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) )
152	151	seqeq3d 10388	. . . . . . . . . . . . . 14 |- ( f = F -> seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) = seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ) )
153	152	fveq1d 5488	. . . . . . . . . . . . 13 |- ( f = F -> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ) ` M ) )
154	153	eqeq2d 2177	. . . . . . . . . . . 12 |- ( f = F -> ( ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` M ) <-> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ) ` M ) ) )
155	147, 154	anbi12d 465	. . . . . . . . . . 11 |- ( f = F -> ( ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` M ) ) <-> ( F : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ) ` M ) ) ) )
156	69, 146, 155	spcedv 2815	. . . . . . . . . 10 |- ( ph -> E. f ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` M ) ) )
157		oveq2 5850	. . . . . . . . . . . . . 14 |- ( m = M -> ( 1 ... m ) = ( 1 ... M ) )
158	157	f1oeq2d 5428	. . . . . . . . . . . . 13 |- ( m = M -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... M ) -1-1-onto-> A ) )
159		fveq2 5486	. . . . . . . . . . . . . 14 |- ( m = M -> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` M ) )
160	159	eqeq2d 2177	. . . . . . . . . . . . 13 |- ( m = M -> ( ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) <-> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` M ) ) )
161	158, 160	anbi12d 465	. . . . . . . . . . . 12 |- ( m = M -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) <-> ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` M ) ) ) )
162	161	exbidv 1813	. . . . . . . . . . 11 |- ( m = M -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) <-> E. f ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` M ) ) ) )
163	162	rspcev 2830	. . . . . . . . . 10 |- ( ( M e. NN /\ E. f ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` M ) ) ) -> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) )
164	11, 156, 163	syl2anc 409	. . . . . . . . 9 |- ( ph -> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) )
165	164	olcd 724	. . . . . . . 8 |- ( ph -> ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) )
166		nfcv 2308	. . . . . . . . . . . . . 14 |- F/_ j if ( k e. A , B , 1 )
167		nfv 1516	. . . . . . . . . . . . . . 15 |- F/ k j e. A
168		nfcsb1v 3078	. . . . . . . . . . . . . . 15 |- F/_ k [_ j / k ]_ B
169		nfcv 2308	. . . . . . . . . . . . . . 15 |- F/_ k 1
170	167, 168, 169	nfif 3548	. . . . . . . . . . . . . 14 |- F/_ k if ( j e. A , [_ j / k ]_ B , 1 )
171		eleq1w 2227	. . . . . . . . . . . . . . 15 |- ( k = j -> ( k e. A <-> j e. A ) )
172		csbeq1a 3054	. . . . . . . . . . . . . . 15 |- ( k = j -> B = [_ j / k ]_ B )
173	171, 172	ifbieq1d 3542	. . . . . . . . . . . . . 14 |- ( k = j -> if ( k e. A , B , 1 ) = if ( j e. A , [_ j / k ]_ B , 1 ) )
174	166, 170, 173	cbvmpt 4077	. . . . . . . . . . . . 13 |- ( k e. ZZ |-> if ( k e. A , B , 1 ) ) = ( j e. ZZ |-> if ( j e. A , [_ j / k ]_ B , 1 ) )
175	168	nfel1 2319	. . . . . . . . . . . . . . 15 |- F/ k [_ j / k ]_ B e. CC
176	172	eleq1d 2235	. . . . . . . . . . . . . . 15 |- ( k = j -> ( B e. CC <-> [_ j / k ]_ B e. CC ) )
177	175, 176	rspc 2824	. . . . . . . . . . . . . 14 |- ( j e. A -> ( A. k e. A B e. CC -> [_ j / k ]_ B e. CC ) )
178	125, 177	mpan9 279	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC )
179		breq1 3985	. . . . . . . . . . . . . . 15 |- ( n = i -> ( n <_ (♯ ` A ) <-> i <_ (♯ ` A ) ) )
180		fveq2 5486	. . . . . . . . . . . . . . . . 17 |- ( n = i -> ( f ` n ) = ( f ` i ) )
181	180	csbeq1d 3052	. . . . . . . . . . . . . . . 16 |- ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / k ]_ B )
182		csbcow 3056	. . . . . . . . . . . . . . . 16 |- [_ ( f ` i ) / j ]_ [_ j / k ]_ B = [_ ( f ` i ) / k ]_ B
183	181, 182	eqtr4di 2217	. . . . . . . . . . . . . . 15 |- ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / j ]_ [_ j / k ]_ B )
184	179, 183	ifbieq1d 3542	. . . . . . . . . . . . . 14 |- ( n = i -> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) = if ( i <_ (♯ ` A ) , [_ ( f ` i ) / j ]_ [_ j / k ]_ B , 1 ) )
185	184	cbvmptv 4078	. . . . . . . . . . . . 13 |- ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) = ( i e. NN |-> if ( i <_ (♯ ` A ) , [_ ( f ` i ) / j ]_ [_ j / k ]_ B , 1 ) )
186	174, 178, 185	prodmodc 11519	. . . . . . . . . . . 12 |- ( ph -> E* x ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) )
187	36, 186	jca 304	. . . . . . . . . . 11 |- ( ph -> ( ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) e. CC /\ E* x ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) ) )
188		breq2 3986	. . . . . . . . . . . . . . . 16 |- ( x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) -> ( seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x <-> seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) )
189	188	anbi2d 460	. . . . . . . . . . . . . . 15 |- ( x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) -> ( ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) <-> ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) ) )
190	189	anbi2d 460	. . . . . . . . . . . . . 14 |- ( x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) -> ( ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) <-> ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) ) ) )
191	190	rexbidv 2467	. . . . . . . . . . . . 13 |- ( x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) -> ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) <-> E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) ) ) )
192		eqeq1 2172	. . . . . . . . . . . . . . . 16 |- ( x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) -> ( x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) <-> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) )
193	192	anbi2d 460	. . . . . . . . . . . . . . 15 |- ( x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) )
194	193	exbidv 1813	. . . . . . . . . . . . . 14 |- ( x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) )
195	194	rexbidv 2467	. . . . . . . . . . . . 13 |- ( x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) <-> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) )
196	191, 195	orbi12d 783	. . . . . . . . . . . 12 |- ( x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) -> ( ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) <-> ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) ) )
197	196	moi2 2907	. . . . . . . . . . 11 |- ( ( ( ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) e. CC /\ E* x ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) ) /\ ( ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) /\ ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) ) ) -> x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) )
198	187, 197	sylan 281	. . . . . . . . . 10 |- ( ( ph /\ ( ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) /\ ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) ) ) -> x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) )
199	198	ancom2s 556	. . . . . . . . 9 |- ( ( ph /\ ( ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) /\ ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) ) ) -> x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) )
200	199	expr 373	. . . . . . . 8 |- ( ( ph /\ ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) ) -> ( ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) -> x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) )
201	165, 200	mpdan 418	. . . . . . 7 |- ( ph -> ( ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) -> x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) )
202	64, 201	syl5bir 152	. . . . . 6 |- ( ph -> ( ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) -> x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) )
203	64, 196	bitr3id 193	. . . . . . 7 |- ( x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) -> ( ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) <-> ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. i e. ( ZZ>= ` m )DECID i e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) ) )
204	165, 203	syl5ibrcom 156	. . . . . 6 |- ( ph -> ( x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) -> ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) ) )
205	202, 204	impbid 128	. . . . 5 |- ( ph -> ( ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) <-> x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) )
206	205	adantr 274	. . . 4 |- ( ( ph /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) e. CC ) -> ( ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) <-> x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) ) )
207	206	iota5 5173	. . 3 |- ( ( ph /\ ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) e. CC ) -> ( iota x ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) )
208	36, 207	mpdan 418	. 2 |- ( ph -> ( iota x ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) )
209	1, 208	syl5eq 2211	1 |- ( ph -> prod_ k e. A B = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   \/ wo 698  DECID wdc 824   = wceq 1343   E.wex 1480   E*wmo 2015   e. wcel 2136   A.wral 2444   E.wrex 2445   _Vcvv 2726   [_csb 3045   C_ wss 3116   ifcif 3520   class class class wbr 3982   |-> cmpt 4043   iotacio 5151   -->wf 5184   -1-1-onto->wf1o 5187   ` cfv 5188  (class class class)co 5842   Fincfn 6706   CCcc 7751   0cc0 7753   1c1 7754   x. cmul 7758   <_ cle 7934   # cap 8479   NNcn 8857   NN0cn0 9114   ZZcz 9191   ZZ>=cuz 9466   ...cfz 9944   seqcseq 10380  ♯chash 10688   ~~> cli 11219   prod_cprod 11491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-13 2138  ax-14 2139  ax-ext 2147  ax-coll 4097  ax-sep 4100  ax-nul 4108  ax-pow 4153  ax-pr 4187  ax-un 4411  ax-setind 4514  ax-iinf 4565  ax-cnex 7844  ax-resscn 7845  ax-1cn 7846  ax-1re 7847  ax-icn 7848  ax-addcl 7849  ax-addrcl 7850  ax-mulcl 7851  ax-mulrcl 7852  ax-addcom 7853  ax-mulcom 7854  ax-addass 7855  ax-mulass 7856  ax-distr 7857  ax-i2m1 7858  ax-0lt1 7859  ax-1rid 7860  ax-0id 7861  ax-rnegex 7862  ax-precex 7863  ax-cnre 7864  ax-pre-ltirr 7865  ax-pre-ltwlin 7866  ax-pre-lttrn 7867  ax-pre-apti 7868  ax-pre-ltadd 7869  ax-pre-mulgt0 7870  ax-pre-mulext 7871  ax-arch 7872  ax-caucvg 7873

This theorem depends on definitions:  df-bi 116  df-dc 825  df-3or 969  df-3an 970  df-tru 1346  df-fal 1349  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ne 2337  df-nel 2432  df-ral 2449  df-rex 2450  df-reu 2451  df-rmo 2452  df-rab 2453  df-v 2728  df-sbc 2952  df-csb 3046  df-dif 3118  df-un 3120  df-in 3122  df-ss 3129  df-nul 3410  df-if 3521  df-pw 3561  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-int 3825  df-iun 3868  df-br 3983  df-opab 4044  df-mpt 4045  df-tr 4081  df-id 4271  df-po 4274  df-iso 4275  df-iord 4344  df-on 4346  df-ilim 4347  df-suc 4349  df-iom 4568  df-xp 4610  df-rel 4611  df-cnv 4612  df-co 4613  df-dm 4614  df-rn 4615  df-res 4616  df-ima 4617  df-iota 5153  df-fun 5190  df-fn 5191  df-f 5192  df-f1 5193  df-fo 5194  df-f1o 5195  df-fv 5196  df-isom 5197  df-riota 5798  df-ov 5845  df-oprab 5846  df-mpo 5847  df-1st 6108  df-2nd 6109  df-recs 6273  df-irdg 6338  df-frec 6359  df-1o 6384  df-oadd 6388  df-er 6501  df-en 6707  df-dom 6708  df-fin 6709  df-pnf 7935  df-mnf 7936  df-xr 7937  df-ltxr 7938  df-le 7939  df-sub 8071  df-neg 8072  df-reap 8473  df-ap 8480  df-div 8569  df-inn 8858  df-2 8916  df-3 8917  df-4 8918  df-n0 9115  df-z 9192  df-uz 9467  df-q 9558  df-rp 9590  df-fz 9945  df-fzo 10078  df-seqfrec 10381  df-exp 10455  df-ihash 10689  df-cj 10784  df-re 10785  df-im 10786  df-rsqrt 10940  df-abs 10941  df-clim 11220  df-proddc 11492

This theorem is referenced by:  prod1dc  11527  fprodf1o  11529  fprodmul  11532  prodsnf  11533