Metamath Proof Explorer

Theorem fprodntriv

Description: A non-triviality lemma for finite sequences. (Contributed by Scott Fenton, 16-Dec-2017)

Ref Expression
Hypotheses fprodntriv.1 
|- Z = ( ZZ>= ` M )
fprodntriv.2 
|- ( ph -> N e. Z )
fprodntriv.3 
|- ( ph -> A C_ ( M ... N ) )
Assertion fprodntriv 
|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> y ) )

Proof

Step Hyp Ref Expression
1 fprodntriv.1 
 |-  Z = ( ZZ>= ` M )
2 fprodntriv.2 
 |-  ( ph -> N e. Z )
3 fprodntriv.3 
 |-  ( ph -> A C_ ( M ... N ) )
4 2 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
5 peano2uz 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
6 4 5 syl 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )
7 6 1 eleqtrrdi 
 |-  ( ph -> ( N + 1 ) e. Z )
8 ax-1ne0 
 |-  1 =/= 0
9 eqid 
 |-  ( ZZ>= ` ( N + 1 ) ) = ( ZZ>= ` ( N + 1 ) )
10 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
11 10 1 eleq2s 
 |-  ( N e. Z -> N e. ZZ )
12 2 11 syl 
 |-  ( ph -> N e. ZZ )
13 12 peano2zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
14 seqex 
 |-  seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) e. _V
15 14 a1i 
 |-  ( ph -> seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) e. _V )
16 1cnd 
 |-  ( ph -> 1 e. CC )
17 simpr 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> n e. ( ZZ>= ` ( N + 1 ) ) )
18 3 ad2antrr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> A C_ ( M ... N ) )
19 12 ad2antrr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> N e. ZZ )
20 19 zred 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> N e. RR )
21 19 peano2zd 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> ( N + 1 ) e. ZZ )
22 21 zred 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> ( N + 1 ) e. RR )
23 elfzelz 
 |-  ( m e. ( ( N + 1 ) ... n ) -> m e. ZZ )
24 23 adantl 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> m e. ZZ )
25 24 zred 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> m e. RR )
26 20 ltp1d 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> N < ( N + 1 ) )
27 elfzle1 
 |-  ( m e. ( ( N + 1 ) ... n ) -> ( N + 1 ) <_ m )
28 27 adantl 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> ( N + 1 ) <_ m )
29 20 22 25 26 28 ltletrd 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> N < m )
30 20 25 ltnled 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> ( N < m <-> -. m <_ N ) )
31 29 30 mpbid 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> -. m <_ N )
32 31 intnand 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> -. ( M <_ m /\ m <_ N ) )
33 32 intnand 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> -. ( ( M e. ZZ /\ N e. ZZ /\ m e. ZZ ) /\ ( M <_ m /\ m <_ N ) ) )
34 elfz2 
 |-  ( m e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ /\ m e. ZZ ) /\ ( M <_ m /\ m <_ N ) ) )
35 33 34 sylnibr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> -. m e. ( M ... N ) )
36 18 35 ssneldd 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> -. m e. A )
37 36 iffalsed 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> if ( m e. A , [_ m / k ]_ B , 1 ) = 1 )
38 fzssuz 
 |-  ( ( N + 1 ) ... n ) C_ ( ZZ>= ` ( N + 1 ) )
39 6 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
40 uzss 
 |-  ( ( N + 1 ) e. ( ZZ>= ` M ) -> ( ZZ>= ` ( N + 1 ) ) C_ ( ZZ>= ` M ) )
41 39 40 syl 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ZZ>= ` ( N + 1 ) ) C_ ( ZZ>= ` M ) )
42 41 1 sseqtrrdi 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ZZ>= ` ( N + 1 ) ) C_ Z )
43 38 42 sstrid 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> ( ( N + 1 ) ... n ) C_ Z )
44 43 sselda 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> m e. Z )
45 ax-1cn 
 |-  1 e. CC
46 37 45 eqeltrdi 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> if ( m e. A , [_ m / k ]_ B , 1 ) e. CC )
47 nfcv 
 |-  F/_ k m
48 nfv 
 |-  F/ k m e. A
49 nfcsb1v 
 |-  F/_ k [_ m / k ]_ B
50 nfcv 
 |-  F/_ k 1
51 48 49 50 nfif 
 |-  F/_ k if ( m e. A , [_ m / k ]_ B , 1 )
