# Metamath Proof Explorer

## Theorem prodfzo03

Description: A product of three factors, indexed starting with zero. (Contributed by Thierry Arnoux, 14-Dec-2021)

Ref Expression
Hypotheses prodfzo03.1 ${⊢}{k}=0\to {D}={A}$
prodfzo03.2 ${⊢}{k}=1\to {D}={B}$
prodfzo03.3 ${⊢}{k}=2\to {D}={C}$
prodfzo03.a ${⊢}\left({\phi }\wedge {k}\in \left(0..^3\right)\right)\to {D}\in ℂ$
Assertion prodfzo03 ${⊢}{\phi }\to \prod _{{k}\in \left(0..^3\right)}{D}={A}{B}{C}$

### Proof

Step Hyp Ref Expression
1 prodfzo03.1 ${⊢}{k}=0\to {D}={A}$
2 prodfzo03.2 ${⊢}{k}=1\to {D}={B}$
3 prodfzo03.3 ${⊢}{k}=2\to {D}={C}$
4 prodfzo03.a ${⊢}\left({\phi }\wedge {k}\in \left(0..^3\right)\right)\to {D}\in ℂ$
5 fzodisjsn ${⊢}\left(0..^2\right)\cap \left\{2\right\}=\varnothing$
6 5 a1i ${⊢}{\phi }\to \left(0..^2\right)\cap \left\{2\right\}=\varnothing$
7 2p1e3 ${⊢}2+1=3$
8 7 oveq2i ${⊢}\left(0..^2+1\right)=\left(0..^3\right)$
9 2eluzge0 ${⊢}2\in {ℤ}_{\ge 0}$
10 fzosplitsn ${⊢}2\in {ℤ}_{\ge 0}\to \left(0..^2+1\right)=\left(0..^2\right)\cup \left\{2\right\}$
11 9 10 ax-mp ${⊢}\left(0..^2+1\right)=\left(0..^2\right)\cup \left\{2\right\}$
12 8 11 eqtr3i ${⊢}\left(0..^3\right)=\left(0..^2\right)\cup \left\{2\right\}$
13 12 a1i ${⊢}{\phi }\to \left(0..^3\right)=\left(0..^2\right)\cup \left\{2\right\}$
14 fzofi ${⊢}\left(0..^3\right)\in \mathrm{Fin}$
15 14 a1i ${⊢}{\phi }\to \left(0..^3\right)\in \mathrm{Fin}$
16 6 13 15 4 fprodsplit ${⊢}{\phi }\to \prod _{{k}\in \left(0..^3\right)}{D}=\prod _{{k}\in \left(0..^2\right)}{D}\prod _{{k}\in \left\{2\right\}}{D}$
17 0ne1 ${⊢}0\ne 1$
18 disjsn2 ${⊢}0\ne 1\to \left\{0\right\}\cap \left\{1\right\}=\varnothing$
19 17 18 mp1i ${⊢}{\phi }\to \left\{0\right\}\cap \left\{1\right\}=\varnothing$
20 fzo0to2pr ${⊢}\left(0..^2\right)=\left\{0,1\right\}$
21 df-pr ${⊢}\left\{0,1\right\}=\left\{0\right\}\cup \left\{1\right\}$
22 20 21 eqtri ${⊢}\left(0..^2\right)=\left\{0\right\}\cup \left\{1\right\}$
23 22 a1i ${⊢}{\phi }\to \left(0..^2\right)=\left\{0\right\}\cup \left\{1\right\}$
24 fzofi ${⊢}\left(0..^2\right)\in \mathrm{Fin}$
25 24 a1i ${⊢}{\phi }\to \left(0..^2\right)\in \mathrm{Fin}$
26 2z ${⊢}2\in ℤ$
27 3z ${⊢}3\in ℤ$
28 2re ${⊢}2\in ℝ$
29 3re ${⊢}3\in ℝ$
30 2lt3 ${⊢}2<3$
31 28 29 30 ltleii ${⊢}2\le 3$
32 eluz2 ${⊢}3\in {ℤ}_{\ge 2}↔\left(2\in ℤ\wedge 3\in ℤ\wedge 2\le 3\right)$
33 26 27 31 32 mpbir3an ${⊢}3\in {ℤ}_{\ge 2}$
34 fzoss2 ${⊢}3\in {ℤ}_{\ge 2}\to \left(0..^2\right)\subseteq \left(0..^3\right)$
35 33 34 ax-mp ${⊢}\left(0..^2\right)\subseteq \left(0..^3\right)$
36 35 sseli ${⊢}{k}\in \left(0..^2\right)\to {k}\in \left(0..^3\right)$
37 36 4 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left(0..^2\right)\right)\to {D}\in ℂ$
38 19 23 25 37 fprodsplit ${⊢}{\phi }\to \prod _{{k}\in \left(0..^2\right)}{D}=\prod _{{k}\in \left\{0\right\}}{D}\prod _{{k}\in \left\{1\right\}}{D}$
39 38 oveq1d ${⊢}{\phi }\to \prod _{{k}\in \left(0..^2\right)}{D}\prod _{{k}\in \left\{2\right\}}{D}=\prod _{{k}\in \left\{0\right\}}{D}\prod _{{k}\in \left\{1\right\}}{D}\prod _{{k}\in \left\{2\right\}}{D}$
40 16 39 eqtrd ${⊢}{\phi }\to \prod _{{k}\in \left(0..^3\right)}{D}=\prod _{{k}\in \left\{0\right\}}{D}\prod _{{k}\in \left\{1\right\}}{D}\prod _{{k}\in \left\{2\right\}}{D}$
41 snfi ${⊢}\left\{0\right\}\in \mathrm{Fin}$
42 41 a1i ${⊢}{\phi }\to \left\{0\right\}\in \mathrm{Fin}$
43 velsn ${⊢}{k}\in \left\{0\right\}↔{k}=0$
44 1 adantl ${⊢}\left({\phi }\wedge {k}=0\right)\to {D}={A}$
45 simpr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^3\right)\right)\wedge {D}={A}\right)\to {D}={A}$
46 4 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^3\right)\right)\wedge {D}={A}\right)\to {D}\in ℂ$
47 45 46 eqeltrrd ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^3\right)\right)\wedge {D}={A}\right)\to {A}\in ℂ$
48 c0ex ${⊢}0\in \mathrm{V}$
49 48 tpid1 ${⊢}0\in \left\{0,1,2\right\}$
50 fzo0to3tp ${⊢}\left(0..^3\right)=\left\{0,1,2\right\}$
51 49 50 eleqtrri ${⊢}0\in \left(0..^3\right)$
52 eqid ${⊢}{A}={A}$
53 1 eqeq1d ${⊢}{k}=0\to \left({D}={A}↔{A}={A}\right)$
54 53 rspcev ${⊢}\left(0\in \left(0..^3\right)\wedge {A}={A}\right)\to \exists {k}\in \left(0..^3\right)\phantom{\rule{.4em}{0ex}}{D}={A}$
55 51 52 54 mp2an ${⊢}\exists {k}\in \left(0..^3\right)\phantom{\rule{.4em}{0ex}}{D}={A}$
56 55 a1i ${⊢}{\phi }\to \exists {k}\in \left(0..^3\right)\phantom{\rule{.4em}{0ex}}{D}={A}$
57 47 56 r19.29a ${⊢}{\phi }\to {A}\in ℂ$
58 57 adantr ${⊢}\left({\phi }\wedge {k}=0\right)\to {A}\in ℂ$
59 44 58 eqeltrd ${⊢}\left({\phi }\wedge {k}=0\right)\to {D}\in ℂ$
60 43 59 sylan2b ${⊢}\left({\phi }\wedge {k}\in \left\{0\right\}\right)\to {D}\in ℂ$
61 42 60 fprodcl ${⊢}{\phi }\to \prod _{{k}\in \left\{0\right\}}{D}\in ℂ$
62 snfi ${⊢}\left\{1\right\}\in \mathrm{Fin}$
63 62 a1i ${⊢}{\phi }\to \left\{1\right\}\in \mathrm{Fin}$
64 velsn ${⊢}{k}\in \left\{1\right\}↔{k}=1$
65 2 adantl ${⊢}\left({\phi }\wedge {k}=1\right)\to {D}={B}$
66 simpr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^3\right)\right)\wedge {D}={B}\right)\to {D}={B}$
67 4 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^3\right)\right)\wedge {D}={B}\right)\to {D}\in ℂ$
68 66 67 eqeltrrd ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^3\right)\right)\wedge {D}={B}\right)\to {B}\in ℂ$
69 1ex ${⊢}1\in \mathrm{V}$
70 69 tpid2 ${⊢}1\in \left\{0,1,2\right\}$
71 70 50 eleqtrri ${⊢}1\in \left(0..^3\right)$
72 eqid ${⊢}{B}={B}$
73 2 eqeq1d ${⊢}{k}=1\to \left({D}={B}↔{B}={B}\right)$
74 73 rspcev ${⊢}\left(1\in \left(0..^3\right)\wedge {B}={B}\right)\to \exists {k}\in \left(0..^3\right)\phantom{\rule{.4em}{0ex}}{D}={B}$
75 71 72 74 mp2an ${⊢}\exists {k}\in \left(0..^3\right)\phantom{\rule{.4em}{0ex}}{D}={B}$
76 75 a1i ${⊢}{\phi }\to \exists {k}\in \left(0..^3\right)\phantom{\rule{.4em}{0ex}}{D}={B}$
77 68 76 r19.29a ${⊢}{\phi }\to {B}\in ℂ$
78 77 adantr ${⊢}\left({\phi }\wedge {k}=1\right)\to {B}\in ℂ$
79 65 78 eqeltrd ${⊢}\left({\phi }\wedge {k}=1\right)\to {D}\in ℂ$
80 64 79 sylan2b ${⊢}\left({\phi }\wedge {k}\in \left\{1\right\}\right)\to {D}\in ℂ$
81 63 80 fprodcl ${⊢}{\phi }\to \prod _{{k}\in \left\{1\right\}}{D}\in ℂ$
82 snfi ${⊢}\left\{2\right\}\in \mathrm{Fin}$
83 82 a1i ${⊢}{\phi }\to \left\{2\right\}\in \mathrm{Fin}$
84 velsn ${⊢}{k}\in \left\{2\right\}↔{k}=2$
85 3 adantl ${⊢}\left({\phi }\wedge {k}=2\right)\to {D}={C}$
86 simpr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^3\right)\right)\wedge {D}={C}\right)\to {D}={C}$
87 4 adantr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^3\right)\right)\wedge {D}={C}\right)\to {D}\in ℂ$
88 86 87 eqeltrrd ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^3\right)\right)\wedge {D}={C}\right)\to {C}\in ℂ$
89 2ex ${⊢}2\in \mathrm{V}$
90 89 tpid3 ${⊢}2\in \left\{0,1,2\right\}$
91 90 50 eleqtrri ${⊢}2\in \left(0..^3\right)$
92 eqid ${⊢}{C}={C}$
93 3 eqeq1d ${⊢}{k}=2\to \left({D}={C}↔{C}={C}\right)$
94 93 rspcev ${⊢}\left(2\in \left(0..^3\right)\wedge {C}={C}\right)\to \exists {k}\in \left(0..^3\right)\phantom{\rule{.4em}{0ex}}{D}={C}$
95 91 92 94 mp2an ${⊢}\exists {k}\in \left(0..^3\right)\phantom{\rule{.4em}{0ex}}{D}={C}$
96 95 a1i ${⊢}{\phi }\to \exists {k}\in \left(0..^3\right)\phantom{\rule{.4em}{0ex}}{D}={C}$
97 88 96 r19.29a ${⊢}{\phi }\to {C}\in ℂ$
98 97 adantr ${⊢}\left({\phi }\wedge {k}=2\right)\to {C}\in ℂ$
99 85 98 eqeltrd ${⊢}\left({\phi }\wedge {k}=2\right)\to {D}\in ℂ$
100 84 99 sylan2b ${⊢}\left({\phi }\wedge {k}\in \left\{2\right\}\right)\to {D}\in ℂ$
101 83 100 fprodcl ${⊢}{\phi }\to \prod _{{k}\in \left\{2\right\}}{D}\in ℂ$
102 61 81 101 mulassd ${⊢}{\phi }\to \prod _{{k}\in \left\{0\right\}}{D}\prod _{{k}\in \left\{1\right\}}{D}\prod _{{k}\in \left\{2\right\}}{D}=\prod _{{k}\in \left\{0\right\}}{D}\prod _{{k}\in \left\{1\right\}}{D}\prod _{{k}\in \left\{2\right\}}{D}$
103 0nn0 ${⊢}0\in {ℕ}_{0}$
104 103 a1i ${⊢}{\phi }\to 0\in {ℕ}_{0}$
105 1 prodsn ${⊢}\left(0\in {ℕ}_{0}\wedge {A}\in ℂ\right)\to \prod _{{k}\in \left\{0\right\}}{D}={A}$
106 104 57 105 syl2anc ${⊢}{\phi }\to \prod _{{k}\in \left\{0\right\}}{D}={A}$
107 1nn0 ${⊢}1\in {ℕ}_{0}$
108 107 a1i ${⊢}{\phi }\to 1\in {ℕ}_{0}$
109 2 prodsn ${⊢}\left(1\in {ℕ}_{0}\wedge {B}\in ℂ\right)\to \prod _{{k}\in \left\{1\right\}}{D}={B}$
110 108 77 109 syl2anc ${⊢}{\phi }\to \prod _{{k}\in \left\{1\right\}}{D}={B}$
111 2nn0 ${⊢}2\in {ℕ}_{0}$
112 111 a1i ${⊢}{\phi }\to 2\in {ℕ}_{0}$
113 3 prodsn ${⊢}\left(2\in {ℕ}_{0}\wedge {C}\in ℂ\right)\to \prod _{{k}\in \left\{2\right\}}{D}={C}$
114 112 97 113 syl2anc ${⊢}{\phi }\to \prod _{{k}\in \left\{2\right\}}{D}={C}$
115 110 114 oveq12d ${⊢}{\phi }\to \prod _{{k}\in \left\{1\right\}}{D}\prod _{{k}\in \left\{2\right\}}{D}={B}{C}$
116 106 115 oveq12d ${⊢}{\phi }\to \prod _{{k}\in \left\{0\right\}}{D}\prod _{{k}\in \left\{1\right\}}{D}\prod _{{k}\in \left\{2\right\}}{D}={A}{B}{C}$
117 40 102 116 3eqtrd ${⊢}{\phi }\to \prod _{{k}\in \left(0..^3\right)}{D}={A}{B}{C}$