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 1ex 
 |-  1 e. _V
70 69 tpid2 
 |-  1 e. { 0 , 1 , 2 }
71 70 50 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
72 eqid 
 |-  B = B
73 2 eqeq1d 
 |-  ( k = 1 -> ( D = B <-> B = B ) )
74 73 rspcev 
 |-  ( ( 1 e. ( 0 ..^ 3 ) /\ B = B ) -> E. k e. ( 0 ..^ 3 ) D = B )
75 71 72 74 mp2an 
 |-  E. k e. ( 0 ..^ 3 ) D = B
76 75 a1i 
 |-  ( ph -> E. k e. ( 0 ..^ 3 ) D = B )
77 68 76 r19.29a 
 |-  ( ph -> B e. CC )
78 77 adantr 
 |-  ( ( ph /\ k = 1 ) -> B e. CC )
79 65 78 eqeltrd 
 |-  ( ( ph /\ k = 1 ) -> D e. CC )
80 64 79 sylan2b 
 |-  ( ( ph /\ k e. { 1 } ) -> D e. CC )
81 63 80 fprodcl 
 |-  ( ph -> prod_ k e. { 1 } D e. CC )
82 snfi 
 |-  { 2 } e. Fin
83 82 a1i 
 |-  ( ph -> { 2 } e. Fin )
84 velsn 
 |-  ( k e. { 2 } <-> k = 2 )
85 3 adantl 
 |-  ( ( ph /\ k = 2 ) -> D = C )
86 simpr 
 |-  ( ( ( ph /\ k e. ( 0 ..^ 3 ) ) /\ D = C ) -> D = C )
87 4 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ..^ 3 ) ) /\ D = C ) -> D e. CC )
88 86 87 eqeltrrd 
 |-  ( ( ( ph /\ k e. ( 0 ..^ 3 ) ) /\ D = C ) -> C e. CC )
89 2ex 
 |-  2 e. _V
90 89 tpid3 
 |-  2 e. { 0 , 1 , 2 }
91 90 50 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
92 eqid 
 |-  C = C
93 3 eqeq1d 
 |-  ( k = 2 -> ( D = C <-> C = C ) )
94 93 rspcev 
 |-  ( ( 2 e. ( 0 ..^ 3 ) /\ C = C ) -> E. k e. ( 0 ..^ 3 ) D = C )
95 91 92 94 mp2an 
 |-  E. k e. ( 0 ..^ 3 ) D = C
96 95 a1i 
 |-  ( ph -> E. k e. ( 0 ..^ 3 ) D = C )
97 88 96 r19.29a 
 |-  ( ph -> C e. CC )
98 97 adantr 
 |-  ( ( ph /\ k = 2 ) -> C e. CC )
99 85 98 eqeltrd 
 |-  ( ( ph /\ k = 2 ) -> D e. CC )
100 84 99 sylan2b 
 |-  ( ( ph /\ k e. { 2 } ) -> D e. CC )
101 83 100 fprodcl 
 |-  ( ph -> prod_ k e. { 2 } D e. CC )
102 61 81 101 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 ) ) )
103 0nn0 
 |-  0 e. NN0
104 103 a1i 
 |-  ( ph -> 0 e. NN0 )
105 1 prodsn 
 |-  ( ( 0 e. NN0 /\ A e. CC ) -> prod_ k e. { 0 } D = A )
106 104 57 105 syl2anc 
 |-  ( ph -> prod_ k e. { 0 } D = A )
107 1nn0 
 |-  1 e. NN0
108 107 a1i 
 |-  ( ph -> 1 e. NN0 )
109 2 prodsn 
 |-  ( ( 1 e. NN0 /\ B e. CC ) -> prod_ k e. { 1 } D = B )
110 108 77 109 syl2anc 
 |-  ( ph -> prod_ k e. { 1 } D = B )
111 2nn0 
 |-  2 e. NN0
112 111 a1i 
 |-  ( ph -> 2 e. NN0 )
113 3 prodsn 
 |-  ( ( 2 e. NN0 /\ C e. CC ) -> prod_ k e. { 2 } D = C )
114 112 97 113 syl2anc 
 |-  ( ph -> prod_ k e. { 2 } D = C )
115 110 114 oveq12d 
 |-  ( ph -> ( prod_ k e. { 1 } D x. prod_ k e. { 2 } D ) = ( B x. C ) )
116 106 115 oveq12d 
 |-  ( ph -> ( prod_ k e. { 0 } D x. ( prod_ k e. { 1 } D x. prod_ k e. { 2 } D ) ) = ( A x. ( B x. C ) ) )
117 40 102 116 3eqtrd 
 |-  ( ph -> prod_ k e. ( 0 ..^ 3 ) D = ( A x. ( B x. C ) ) )