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 𝑍 = ( ℤ𝑀 )
fprodntriv.2 ( 𝜑𝑁𝑍 )
fprodntriv.3 ( 𝜑𝐴 ⊆ ( 𝑀 ... 𝑁 ) )
Assertion fprodntriv ( 𝜑 → ∃ 𝑛𝑍𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 fprodntriv.1 𝑍 = ( ℤ𝑀 )
2 fprodntriv.2 ( 𝜑𝑁𝑍 )
3 fprodntriv.3 ( 𝜑𝐴 ⊆ ( 𝑀 ... 𝑁 ) )
4 2 1 eleqtrdi ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
5 peano2uz ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ𝑀 ) )
6 4 5 syl ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ𝑀 ) )
7 6 1 eleqtrrdi ( 𝜑 → ( 𝑁 + 1 ) ∈ 𝑍 )
8 ax-1ne0 1 ≠ 0
9 eqid ( ℤ ‘ ( 𝑁 + 1 ) ) = ( ℤ ‘ ( 𝑁 + 1 ) )
10 eluzelz ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑁 ∈ ℤ )
11 10 1 eleq2s ( 𝑁𝑍𝑁 ∈ ℤ )
12 2 11 syl ( 𝜑𝑁 ∈ ℤ )
13 12 peano2zd ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
14 seqex seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ∈ V
15 14 a1i ( 𝜑 → seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ∈ V )
16 1cnd ( 𝜑 → 1 ∈ ℂ )
17 simpr ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) → 𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) )
18 3 ad2antrr ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → 𝐴 ⊆ ( 𝑀 ... 𝑁 ) )
19 12 ad2antrr ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → 𝑁 ∈ ℤ )
20 19 zred ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → 𝑁 ∈ ℝ )
21 19 peano2zd ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ( 𝑁 + 1 ) ∈ ℤ )
22 21 zred ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ( 𝑁 + 1 ) ∈ ℝ )
23 elfzelz ( 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) → 𝑚 ∈ ℤ )
24 23 adantl ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → 𝑚 ∈ ℤ )
25 24 zred ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → 𝑚 ∈ ℝ )
26 20 ltp1d ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → 𝑁 < ( 𝑁 + 1 ) )
27 elfzle1 ( 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) → ( 𝑁 + 1 ) ≤ 𝑚 )
28 27 adantl ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ( 𝑁 + 1 ) ≤ 𝑚 )
29 20 22 25 26 28 ltletrd ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → 𝑁 < 𝑚 )
30 20 25 ltnled ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ( 𝑁 < 𝑚 ↔ ¬ 𝑚𝑁 ) )
31 29 30 mpbid ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ¬ 𝑚𝑁 )
32 31 intnand ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ¬ ( 𝑀𝑚𝑚𝑁 ) )
33 32 intnand ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ¬ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑀𝑚𝑚𝑁 ) ) )
34 elfz2 ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑀𝑚𝑚𝑁 ) ) )
35 33 34 sylnibr ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ¬ 𝑚 ∈ ( 𝑀 ... 𝑁 ) )
36 18 35 ssneldd ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ¬ 𝑚𝐴 )
37 36 iffalsed ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → if ( 𝑚𝐴 , 𝑚 / 𝑘 𝐵 , 1 ) = 1 )
38 fzssuz ( ( 𝑁 + 1 ) ... 𝑛 ) ⊆ ( ℤ ‘ ( 𝑁 + 1 ) )
39 6 adantr ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) → ( 𝑁 + 1 ) ∈ ( ℤ𝑀 ) )
40 uzss ( ( 𝑁 + 1 ) ∈ ( ℤ𝑀 ) → ( ℤ ‘ ( 𝑁 + 1 ) ) ⊆ ( ℤ𝑀 ) )
41 39 40 syl ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) → ( ℤ ‘ ( 𝑁 + 1 ) ) ⊆ ( ℤ𝑀 ) )
42 41 1 sseqtrrdi ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) → ( ℤ ‘ ( 𝑁 + 1 ) ) ⊆ 𝑍 )
43 38 42 sstrid ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) ... 𝑛 ) ⊆ 𝑍 )
44 43 sselda ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → 𝑚𝑍 )
45 ax-1cn 1 ∈ ℂ
46 37 45 eqeltrdi ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → if ( 𝑚𝐴 , 𝑚 / 𝑘 𝐵 , 1 ) ∈ ℂ )
47 nfcv 𝑘 𝑚
48 nfv 𝑘 𝑚𝐴
49 nfcsb1v 𝑘 𝑚 / 𝑘 𝐵
50 nfcv 𝑘 1
51 48 49 50 nfif 𝑘 if ( 𝑚𝐴 , 𝑚 / 𝑘 𝐵 , 1 )
52 eleq1w ( 𝑘 = 𝑚 → ( 𝑘𝐴𝑚𝐴 ) )
53 csbeq1a ( 𝑘 = 𝑚𝐵 = 𝑚 / 𝑘 𝐵 )
54 52 53 ifbieq1d ( 𝑘 = 𝑚 → if ( 𝑘𝐴 , 𝐵 , 1 ) = if ( 𝑚𝐴 , 𝑚 / 𝑘 𝐵 , 1 ) )
55 eqid ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) = ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) )
56 47 51 54 55 fvmptf ( ( 𝑚𝑍 ∧ if ( 𝑚𝐴 , 𝑚 / 𝑘 𝐵 , 1 ) ∈ ℂ ) → ( ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ‘ 𝑚 ) = if ( 𝑚𝐴 , 𝑚 / 𝑘 𝐵 , 1 ) )
57 44 46 56 syl2anc ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ( ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ‘ 𝑚 ) = if ( 𝑚𝐴 , 𝑚 / 𝑘 𝐵 , 1 ) )
58 elfzuz ( 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) → 𝑚 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) )
59 58 adantl ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → 𝑚 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) )
60 1ex 1 ∈ V
61 60 fvconst2 ( 𝑚 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) → ( ( ( ℤ ‘ ( 𝑁 + 1 ) ) × { 1 } ) ‘ 𝑚 ) = 1 )
62 59 61 syl ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ( ( ( ℤ ‘ ( 𝑁 + 1 ) ) × { 1 } ) ‘ 𝑚 ) = 1 )
63 37 57 62 3eqtr4d ( ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ( ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ‘ 𝑚 ) = ( ( ( ℤ ‘ ( 𝑁 + 1 ) ) × { 1 } ) ‘ 𝑚 ) )
64 17 63 seqfveq ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) → ( seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ‘ 𝑛 ) = ( seq ( 𝑁 + 1 ) ( · , ( ( ℤ ‘ ( 𝑁 + 1 ) ) × { 1 } ) ) ‘ 𝑛 ) )
65 9 prodf1 ( 𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) → ( seq ( 𝑁 + 1 ) ( · , ( ( ℤ ‘ ( 𝑁 + 1 ) ) × { 1 } ) ) ‘ 𝑛 ) = 1 )
66 65 adantl ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) → ( seq ( 𝑁 + 1 ) ( · , ( ( ℤ ‘ ( 𝑁 + 1 ) ) × { 1 } ) ) ‘ 𝑛 ) = 1 )
67 64 66 eqtrd ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) → ( seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ‘ 𝑛 ) = 1 )
68 9 13 15 16 67 climconst ( 𝜑 → seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 1 )
69 neeq1 ( 𝑦 = 1 → ( 𝑦 ≠ 0 ↔ 1 ≠ 0 ) )
70 breq2 ( 𝑦 = 1 → ( seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ↔ seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 1 ) )
71 69 70 anbi12d ( 𝑦 = 1 → ( ( 𝑦 ≠ 0 ∧ seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ( 1 ≠ 0 ∧ seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 1 ) ) )
72 60 71 spcev ( ( 1 ≠ 0 ∧ seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 1 ) → ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) )
73 8 68 72 sylancr ( 𝜑 → ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) )
74 seqeq1 ( 𝑛 = ( 𝑁 + 1 ) → seq 𝑛 ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) = seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) )
75 74 breq1d ( 𝑛 = ( 𝑁 + 1 ) → ( seq 𝑛 ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ↔ seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) )
76 75 anbi2d ( 𝑛 = ( 𝑁 + 1 ) → ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ( 𝑦 ≠ 0 ∧ seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ) )
77 76 exbidv ( 𝑛 = ( 𝑁 + 1 ) → ( ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ) )
78 77 rspcev ( ( ( 𝑁 + 1 ) ∈ 𝑍 ∧ ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq ( 𝑁 + 1 ) ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ) → ∃ 𝑛𝑍𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) )
79 7 73 78 syl2anc ( 𝜑 → ∃ 𝑛𝑍𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘𝑍 ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) )