Theorem fprodseq 12089

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 12057	. 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 9754	. . . . 5 |- NN = ( ZZ>= ` 1 )
3		1zzd 9469	. . . . 5 |- ( ph -> 1 e. ZZ )
4		eqid 2229	. . . . . . 7 |- ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) = ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) )
5		breq1 4085	. . . . . . . 8 |- ( n = p -> ( n <_ M <-> p <_ M ) )
6		fveq2 5626	. . . . . . . 8 |- ( n = p -> ( G ` n ) = ( G ` p ) )
7	5, 6	ifbieq1d 3625	. . . . . . 7 |- ( n = p -> if ( n <_ M , ( G ` n ) , 1 ) = if ( p <_ M , ( G ` p ) , 1 ) )
8		simpr 110	. . . . . . 7 |- ( ( ph /\ p e. NN ) -> p e. NN )
9		simpll 527	. . . . . . . . 9 |- ( ( ( ph /\ p e. NN ) /\ p <_ M ) -> ph )
10	8	anim1i 340	. . . . . . . . . 10 |- ( ( ( ph /\ p e. NN ) /\ p <_ M ) -> ( p e. NN /\ p <_ M ) )
11		fprod.2	. . . . . . . . . . . . 13 |- ( ph -> M e. NN )
12	11	nnzd 9564	. . . . . . . . . . . 12 |- ( ph -> M e. ZZ )
13		fznn 10281	. . . . . . . . . . . 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 488	. . . . . . . . . 10 |- ( ( ( ph /\ p e. NN ) /\ p <_ M ) -> ( p e. ( 1 ... M ) <-> ( p e. NN /\ p <_ M ) ) )
16	10, 15	mpbird 167	. . . . . . . . 9 |- ( ( ( ph /\ p e. NN ) /\ p <_ M ) -> p e. ( 1 ... M ) )
17	6	eleq1d 2298	. . . . . . . . . 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 11892	. . . . . . . . . . 11 |- ( ph -> A. n e. ( 1 ... M ) ( G ` n ) e. CC )
23	22	adantr 276	. . . . . . . . . 10 |- ( ( ph /\ p e. ( 1 ... M ) ) -> A. n e. ( 1 ... M ) ( G ` n ) e. CC )
24		simpr 110	. . . . . . . . . 10 |- ( ( ph /\ p e. ( 1 ... M ) ) -> p e. ( 1 ... M ) )
25	17, 23, 24	rspcdva 2912	. . . . . . . . 9 |- ( ( ph /\ p e. ( 1 ... M ) ) -> ( G ` p ) e. CC )
26	9, 16, 25	syl2anc 411	. . . . . . . 8 |- ( ( ( ph /\ p e. NN ) /\ p <_ M ) -> ( G ` p ) e. CC )
27		1cnd 8158	. . . . . . . 8 |- ( ( ( ph /\ p e. NN ) /\ -. p <_ M ) -> 1 e. CC )
28	8	nnzd 9564	. . . . . . . . 9 |- ( ( ph /\ p e. NN ) -> p e. ZZ )
29	12	adantr 276	. . . . . . . . 9 |- ( ( ph /\ p e. NN ) -> M e. ZZ )
30		zdcle 9519	. . . . . . . . 9 |- ( ( p e. ZZ /\ M e. ZZ ) -> DECID p <_ M )
31	28, 29, 30	syl2anc 411	. . . . . . . 8 |- ( ( ph /\ p e. NN ) -> DECID p <_ M )
32	26, 27, 31	ifcldadc 3632	. . . . . . 7 |- ( ( ph /\ p e. NN ) -> if ( p <_ M , ( G ` p ) , 1 ) e. CC )
33	4, 7, 8, 32	fvmptd3 5727	. . . . . 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 2306	. . . . 5 |- ( ( ph /\ p e. NN ) -> ( ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ` p ) e. CC )
35	2, 3, 34	prodf 12044	. . . 4 |- ( ph -> seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) : NN --> CC )
36	35, 11	ffvelcdmd 5770	. . 3 |- ( ph -> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) e. CC )
37		eleq1w 2290	. . . . . . . . . . . . 13 |- ( i = j -> ( i e. A <-> j e. A ) )
38	37	dcbid 843	. . . . . . . . . . . 12 |- ( i = j -> (DECID i e. A <-> DECID j e. A ) )
39	38	cbvralv 2765	. . . . . . . . . . 11 |- ( A. i e. ( ZZ>= ` m )DECID i e. A <-> A. j e. ( ZZ>= ` m )DECID j e. A )
40	39	anbi2i 457	. . . . . . . . . 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 458	. . . . . . . . 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 2537	. . . . . . . 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 9372	. . . . . . . . . . . . . . . . . . . . 21 |- ( m e. NN -> m e. NN0 )
44		hashfz1 11000	. . . . . . . . . . . . . . . . . . . . 21 |- ( m e. NN0 -> (♯ ` ( 1 ... m ) ) = m )
45	43, 44	syl 14	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. NN -> (♯ ` ( 1 ... m ) ) = m )
46	45	adantr 276	. . . . . . . . . . . . . . . . . . 19 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> (♯ ` ( 1 ... m ) ) = m )
47		1zzd 9469	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> 1 e. ZZ )
48		nnz 9461	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m e. NN -> m e. ZZ )
49	48	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> m e. ZZ )
50	47, 49	fzfigd 10648	. . . . . . . . . . . . . . . . . . . 20 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( 1 ... m ) e. Fin )
51		simpr 110	. . . . . . . . . . . . . . . . . . . 20 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> f : ( 1 ... m ) -1-1-onto-> A )
52	50, 51	fihasheqf1od 11006	. . . . . . . . . . . . . . . . . . 19 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> (♯ ` ( 1 ... m ) ) = (♯ ` A ) )
53	46, 52	eqtr3d 2264	. . . . . . . . . . . . . . . . . 18 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> m = (♯ ` A ) )
54	53	breq2d 4094	. . . . . . . . . . . . . . . . 17 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( n <_ m <-> n <_ (♯ ` A ) ) )
55	54	ifbid 3624	. . . . . . . . . . . . . . . 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 4174	. . . . . . . . . . . . . . 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 10672	. . . . . . . . . . . . . 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 5628	. . . . . . . . . . . . 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 2241	. . . . . . . . . . . 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 452	. . . . . . . . . . 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 1871	. . . . . . . . . 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 2545	. . . . . . . . 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 132	. . . . . . . 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 769	. . . . . . 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 5571	. . . . . . . . . . . . 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 10648	. . . . . . . . . . . 12 |- ( ph -> ( 1 ... M ) e. Fin )
68		fex 5867	. . . . . . . . . . . 12 |- ( ( F : ( 1 ... M ) --> A /\ ( 1 ... M ) e. Fin ) -> F e. _V )
69	66, 67, 68	syl2anc 411	. . . . . . . . . . 11 |- ( ph -> F e. _V )
70	11, 2	eleqtrdi 2322	. . . . . . . . . . . . 13 |- ( ph -> M e. ( ZZ>= ` 1 ) )
71		fveq2 5626	. . . . . . . . . . . . . . . . 17 |- ( n = u -> ( F ` n ) = ( F ` u ) )
72	71	csbeq1d 3131	. . . . . . . . . . . . . . . 16 |- ( n = u -> [_ ( F ` n ) / k ]_ B = [_ ( F ` u ) / k ]_ B )
73		fveq2 5626	. . . . . . . . . . . . . . . 16 |- ( n = u -> ( G ` n ) = ( G ` u ) )
74	72, 73	eqeq12d 2244	. . . . . . . . . . . . . . 15 |- ( n = u -> ( [_ ( F ` n ) / k ]_ B = ( G ` n ) <-> [_ ( F ` u ) / k ]_ B = ( G ` u ) ) )
75	66	ffvelcdmda 5769	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n e. ( 1 ... M ) ) -> ( F ` n ) e. A )
76	18	adantl 277	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. ( 1 ... M ) ) /\ k = ( F ` n ) ) -> B = C )
77	75, 76	csbied 3171	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. ( 1 ... M ) ) -> [_ ( F ` n ) / k ]_ B = C )
78	77, 21	eqtr4d 2265	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. ( 1 ... M ) ) -> [_ ( F ` n ) / k ]_ B = ( G ` n ) )
79	78	ralrimiva 2603	. . . . . . . . . . . . . . . 16 |- ( ph -> A. n e. ( 1 ... M ) [_ ( F ` n ) / k ]_ B = ( G ` n ) )
80	79	adantr 276	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( 1 ... M ) ) -> A. n e. ( 1 ... M ) [_ ( F ` n ) / k ]_ B = ( G ` n ) )
81		simpr 110	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u e. ( 1 ... M ) )
82	74, 80, 81	rspcdva 2912	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( 1 ... M ) ) -> [_ ( F ` u ) / k ]_ B = ( G ` u ) )
83		eqid 2229	. . . . . . . . . . . . . . . 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 4085	. . . . . . . . . . . . . . . . 17 |- ( n = u -> ( n <_ (♯ ` A ) <-> u <_ (♯ ` A ) ) )
85	84, 72	ifbieq1d 3625	. . . . . . . . . . . . . . . 16 |- ( n = u -> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) = if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) )
86		elfznn 10246	. . . . . . . . . . . . . . . . 17 |- ( u e. ( 1 ... M ) -> u e. NN )
87	86	adantl 277	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u e. NN )
88		elfzle2 10220	. . . . . . . . . . . . . . . . . . . . 21 |- ( u e. ( 1 ... M ) -> u <_ M )
89	88	adantl 277	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u <_ M )
90	11	nnnn0d 9418	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> M e. NN0 )
91		hashfz1 11000	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( M e. NN0 -> (♯ ` ( 1 ... M ) ) = M )
92	90, 91	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> (♯ ` ( 1 ... M ) ) = M )
93	67, 19	fihasheqf1od 11006	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> (♯ ` ( 1 ... M ) ) = (♯ ` A ) )
94	92, 93	eqtr3d 2264	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> M = (♯ ` A ) )
95	94	adantr 276	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( 1 ... M ) ) -> M = (♯ ` A ) )
96	89, 95	breqtrd 4108	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u <_ (♯ ` A ) )
97	96	iftrued 3609	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) = [_ ( F ` u ) / k ]_ B )
98	97, 82	eqtrd 2262	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) = ( G ` u ) )
99	73	eleq1d 2298	. . . . . . . . . . . . . . . . . 18 |- ( n = u -> ( ( G ` n ) e. CC <-> ( G ` u ) e. CC ) )
100	22	adantr 276	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( 1 ... M ) ) -> A. n e. ( 1 ... M ) ( G ` n ) e. CC )
101	99, 100, 81	rspcdva 2912	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( G ` u ) e. CC )
102	98, 101	eqeltrd 2306	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) e. CC )
103	83, 85, 87, 102	fvmptd3 5727	. . . . . . . . . . . . . . 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 2262	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ` u ) = [_ ( F ` u ) / k ]_ B )
105		breq1 4085	. . . . . . . . . . . . . . . . 17 |- ( n = u -> ( n <_ M <-> u <_ M ) )
106	105, 73	ifbieq1d 3625	. . . . . . . . . . . . . . . 16 |- ( n = u -> if ( n <_ M , ( G ` n ) , 1 ) = if ( u <_ M , ( G ` u ) , 1 ) )
107	89	iftrued 3609	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ M , ( G ` u ) , 1 ) = ( G ` u ) )
108	107, 101	eqeltrd 2306	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ M , ( G ` u ) , 1 ) e. CC )
109	4, 106, 87, 108	fvmptd3 5727	. . . . . . . . . . . . . . 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 2262	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ` u ) = ( G ` u ) )
111	82, 104, 110	3eqtr4rd 2273	. . . . . . . . . . . . 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 9755	. . . . . . . . . . . . . 14 |- ( p e. NN <-> p e. ( ZZ>= ` 1 ) )
113	112, 34	sylan2br 288	. . . . . . . . . . . . 13 |- ( ( ph /\ p e. ( ZZ>= ` 1 ) ) -> ( ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ` p ) e. CC )
114		breq1 4085	. . . . . . . . . . . . . . . . 17 |- ( n = p -> ( n <_ (♯ ` A ) <-> p <_ (♯ ` A ) ) )
115		fveq2 5626	. . . . . . . . . . . . . . . . . 18 |- ( n = p -> ( F ` n ) = ( F ` p ) )
116	115	csbeq1d 3131	. . . . . . . . . . . . . . . . 17 |- ( n = p -> [_ ( F ` n ) / k ]_ B = [_ ( F ` p ) / k ]_ B )
117	114, 116	ifbieq1d 3625	. . . . . . . . . . . . . . . 16 |- ( n = p -> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) = if ( p <_ (♯ ` A ) , [_ ( F ` p ) / k ]_ B , 1 ) )
118		simpll 527	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ p e. NN ) /\ p <_ (♯ ` A ) ) -> ph )
119		simpr 110	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ p e. NN ) /\ p <_ (♯ ` A ) ) -> p <_ (♯ ` A ) )
120	94	breq2d 4094	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( p <_ M <-> p <_ (♯ ` A ) ) )
121	120	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ p e. NN ) /\ p <_ (♯ ` A ) ) -> ( p <_ M <-> p <_ (♯ ` A ) ) )
122	119, 121	mpbird 167	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ p e. NN ) /\ p <_ (♯ ` A ) ) -> p <_ M )
123	122, 16	syldan 282	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ p e. NN ) /\ p <_ (♯ ` A ) ) -> p e. ( 1 ... M ) )
124	66	ffvelcdmda 5769	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( 1 ... M ) ) -> ( F ` p ) e. A )
125	20	ralrimiva 2603	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> A. k e. A B e. CC )
126	125	adantr 276	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( 1 ... M ) ) -> A. k e. A B e. CC )
127		nfcsb1v 3157	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ k [_ ( F ` p ) / k ]_ B
128	127	nfel1 2383	. . . . . . . . . . . . . . . . . . . 20 |- F/ k [_ ( F ` p ) / k ]_ B e. CC
129		csbeq1a 3133	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = ( F ` p ) -> B = [_ ( F ` p ) / k ]_ B )
130	129	eleq1d 2298	. . . . . . . . . . . . . . . . . . . 20 |- ( k = ( F ` p ) -> ( B e. CC <-> [_ ( F ` p ) / k ]_ B e. CC ) )
131	128, 130	rspc 2901	. . . . . . . . . . . . . . . . . . 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 411	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ p e. NN ) /\ p <_ (♯ ` A ) ) -> [_ ( F ` p ) / k ]_ B e. CC )
134		1cnd 8158	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ p e. NN ) /\ -. p <_ (♯ ` A ) ) -> 1 e. CC )
135	94, 12	eqeltrrd 2307	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> (♯ ` A ) e. ZZ )
136	135	adantr 276	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ p e. NN ) -> (♯ ` A ) e. ZZ )
137		zdcle 9519	. . . . . . . . . . . . . . . . . 18 |- ( ( p e. ZZ /\ (♯ ` A ) e. ZZ ) -> DECID p <_ (♯ ` A ) )
138	28, 136, 137	syl2anc 411	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. NN ) -> DECID p <_ (♯ ` A ) )
139	133, 134, 138	ifcldadc 3632	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ p e. NN ) -> if ( p <_ (♯ ` A ) , [_ ( F ` p ) / k ]_ B , 1 ) e. CC )
140	83, 117, 8, 139	fvmptd3 5727	. . . . . . . . . . . . . . 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 2306	. . . . . . . . . . . . . 14 |- ( ( ph /\ p e. NN ) -> ( ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ` p ) e. CC )
142	112, 141	sylan2br 288	. . . . . . . . . . . . 13 |- ( ( ph /\ p e. ( ZZ>= ` 1 ) ) -> ( ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ` p ) e. CC )
143		mulcl 8122	. . . . . . . . . . . . . 14 |- ( ( p e. CC /\ q e. CC ) -> ( p x. q ) e. CC )
144	143	adantl 277	. . . . . . . . . . . . 13 |- ( ( ph /\ ( p e. CC /\ q e. CC ) ) -> ( p x. q ) e. CC )
145	70, 111, 113, 142, 144	seq3fveq 10696	. . . . . . . . . . . 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 306	. . . . . . . . . . 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 5559	. . . . . . . . . . . 12 |- ( f = F -> ( f : ( 1 ... M ) -1-1-onto-> A <-> F : ( 1 ... M ) -1-1-onto-> A ) )
148		fveq1 5625	. . . . . . . . . . . . . . . . . 18 |- ( f = F -> ( f ` n ) = ( F ` n ) )
149	148	csbeq1d 3131	. . . . . . . . . . . . . . . . 17 |- ( f = F -> [_ ( f ` n ) / k ]_ B = [_ ( F ` n ) / k ]_ B )
150	149	ifeq1d 3620	. . . . . . . . . . . . . . . 16 |- ( f = F -> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) = if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) )
151	150	mpteq2dv 4174	. . . . . . . . . . . . . . 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 10672	. . . . . . . . . . . . . 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 5628	. . . . . . . . . . . . 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 2241	. . . . . . . . . . . 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 473	. . . . . . . . . . 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 2892	. . . . . . . . . 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 6008	. . . . . . . . . . . . . 14 |- ( m = M -> ( 1 ... m ) = ( 1 ... M ) )
158	157	f1oeq2d 5567	. . . . . . . . . . . . 13 |- ( m = M -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... M ) -1-1-onto-> A ) )
159		fveq2 5626	. . . . . . . . . . . . . 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 2241	. . . . . . . . . . . . 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 473	. . . . . . . . . . . 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 1871	. . . . . . . . . . 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 2907	. . . . . . . . . 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 411	. . . . . . . . 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 739	. . . . . . . 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 2372	. . . . . . . . . . . . . 14 |- F/_ j if ( k e. A , B , 1 )
167		nfv 1574	. . . . . . . . . . . . . . 15 |- F/ k j e. A
168		nfcsb1v 3157	. . . . . . . . . . . . . . 15 |- F/_ k [_ j / k ]_ B
169		nfcv 2372	. . . . . . . . . . . . . . 15 |- F/_ k 1
170	167, 168, 169	nfif 3631	. . . . . . . . . . . . . 14 |- F/_ k if ( j e. A , [_ j / k ]_ B , 1 )
171		eleq1w 2290	. . . . . . . . . . . . . . 15 |- ( k = j -> ( k e. A <-> j e. A ) )
172		csbeq1a 3133	. . . . . . . . . . . . . . 15 |- ( k = j -> B = [_ j / k ]_ B )
173	171, 172	ifbieq1d 3625	. . . . . . . . . . . . . 14 |- ( k = j -> if ( k e. A , B , 1 ) = if ( j e. A , [_ j / k ]_ B , 1 ) )
174	166, 170, 173	cbvmpt 4178	. . . . . . . . . . . . 13 |- ( k e. ZZ |-> if ( k e. A , B , 1 ) ) = ( j e. ZZ |-> if ( j e. A , [_ j / k ]_ B , 1 ) )
175	168	nfel1 2383	. . . . . . . . . . . . . . 15 |- F/ k [_ j / k ]_ B e. CC
176	172	eleq1d 2298	. . . . . . . . . . . . . . 15 |- ( k = j -> ( B e. CC <-> [_ j / k ]_ B e. CC ) )
177	175, 176	rspc 2901	. . . . . . . . . . . . . 14 |- ( j e. A -> ( A. k e. A B e. CC -> [_ j / k ]_ B e. CC ) )
178	125, 177	mpan9 281	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC )
179		breq1 4085	. . . . . . . . . . . . . . 15 |- ( n = i -> ( n <_ (♯ ` A ) <-> i <_ (♯ ` A ) ) )
180		fveq2 5626	. . . . . . . . . . . . . . . . 17 |- ( n = i -> ( f ` n ) = ( f ` i ) )
181	180	csbeq1d 3131	. . . . . . . . . . . . . . . 16 |- ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / k ]_ B )
182		csbcow 3135	. . . . . . . . . . . . . . . 16 |- [_ ( f ` i ) / j ]_ [_ j / k ]_ B = [_ ( f ` i ) / k ]_ B
183	181, 182	eqtr4di 2280	. . . . . . . . . . . . . . 15 |- ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / j ]_ [_ j / k ]_ B )
184	179, 183	ifbieq1d 3625	. . . . . . . . . . . . . 14 |- ( n = i -> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) = if ( i <_ (♯ ` A ) , [_ ( f ` i ) / j ]_ [_ j / k ]_ B , 1 ) )
185	184	cbvmptv 4179	. . . . . . . . . . . . 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 12084	. . . . . . . . . . . 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 306	. . . . . . . . . . 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 4086	. . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . 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 2531	. . . . . . . . . . . . 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 2236	. . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . 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 1871	. . . . . . . . . . . . . 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 2531	. . . . . . . . . . . . 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 798	. . . . . . . . . . . 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 2984	. . . . . . . . . . 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 283	. . . . . . . . . 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 566	. . . . . . . . 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 375	. . . . . . . 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 421	. . . . . . 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	biimtrrid 153	. . . . . 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 194	. . . . . . 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 157	. . . . . 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 129	. . . . 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 276	. . . 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 5299	. . 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 421	. 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	eqtrid 2274	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 104   <-> wb 105   \/ wo 713  DECID wdc 839   = wceq 1395   E.wex 1538   E*wmo 2078   e. wcel 2200   A.wral 2508   E.wrex 2509   _Vcvv 2799   [_csb 3124   C_ wss 3197   ifcif 3602   class class class wbr 4082   |-> cmpt 4144   iotacio 5275   -->wf 5313   -1-1-onto->wf1o 5316   ` cfv 5317  (class class class)co 6000   Fincfn 6885   CCcc 7993   0cc0 7995   1c1 7996   x. cmul 8000   <_ cle 8178   # cap 8724   NNcn 9106   NN0cn0 9365   ZZcz 9442   ZZ>=cuz 9718   ...cfz 10200   seqcseq 10664  ♯chash 10992   ~~> cli 11784   prod_cprod 12056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4198  ax-sep 4201  ax-nul 4209  ax-pow 4257  ax-pr 4292  ax-un 4523  ax-setind 4628  ax-iinf 4679  ax-cnex 8086  ax-resscn 8087  ax-1cn 8088  ax-1re 8089  ax-icn 8090  ax-addcl 8091  ax-addrcl 8092  ax-mulcl 8093  ax-mulrcl 8094  ax-addcom 8095  ax-mulcom 8096  ax-addass 8097  ax-mulass 8098  ax-distr 8099  ax-i2m1 8100  ax-0lt1 8101  ax-1rid 8102  ax-0id 8103  ax-rnegex 8104  ax-precex 8105  ax-cnre 8106  ax-pre-ltirr 8107  ax-pre-ltwlin 8108  ax-pre-lttrn 8109  ax-pre-apti 8110  ax-pre-ltadd 8111  ax-pre-mulgt0 8112  ax-pre-mulext 8113  ax-arch 8114  ax-caucvg 8115

This theorem depends on definitions:  df-bi 117  df-dc 840  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rmo 2516  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-nul 3492  df-if 3603  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-int 3923  df-iun 3966  df-br 4083  df-opab 4145  df-mpt 4146  df-tr 4182  df-id 4383  df-po 4386  df-iso 4387  df-iord 4456  df-on 4458  df-ilim 4459  df-suc 4461  df-iom 4682  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-rn 4729  df-res 4730  df-ima 4731  df-iota 5277  df-fun 5319  df-fn 5320  df-f 5321  df-f1 5322  df-fo 5323  df-f1o 5324  df-fv 5325  df-isom 5326  df-riota 5953  df-ov 6003  df-oprab 6004  df-mpo 6005  df-1st 6284  df-2nd 6285  df-recs 6449  df-irdg 6514  df-frec 6535  df-1o 6560  df-oadd 6564  df-er 6678  df-en 6886  df-dom 6887  df-fin 6888  df-pnf 8179  df-mnf 8180  df-xr 8181  df-ltxr 8182  df-le 8183  df-sub 8315  df-neg 8316  df-reap 8718  df-ap 8725  df-div 8816  df-inn 9107  df-2 9165  df-3 9166  df-4 9167  df-n0 9366  df-z 9443  df-uz 9719  df-q 9811  df-rp 9846  df-fz 10201  df-fzo 10335  df-seqfrec 10665  df-exp 10756  df-ihash 10993  df-cj 11348  df-re 11349  df-im 11350  df-rsqrt 11504  df-abs 11505  df-clim 11785  df-proddc 12057

This theorem is referenced by:  prod1dc  12092  fprodf1o  12094  fprodmul  12097  prodsnf  12098