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 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 ) 𝐷 = ( 𝐴 · ( 𝐵 · 𝐶 ) ) )