Theorem prodfzo03

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

	Ref	Expression
Hypotheses	prodfzo03.1	⊢ ( 𝑘 = 0 → 𝐷 = 𝐴 )
	prodfzo03.2	⊢ ( 𝑘 = 1 → 𝐷 = 𝐵 )
	prodfzo03.3	⊢ ( 𝑘 = 2 → 𝐷 = 𝐶 )
	prodfzo03.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 3 ) ) → 𝐷 ∈ ℂ )
Assertion	prodfzo03	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 0 ..^ 3 ) 𝐷 = ( 𝐴 · ( 𝐵 · 𝐶 ) ) )

Proof

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