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 
|- ( ( ph /\ k e. ( 0 ..^ 3 ) ) -> D e. CC )
Assertion prodfzo03 
|- ( ph -> prod_ k e. ( 0 ..^ 3 ) D = ( A x. ( B x. 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 
 |-  ( ( ph /\ k e. ( 0 ..^ 3 ) ) -> D e. CC )
5 fzodisjsn 
 |-  ( ( 0 ..^ 2 ) i^i { 2 } ) = (/)
6 5 a1i 
 |-  ( ph -> ( ( 0 ..^ 2 ) i^i { 2 } ) = (/) )
7 2p1e3 
 |-  ( 2 + 1 ) = 3
8 7 oveq2i 
 |-  ( 0 ..^ ( 2 + 1 ) ) = ( 0 ..^ 3 )
9 2eluzge0 
 |-  2 e. ( ZZ>= ` 0 )
10 fzosplitsn 
 |-  ( 2 e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( 2 + 1 ) ) = ( ( 0 ..^ 2 ) u. { 2 } ) )
11 9 10 ax-mp 
 |-  ( 0 ..^ ( 2 + 1 ) ) = ( ( 0 ..^ 2 ) u. { 2 } )
12 8 11 eqtr3i 
 |-  ( 0 ..^ 3 ) = ( ( 0 ..^ 2 ) u. { 2 } )
13 12 a1i 
 |-  ( ph -> ( 0 ..^ 3 ) = ( ( 0 ..^ 2 ) u. { 2 } ) )
14 fzofi 
 |-  ( 0 ..^ 3 ) e. Fin
15 14 a1i 
 |-  ( ph -> ( 0 ..^ 3 ) e. Fin )
16 6 13 15 4 fprodsplit 
 |-  ( ph -> prod_ k e. ( 0 ..^ 3 ) D = ( prod_ k e. ( 0 ..^ 2 ) D x. prod_ k e. { 2 } D ) )
17 0ne1 
 |-  0 =/= 1
18 disjsn2 
 |-  ( 0 =/= 1 -> ( { 0 } i^i { 1 } ) = (/) )
19 17 18 mp1i 
 |-  ( ph -> ( { 0 } i^i { 1 } ) = (/) )
20 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
21 df-pr 
 |-  { 0 , 1 } = ( { 0 } u. { 1 } )
22 20 21 eqtri 
 |-  ( 0 ..^ 2 ) = ( { 0 } u. { 1 } )
23 22 a1i 
 |-  ( ph -> ( 0 ..^ 2 ) = ( { 0 } u. { 1 } ) )
24 fzofi 
 |-  ( 0 ..^ 2 ) e. Fin
25 24 a1i 
 |-  ( ph -> ( 0 ..^ 2 ) e. Fin )
26 2z 
 |-  2 e. ZZ
27 3z 
 |-  3 e. ZZ
28 2re 
 |-  2 e. RR
29 3re 
 |-  3 e. RR
30 2lt3 
 |-  2 < 3
31 28 29 30 ltleii 
 |-  2 <_ 3
32 eluz2 
 |-  ( 3 e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ 3 e. ZZ /\ 2 <_ 3 ) )
33 26 27 31 32 mpbir3an 
 |-  3 e. ( ZZ>= ` 2 )
34 fzoss2 
 |-  ( 3 e. ( ZZ>= ` 2 ) -> ( 0 ..^ 2 ) C_ ( 0 ..^ 3 ) )
35 33 34 ax-mp 
 |-  ( 0 ..^ 2 ) C_ ( 0 ..^ 3 )
36 35 sseli 
 |-  ( k e. ( 0 ..^ 2 ) -> k e. ( 0 ..^ 3 ) )
37 36 4 sylan2 
 |-  ( ( ph /\ k e. ( 0 ..^ 2 ) ) -> D e. CC )
38 19 23 25 37 fprodsplit 
 |-  ( ph -> prod_ k e. ( 0 ..^ 2 ) D = ( prod_ k e. { 0 } D x. prod_ k e. { 1 } D ) )
39 38 oveq1d 
 |-  ( ph -> ( prod_ k e. ( 0 ..^ 2 ) D x. prod_ k e. { 2 } D ) = ( ( prod_ k e. { 0 } D x. prod_ k e. { 1 } D ) x. prod_ k e. { 2 } D ) )
40 16 39 eqtrd 
 |-  ( ph -> prod_ k e. ( 0 ..^ 3 ) D = ( ( prod_ k e. { 0 } D x. prod_ k e. { 1 } D ) x. prod_ k e. { 2 } D ) )
41 snfi 
 |-  { 0 } e. Fin
42 41 a1i 
 |-  ( ph -> { 0 } e. Fin )
43 velsn 
 |-  ( k e. { 0 } <-> k = 0 )
44 1 adantl 
 |-  ( ( ph /\ k = 0 ) -> D = A )
45 simpr 
 |-  ( ( ( ph /\ k e. ( 0 ..^ 3 ) ) /\ D = A ) -> D = A )
46 4 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ..^ 3 ) ) /\ D = A ) -> D e. CC )
47 45 46 eqeltrrd 
 |-  ( ( ( ph /\ k e. ( 0 ..^ 3 ) ) /\ D = A ) -> A e. CC )
48 c0ex 
 |-  0 e. _V
49 48 tpid1 
 |-  0 e. { 0 , 1 , 2 }
50 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
51 49 50 eleqtrri 
 |-  0 e. ( 0 ..^ 3 )
52 eqid 
 |-  A = A
53 1 eqeq1d 
 |-  ( k = 0 -> ( D = A <-> A = A ) )
54 53 rspcev 
 |-  ( ( 0 e. ( 0 ..^ 3 ) /\ A = A ) -> E. k e. ( 0 ..^ 3 ) D = A )
55 51 52 54 mp2an 
 |-  E. k e. ( 0 ..^ 3 ) D = A
56 55 a1i 
 |-  ( ph -> E. k e. ( 0 ..^ 3 ) D = A )
57 47 56 r19.29a 
 |-  ( ph -> A e. CC )
58 57 adantr 
 |-  ( ( ph /\ k = 0 ) -> A e. CC )
59 44 58 eqeltrd 
 |-  ( ( ph /\ k = 0 ) -> D e. CC )
60 43 59 sylan2b 
 |-  ( ( ph /\ k e. { 0 } ) -> D e. CC )
61 42 60 fprodcl 
 |-  ( ph -> prod_ k e. { 0 } D e. CC )
62 snfi 
 |-  { 1 } e. Fin
63 62 a1i 
 |-  ( ph -> { 1 } e. Fin )
64 velsn 
 |-  ( k e. { 1 } <-> k = 1 )
65 2 adantl 
 |-  ( ( ph /\ k = 1 ) -> D = B )
66 simpr 
 |-  ( ( ( ph /\ k e. ( 0 ..^ 3 ) ) /\ D = B ) -> D = B )
67 4 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ..^ 3 ) ) /\ D = B ) -> D e. CC )
68 66 67 eqeltrrd 
 |-  ( ( ( ph /\ k e. ( 0 ..^ 3 ) ) /\ D = B ) -> B e. CC )
69 1eltp012 
 |-  1 e. { 0 , 1 , 2 }
70 69 50 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
71 eqid 
 |-  B = B
72 2 eqeq1d 
 |-  ( k = 1 -> ( D = B <-> B = B ) )
73 72 rspcev 
 |-  ( ( 1 e. ( 0 ..^ 3 ) /\ B = B ) -> E. k e. ( 0 ..^ 3 ) D = B )
74 70 71 73 mp2an 
 |-  E. k e. ( 0 ..^ 3 ) D = B
75 74 a1i 
 |-  ( ph -> E. k e. ( 0 ..^ 3 ) D = B )
76 68 75 r19.29a 
 |-  ( ph -> B e. CC )
77 76 adantr 
 |-  ( ( ph /\ k = 1 ) -> B e. CC )
78 65 77 eqeltrd 
 |-  ( ( ph /\ k = 1 ) -> D e. CC )
79 64 78 sylan2b 
 |-  ( ( ph /\ k e. { 1 } ) -> D e. CC )
80 63 79 fprodcl 
 |-  ( ph -> prod_ k e. { 1 } D e. CC )
81 snfi 
 |-  { 2 } e. Fin
82 81 a1i 
 |-  ( ph -> { 2 } e. Fin )
83 velsn 
 |-  ( k e. { 2 } <-> k = 2 )
84 3 adantl 
 |-  ( ( ph /\ k = 2 ) -> D = C )
85 simpr 
 |-  ( ( ( ph /\ k e. ( 0 ..^ 3 ) ) /\ D = C ) -> D = C )
86 4 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ..^ 3 ) ) /\ D = C ) -> D e. CC )
87 85 86 eqeltrrd 
 |-  ( ( ( ph /\ k e. ( 0 ..^ 3 ) ) /\ D = C ) -> C e. CC )
88 2ex 
 |-  2 e. _V
89 88 tpid3 
 |-  2 e. { 0 , 1 , 2 }
90 89 50 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
91 eqid 
 |-  C = C
92 3 eqeq1d 
 |-  ( k = 2 -> ( D = C <-> C = C ) )
93 92 rspcev 
 |-  ( ( 2 e. ( 0 ..^ 3 ) /\ C = C ) -> E. k e. ( 0 ..^ 3 ) D = C )
94 90 91 93 mp2an 
 |-  E. k e. ( 0 ..^ 3 ) D = C
95 94 a1i 
 |-  ( ph -> E. k e. ( 0 ..^ 3 ) D = C )
96 87 95 r19.29a 
 |-  ( ph -> C e. CC )
97 96 adantr 
 |-  ( ( ph /\ k = 2 ) -> C e. CC )
98 84 97 eqeltrd 
 |-  ( ( ph /\ k = 2 ) -> D e. CC )
99 83 98 sylan2b 
 |-  ( ( ph /\ k e. { 2 } ) -> D e. CC )
100 82 99 fprodcl 
 |-  ( ph -> prod_ k e. { 2 } D e. CC )
101 61 80 100 mulassd 
 |-  ( ph -> ( ( prod_ k e. { 0 } D x. prod_ k e. { 1 } D ) x. prod_ k e. { 2 } D ) = ( prod_ k e. { 0 } D x. ( prod_ k e. { 1 } D x. prod_ k e. { 2 } D ) ) )
102 0nn0 
 |-  0 e. NN0
103 102 a1i 
 |-  ( ph -> 0 e. NN0 )
104 1 prodsn 
 |-  ( ( 0 e. NN0 /\ A e. CC ) -> prod_ k e. { 0 } D = A )
105 103 57 104 syl2anc 
 |-  ( ph -> prod_ k e. { 0 } D = A )
106 1nn0 
 |-  1 e. NN0
107 106 a1i 
 |-  ( ph -> 1 e. NN0 )
108 2 prodsn 
 |-  ( ( 1 e. NN0 /\ B e. CC ) -> prod_ k e. { 1 } D = B )
109 107 76 108 syl2anc 
 |-  ( ph -> prod_ k e. { 1 } D = B )
110 2nn0 
 |-  2 e. NN0
111 110 a1i 
 |-  ( ph -> 2 e. NN0 )
112 3 prodsn 
 |-  ( ( 2 e. NN0 /\ C e. CC ) -> prod_ k e. { 2 } D = C )
113 111 96 112 syl2anc 
 |-  ( ph -> prod_ k e. { 2 } D = C )
114 109 113 oveq12d 
 |-  ( ph -> ( prod_ k e. { 1 } D x. prod_ k e. { 2 } D ) = ( B x. C ) )
115 105 114 oveq12d 
 |-  ( ph -> ( prod_ k e. { 0 } D x. ( prod_ k e. { 1 } D x. prod_ k e. { 2 } D ) ) = ( A x. ( B x. C ) ) )
116 40 101 115 3eqtrd 
 |-  ( ph -> prod_ k e. ( 0 ..^ 3 ) D = ( A x. ( B x. C ) ) )