Metamath Proof Explorer

Theorem zprod

Description: Series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 5-Dec-2017)

Ref Expression
Hypotheses zprod.1 
|- Z = ( ZZ>= ` M )
zprod.2 
|- ( ph -> M e. ZZ )
zprod.3 
|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )
zprod.4 
|- ( ph -> A C_ Z )
zprod.5 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 1 ) )
zprod.6 
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion zprod 
|- ( ph -> prod_ k e. A B = ( ~~> ` seq M ( x. , F ) ) )

Proof

Step Hyp Ref Expression
1 zprod.1 
 |-  Z = ( ZZ>= ` M )
2 zprod.2 
 |-  ( ph -> M e. ZZ )
3 zprod.3 
 |-  ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )
4 zprod.4 
 |-  ( ph -> A C_ Z )
5 zprod.5 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 1 ) )
6 zprod.6 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
7 3simpb 
 |-  ( ( A C_ ( ZZ>= ` 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 ) -> ( A C_ ( ZZ>= ` m ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) )
8 nfcv 
 |-  F/_ i if ( k e. A , B , 1 )
9 nfv 
 |-  F/ k i e. A
10 nfcsb1v 
 |-  F/_ k [_ i / k ]_ B
11 nfcv 
 |-  F/_ k 1
12 9 10 11 nfif 
 |-  F/_ k if ( i e. A , [_ i / k ]_ B , 1 )
13 eleq1w 
 |-  ( k = i -> ( k e. A <-> i e. A ) )
14 csbeq1a 
 |-  ( k = i -> B = [_ i / k ]_ B )
15 13 14 ifbieq1d 
 |-  ( k = i -> if ( k e. A , B , 1 ) = if ( i e. A , [_ i / k ]_ B , 1 ) )
16 8 12 15 cbvmpt 
 |-  ( k e. ZZ |-> if ( k e. A , B , 1 ) ) = ( i e. ZZ |-> if ( i e. A , [_ i / k ]_ B , 1 ) )
17 simpll 
 |-  ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> ph )
18 6 ralrimiva 
 |-  ( ph -> A. k e. A B e. CC )
19 10 nfel1 
 |-  F/ k [_ i / k ]_ B e. CC
20 14 eleq1d 
 |-  ( k = i -> ( B e. CC <-> [_ i / k ]_ B e. CC ) )
21 19 20 rspc 
 |-  ( i e. A -> ( A. k e. A B e. CC -> [_ i / k ]_ B e. CC ) )
22 18 21 syl5 
 |-  ( i e. A -> ( ph -> [_ i / k ]_ B e. CC ) )
23 17 22 mpan9 
 |-  ( ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) /\ i e. A ) -> [_ i / k ]_ B e. CC )
24 simplr 
 |-  ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> m e. ZZ )
25 2 ad2antrr 
 |-  ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> M e. ZZ )
26 simpr 
 |-  ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> A C_ ( ZZ>= ` m ) )
27 4 1 sseqtrdi 
 |-  ( ph -> A C_ ( ZZ>= ` M ) )
28 27 ad2antrr 
 |-  ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` m ) ) -> A C_ ( ZZ>= ` M ) )
29 16 23 24 25 26 28 prodrb 
 |-  ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` 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 ) ) ) ~~> x ) )
30 29 biimpd 
 |-  ( ( ( ph /\ m e. ZZ ) /\ A C_ ( ZZ>= ` 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 ) ) ) ~~> x ) )
31 30 expimpd 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( A C_ ( ZZ>= ` 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 ) ) ) ~~> x ) )
32 7 31 syl5 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( A C_ ( ZZ>= ` 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 ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) )
33 32 rexlimdva 
 |-  ( ph -> ( E. m e. ZZ ( A C_ ( ZZ>= ` 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 ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) )
34 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
35 zssre 
 |-  ZZ C_ RR
