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

Metamath Proof Explorer

Theorem prodfzo03

Proof