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