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 1ex ⊢ 1 ∈ V
70 69 tpid2 ⊢ 1 ∈ 0 1 2
71 70 50 eleqtrri ⊢ 1 ∈ 0 ..^ 3
72 eqid ⊢ B = B
73 2 eqeq1d ⊢ k = 1 → D = B ↔ B = B
74 73 rspcev ⊢ 1 ∈ 0 ..^ 3 ∧ B = B → ∃ k ∈ 0 ..^ 3 D = B
75 71 72 74 mp2an ⊢ ∃ k ∈ 0 ..^ 3 D = B
76 75 a1i ⊢ φ → ∃ k ∈ 0 ..^ 3 D = B
77 68 76 r19.29a ⊢ φ → B ∈ ℂ
78 77 adantr ⊢ φ ∧ k = 1 → B ∈ ℂ
79 65 78 eqeltrd ⊢ φ ∧ k = 1 → D ∈ ℂ
80 64 79 sylan2b ⊢ φ ∧ k ∈ 1 → D ∈ ℂ
81 63 80 fprodcl ⊢ φ → ∏ k ∈ 1 D ∈ ℂ
82 snfi ⊢ 2 ∈ Fin
83 82 a1i ⊢ φ → 2 ∈ Fin
84 velsn ⊢ k ∈ 2 ↔ k = 2
85 3 adantl ⊢ φ ∧ k = 2 → D = C
86 simpr ⊢ φ ∧ k ∈ 0 ..^ 3 ∧ D = C → D = C
87 4 adantr ⊢ φ ∧ k ∈ 0 ..^ 3 ∧ D = C → D ∈ ℂ
88 86 87 eqeltrrd ⊢ φ ∧ k ∈ 0 ..^ 3 ∧ D = C → C ∈ ℂ
89 2ex ⊢ 2 ∈ V
90 89 tpid3 ⊢ 2 ∈ 0 1 2
91 90 50 eleqtrri ⊢ 2 ∈ 0 ..^ 3
92 eqid ⊢ C = C
93 3 eqeq1d ⊢ k = 2 → D = C ↔ C = C
94 93 rspcev ⊢ 2 ∈ 0 ..^ 3 ∧ C = C → ∃ k ∈ 0 ..^ 3 D = C
95 91 92 94 mp2an ⊢ ∃ k ∈ 0 ..^ 3 D = C
96 95 a1i ⊢ φ → ∃ k ∈ 0 ..^ 3 D = C
97 88 96 r19.29a ⊢ φ → C ∈ ℂ
98 97 adantr ⊢ φ ∧ k = 2 → C ∈ ℂ
99 85 98 eqeltrd ⊢ φ ∧ k = 2 → D ∈ ℂ
100 84 99 sylan2b ⊢ φ ∧ k ∈ 2 → D ∈ ℂ
101 83 100 fprodcl ⊢ φ → ∏ k ∈ 2 D ∈ ℂ
102 61 81 101 mulassd ⊢ φ → ∏ k ∈ 0 D ⁢ ∏ k ∈ 1 D ⁢ ∏ k ∈ 2 D = ∏ k ∈ 0 D ⁢ ∏ k ∈ 1 D ⁢ ∏ k ∈ 2 D
103 0nn0 ⊢ 0 ∈ ℕ 0
104 103 a1i ⊢ φ → 0 ∈ ℕ 0
105 1 prodsn ⊢ 0 ∈ ℕ 0 ∧ A ∈ ℂ → ∏ k ∈ 0 D = A
106 104 57 105 syl2anc ⊢ φ → ∏ k ∈ 0 D = A
107 1nn0 ⊢ 1 ∈ ℕ 0
108 107 a1i ⊢ φ → 1 ∈ ℕ 0
109 2 prodsn ⊢ 1 ∈ ℕ 0 ∧ B ∈ ℂ → ∏ k ∈ 1 D = B
110 108 77 109 syl2anc ⊢ φ → ∏ k ∈ 1 D = B
111 2nn0 ⊢ 2 ∈ ℕ 0
112 111 a1i ⊢ φ → 2 ∈ ℕ 0
113 3 prodsn ⊢ 2 ∈ ℕ 0 ∧ C ∈ ℂ → ∏ k ∈ 2 D = C
114 112 97 113 syl2anc ⊢ φ → ∏ k ∈ 2 D = C
115 110 114 oveq12d ⊢ φ → ∏ k ∈ 1 D ⁢ ∏ k ∈ 2 D = B ⁢ C
116 106 115 oveq12d ⊢ φ → ∏ k ∈ 0 D ⁢ ∏ k ∈ 1 D ⁢ ∏ k ∈ 2 D = A ⁢ B ⁢ C
117 40 102 116 3eqtrd ⊢ φ → ∏ k ∈ 0 ..^ 3 D = A ⁢ B ⁢ C