Theorem fprodseq 11457

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 11425	. 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 9453	. . . . 5 |- NN = ( ZZ>= ` 1 )
3		1zzd 9173	. . . . 5 |- ( ph -> 1 e. ZZ )
4		eqid 2154	. . . . . . 7 |- ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) = ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) )
5		breq1 3964	. . . . . . . 8 |- ( n = p -> ( n <_ M <-> p <_ M ) )
6		fveq2 5461	. . . . . . . 8 |- ( n = p -> ( G ` n ) = ( G ` p ) )
7	5, 6	ifbieq1d 3523	. . . . . . 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 9264	. . . . . . . . . . . 12 |- ( ph -> M e. ZZ )
13		fznn 9969	. . . . . . . . . . . 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 2223	. . . . . . . . . 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 11260	. . . . . . . . . . 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 2818	. . . . . . . . 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 7873	. . . . . . . 8 |- ( ( ( ph /\ p e. NN ) /\ -. p <_ M ) -> 1 e. CC )
28	8	nnzd 9264	. . . . . . . . 9 |- ( ( ph /\ p e. NN ) -> p e. ZZ )
29	12	adantr 274	. . . . . . . . 9 |- ( ( ph /\ p e. NN ) -> M e. ZZ )
30		zdcle 9219	. . . . . . . . 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 3530	. . . . . . 7 |- ( ( ph /\ p e. NN ) -> if ( p <_ M , ( G ` p ) , 1 ) e. CC )
33	4, 7, 8, 32	fvmptd3 5554	. . . . . 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 2231	. . . . 5 |- ( ( ph /\ p e. NN ) -> ( ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ` p ) e. CC )
35	2, 3, 34	prodf 11412	. . . 4 |- ( ph -> seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) : NN --> CC )
36	35, 11	ffvelrnd 5596	. . 3 |- ( ph -> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) e. CC )
37		eleq1w 2215	. . . . . . . . . . . . 13 |- ( i = j -> ( i e. A <-> j e. A ) )
38	37	dcbid 824	. . . . . . . . . . . 12 |- ( i = j -> (DECID i e. A <-> DECID j e. A ) )
39	38	cbvralv 2677	. . . . . . . . . . 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 2461	. . . . . . . 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 9076	. . . . . . . . . . . . . . . . . . . . 21 |- ( m e. NN -> m e. NN0 )
44		hashfz1 10634	. . . . . . . . . . . . . . . . . . . . 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 9173	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> 1 e. ZZ )
48		nnz 9165	. . . . . . . . . . . . . . . . . . . . . 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 10308	. . . . . . . . . . . . . . . . . . . 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 10641	. . . . . . . . . . . . . . . . . . 19 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> (♯ ` ( 1 ... m ) ) = (♯ ` A ) )
53	46, 52	eqtr3d 2189	. . . . . . . . . . . . . . . . . 18 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> m = (♯ ` A ) )
54	53	breq2d 3973	. . . . . . . . . . . . . . . . 17 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( n <_ m <-> n <_ (♯ ` A ) ) )
55	54	ifbid 3522	. . . . . . . . . . . . . . . 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 4051	. . . . . . . . . . . . . . 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 10330	. . . . . . . . . . . . . 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 5463	. . . . . . . . . . . . 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 2166	. . . . . . . . . . . 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 1802	. . . . . . . . . 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 2469	. . . . . . . . 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 5407	. . . . . . . . . . . . 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 10308	. . . . . . . . . . . 12 |- ( ph -> ( 1 ... M ) e. Fin )
68		fex 5687	. . . . . . . . . . . 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 2247	. . . . . . . . . . . . 13 |- ( ph -> M e. ( ZZ>= ` 1 ) )
71		fveq2 5461	. . . . . . . . . . . . . . . . 17 |- ( n = u -> ( F ` n ) = ( F ` u ) )
72	71	csbeq1d 3034	. . . . . . . . . . . . . . . 16 |- ( n = u -> [_ ( F ` n ) / k ]_ B = [_ ( F ` u ) / k ]_ B )
73		fveq2 5461	. . . . . . . . . . . . . . . 16 |- ( n = u -> ( G ` n ) = ( G ` u ) )
74	72, 73	eqeq12d 2169	. . . . . . . . . . . . . . 15 |- ( n = u -> ( [_ ( F ` n ) / k ]_ B = ( G ` n ) <-> [_ ( F ` u ) / k ]_ B = ( G ` u ) ) )
75	66	ffvelrnda 5595	. . . . . . . . . . . . . . . . . . 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 3073	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. ( 1 ... M ) ) -> [_ ( F ` n ) / k ]_ B = C )
78	77, 21	eqtr4d 2190	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. ( 1 ... M ) ) -> [_ ( F ` n ) / k ]_ B = ( G ` n ) )
79	78	ralrimiva 2527	. . . . . . . . . . . . . . . 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 2818	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( 1 ... M ) ) -> [_ ( F ` u ) / k ]_ B = ( G ` u ) )
83		eqid 2154	. . . . . . . . . . . . . . . 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 3964	. . . . . . . . . . . . . . . . 17 |- ( n = u -> ( n <_ (♯ ` A ) <-> u <_ (♯ ` A ) ) )
85	84, 72	ifbieq1d 3523	. . . . . . . . . . . . . . . 16 |- ( n = u -> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) = if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) )
86		elfznn 9934	. . . . . . . . . . . . . . . . 17 |- ( u e. ( 1 ... M ) -> u e. NN )
87	86	adantl 275	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u e. NN )
88		elfzle2 9908	. . . . . . . . . . . . . . . . . . . . 21 |- ( u e. ( 1 ... M ) -> u <_ M )
89	88	adantl 275	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u <_ M )
90	11	nnnn0d 9122	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> M e. NN0 )
91		hashfz1 10634	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( M e. NN0 -> (♯ ` ( 1 ... M ) ) = M )
92	90, 91	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> (♯ ` ( 1 ... M ) ) = M )
93	67, 19	fihasheqf1od 10641	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> (♯ ` ( 1 ... M ) ) = (♯ ` A ) )
94	92, 93	eqtr3d 2189	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> M = (♯ ` A ) )
95	94	adantr 274	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( 1 ... M ) ) -> M = (♯ ` A ) )
96	89, 95	breqtrd 3986	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u <_ (♯ ` A ) )
97	96	iftrued 3508	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) = [_ ( F ` u ) / k ]_ B )
98	97, 82	eqtrd 2187	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) = ( G ` u ) )
99	73	eleq1d 2223	. . . . . . . . . . . . . . . . . 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 2818	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( G ` u ) e. CC )
102	98, 101	eqeltrd 2231	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) e. CC )
103	83, 85, 87, 102	fvmptd3 5554	. . . . . . . . . . . . . . 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 2187	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ` u ) = [_ ( F ` u ) / k ]_ B )
105		breq1 3964	. . . . . . . . . . . . . . . . 17 |- ( n = u -> ( n <_ M <-> u <_ M ) )
106	105, 73	ifbieq1d 3523	. . . . . . . . . . . . . . . 16 |- ( n = u -> if ( n <_ M , ( G ` n ) , 1 ) = if ( u <_ M , ( G ` u ) , 1 ) )
107	89	iftrued 3508	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ M , ( G ` u ) , 1 ) = ( G ` u ) )
108	107, 101	eqeltrd 2231	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ M , ( G ` u ) , 1 ) e. CC )
109	4, 106, 87, 108	fvmptd3 5554	. . . . . . . . . . . . . . 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 2187	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ` u ) = ( G ` u ) )
111	82, 104, 110	3eqtr4rd 2198	. . . . . . . . . . . . 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 9454	. . . . . . . . . . . . . 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 3964	. . . . . . . . . . . . . . . . 17 |- ( n = p -> ( n <_ (♯ ` A ) <-> p <_ (♯ ` A ) ) )
115		fveq2 5461	. . . . . . . . . . . . . . . . . 18 |- ( n = p -> ( F ` n ) = ( F ` p ) )
116	115	csbeq1d 3034	. . . . . . . . . . . . . . . . 17 |- ( n = p -> [_ ( F ` n ) / k ]_ B = [_ ( F ` p ) / k ]_ B )
117	114, 116	ifbieq1d 3523	. . . . . . . . . . . . . . . 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 3973	. . . . . . . . . . . . . . . . . . . . 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 5595	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( 1 ... M ) ) -> ( F ` p ) e. A )
125	20	ralrimiva 2527	. . . . . . . . . . . . . . . . . . . 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 3060	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ k [_ ( F ` p ) / k ]_ B
128	127	nfel1 2307	. . . . . . . . . . . . . . . . . . . 20 |- F/ k [_ ( F ` p ) / k ]_ B e. CC
129		csbeq1a 3036	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = ( F ` p ) -> B = [_ ( F ` p ) / k ]_ B )
130	129	eleq1d 2223	. . . . . . . . . . . . . . . . . . . 20 |- ( k = ( F ` p ) -> ( B e. CC <-> [_ ( F ` p ) / k ]_ B e. CC ) )
131	128, 130	rspc 2807	. . . . . . . . . . . . . . . . . . 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 7873	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ p e. NN ) /\ -. p <_ (♯ ` A ) ) -> 1 e. CC )
135	94, 12	eqeltrrd 2232	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> (♯ ` A ) e. ZZ )
136	135	adantr 274	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ p e. NN ) -> (♯ ` A ) e. ZZ )
137		zdcle 9219	. . . . . . . . . . . . . . . . . 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 3530	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ p e. NN ) -> if ( p <_ (♯ ` A ) , [_ ( F ` p ) / k ]_ B , 1 ) e. CC )
140	83, 117, 8, 139	fvmptd3 5554	. . . . . . . . . . . . . . 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 2231	. . . . . . . . . . . . . 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 7838	. . . . . . . . . . . . . 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 10348	. . . . . . . . . . . 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 5396	. . . . . . . . . . . 12 |- ( f = F -> ( f : ( 1 ... M ) -1-1-onto-> A <-> F : ( 1 ... M ) -1-1-onto-> A ) )
148		fveq1 5460	. . . . . . . . . . . . . . . . . 18 |- ( f = F -> ( f ` n ) = ( F ` n ) )
149	148	csbeq1d 3034	. . . . . . . . . . . . . . . . 17 |- ( f = F -> [_ ( f ` n ) / k ]_ B = [_ ( F ` n ) / k ]_ B )
150	149	ifeq1d 3518	. . . . . . . . . . . . . . . 16 |- ( f = F -> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) = if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) )
151	150	mpteq2dv 4051	. . . . . . . . . . . . . . 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 10330	. . . . . . . . . . . . . 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 5463	. . . . . . . . . . . . 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 2166	. . . . . . . . . . . 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 2798	. . . . . . . . . 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 5822	. . . . . . . . . . . . . 14 |- ( m = M -> ( 1 ... m ) = ( 1 ... M ) )
158	157	f1oeq2d 5403	. . . . . . . . . . . . 13 |- ( m = M -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... M ) -1-1-onto-> A ) )
159		fveq2 5461	. . . . . . . . . . . . . 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 2166	. . . . . . . . . . . . 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 1802	. . . . . . . . . . 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 2813	. . . . . . . . . 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 2296	. . . . . . . . . . . . . 14 |- F/_ j if ( k e. A , B , 1 )
167		nfv 1505	. . . . . . . . . . . . . . 15 |- F/ k j e. A
168		nfcsb1v 3060	. . . . . . . . . . . . . . 15 |- F/_ k [_ j / k ]_ B
169		nfcv 2296	. . . . . . . . . . . . . . 15 |- F/_ k 1
170	167, 168, 169	nfif 3529	. . . . . . . . . . . . . 14 |- F/_ k if ( j e. A , [_ j / k ]_ B , 1 )
171		eleq1w 2215	. . . . . . . . . . . . . . 15 |- ( k = j -> ( k e. A <-> j e. A ) )
172		csbeq1a 3036	. . . . . . . . . . . . . . 15 |- ( k = j -> B = [_ j / k ]_ B )
173	171, 172	ifbieq1d 3523	. . . . . . . . . . . . . 14 |- ( k = j -> if ( k e. A , B , 1 ) = if ( j e. A , [_ j / k ]_ B , 1 ) )
174	166, 170, 173	cbvmpt 4055	. . . . . . . . . . . . 13 |- ( k e. ZZ |-> if ( k e. A , B , 1 ) ) = ( j e. ZZ |-> if ( j e. A , [_ j / k ]_ B , 1 ) )
175	168	nfel1 2307	. . . . . . . . . . . . . . 15 |- F/ k [_ j / k ]_ B e. CC
176	172	eleq1d 2223	. . . . . . . . . . . . . . 15 |- ( k = j -> ( B e. CC <-> [_ j / k ]_ B e. CC ) )
177	175, 176	rspc 2807	. . . . . . . . . . . . . 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 3964	. . . . . . . . . . . . . . 15 |- ( n = i -> ( n <_ (♯ ` A ) <-> i <_ (♯ ` A ) ) )
180		fveq2 5461	. . . . . . . . . . . . . . . . 17 |- ( n = i -> ( f ` n ) = ( f ` i ) )
181	180	csbeq1d 3034	. . . . . . . . . . . . . . . 16 |- ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / k ]_ B )
182		csbcow 3038	. . . . . . . . . . . . . . . 16 |- [_ ( f ` i ) / j ]_ [_ j / k ]_ B = [_ ( f ` i ) / k ]_ B
183	181, 182	eqtr4di 2205	. . . . . . . . . . . . . . 15 |- ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / j ]_ [_ j / k ]_ B )
184	179, 183	ifbieq1d 3523	. . . . . . . . . . . . . 14 |- ( n = i -> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) = if ( i <_ (♯ ` A ) , [_ ( f ` i ) / j ]_ [_ j / k ]_ B , 1 ) )
185	184	cbvmptv 4056	. . . . . . . . . . . . 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 11452	. . . . . . . . . . . 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 3965	. . . . . . . . . . . . . . . 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 2455	. . . . . . . . . . . . 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 2161	. . . . . . . . . . . . . . . 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 1802	. . . . . . . . . . . . . 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 2455	. . . . . . . . . . . . 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 2889	. . . . . . . . . . 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 5148	. . 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 2199	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 820   = wceq 1332   E.wex 1469   E*wmo 2004   e. wcel 2125   A.wral 2432   E.wrex 2433   _Vcvv 2709   [_csb 3027   C_ wss 3098   ifcif 3501   class class class wbr 3961   |-> cmpt 4021   iotacio 5126   -->wf 5159   -1-1-onto->wf1o 5162   ` cfv 5163  (class class class)co 5814   Fincfn 6674   CCcc 7709   0cc0 7711   1c1 7712   x. cmul 7716   <_ cle 7892   # cap 8435   NNcn 8812   NN0cn0 9069   ZZcz 9146   ZZ>=cuz 9418   ...cfz 9890   seqcseq 10322  ♯chash 10626   ~~> cli 11152   prod_cprod 11424

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2127  ax-14 2128  ax-ext 2136  ax-coll 4075  ax-sep 4078  ax-nul 4086  ax-pow 4130  ax-pr 4164  ax-un 4388  ax-setind 4490  ax-iinf 4541  ax-cnex 7802  ax-resscn 7803  ax-1cn 7804  ax-1re 7805  ax-icn 7806  ax-addcl 7807  ax-addrcl 7808  ax-mulcl 7809  ax-mulrcl 7810  ax-addcom 7811  ax-mulcom 7812  ax-addass 7813  ax-mulass 7814  ax-distr 7815  ax-i2m1 7816  ax-0lt1 7817  ax-1rid 7818  ax-0id 7819  ax-rnegex 7820  ax-precex 7821  ax-cnre 7822  ax-pre-ltirr 7823  ax-pre-ltwlin 7824  ax-pre-lttrn 7825  ax-pre-apti 7826  ax-pre-ltadd 7827  ax-pre-mulgt0 7828  ax-pre-mulext 7829  ax-arch 7830  ax-caucvg 7831

This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1740  df-eu 2006  df-mo 2007  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ne 2325  df-nel 2420  df-ral 2437  df-rex 2438  df-reu 2439  df-rmo 2440  df-rab 2441  df-v 2711  df-sbc 2934  df-csb 3028  df-dif 3100  df-un 3102  df-in 3104  df-ss 3111  df-nul 3391  df-if 3502  df-pw 3541  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-int 3804  df-iun 3847  df-br 3962  df-opab 4022  df-mpt 4023  df-tr 4059  df-id 4248  df-po 4251  df-iso 4252  df-iord 4321  df-on 4323  df-ilim 4324  df-suc 4326  df-iom 4544  df-xp 4585  df-rel 4586  df-cnv 4587  df-co 4588  df-dm 4589  df-rn 4590  df-res 4591  df-ima 4592  df-iota 5128  df-fun 5165  df-fn 5166  df-f 5167  df-f1 5168  df-fo 5169  df-f1o 5170  df-fv 5171  df-isom 5172  df-riota 5770  df-ov 5817  df-oprab 5818  df-mpo 5819  df-1st 6078  df-2nd 6079  df-recs 6242  df-irdg 6307  df-frec 6328  df-1o 6353  df-oadd 6357  df-er 6469  df-en 6675  df-dom 6676  df-fin 6677  df-pnf 7893  df-mnf 7894  df-xr 7895  df-ltxr 7896  df-le 7897  df-sub 8027  df-neg 8028  df-reap 8429  df-ap 8436  df-div 8525  df-inn 8813  df-2 8871  df-3 8872  df-4 8873  df-n0 9070  df-z 9147  df-uz 9419  df-q 9507  df-rp 9539  df-fz 9891  df-fzo 10020  df-seqfrec 10323  df-exp 10397  df-ihash 10627  df-cj 10719  df-re 10720  df-im 10721  df-rsqrt 10875  df-abs 10876  df-clim 11153  df-proddc 11425

This theorem is referenced by:  prod1dc  11460  fprodf1o  11462  fprodmul  11465  prodsnf  11466