36 34 35 sstri 
 |-  ( ZZ>= ` M ) C_ RR
37 1 36 eqsstri 
 |-  Z C_ RR
38 4 37 sstrdi 
 |-  ( ph -> A C_ RR )
39 38 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> A C_ RR )
40 ltso 
 |-  < Or RR
41 soss 
 |-  ( A C_ RR -> ( < Or RR -> < Or A ) )
42 39 40 41 mpisyl 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> < Or A )
43 fzfi 
 |-  ( 1 ... m ) e. Fin
44 ovex 
 |-  ( 1 ... m ) e. _V
45 44 f1oen 
 |-  ( f : ( 1 ... m ) -1-1-onto-> A -> ( 1 ... m ) ~~ A )
46 45 adantl 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( 1 ... m ) ~~ A )
47 46 ensymd 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> A ~~ ( 1 ... m ) )
48 enfii 
 |-  ( ( ( 1 ... m ) e. Fin /\ A ~~ ( 1 ... m ) ) -> A e. Fin )
49 43 47 48 sylancr 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> A e. Fin )
50 fz1iso 
 |-  ( ( < Or A /\ A e. Fin ) -> E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
51 42 49 50 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
52 simpll 
 |-  ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> ph )
53 52 22 mpan9 
 |-  ( ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) /\ i e. A ) -> [_ i / k ]_ B e. CC )
54 fveq2 
 |-  ( n = j -> ( f ` n ) = ( f ` j ) )
55 54 csbeq1d 
 |-  ( n = j -> [_ ( f ` n ) / k ]_ B = [_ ( f ` j ) / k ]_ B )
56 csbcow 
 |-  [_ ( f ` j ) / i ]_ [_ i / k ]_ B = [_ ( f ` j ) / k ]_ B
57 55 56 eqtr4di 
 |-  ( n = j -> [_ ( f ` n ) / k ]_ B = [_ ( f ` j ) / i ]_ [_ i / k ]_ B )
58 57 cbvmptv 
 |-  ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( j e. NN |-> [_ ( f ` j ) / i ]_ [_ i / k ]_ B )
59 eqid 
 |-  ( j e. NN |-> [_ ( g ` j ) / i ]_ [_ i / k ]_ B ) = ( j e. NN |-> [_ ( g ` j ) / i ]_ [_ i / k ]_ B )
60 simplr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> m e. NN )
61 2 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> M e. ZZ )
62 27 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> A C_ ( ZZ>= ` M ) )
63 simprl 
 |-  ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> f : ( 1 ... m ) -1-1-onto-> A )
64 simprr 
 |-  ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
65 16 53 58 59 60 61 62 63 64 prodmolem2a 
 |-  ( ( ( ph /\ m e. NN ) /\ ( f : ( 1 ... m ) -1-1-onto-> A /\ g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) ) ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
66 65 expr 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
67 66 exlimdv 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( E. g g Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
68 51 67 mpd 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
69 breq2 
 |-  ( x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` 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 |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
70 68 69 syl5ibrcom 
 |-  ( ( ( ph /\ m e. NN ) /\ f : ( 1 ... m ) -1-1-onto-> A ) -> ( x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) )
71 70 expimpd 
 |-  ( ( ph /\ m e. NN ) -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) )
72 71 exlimdv 
 |-  ( ( ph /\ m e. NN ) -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) )
73 72 rexlimdva 
 |-  ( ph -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) )
74 33 73 jaod 
 |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` 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. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) )
75 2 adantr 
 |-  ( ( ph /\ seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) -> M e. ZZ )
76 4 adantr 
 |-  ( ( ph /\ seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) -> A C_ Z )
77 1 eleq2i 
 |-  ( n e. Z <-> n e. ( ZZ>= ` M ) )
78 eluzelz 
 |-  ( n e. ( ZZ>= ` M ) -> n e. ZZ )
79 78 adantl 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> n e. ZZ )
80 uztrn 
 |-  ( ( z e. ( ZZ>= ` n ) /\ n e. ( ZZ>= ` M ) ) -> z e. ( ZZ>= ` M ) )
81 80 ancoms 
 |-  ( ( n e. ( ZZ>= ` M ) /\ z e. ( ZZ>= ` n ) ) -> z e. ( ZZ>= ` M ) )
82 1 eleq2i 
 |-  ( k e. Z <-> k e. ( ZZ>= ` M ) )
83 1 34 eqsstri 
 |-  Z C_ ZZ
84 83 sseli 
 |-  ( k e. Z -> k e. ZZ )
85 iftrue 
 |-  ( k e. A -> if ( k e. A , B , 1 ) = B )
86 85 adantl 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , B , 1 ) = B )
87 86 6 eqeltrd 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , B , 1 ) e. CC )
88 87 ex 
 |-  ( ph -> ( k e. A -> if ( k e. A , B , 1 ) e. CC ) )
89 iffalse 
 |-  ( -. k e. A -> if ( k e. A , B , 1 ) = 1 )
90 ax-1cn 
 |-  1 e. CC
91 89 90 eqeltrdi 
 |-  ( -. k e. A -> if ( k e. A , B , 1 ) e. CC )
92 88 91 pm2.61d1 
 |-  ( ph -> if ( k e. A , B , 1 ) e. CC )
93 eqid 
 |-  ( k e. ZZ |-> if ( k e. A , B , 1 ) ) = ( k e. ZZ |-> if ( k e. A , B , 1 ) )
94 93 fvmpt2 
 |-  ( ( k e. ZZ /\ if ( k e. A , B , 1 ) e. CC ) -> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = if ( k e. A , B , 1 ) )
