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 → D = A
prodfzo03.2 ⊢ k = 1 → D = B
prodfzo03.3 ⊢ k = 2 → D = C
prodfzo03.a ⊢ φ ∧ k ∈ 0 ..^ 3 → D ∈ ℂ
Assertion prodfzo03 ⊢ φ → ∏ k ∈ 0 ..^ 3 D = A ⁢ B ⁢ C

Proof

Step Hyp Ref Expression
1 prodfzo03.1 ⊢ k = 0 → D = A
2 prodfzo03.2 ⊢ k = 1 → D = B
3 prodfzo03.3 ⊢ k = 2 → D = C
4 prodfzo03.a ⊢ φ ∧ k ∈ 0 ..^ 3 → D ∈ ℂ
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 ⊢ φ → ∏ k ∈ 0 ..^ 3 D = ∏ k ∈ 0 ..^ 2 D ⁢ ∏ k ∈ 2 D
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 ⊢ k ∈ 0 ..^ 2 → k ∈ 0 ..^ 3
37 36 4 sylan2 ⊢ φ ∧ k ∈ 0 ..^ 2 → D ∈ ℂ
38 19 23 25 37 fprodsplit ⊢ φ → ∏ k ∈ 0 ..^ 2 D = ∏ k ∈ 0 D ⁢ ∏ k ∈ 1 D
39 38 oveq1d ⊢ φ → ∏ k ∈ 0 ..^ 2 D ⁢ ∏ k ∈ 2 D = ∏ k ∈ 0 D ⁢ ∏ k ∈ 1 D ⁢ ∏ k ∈ 2 D
40 16 39 eqtrd ⊢ φ → ∏ k ∈ 0 ..^ 3 D = ∏ k ∈ 0 D ⁢ ∏ k ∈ 1 D ⁢ ∏ k ∈ 2 D
41 snfi ⊢ 0 ∈ Fin
42 41 a1i ⊢ φ → 0 ∈ Fin
43 velsn ⊢ k ∈ 0 ↔ k = 0
44 1 adantl ⊢ φ ∧ k = 0 → D = A
45 simpr ⊢ φ ∧ k ∈ 0 ..^ 3 ∧ D = A → D = A
46 4 adantr ⊢ φ ∧ k ∈ 0 ..^ 3 ∧ D = A → D ∈ ℂ
47 45 46 eqeltrrd ⊢ φ ∧ k ∈ 0 ..^ 3 ∧ D = A → A ∈ ℂ
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 ⊢ A = A
53 1 eqeq1d ⊢ k = 0 → D = A ↔ A = A
54 53 rspcev ⊢ 0 ∈ 0 ..^ 3 ∧ A = A → ∃ k ∈ 0 ..^ 3 D = A
55 51 52 54 mp2an ⊢ ∃ k ∈ 0 ..^ 3 D = A
56 55 a1i ⊢ φ → ∃ k ∈ 0 ..^ 3 D = A
57 47 56 r19.29a ⊢ φ → A ∈ ℂ
58 57 adantr ⊢ φ ∧ k = 0 → A ∈ ℂ
59 44 58 eqeltrd ⊢ φ ∧ k = 0 → D ∈ ℂ
60 43 59 sylan2b ⊢ φ ∧ k ∈ 0 → D ∈ ℂ
61 42 60 fprodcl ⊢ φ → ∏ k ∈ 0 D ∈ ℂ
62 snfi ⊢ 1 ∈ Fin
63 62 a1i ⊢ φ → 1 ∈ Fin
64 velsn ⊢ k ∈ 1 ↔ k = 1
65 2 adantl ⊢ φ ∧ k = 1 → D = B
66 simpr ⊢ φ ∧ k ∈ 0 ..^ 3 ∧ D = B → D = B
67 4 adantr ⊢ φ ∧ k ∈ 0 ..^ 3 ∧ D = B → D ∈ ℂ
68 66 67 eqeltrrd ⊢ φ ∧ k ∈ 0 ..^ 3 ∧ D = B → B ∈ ℂ
69 1eltp012 ⊢ 1 ∈ 0 1 2
70 69 50 eleqtrri ⊢ 1 ∈ 0 ..^ 3
71 eqid ⊢ B = B
72 2 eqeq1d ⊢ k = 1 → D = B ↔ B = B
73 72 rspcev ⊢ 1 ∈ 0 ..^ 3 ∧ B = B → ∃ k ∈ 0 ..^ 3 D = B
74 70 71 73 mp2an ⊢ ∃ k ∈ 0 ..^ 3 D = B
75 74 a1i ⊢ φ → ∃ k ∈ 0 ..^ 3 D = B
76 68 75 r19.29a ⊢ φ → B ∈ ℂ
77 76 adantr ⊢ φ ∧ k = 1 → B ∈ ℂ
78 65 77 eqeltrd ⊢ φ ∧ k = 1 → D ∈ ℂ
79 64 78 sylan2b ⊢ φ ∧ k ∈ 1 → D ∈ ℂ
80 63 79 fprodcl ⊢ φ → ∏ k ∈ 1 D ∈ ℂ
81 snfi ⊢ 2 ∈ Fin
82 81 a1i ⊢ φ → 2 ∈ Fin
83 velsn ⊢ k ∈ 2 ↔ k = 2
84 3 adantl ⊢ φ ∧ k = 2 → D = C
85 simpr ⊢ φ ∧ k ∈ 0 ..^ 3 ∧ D = C → D = C
86 4 adantr ⊢ φ ∧ k ∈ 0 ..^ 3 ∧ D = C → D ∈ ℂ
87 85 86 eqeltrrd ⊢ φ ∧ k ∈ 0 ..^ 3 ∧ D = C → C ∈ ℂ
88 2ex ⊢ 2 ∈ V
89 88 tpid3 ⊢ 2 ∈ 0 1 2
90 89 50 eleqtrri ⊢ 2 ∈ 0 ..^ 3
91 eqid ⊢ C = C
92 3 eqeq1d ⊢ k = 2 → D = C ↔ C = C
93 92 rspcev ⊢ 2 ∈ 0 ..^ 3 ∧ C = C → ∃ k ∈ 0 ..^ 3 D = C
94 90 91 93 mp2an ⊢ ∃ k ∈ 0 ..^ 3 D = C
95 94 a1i ⊢ φ → ∃ k ∈ 0 ..^ 3 D = C
96 87 95 r19.29a ⊢ φ → C ∈ ℂ
97 96 adantr ⊢ φ ∧ k = 2 → C ∈ ℂ
98 84 97 eqeltrd ⊢ φ ∧ k = 2 → D ∈ ℂ
99 83 98 sylan2b ⊢ φ ∧ k ∈ 2 → D ∈ ℂ
100 82 99 fprodcl ⊢ φ → ∏ k ∈ 2 D ∈ ℂ
101 61 80 100 mulassd ⊢ φ → ∏ k ∈ 0 D ⁢ ∏ k ∈ 1 D ⁢ ∏ k ∈ 2 D = ∏ k ∈ 0 D ⁢ ∏ k ∈ 1 D ⁢ ∏ k ∈ 2 D
102 0nn0 ⊢ 0 ∈ ℕ 0
103 102 a1i ⊢ φ → 0 ∈ ℕ 0
104 1 prodsn ⊢ 0 ∈ ℕ 0 ∧ A ∈ ℂ → ∏ k ∈ 0 D = A
105 103 57 104 syl2anc ⊢ φ → ∏ k ∈ 0 D = A
106 1nn0 ⊢ 1 ∈ ℕ 0
107 106 a1i ⊢ φ → 1 ∈ ℕ 0
108 2 prodsn ⊢ 1 ∈ ℕ 0 ∧ B ∈ ℂ → ∏ k ∈ 1 D = B
109 107 76 108 syl2anc ⊢ φ → ∏ k ∈ 1 D = B
110 2nn0 ⊢ 2 ∈ ℕ 0
111 110 a1i ⊢ φ → 2 ∈ ℕ 0
112 3 prodsn ⊢ 2 ∈ ℕ 0 ∧ C ∈ ℂ → ∏ k ∈ 2 D = C
113 111 96 112 syl2anc ⊢ φ → ∏ k ∈ 2 D = C
114 109 113 oveq12d ⊢ φ → ∏ k ∈ 1 D ⁢ ∏ k ∈ 2 D = B ⁢ C
115 105 114 oveq12d ⊢ φ → ∏ k ∈ 0 D ⁢ ∏ k ∈ 1 D ⁢ ∏ k ∈ 2 D = A ⁢ B ⁢ C
116 40 101 115 3eqtrd ⊢ φ → ∏ k ∈ 0 ..^ 3 D = A ⁢ B ⁢ C