Theorem fprodseq 12350

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 12318	. 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 9958	. . . . 5 |- NN = ( ZZ>= ` 1 )
3		1zzd 9671	. . . . 5 |- ( ph -> 1 e. ZZ )
4		eqid 2238	. . . . . . 7 |- ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) = ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) )
5		breq1 4133	. . . . . . . 8 |- ( n = p -> ( n <_ M <-> p <_ M ) )
6		fveq2 5695	. . . . . . . 8 |- ( n = p -> ( G ` n ) = ( G ` p ) )
7	5, 6	ifbieq1d 3663	. . . . . . 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 531	. . . . . . . . 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 9767	. . . . . . . . . . . 12 |- ( ph -> M e. ZZ )
13		fznn 10496	. . . . . . . . . . . 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 492	. . . . . . . . . 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 2307	. . . . . . . . . 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 12153	. . . . . . . . . . 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 2934	. . . . . . . . 9 |- ( ( ph /\ p e. ( 1 ... M ) ) -> ( G ` p ) e. CC )
26	9, 16, 25	syl2anc 415	. . . . . . . 8 |- ( ( ( ph /\ p e. NN ) /\ p <_ M ) -> ( G ` p ) e. CC )
27		1cnd 8342	. . . . . . . 8 |- ( ( ( ph /\ p e. NN ) /\ -. p <_ M ) -> 1 e. CC )
28	8	nnzd 9767	. . . . . . . . 9 |- ( ( ph /\ p e. NN ) -> p e. ZZ )
29	12	adantr 276	. . . . . . . . 9 |- ( ( ph /\ p e. NN ) -> M e. ZZ )
30		zdcle 9721	. . . . . . . . 9 |- ( ( p e. ZZ /\ M e. ZZ ) -> DECID p <_ M )
31	28, 29, 30	syl2anc 415	. . . . . . . 8 |- ( ( ph /\ p e. NN ) -> DECID p <_ M )
32	26, 27, 31	ifcldadc 3670	. . . . . . 7 |- ( ( ph /\ p e. NN ) -> if ( p <_ M , ( G ` p ) , 1 ) e. CC )
33	4, 7, 8, 32	fvmptd3 5799	. . . . . 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 2315	. . . . 5 |- ( ( ph /\ p e. NN ) -> ( ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ` p ) e. CC )
35	2, 3, 34	prodf 12305	. . . 4 |- ( ph -> seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) : NN --> CC )
36	35, 11	ffvelcdmd 5844	. . 3 |- ( ph -> ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) e. CC )
37		eleq1w 2299	. . . . . . . . . . . . 13 |- ( i = j -> ( i e. A <-> j e. A ) )
38	37	dcbid 850	. . . . . . . . . . . 12 |- ( i = j -> (DECID i e. A <-> DECID j e. A ) )
39	38	cbvralv 2786	. . . . . . . . . . 11 |- ( A. i e. ( ZZ>= ` m )DECID i e. A <-> A. j e. ( ZZ>= ` m )DECID j e. A )
40	39	anbi2i 461	. . . . . . . . . 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 462	. . . . . . . . 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 2557	. . . . . . . 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 9570	. . . . . . . . . . . . . . . . . . . . 21 |- ( m e. NN -> m e. NN0 )
44		hashfz1 11222	. . . . . . . . . . . . . . . . . . . . 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 9671	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> 1 e. ZZ )
48		nnz 9663	. . . . . . . . . . . . . . . . . . . . . 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 10868	. . . . . . . . . . . . . . . . . . . 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 11228	. . . . . . . . . . . . . . . . . . 19 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> (♯ ` ( 1 ... m ) ) = (♯ ` A ) )
53	46, 52	eqtr3d 2273	. . . . . . . . . . . . . . . . . 18 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> m = (♯ ` A ) )
54	53	breq2d 4142	. . . . . . . . . . . . . . . . 17 |- ( ( m e. NN /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( n <_ m <-> n <_ (♯ ` A ) ) )
55	54	ifbid 3662	. . . . . . . . . . . . . . . 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 4222	. . . . . . . . . . . . . . 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 10892	. . . . . . . . . . . . . 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 5697	. . . . . . . . . . . . 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 2250	. . . . . . . . . . . 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 456	. . . . . . . . . . 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 1878	. . . . . . . . . 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 2565	. . . . . . . . 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 776	. . . . . . 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 5639	. . . . . . . . . . . . 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 10868	. . . . . . . . . . . 12 |- ( ph -> ( 1 ... M ) e. Fin )
68		fex 5947	. . . . . . . . . . . 12 |- ( ( F : ( 1 ... M ) --> A /\ ( 1 ... M ) e. Fin ) -> F e. _V )
69	66, 67, 68	syl2anc 415	. . . . . . . . . . 11 |- ( ph -> F e. _V )
70	11, 2	eleqtrdi 2331	. . . . . . . . . . . . 13 |- ( ph -> M e. ( ZZ>= ` 1 ) )
71		fveq2 5695	. . . . . . . . . . . . . . . . 17 |- ( n = u -> ( F ` n ) = ( F ` u ) )
72	71	csbeq1d 3154	. . . . . . . . . . . . . . . 16 |- ( n = u -> [_ ( F ` n ) / k ]_ B = [_ ( F ` u ) / k ]_ B )
73		fveq2 5695	. . . . . . . . . . . . . . . 16 |- ( n = u -> ( G ` n ) = ( G ` u ) )
74	72, 73	eqeq12d 2253	. . . . . . . . . . . . . . 15 |- ( n = u -> ( [_ ( F ` n ) / k ]_ B = ( G ` n ) <-> [_ ( F ` u ) / k ]_ B = ( G ` u ) ) )
75	66	ffvelcdmda 5843	. . . . . . . . . . . . . . . . . . 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 3194	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n e. ( 1 ... M ) ) -> [_ ( F ` n ) / k ]_ B = C )
78	77, 21	eqtr4d 2274	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. ( 1 ... M ) ) -> [_ ( F ` n ) / k ]_ B = ( G ` n ) )
79	78	ralrimiva 2623	. . . . . . . . . . . . . . . 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 2934	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( 1 ... M ) ) -> [_ ( F ` u ) / k ]_ B = ( G ` u ) )
83		eqid 2238	. . . . . . . . . . . . . . . 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 4133	. . . . . . . . . . . . . . . . 17 |- ( n = u -> ( n <_ (♯ ` A ) <-> u <_ (♯ ` A ) ) )
85	84, 72	ifbieq1d 3663	. . . . . . . . . . . . . . . 16 |- ( n = u -> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) = if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) )
86		elfznn 10460	. . . . . . . . . . . . . . . . 17 |- ( u e. ( 1 ... M ) -> u e. NN )
87	86	adantl 277	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u e. NN )
88		elfzle2 10432	. . . . . . . . . . . . . . . . . . . . 21 |- ( u e. ( 1 ... M ) -> u <_ M )
89	88	adantl 277	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u <_ M )
90	11	nnnn0d 9620	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> M e. NN0 )
91		hashfz1 11222	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( M e. NN0 -> (♯ ` ( 1 ... M ) ) = M )
92	90, 91	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> (♯ ` ( 1 ... M ) ) = M )
93	67, 19	fihasheqf1od 11228	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> (♯ ` ( 1 ... M ) ) = (♯ ` A ) )
94	92, 93	eqtr3d 2273	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> M = (♯ ` A ) )
95	94	adantr 276	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( 1 ... M ) ) -> M = (♯ ` A ) )
96	89, 95	breqtrd 4156	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ u e. ( 1 ... M ) ) -> u <_ (♯ ` A ) )
97	96	iftrued 3647	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) = [_ ( F ` u ) / k ]_ B )
98	97, 82	eqtrd 2271	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) = ( G ` u ) )
99	73	eleq1d 2307	. . . . . . . . . . . . . . . . . 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 2934	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( G ` u ) e. CC )
102	98, 101	eqeltrd 2315	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ (♯ ` A ) , [_ ( F ` u ) / k ]_ B , 1 ) e. CC )
103	83, 85, 87, 102	fvmptd3 5799	. . . . . . . . . . . . . . 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 2271	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( ( n e. NN |-> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) ) ` u ) = [_ ( F ` u ) / k ]_ B )
105		breq1 4133	. . . . . . . . . . . . . . . . 17 |- ( n = u -> ( n <_ M <-> u <_ M ) )
106	105, 73	ifbieq1d 3663	. . . . . . . . . . . . . . . 16 |- ( n = u -> if ( n <_ M , ( G ` n ) , 1 ) = if ( u <_ M , ( G ` u ) , 1 ) )
107	89	iftrued 3647	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ M , ( G ` u ) , 1 ) = ( G ` u ) )
108	107, 101	eqeltrd 2315	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( 1 ... M ) ) -> if ( u <_ M , ( G ` u ) , 1 ) e. CC )
109	4, 106, 87, 108	fvmptd3 5799	. . . . . . . . . . . . . . 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 2271	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( 1 ... M ) ) -> ( ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ` u ) = ( G ` u ) )
111	82, 104, 110	3eqtr4rd 2282	. . . . . . . . . . . . 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 9959	. . . . . . . . . . . . . 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 4133	. . . . . . . . . . . . . . . . 17 |- ( n = p -> ( n <_ (♯ ` A ) <-> p <_ (♯ ` A ) ) )
115		fveq2 5695	. . . . . . . . . . . . . . . . . 18 |- ( n = p -> ( F ` n ) = ( F ` p ) )
116	115	csbeq1d 3154	. . . . . . . . . . . . . . . . 17 |- ( n = p -> [_ ( F ` n ) / k ]_ B = [_ ( F ` p ) / k ]_ B )
117	114, 116	ifbieq1d 3663	. . . . . . . . . . . . . . . 16 |- ( n = p -> if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) = if ( p <_ (♯ ` A ) , [_ ( F ` p ) / k ]_ B , 1 ) )
118		simpll 531	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ p e. NN ) /\ p <_ (♯ ` A ) ) -> ph )
119		simpr 110	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ p e. NN ) /\ p <_ (♯ ` A ) ) -> p <_ (♯ ` A ) )
120	94	breq2d 4142	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( p <_ M <-> p <_ (♯ ` A ) ) )
121	120	ad2antrr 492	. . . . . . . . . . . . . . . . . . . 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 5843	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( 1 ... M ) ) -> ( F ` p ) e. A )
125	20	ralrimiva 2623	. . . . . . . . . . . . . . . . . . . 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 3180	. . . . . . . . . . . . . . . . . . . . 21 |- F/_ k [_ ( F ` p ) / k ]_ B
128	127	nfel1 2403	. . . . . . . . . . . . . . . . . . . 20 |- F/ k [_ ( F ` p ) / k ]_ B e. CC
129		csbeq1a 3156	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = ( F ` p ) -> B = [_ ( F ` p ) / k ]_ B )
130	129	eleq1d 2307	. . . . . . . . . . . . . . . . . . . 20 |- ( k = ( F ` p ) -> ( B e. CC <-> [_ ( F ` p ) / k ]_ B e. CC ) )
131	128, 130	rspc 2923	. . . . . . . . . . . . . . . . . . 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 415	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ p e. NN ) /\ p <_ (♯ ` A ) ) -> [_ ( F ` p ) / k ]_ B e. CC )
134		1cnd 8342	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ p e. NN ) /\ -. p <_ (♯ ` A ) ) -> 1 e. CC )
135	94, 12	eqeltrrd 2316	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> (♯ ` A ) e. ZZ )
136	135	adantr 276	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ p e. NN ) -> (♯ ` A ) e. ZZ )
137		zdcle 9721	. . . . . . . . . . . . . . . . . 18 |- ( ( p e. ZZ /\ (♯ ` A ) e. ZZ ) -> DECID p <_ (♯ ` A ) )
138	28, 136, 137	syl2anc 415	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. NN ) -> DECID p <_ (♯ ` A ) )
139	133, 134, 138	ifcldadc 3670	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ p e. NN ) -> if ( p <_ (♯ ` A ) , [_ ( F ` p ) / k ]_ B , 1 ) e. CC )
140	83, 117, 8, 139	fvmptd3 5799	. . . . . . . . . . . . . . 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 2315	. . . . . . . . . . . . . 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 8306	. . . . . . . . . . . . . 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 10916	. . . . . . . . . . . 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 5627	. . . . . . . . . . . 12 |- ( f = F -> ( f : ( 1 ... M ) -1-1-onto-> A <-> F : ( 1 ... M ) -1-1-onto-> A ) )
148		fveq1 5694	. . . . . . . . . . . . . . . . . 18 |- ( f = F -> ( f ` n ) = ( F ` n ) )
149	148	csbeq1d 3154	. . . . . . . . . . . . . . . . 17 |- ( f = F -> [_ ( f ` n ) / k ]_ B = [_ ( F ` n ) / k ]_ B )
150	149	ifeq1d 3658	. . . . . . . . . . . . . . . 16 |- ( f = F -> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) = if ( n <_ (♯ ` A ) , [_ ( F ` n ) / k ]_ B , 1 ) )
151	150	mpteq2dv 4222	. . . . . . . . . . . . . . 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 10892	. . . . . . . . . . . . . 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 5697	. . . . . . . . . . . . 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 2250	. . . . . . . . . . . 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 477	. . . . . . . . . . 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 2914	. . . . . . . . . 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 6093	. . . . . . . . . . . . . 14 |- ( m = M -> ( 1 ... m ) = ( 1 ... M ) )
158	157	f1oeq2d 5635	. . . . . . . . . . . . 13 |- ( m = M -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... M ) -1-1-onto-> A ) )
159		fveq2 5695	. . . . . . . . . . . . . 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 2250	. . . . . . . . . . . . 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 477	. . . . . . . . . . . 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 1878	. . . . . . . . . . 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 2929	. . . . . . . . . 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 415	. . . . . . . . 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 746	. . . . . . . 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 2392	. . . . . . . . . . . . . 14 |- F/_ j if ( k e. A , B , 1 )
167		nfv 1581	. . . . . . . . . . . . . . 15 |- F/ k j e. A
168		nfcsb1v 3180	. . . . . . . . . . . . . . 15 |- F/_ k [_ j / k ]_ B
169		nfcv 2392	. . . . . . . . . . . . . . 15 |- F/_ k 1
170	167, 168, 169	nfif 3669	. . . . . . . . . . . . . 14 |- F/_ k if ( j e. A , [_ j / k ]_ B , 1 )
171		eleq1w 2299	. . . . . . . . . . . . . . 15 |- ( k = j -> ( k e. A <-> j e. A ) )
172		csbeq1a 3156	. . . . . . . . . . . . . . 15 |- ( k = j -> B = [_ j / k ]_ B )
173	171, 172	ifbieq1d 3663	. . . . . . . . . . . . . 14 |- ( k = j -> if ( k e. A , B , 1 ) = if ( j e. A , [_ j / k ]_ B , 1 ) )
174	166, 170, 173	cbvmpt 4226	. . . . . . . . . . . . 13 |- ( k e. ZZ |-> if ( k e. A , B , 1 ) ) = ( j e. ZZ |-> if ( j e. A , [_ j / k ]_ B , 1 ) )
175	168	nfel1 2403	. . . . . . . . . . . . . . 15 |- F/ k [_ j / k ]_ B e. CC
176	172	eleq1d 2307	. . . . . . . . . . . . . . 15 |- ( k = j -> ( B e. CC <-> [_ j / k ]_ B e. CC ) )
177	175, 176	rspc 2923	. . . . . . . . . . . . . 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 4133	. . . . . . . . . . . . . . 15 |- ( n = i -> ( n <_ (♯ ` A ) <-> i <_ (♯ ` A ) ) )
180		fveq2 5695	. . . . . . . . . . . . . . . . 17 |- ( n = i -> ( f ` n ) = ( f ` i ) )
181	180	csbeq1d 3154	. . . . . . . . . . . . . . . 16 |- ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / k ]_ B )
182		csbcow 3158	. . . . . . . . . . . . . . . 16 |- [_ ( f ` i ) / j ]_ [_ j / k ]_ B = [_ ( f ` i ) / k ]_ B
183	181, 182	eqtr4di 2289	. . . . . . . . . . . . . . 15 |- ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / j ]_ [_ j / k ]_ B )
184	179, 183	ifbieq1d 3663	. . . . . . . . . . . . . 14 |- ( n = i -> if ( n <_ (♯ ` A ) , [_ ( f ` n ) / k ]_ B , 1 ) = if ( i <_ (♯ ` A ) , [_ ( f ` i ) / j ]_ [_ j / k ]_ B , 1 ) )
185	184	cbvmptv 4227	. . . . . . . . . . . . 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 12345	. . . . . . . . . . . 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 4134	. . . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . 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 2551	. . . . . . . . . . . . 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 2245	. . . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . 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 1878	. . . . . . . . . . . . . 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 2551	. . . . . . . . . . . . 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 805	. . . . . . . . . . . 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 3007	. . . . . . . . . . 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 572	. . . . . . . . 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 425	. . . . . . 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 5359	. . 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 425	. 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 2283	1 |- ( ph -> prod_ k e. A B = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ M , ( G ` n ) , 1 ) ) ) ` M ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 720  DECID wdc 846   = wceq 1402   E.wex 1545   E*wmo 2087   e. wcel 2209   A.wral 2528   E.wrex 2529   _Vcvv 2821   [_csb 3147   C_ wss 3220   ifcif 3638   class class class wbr 4130   |-> cmpt 4192   iotacio 5335   -->wf 5373   -1-1-onto->wf1o 5376   ` cfv 5377  (class class class)co 6085   Fincfn 7022   CCcc 8177   0cc0 8179   1c1 8180   x. cmul 8184   <_ cle 8361   # cap 8909   NNcn 9304   NN0cn0 9563   ZZcz 9644   ZZ>=cuz 9921   ...cfz 10411   seqcseq 10884  ♯chash 11214   ~~> cli 12044   prod_cprod 12317

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-iinf 4735  ax-cnex 8270  ax-resscn 8271  ax-1cn 8272  ax-1re 8273  ax-icn 8274  ax-addcl 8275  ax-addrcl 8276  ax-mulcl 8277  ax-mulrcl 8278  ax-addcom 8279  ax-mulcom 8280  ax-addass 8281  ax-mulass 8282  ax-distr 8283  ax-i2m1 8284  ax-0lt1 8285  ax-1rid 8286  ax-0id 8287  ax-rnegex 8288  ax-precex 8289  ax-cnre 8290  ax-pre-ltirr 8291  ax-pre-ltwlin 8292  ax-pre-lttrn 8293  ax-pre-apti 8294  ax-pre-ltadd 8295  ax-pre-mulgt0 8296  ax-pre-mulext 8297  ax-arch 8298  ax-caucvg 8299

This proof depends on definitions:  df-bi 117  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-tr 4230  df-id 4438  df-po 4441  df-iso 4442  df-iord 4511  df-on 4513  df-ilim 4514  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-isom 5386  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-1st 6374  df-2nd 6375  df-recs 6576  df-irdg 6641  df-frec 6662  df-1o 6687  df-oadd 6691  df-er 6807  df-en 7023  df-dom 7024  df-fin 7025  df-pnf 8362  df-mnf 8363  df-xr 8364  df-ltxr 8365  df-le 8366  df-sub 8499  df-neg 8500  df-reap 8903  df-ap 8910  df-div 9003  df-inn 9305  df-2 9363  df-3 9364  df-4 9365  df-n0 9564  df-z 9645  df-uz 9922  df-q 10020  df-rp 10055  df-fz 10412  df-fzo 10550  df-seqfrec 10885  df-exp 10976  df-ihash 11215  df-cj 11607  df-re 11608  df-im 11609  df-rsqrt 11764  df-abs 11765  df-clim 12045  df-proddc 12318

This theorem is used by:  prod1dc  12353  fprodf1o  12355  fprodmul  12358  prodsnf  12359