95 84 92 94 syl2anr 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = if ( k e. A , B , 1 ) )
96 5 95 eqtr4d 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) )
97 82 96 sylan2br 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) )
98 97 ralrimiva 
 |-  ( ph -> A. k e. ( ZZ>= ` M ) ( F ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) )
99 nffvmpt1 
 |-  F/_ k ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z )
100 99 nfeq2 
 |-  F/ k ( F ` z ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z )
101 fveq2 
 |-  ( k = z -> ( F ` k ) = ( F ` z ) )
102 fveq2 
 |-  ( k = z -> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) )
103 101 102 eqeq12d 
 |-  ( k = z -> ( ( F ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) <-> ( F ` z ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) ) )
104 100 103 rspc 
 |-  ( z e. ( ZZ>= ` M ) -> ( A. k e. ( ZZ>= ` M ) ( F ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) -> ( F ` z ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) ) )
105 98 104 mpan9 
 |-  ( ( ph /\ z e. ( ZZ>= ` M ) ) -> ( F ` z ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) )
106 81 105 sylan2 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ z e. ( ZZ>= ` n ) ) ) -> ( F ` z ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) )
107 106 anassrs 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` M ) ) /\ z e. ( ZZ>= ` n ) ) -> ( F ` z ) = ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) )
108 79 107 seqfeq 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> seq n ( x. , F ) = seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) )
109 108 breq1d 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( seq n ( x. , F ) ~~> y <-> seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) )
110 109 anbi2d 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) <-> ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) )
111 110 exbidv 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) <-> E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) )
112 77 111 sylan2b 
 |-  ( ( ph /\ n e. Z ) -> ( E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) <-> E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) )
113 112 rexbidva 
 |-  ( ph -> ( E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) <-> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) )
114 3 113 mpbid 
 |-  ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) )
115 114 adantr 
 |-  ( ( ph /\ seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) )
116 simpr 
 |-  ( ( ph /\ 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 ) ) ) ~~> x )
117 fveq2 
 |-  ( m = M -> ( ZZ>= ` m ) = ( ZZ>= ` M ) )
118 117 1 eqtr4di 
 |-  ( m = M -> ( ZZ>= ` m ) = Z )
119 118 sseq2d 
 |-  ( m = M -> ( A C_ ( ZZ>= ` m ) <-> A C_ Z ) )
120 118 rexeqdv 
 |-  ( m = M -> ( E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) <-> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) )
121 seqeq1 
 |-  ( m = M -> seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) = seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) )
122 121 breq1d 
 |-  ( m = 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 ) ) ) ~~> x ) )
123 119 120 122 3anbi123d 
 |-  ( m = M -> ( ( A C_ ( ZZ>= ` 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 ) <-> ( A C_ Z /\ E. n e. Z 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 ) ) )
124 123 rspcev 
 |-  ( ( M e. ZZ /\ ( A C_ Z /\ E. n e. Z 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 ) /\ 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 ) )
125 75 76 115 116 124 syl13anc 
 |-  ( ( ph /\ seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) -> E. m e. ZZ ( A C_ ( ZZ>= ` 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 ) )
126 125 orcd 
 |-  ( ( ph /\ seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) -> ( E. m e. ZZ ( A C_ ( ZZ>= ` 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. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
127 126 ex 
 |-  ( ph -> ( seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x -> ( E. m e. ZZ ( A C_ ( ZZ>= ` 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. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) )
128 74 127 impbid 
 |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` 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. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) <-> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) )
129 95 5 eqtr4d 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = ( F ` k ) )
130 82 129 sylan2br 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = ( F ` k ) )
131 130 ralrimiva 
 |-  ( ph -> A. k e. ( ZZ>= ` M ) ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = ( F ` k ) )
132 99 nfeq1 
 |-  F/ k ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) = ( F ` z )
133 102 101 eqeq12d 
 |-  ( k = z -> ( ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = ( F ` k ) <-> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) = ( F ` z ) ) )
134 132 133 rspc 
 |-  ( z e. ( ZZ>= ` M ) -> ( A. k e. ( ZZ>= ` M ) ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` k ) = ( F ` k ) -> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) = ( F ` z ) ) )
135 131 134 mpan9 
 |-  ( ( ph /\ z e. ( ZZ>= ` M ) ) -> ( ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ` z ) = ( F ` z ) )
136 2 135 seqfeq 
 |-  ( ph -> seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) = seq M ( x. , F ) )
137 136 breq1d 
 |-  ( ph -> ( seq M ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x <-> seq M ( x. , F ) ~~> x ) )
138 128 137 bitrd 
 |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` 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. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) <-> seq M ( x. , F ) ~~> x ) )
139 138 iotabidv 
 |-  ( ph -> ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` 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. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) = ( iota x seq M ( x. , F ) ~~> x ) )
140 df-prod 
 |-  prod_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` 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. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
141 df-fv 
 |-  ( ~~> ` seq M ( x. , F ) ) = ( iota x seq M ( x. , F ) ~~> x )
142 139 140 141 3eqtr4g 
 |-  ( ph -> prod_ k e. A B = ( ~~> ` seq M ( x. , F ) ) )