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 ) ) )