Theorem fprodseq 11765

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 11733	. 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 9654	. . . . 5 |- NN = ( ZZ>= ` 1 )
3		1zzd 9370	. . . . 5 |- ( ph -> 1 e. ZZ )
4		eqid 2196	. . . . . . 7 |- ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) = ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) )
5		breq1 4037	. . . . . . . 8 |- ( n = p -> ( n <_ M <-> p <_ M ) )
6		fveq2 5561	. . . . . . . 8 |- ( n = p -> ( G ` n ) = ( G ` p ) )
7	5, 6	ifbieq1d 3584	. . . . . . 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 9464	. . . . . . . . . . . 12 |- ( ph -> M e. ZZ )
13		fznn 10181	. . . . . . . . . . . 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 2265	. . . . . . . . . 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 11568	. . . . . . . . . . 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 2873	. . . . . . . . 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 8059	. . . . . . . 8 |- ( ( ( ph /\ p e. NN ) /\ -. p <_ M ) -> 1 e. CC )
28	8	nnzd 9464	. . . . . . . . 9 |- ( ( ph /\ p e. NN ) -> p e. ZZ )
29	12	adantr 276	. . . . . . . . 9 |- ( ( ph /\ p e. NN ) -> M e. ZZ )
30		zdcle 9419	. . . . . . . . 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 3591	. . . . . . 7 |- ( ( ph /\ p e. NN ) -> if ( p <_ M , ( G ` p ) , 1 ) e. CC )
33	4, 7, 8, 32	fvmptd3 5658	. . . . . 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 2273	. . . . 5 |- ( ( ph /\ p e. NN ) -> ( ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ` p ) e. CC )
35	2, 3, 34	prodf 11720	. . . 4 |- ( ph -> seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) : NN --> CC )
36	35, 11	ffvelcdmd 5701	. . 3 |- ( ph -> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) e. CC )
37		eleq1w 2257	. . . . . . . . . . . . 13 |- ( i = j -> ( i e. A <-> j e. A ) )
38	37	dcbid 839	. . . . . . . . . . . 12 |- ( i = j -> (DECID i e. A <-> DECID j e. A ) )
39	38	cbvralv 2729	. . . . . . . . . . 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 2504	. . . . . . . 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 9273	. . . . . . . . . . . . . . . . . . . . 21 |- ( m e. NN -> m e. NN0 )
44		hashfz1 10892	. . . . . . . . . . . . . . . . . . . . 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 9370	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> 1 e. ZZ )
48		nnz 9362	. . . . . . . . . . . . . . . . . . . . . 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 10540	. . . . . . . . . . . . . . . . . . . 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 10898	. . . . . . . . . . . . . . . . . . 19 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> (♯ ` ( 1 ... m ) ) = (♯ ` A ) )
53	46, 52	eqtr3d 2231	. . . . . . . . . . . . . . . . . 18 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> m = (♯ ` A ) )
54	53	breq2d 4046	. . . . . . . . . . . . . . . . 17 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( n <_ m <-> n <_ (♯ ` A ) ) )
55	54	ifbid 3583	. . . . . . . . . . . . . . . 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 4125	. . . . . . . . . . . . . . 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 10564	. . . . . . . . . . . . . 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 5563	. . . . . . . . . . . . 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 2208	. . . . . . . . . . . 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 1839	. . . . . . . . . 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 2512	. . . . . . . . 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 765	. . . . . . 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 5507	. . . . . . . . . . . . 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 10540	. . . . . . . . . . . 12 |- ( ph -> ( 1 ... M ) e. Fin )
68		fex 5794	. . . . . . . . . . . 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 2289	. . . . . . . . . . . . 13 |- ( ph -> M e. ( ZZ>= ` 1 ) )
71		fveq2 5561	. . . . . . . . . . . . . . . . 17 |- ( n = u -> ( F ` n ) = ( F ` u ) )
72	71	csbeq1d 3091	. . . . . . . . . . . . . . . 16 |- ( n = u -> [_ ( F ` n ) / k ]_ B = [_ ( F ` u ) / k ]_ B )
73		fveq2 5561	. . . . . . . . . . . . . . . 16 |- ( n = u -> ( G ` n ) = ( G ` u ) )
74	72, 73	eqeq12d 2211	. . . . . . . . . . . . . . 15 |- ( n = u -> ( [_ ( F ` n ) / k ]_ B = ( G ` n ) <-> [_ ( F ` u ) / k ]_ B = ( G ` u ) ) )
75	66	ffvelcdmda 5700	. . . . . . . . . . . . . . . . . . 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 3131	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. ( 1 ... M ) ) -> [_ ( F ` n ) / k ]_ B = C )
78	77, 21	eqtr4d 2232	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. ( 1 ... M ) ) -> [_ ( F ` n ) / k ]_ B = ( G ` n ) )
79	78	ralrimiva 2570	. . . . . . . . . . . . . . . 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 2873	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( 1 ... M ) ) -> [_ ( F ` u ) / k ]_ B = ( G ` u ) )
83		eqid 2196	. . . . . . . . . . . . . . . 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 4037	. . . . . . . . . . . . . . . . 17 |- ( n = u -> ( n <_ (♯ ` A ) <-> u <_ (♯ ` A ) ) )
85	84, 72	ifbieq1d 3584	. . . . . . . . . . . . . . . 16 |- ( n = u -> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) = if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) )
86		elfznn 10146	. . . . . . . . . . . . . . . . 17 |- ( u e. ( 1 ... M ) -> u e. NN )
87	86	adantl 277	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u e. NN )
88		elfzle2 10120	. . . . . . . . . . . . . . . . . . . . 21 |- ( u e. ( 1 ... M ) -> u <_ M )
89	88	adantl 277	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u <_ M )
90	11	nnnn0d 9319	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> M e. NN0 )
91		hashfz1 10892	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( M e. NN0 -> (♯ ` ( 1 ... M ) ) = M )
92	90, 91	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> (♯ ` ( 1 ... M ) ) = M )
93	67, 19	fihasheqf1od 10898	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> (♯ ` ( 1 ... M ) ) = (♯ ` A ) )
94	92, 93	eqtr3d 2231	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> M = (♯ ` A ) )
95	94	adantr 276	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( 1 ... M ) ) -> M = (♯ ` A ) )
96	89, 95	breqtrd 4060	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u <_ (♯ ` A ) )
97	96	iftrued 3569	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) = [_ ( F ` u ) / k ]_ B )
98	97, 82	eqtrd 2229	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) = ( G ` u ) )
99	73	eleq1d 2265	. . . . . . . . . . . . . . . . . 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 2873	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( G ` u ) e. CC )
102	98, 101	eqeltrd 2273	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) e. CC )
103	83, 85, 87, 102	fvmptd3 5658	. . . . . . . . . . . . . . 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 2229	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ` u ) = [_ ( F ` u ) / k ]_ B )
105		breq1 4037	. . . . . . . . . . . . . . . . 17 |- ( n = u -> ( n <_ M <-> u <_ M ) )
106	105, 73	ifbieq1d 3584	. . . . . . . . . . . . . . . 16 |- ( n = u -> if ( n <_ M , ( G ` n ) , 1 ) = if ( u <_ M , ( G ` u ) , 1 ) )
107	89	iftrued 3569	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ M , ( G ` u ) , 1 ) = ( G ` u ) )
108	107, 101	eqeltrd 2273	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ M , ( G ` u ) , 1 ) e. CC )
109	4, 106, 87, 108	fvmptd3 5658	. . . . . . . . . . . . . . 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 2229	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ` u ) = ( G ` u ) )
111	82, 104, 110	3eqtr4rd 2240	. . . . . . . . . . . . 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 9655	. . . . . . . . . . . . . 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 4037	. . . . . . . . . . . . . . . . 17 |- ( n = p -> ( n <_ (♯ ` A ) <-> p <_ (♯ ` A ) ) )
115		fveq2 5561	. . . . . . . . . . . . . . . . . 18 |- ( n = p -> ( F ` n ) = ( F ` p ) )
116	115	csbeq1d 3091	. . . . . . . . . . . . . . . . 17 |- ( n = p -> [_ ( F ` n ) / k ]_ B = [_ ( F ` p ) / k ]_ B )
117	114, 116	ifbieq1d 3584	. . . . . . . . . . . . . . . 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 4046	. . . . . . . . . . . . . . . . . . . . 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 5700	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( 1 ... M ) ) -> ( F ` p ) e. A )
125	20	ralrimiva 2570	. . . . . . . . . . . . . . . . . . . 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 3117	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ k [_ ( F ` p ) / k ]_ B
128	127	nfel1 2350	. . . . . . . . . . . . . . . . . . . 20 |- F/ k [_ ( F ` p ) / k ]_ B e. CC
129		csbeq1a 3093	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = ( F ` p ) -> B = [_ ( F ` p ) / k ]_ B )
130	129	eleq1d 2265	. . . . . . . . . . . . . . . . . . . 20 |- ( k = ( F ` p ) -> ( B e. CC <-> [_ ( F ` p ) / k ]_ B e. CC ) )
131	128, 130	rspc 2862	. . . . . . . . . . . . . . . . . . 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 8059	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ p e. NN ) /\ -. p <_ (♯ ` A ) ) -> 1 e. CC )
135	94, 12	eqeltrrd 2274	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> (♯ ` A ) e. ZZ )
136	135	adantr 276	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ p e. NN ) -> (♯ ` A ) e. ZZ )
137		zdcle 9419	. . . . . . . . . . . . . . . . . 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 3591	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ p e. NN ) -> if ( p <_ (♯ ` A ) , [_ ( F ` p ) / k ]_ B , 1 ) e. CC )
140	83, 117, 8, 139	fvmptd3 5658	. . . . . . . . . . . . . . 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 2273	. . . . . . . . . . . . . 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 8023	. . . . . . . . . . . . . 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 10588	. . . . . . . . . . . 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 5495	. . . . . . . . . . . 12 |- ( f = F -> ( f : ( 1 ... M ) -1-1-onto-> A <-> F : ( 1 ... M ) -1-1-onto-> A ) )
148		fveq1 5560	. . . . . . . . . . . . . . . . . 18 |- ( f = F -> ( f ` n ) = ( F ` n ) )
149	148	csbeq1d 3091	. . . . . . . . . . . . . . . . 17 |- ( f = F -> [_ ( f ` n ) / k ]_ B = [_ ( F ` n ) / k ]_ B )
150	149	ifeq1d 3579	. . . . . . . . . . . . . . . 16 |- ( f = F -> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) = if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) )
151	150	mpteq2dv 4125	. . . . . . . . . . . . . . 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 10564	. . . . . . . . . . . . . 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 5563	. . . . . . . . . . . . 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 2208	. . . . . . . . . . . 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 2853	. . . . . . . . . 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 5933	. . . . . . . . . . . . . 14 |- ( m = M -> ( 1 ... m ) = ( 1 ... M ) )
158	157	f1oeq2d 5503	. . . . . . . . . . . . 13 |- ( m = M -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... M ) -1-1-onto-> A ) )
159		fveq2 5561	. . . . . . . . . . . . . 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 2208	. . . . . . . . . . . . 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 1839	. . . . . . . . . . 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 2868	. . . . . . . . . 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 735	. . . . . . . 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 2339	. . . . . . . . . . . . . 14 |- F/_ j if ( k e. A , B , 1 )
167		nfv 1542	. . . . . . . . . . . . . . 15 |- F/ k j e. A
168		nfcsb1v 3117	. . . . . . . . . . . . . . 15 |- F/_ k [_ j / k ]_ B
169		nfcv 2339	. . . . . . . . . . . . . . 15 |- F/_ k 1
170	167, 168, 169	nfif 3590	. . . . . . . . . . . . . 14 |- F/_ k if ( j e. A , [_ j / k ]_ B , 1 )
171		eleq1w 2257	. . . . . . . . . . . . . . 15 |- ( k = j -> ( k e. A <-> j e. A ) )
172		csbeq1a 3093	. . . . . . . . . . . . . . 15 |- ( k = j -> B = [_ j / k ]_ B )
173	171, 172	ifbieq1d 3584	. . . . . . . . . . . . . 14 |- ( k = j -> if ( k e. A , B , 1 ) = if ( j e. A , [_ j / k ]_ B , 1 ) )
174	166, 170, 173	cbvmpt 4129	. . . . . . . . . . . . 13 |- ( k e. ZZ |-> if ( k e. A , B , 1 ) ) = ( j e. ZZ |-> if ( j e. A , [_ j / k ]_ B , 1 ) )
175	168	nfel1 2350	. . . . . . . . . . . . . . 15 |- F/ k [_ j / k ]_ B e. CC
176	172	eleq1d 2265	. . . . . . . . . . . . . . 15 |- ( k = j -> ( B e. CC <-> [_ j / k ]_ B e. CC ) )
177	175, 176	rspc 2862	. . . . . . . . . . . . . 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 4037	. . . . . . . . . . . . . . 15 |- ( n = i -> ( n <_ (♯ ` A ) <-> i <_ (♯ ` A ) ) )
180		fveq2 5561	. . . . . . . . . . . . . . . . 17 |- ( n = i -> ( f ` n ) = ( f ` i ) )
181	180	csbeq1d 3091	. . . . . . . . . . . . . . . 16 |- ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / k ]_ B )
182		csbcow 3095	. . . . . . . . . . . . . . . 16 |- [_ ( f ` i ) / j ]_ [_ j / k ]_ B = [_ ( f ` i ) / k ]_ B
183	181, 182	eqtr4di 2247	. . . . . . . . . . . . . . 15 |- ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / j ]_ [_ j / k ]_ B )
184	179, 183	ifbieq1d 3584	. . . . . . . . . . . . . 14 |- ( n = i -> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) = if ( i <_ (♯ ` A ) , [_ ( f ` i ) / j ]_ [_ j / k ]_ B , 1 ) )
185	184	cbvmptv 4130	. . . . . . . . . . . . 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 11760	. . . . . . . . . . . 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 4038	. . . . . . . . . . . . . . . 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 2498	. . . . . . . . . . . . 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 2203	. . . . . . . . . . . . . . . 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 1839	. . . . . . . . . . . . . 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 2498	. . . . . . . . . . . . 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 794	. . . . . . . . . . . 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 2945	. . . . . . . . . . 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 5241	. . 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 2241	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 709  DECID wdc 835   = wceq 1364   E.wex 1506   E*wmo 2046   e. wcel 2167   A.wral 2475   E.wrex 2476   _Vcvv 2763   [_csb 3084   C_ wss 3157   ifcif 3562   class class class wbr 4034   |-> cmpt 4095   iotacio 5218   -->wf 5255   -1-1-onto->wf1o 5258   ` cfv 5259  (class class class)co 5925   Fincfn 6808   CCcc 7894   0cc0 7896   1c1 7897   x. cmul 7901   <_ cle 8079   # cap 8625   NNcn 9007   NN0cn0 9266   ZZcz 9343   ZZ>=cuz 9618   ...cfz 10100   seqcseq 10556  ♯chash 10884   ~~> cli 11460   prod_cprod 11732

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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4149  ax-sep 4152  ax-nul 4160  ax-pow 4208  ax-pr 4243  ax-un 4469  ax-setind 4574  ax-iinf 4625  ax-cnex 7987  ax-resscn 7988  ax-1cn 7989  ax-1re 7990  ax-icn 7991  ax-addcl 7992  ax-addrcl 7993  ax-mulcl 7994  ax-mulrcl 7995  ax-addcom 7996  ax-mulcom 7997  ax-addass 7998  ax-mulass 7999  ax-distr 8000  ax-i2m1 8001  ax-0lt1 8002  ax-1rid 8003  ax-0id 8004  ax-rnegex 8005  ax-precex 8006  ax-cnre 8007  ax-pre-ltirr 8008  ax-pre-ltwlin 8009  ax-pre-lttrn 8010  ax-pre-apti 8011  ax-pre-ltadd 8012  ax-pre-mulgt0 8013  ax-pre-mulext 8014  ax-arch 8015  ax-caucvg 8016

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rmo 2483  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3452  df-if 3563  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-int 3876  df-iun 3919  df-br 4035  df-opab 4096  df-mpt 4097  df-tr 4133  df-id 4329  df-po 4332  df-iso 4333  df-iord 4402  df-on 4404  df-ilim 4405  df-suc 4407  df-iom 4628  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-rn 4675  df-res 4676  df-ima 4677  df-iota 5220  df-fun 5261  df-fn 5262  df-f 5263  df-f1 5264  df-fo 5265  df-f1o 5266  df-fv 5267  df-isom 5268  df-riota 5880  df-ov 5928  df-oprab 5929  df-mpo 5930  df-1st 6207  df-2nd 6208  df-recs 6372  df-irdg 6437  df-frec 6458  df-1o 6483  df-oadd 6487  df-er 6601  df-en 6809  df-dom 6810  df-fin 6811  df-pnf 8080  df-mnf 8081  df-xr 8082  df-ltxr 8083  df-le 8084  df-sub 8216  df-neg 8217  df-reap 8619  df-ap 8626  df-div 8717  df-inn 9008  df-2 9066  df-3 9067  df-4 9068  df-n0 9267  df-z 9344  df-uz 9619  df-q 9711  df-rp 9746  df-fz 10101  df-fzo 10235  df-seqfrec 10557  df-exp 10648  df-ihash 10885  df-cj 11024  df-re 11025  df-im 11026  df-rsqrt 11180  df-abs 11181  df-clim 11461  df-proddc 11733

This theorem is referenced by:  prod1dc  11768  fprodf1o  11770  fprodmul  11773  prodsnf  11774