52 eleq1w 
 |-  ( k = m -> ( k e. A <-> m e. A ) )
53 csbeq1a 
 |-  ( k = m -> B = [_ m / k ]_ B )
54 52 53 ifbieq1d 
 |-  ( k = m -> if ( k e. A , B , 1 ) = if ( m e. A , [_ m / k ]_ B , 1 ) )
55 eqid 
 |-  ( k e. Z |-> if ( k e. A , B , 1 ) ) = ( k e. Z |-> if ( k e. A , B , 1 ) )
56 47 51 54 55 fvmptf 
 |-  ( ( m e. Z /\ if ( m e. A , [_ m / k ]_ B , 1 ) e. CC ) -> ( ( k e. Z |-> if ( k e. A , B , 1 ) ) ` m ) = if ( m e. A , [_ m / k ]_ B , 1 ) )
57 44 46 56 syl2anc 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> ( ( k e. Z |-> if ( k e. A , B , 1 ) ) ` m ) = if ( m e. A , [_ m / k ]_ B , 1 ) )
58 elfzuz 
 |-  ( m e. ( ( N + 1 ) ... n ) -> m e. ( ZZ>= ` ( N + 1 ) ) )
59 58 adantl 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> m e. ( ZZ>= ` ( N + 1 ) ) )
60 1ex 
 |-  1 e. _V
61 60 fvconst2 
 |-  ( m e. ( ZZ>= ` ( N + 1 ) ) -> ( ( ( ZZ>= ` ( N + 1 ) ) X. { 1 } ) ` m ) = 1 )
62 59 61 syl 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> ( ( ( ZZ>= ` ( N + 1 ) ) X. { 1 } ) ` m ) = 1 )
63 37 57 62 3eqtr4d 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> ( ( k e. Z |-> if ( k e. A , B , 1 ) ) ` m ) = ( ( ( ZZ>= ` ( N + 1 ) ) X. { 1 } ) ` m ) )
64 17 63 seqfveq 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ` n ) = ( seq ( N + 1 ) ( x. , ( ( ZZ>= ` ( N + 1 ) ) X. { 1 } ) ) ` n ) )
65 9 prodf1 
 |-  ( n e. ( ZZ>= ` ( N + 1 ) ) -> ( seq ( N + 1 ) ( x. , ( ( ZZ>= ` ( N + 1 ) ) X. { 1 } ) ) ` n ) = 1 )
66 65 adantl 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq ( N + 1 ) ( x. , ( ( ZZ>= ` ( N + 1 ) ) X. { 1 } ) ) ` n ) = 1 )
67 64 66 eqtrd 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ` n ) = 1 )
68 9 13 15 16 67 climconst 
 |-  ( ph -> seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> 1 )
69 neeq1 
 |-  ( y = 1 -> ( y =/= 0 <-> 1 =/= 0 ) )
70 breq2 
 |-  ( y = 1 -> ( seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> y <-> seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> 1 ) )
71 69 70 anbi12d 
 |-  ( y = 1 -> ( ( y =/= 0 /\ seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> y ) <-> ( 1 =/= 0 /\ seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> 1 ) ) )
72 60 71 spcev 
 |-  ( ( 1 =/= 0 /\ seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> 1 ) -> E. y ( y =/= 0 /\ seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> y ) )
73 8 68 72 sylancr 
 |-  ( ph -> E. y ( y =/= 0 /\ seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> y ) )
74 seqeq1 
 |-  ( n = ( N + 1 ) -> seq n ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) = seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) )
75 74 breq1d 
 |-  ( n = ( N + 1 ) -> ( seq n ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> y <-> seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> y ) )
76 75 anbi2d 
 |-  ( n = ( N + 1 ) -> ( ( y =/= 0 /\ seq n ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> y ) <-> ( y =/= 0 /\ seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) )
77 76 exbidv 
 |-  ( n = ( N + 1 ) -> ( E. y ( y =/= 0 /\ seq n ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> y ) <-> E. y ( y =/= 0 /\ seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) )
78 77 rspcev 
 |-  ( ( ( N + 1 ) e. Z /\ E. y ( y =/= 0 /\ seq ( N + 1 ) ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> y ) ) -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> y ) )
79 7 73 78 syl2anc 
 |-  ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. Z |-> if ( k e. A , B , 1 ) ) ) ~~> y ) )