Metamath Proof Explorer


Theorem fprodeq0

Description: Any finite product containing a zero term is itself zero. (Contributed by Scott Fenton, 27-Dec-2017)

Ref Expression
Hypotheses fprodeq0.1 Z = M
fprodeq0.2 φ N Z
fprodeq0.3 φ k Z A
fprodeq0.4 φ k = N A = 0
Assertion fprodeq0 φ K N k = M K A = 0

Proof

Step Hyp Ref Expression
1 fprodeq0.1 Z = M
2 fprodeq0.2 φ N Z
3 fprodeq0.3 φ k Z A
4 fprodeq0.4 φ k = N A = 0
5 eluzel2 K N N
6 5 adantl φ K N N
7 6 zred φ K N N
8 7 ltp1d φ K N N < N + 1
9 fzdisj N < N + 1 M N N + 1 K =
10 8 9 syl φ K N M N N + 1 K =
11 eluzel2 N M M
12 11 1 eleq2s N Z M
13 2 12 syl φ M
14 13 adantr φ K N M
15 eluzelz K N K
16 15 adantl φ K N K
17 14 16 6 3jca φ K N M K N
18 eluzle N M M N
19 18 1 eleq2s N Z M N
20 2 19 syl φ M N
21 eluzle K N N K
22 20 21 anim12i φ K N M N N K
23 elfz2 N M K M K N M N N K
24 17 22 23 sylanbrc φ K N N M K
25 fzsplit N M K M K = M N N + 1 K
26 24 25 syl φ K N M K = M N N + 1 K
27 fzfid φ K N M K Fin
28 elfzuz k M K k M
29 28 1 eleqtrrdi k M K k Z
30 29 3 sylan2 φ k M K A
31 30 adantlr φ K N k M K A
32 10 26 27 31 fprodsplit φ K N k = M K A = k = M N A k = N + 1 K A
33 2 1 eleqtrdi φ N M
34 elfzuz k M N k M
35 34 1 eleqtrrdi k M N k Z
36 35 3 sylan2 φ k M N A
37 33 36 fprodm1s φ k = M N A = k = M N 1 A N / k A
38 2 4 csbied φ N / k A = 0
39 38 oveq2d φ k = M N 1 A N / k A = k = M N 1 A 0
40 fzfid φ M N 1 Fin
41 elfzuz k M N 1 k M
42 41 1 eleqtrrdi k M N 1 k Z
43 42 3 sylan2 φ k M N 1 A
44 40 43 fprodcl φ k = M N 1 A
45 44 mul01d φ k = M N 1 A 0 = 0
46 37 39 45 3eqtrd φ k = M N A = 0
47 46 adantr φ K N k = M N A = 0
48 47 oveq1d φ K N k = M N A k = N + 1 K A = 0 k = N + 1 K A
49 fzfid φ K N N + 1 K Fin
50 1 peano2uzs N Z N + 1 Z
51 2 50 syl φ N + 1 Z
52 elfzuz k N + 1 K k N + 1
53 1 uztrn2 N + 1 Z k N + 1 k Z
54 51 52 53 syl2an φ k N + 1 K k Z
55 54 adantrl φ K N k N + 1 K k Z
56 55 3 syldan φ K N k N + 1 K A
57 56 anassrs φ K N k N + 1 K A
58 49 57 fprodcl φ K N k = N + 1 K A
59 58 mul02d φ K N 0 k = N + 1 K A = 0
60 32 48 59 3eqtrd φ K N k = M K A = 0