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