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=ℤ≥M
fprodntriv.2 ⊢φ→N∈Z
fprodntriv.3 ⊢φ→A⊆M…N
Assertion fprodntriv ⊢φ→∃n∈Z∃yy≠0∧seqn×k∈Z⟼ifk∈AB1⇝y

Proof

Step Hyp Ref Expression
1 fprodntriv.1 ⊢Z=ℤ≥M
2 fprodntriv.2 ⊢φ→N∈Z
3 fprodntriv.3 ⊢φ→A⊆M…N
4 2 1 eleqtrdi ⊢φ→N∈ℤ≥M
5 peano2uz ⊢N∈ℤ≥M→N+1∈ℤ≥M
6 4 5 syl ⊢φ→N+1∈ℤ≥M
7 6 1 eleqtrrdi ⊢φ→N+1∈Z
8 ax-1ne0 ⊢1≠0
9 eqid ⊢ℤ≥N+1=ℤ≥N+1
10 eluzelz ⊢N∈ℤ≥M→N∈ℤ
11 10 1 eleq2s ⊢N∈Z→N∈ℤ
12 2 11 syl ⊢φ→N∈ℤ
13 12 peano2zd ⊢φ→N+1∈ℤ
14 seqex ⊢seqN+1×k∈Z⟼ifk∈AB1∈V
15 14 a1i ⊢φ→seqN+1×k∈Z⟼ifk∈AB1∈V
16 1cnd ⊢φ→1∈ℂ
17 simpr ⊢φ∧n∈ℤ≥N+1→n∈ℤ≥N+1
18 3 ad2antrr ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→A⊆M…N
19 12 ad2antrr ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→N∈ℤ
20 19 zred ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→N∈ℝ
21 19 peano2zd ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→N+1∈ℤ
22 21 zred ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→N+1∈ℝ
23 elfzelz ⊢m∈N+1…n→m∈ℤ
24 23 adantl ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→m∈ℤ
25 24 zred ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→m∈ℝ
26 20 ltp1d ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→N<N+1
27 elfzle1 ⊢m∈N+1…n→N+1≤m
28 27 adantl ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→N+1≤m
29 20 22 25 26 28 ltletrd ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→N<m
30 20 25 ltnled ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→N<m↔¬m≤N
31 29 30 mpbid ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→¬m≤N
32 31 intnand ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→¬M≤m∧m≤N
33 32 intnand ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→¬M∈ℤ∧N∈ℤ∧m∈ℤ∧M≤m∧m≤N
34 elfz2 ⊢m∈M…N↔M∈ℤ∧N∈ℤ∧m∈ℤ∧M≤m∧m≤N
35 33 34 sylnibr ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→¬m∈M…N
36 18 35 ssneldd ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→¬m∈A
37 36 iffalsed ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→ifm∈A⦋m/k⦌B1=1
38 fzssuz ⊢N+1…n⊆ℤ≥N+1
39 6 adantr ⊢φ∧n∈ℤ≥N+1→N+1∈ℤ≥M
40 uzss ⊢N+1∈ℤ≥M→ℤ≥N+1⊆ℤ≥M
41 39 40 syl ⊢φ∧n∈ℤ≥N+1→ℤ≥N+1⊆ℤ≥M
42 41 1 sseqtrrdi ⊢φ∧n∈ℤ≥N+1→ℤ≥N+1⊆Z
43 38 42 sstrid ⊢φ∧n∈ℤ≥N+1→N+1…n⊆Z
44 43 sselda ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→m∈Z
45 ax-1cn ⊢1∈ℂ
46 37 45 eqeltrdi ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→ifm∈A⦋m/k⦌B1∈ℂ
47 nfcv ⊢Ⅎ_km
48 nfv ⊢Ⅎkm∈A
49 nfcsb1v ⊢Ⅎ_k⦋m/k⦌B
50 nfcv ⊢Ⅎ_k1
51 48 49 50 nfif ⊢Ⅎ_kifm∈A⦋m/k⦌B1
52 eleq1w ⊢k=m→k∈A↔m∈A
53 csbeq1a ⊢k=m→B=⦋m/k⦌B
54 52 53 ifbieq1d ⊢k=m→ifk∈AB1=ifm∈A⦋m/k⦌B1
55 eqid ⊢k∈Z⟼ifk∈AB1=k∈Z⟼ifk∈AB1
56 47 51 54 55 fvmptf ⊢m∈Z∧ifm∈A⦋m/k⦌B1∈ℂ→k∈Z⟼ifk∈AB1⁡m=ifm∈A⦋m/k⦌B1
57 44 46 56 syl2anc ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→k∈Z⟼ifk∈AB1⁡m=ifm∈A⦋m/k⦌B1
58 elfzuz ⊢m∈N+1…n→m∈ℤ≥N+1
59 58 adantl ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→m∈ℤ≥N+1
60 1ex ⊢1∈V
61 60 fvconst2 ⊢m∈ℤ≥N+1→ℤ≥N+1×1⁡m=1
62 59 61 syl ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→ℤ≥N+1×1⁡m=1
63 37 57 62 3eqtr4d ⊢φ∧n∈ℤ≥N+1∧m∈N+1…n→k∈Z⟼ifk∈AB1⁡m=ℤ≥N+1×1⁡m
64 17 63 seqfveq ⊢φ∧n∈ℤ≥N+1→seqN+1×k∈Z⟼ifk∈AB1⁡n=seqN+1×ℤ≥N+1×1⁡n
65 9 prodf1 ⊢n∈ℤ≥N+1→seqN+1×ℤ≥N+1×1⁡n=1
66 65 adantl ⊢φ∧n∈ℤ≥N+1→seqN+1×ℤ≥N+1×1⁡n=1
67 64 66 eqtrd ⊢φ∧n∈ℤ≥N+1→seqN+1×k∈Z⟼ifk∈AB1⁡n=1
68 9 13 15 16 67 climconst ⊢φ→seqN+1×k∈Z⟼ifk∈AB1⇝1
69 neeq1 ⊢y=1→y≠0↔1≠0
70 breq2 ⊢y=1→seqN+1×k∈Z⟼ifk∈AB1⇝y↔seqN+1×k∈Z⟼ifk∈AB1⇝1
71 69 70 anbi12d ⊢y=1→y≠0∧seqN+1×k∈Z⟼ifk∈AB1⇝y↔1≠0∧seqN+1×k∈Z⟼ifk∈AB1⇝1
72 60 71 spcev ⊢1≠0∧seqN+1×k∈Z⟼ifk∈AB1⇝1→∃yy≠0∧seqN+1×k∈Z⟼ifk∈AB1⇝y
73 8 68 72 sylancr ⊢φ→∃yy≠0∧seqN+1×k∈Z⟼ifk∈AB1⇝y
74 seqeq1 ⊢n=N+1→seqn×k∈Z⟼ifk∈AB1=seqN+1×k∈Z⟼ifk∈AB1
75 74 breq1d ⊢n=N+1→seqn×k∈Z⟼ifk∈AB1⇝y↔seqN+1×k∈Z⟼ifk∈AB1⇝y
76 75 anbi2d ⊢n=N+1→y≠0∧seqn×k∈Z⟼ifk∈AB1⇝y↔y≠0∧seqN+1×k∈Z⟼ifk∈AB1⇝y
77 76 exbidv ⊢n=N+1→∃yy≠0∧seqn×k∈Z⟼ifk∈AB1⇝y↔∃yy≠0∧seqN+1×k∈Z⟼ifk∈AB1⇝y
78 77 rspcev ⊢N+1∈Z∧∃yy≠0∧seqN+1×k∈Z⟼ifk∈AB1⇝y→∃n∈Z∃yy≠0∧seqn×k∈Z⟼ifk∈AB1⇝y
79 7 73 78 syl2anc ⊢φ→∃n∈Z∃yy≠0∧seqn×k∈Z⟼ifk∈AB1⇝y