Step | Hyp | Ref
| Expression |
1 | | fzodisjsn 13616 |
. . . . 5
โข ((0..^2)
โฉ {2}) = โ
|
2 | 1 | a1i 11 |
. . . 4
โข (๐ โ ((0..^2) โฉ {2}) =
โ
) |
3 | | 2p1e3 12300 |
. . . . . . 7
โข (2 + 1) =
3 |
4 | 3 | oveq2i 7369 |
. . . . . 6
โข (0..^(2 +
1)) = (0..^3) |
5 | | 2eluzge0 12823 |
. . . . . . 7
โข 2 โ
(โคโฅโ0) |
6 | | fzosplitsn 13686 |
. . . . . . 7
โข (2 โ
(โคโฅโ0) โ (0..^(2 + 1)) = ((0..^2) โช
{2})) |
7 | 5, 6 | ax-mp 5 |
. . . . . 6
โข (0..^(2 +
1)) = ((0..^2) โช {2}) |
8 | 4, 7 | eqtr3i 2763 |
. . . . 5
โข (0..^3) =
((0..^2) โช {2}) |
9 | 8 | a1i 11 |
. . . 4
โข (๐ โ (0..^3) = ((0..^2) โช
{2})) |
10 | | fzofi 13885 |
. . . . 5
โข (0..^3)
โ Fin |
11 | 10 | a1i 11 |
. . . 4
โข (๐ โ (0..^3) โ
Fin) |
12 | | prodfzo03.a |
. . . 4
โข ((๐ โง ๐ โ (0..^3)) โ ๐ท โ โ) |
13 | 2, 9, 11, 12 | fprodsplit 15854 |
. . 3
โข (๐ โ โ๐ โ (0..^3)๐ท = (โ๐ โ (0..^2)๐ท ยท โ๐ โ {2}๐ท)) |
14 | | 0ne1 12229 |
. . . . . 6
โข 0 โ
1 |
15 | | disjsn2 4674 |
. . . . . 6
โข (0 โ 1
โ ({0} โฉ {1}) = โ
) |
16 | 14, 15 | mp1i 13 |
. . . . 5
โข (๐ โ ({0} โฉ {1}) =
โ
) |
17 | | fzo0to2pr 13663 |
. . . . . . 7
โข (0..^2) =
{0, 1} |
18 | | df-pr 4590 |
. . . . . . 7
โข {0, 1} =
({0} โช {1}) |
19 | 17, 18 | eqtri 2761 |
. . . . . 6
โข (0..^2) =
({0} โช {1}) |
20 | 19 | a1i 11 |
. . . . 5
โข (๐ โ (0..^2) = ({0} โช
{1})) |
21 | | fzofi 13885 |
. . . . . 6
โข (0..^2)
โ Fin |
22 | 21 | a1i 11 |
. . . . 5
โข (๐ โ (0..^2) โ
Fin) |
23 | | 2z 12540 |
. . . . . . . . 9
โข 2 โ
โค |
24 | | 3z 12541 |
. . . . . . . . 9
โข 3 โ
โค |
25 | | 2re 12232 |
. . . . . . . . . 10
โข 2 โ
โ |
26 | | 3re 12238 |
. . . . . . . . . 10
โข 3 โ
โ |
27 | | 2lt3 12330 |
. . . . . . . . . 10
โข 2 <
3 |
28 | 25, 26, 27 | ltleii 11283 |
. . . . . . . . 9
โข 2 โค
3 |
29 | | eluz2 12774 |
. . . . . . . . 9
โข (3 โ
(โคโฅโ2) โ (2 โ โค โง 3 โ
โค โง 2 โค 3)) |
30 | 23, 24, 28, 29 | mpbir3an 1342 |
. . . . . . . 8
โข 3 โ
(โคโฅโ2) |
31 | | fzoss2 13606 |
. . . . . . . 8
โข (3 โ
(โคโฅโ2) โ (0..^2) โ
(0..^3)) |
32 | 30, 31 | ax-mp 5 |
. . . . . . 7
โข (0..^2)
โ (0..^3) |
33 | 32 | sseli 3941 |
. . . . . 6
โข (๐ โ (0..^2) โ ๐ โ
(0..^3)) |
34 | 33, 12 | sylan2 594 |
. . . . 5
โข ((๐ โง ๐ โ (0..^2)) โ ๐ท โ โ) |
35 | 16, 20, 22, 34 | fprodsplit 15854 |
. . . 4
โข (๐ โ โ๐ โ (0..^2)๐ท = (โ๐ โ {0}๐ท ยท โ๐ โ {1}๐ท)) |
36 | 35 | oveq1d 7373 |
. . 3
โข (๐ โ (โ๐ โ (0..^2)๐ท ยท โ๐ โ {2}๐ท) = ((โ๐ โ {0}๐ท ยท โ๐ โ {1}๐ท) ยท โ๐ โ {2}๐ท)) |
37 | 13, 36 | eqtrd 2773 |
. 2
โข (๐ โ โ๐ โ (0..^3)๐ท = ((โ๐ โ {0}๐ท ยท โ๐ โ {1}๐ท) ยท โ๐ โ {2}๐ท)) |
38 | | snfi 8991 |
. . . . 5
โข {0}
โ Fin |
39 | 38 | a1i 11 |
. . . 4
โข (๐ โ {0} โ
Fin) |
40 | | velsn 4603 |
. . . . 5
โข (๐ โ {0} โ ๐ = 0) |
41 | | prodfzo03.1 |
. . . . . . 7
โข (๐ = 0 โ ๐ท = ๐ด) |
42 | 41 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ = 0) โ ๐ท = ๐ด) |
43 | | simpr 486 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (0..^3)) โง ๐ท = ๐ด) โ ๐ท = ๐ด) |
44 | 12 | adantr 482 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (0..^3)) โง ๐ท = ๐ด) โ ๐ท โ โ) |
45 | 43, 44 | eqeltrrd 2835 |
. . . . . . . 8
โข (((๐ โง ๐ โ (0..^3)) โง ๐ท = ๐ด) โ ๐ด โ โ) |
46 | | c0ex 11154 |
. . . . . . . . . . . 12
โข 0 โ
V |
47 | 46 | tpid1 4730 |
. . . . . . . . . . 11
โข 0 โ
{0, 1, 2} |
48 | | fzo0to3tp 13664 |
. . . . . . . . . . 11
โข (0..^3) =
{0, 1, 2} |
49 | 47, 48 | eleqtrri 2833 |
. . . . . . . . . 10
โข 0 โ
(0..^3) |
50 | | eqid 2733 |
. . . . . . . . . 10
โข ๐ด = ๐ด |
51 | 41 | eqeq1d 2735 |
. . . . . . . . . . 11
โข (๐ = 0 โ (๐ท = ๐ด โ ๐ด = ๐ด)) |
52 | 51 | rspcev 3580 |
. . . . . . . . . 10
โข ((0
โ (0..^3) โง ๐ด =
๐ด) โ โ๐ โ (0..^3)๐ท = ๐ด) |
53 | 49, 50, 52 | mp2an 691 |
. . . . . . . . 9
โข
โ๐ โ
(0..^3)๐ท = ๐ด |
54 | 53 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ๐ โ (0..^3)๐ท = ๐ด) |
55 | 45, 54 | r19.29a 3156 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
56 | 55 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ = 0) โ ๐ด โ โ) |
57 | 42, 56 | eqeltrd 2834 |
. . . . 5
โข ((๐ โง ๐ = 0) โ ๐ท โ โ) |
58 | 40, 57 | sylan2b 595 |
. . . 4
โข ((๐ โง ๐ โ {0}) โ ๐ท โ โ) |
59 | 39, 58 | fprodcl 15840 |
. . 3
โข (๐ โ โ๐ โ {0}๐ท โ โ) |
60 | | snfi 8991 |
. . . . 5
โข {1}
โ Fin |
61 | 60 | a1i 11 |
. . . 4
โข (๐ โ {1} โ
Fin) |
62 | | velsn 4603 |
. . . . 5
โข (๐ โ {1} โ ๐ = 1) |
63 | | prodfzo03.2 |
. . . . . . 7
โข (๐ = 1 โ ๐ท = ๐ต) |
64 | 63 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ = 1) โ ๐ท = ๐ต) |
65 | | simpr 486 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (0..^3)) โง ๐ท = ๐ต) โ ๐ท = ๐ต) |
66 | 12 | adantr 482 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (0..^3)) โง ๐ท = ๐ต) โ ๐ท โ โ) |
67 | 65, 66 | eqeltrrd 2835 |
. . . . . . . 8
โข (((๐ โง ๐ โ (0..^3)) โง ๐ท = ๐ต) โ ๐ต โ โ) |
68 | | 1ex 11156 |
. . . . . . . . . . . 12
โข 1 โ
V |
69 | 68 | tpid2 4732 |
. . . . . . . . . . 11
โข 1 โ
{0, 1, 2} |
70 | 69, 48 | eleqtrri 2833 |
. . . . . . . . . 10
โข 1 โ
(0..^3) |
71 | | eqid 2733 |
. . . . . . . . . 10
โข ๐ต = ๐ต |
72 | 63 | eqeq1d 2735 |
. . . . . . . . . . 11
โข (๐ = 1 โ (๐ท = ๐ต โ ๐ต = ๐ต)) |
73 | 72 | rspcev 3580 |
. . . . . . . . . 10
โข ((1
โ (0..^3) โง ๐ต =
๐ต) โ โ๐ โ (0..^3)๐ท = ๐ต) |
74 | 70, 71, 73 | mp2an 691 |
. . . . . . . . 9
โข
โ๐ โ
(0..^3)๐ท = ๐ต |
75 | 74 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ๐ โ (0..^3)๐ท = ๐ต) |
76 | 67, 75 | r19.29a 3156 |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
77 | 76 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ = 1) โ ๐ต โ โ) |
78 | 64, 77 | eqeltrd 2834 |
. . . . 5
โข ((๐ โง ๐ = 1) โ ๐ท โ โ) |
79 | 62, 78 | sylan2b 595 |
. . . 4
โข ((๐ โง ๐ โ {1}) โ ๐ท โ โ) |
80 | 61, 79 | fprodcl 15840 |
. . 3
โข (๐ โ โ๐ โ {1}๐ท โ โ) |
81 | | snfi 8991 |
. . . . 5
โข {2}
โ Fin |
82 | 81 | a1i 11 |
. . . 4
โข (๐ โ {2} โ
Fin) |
83 | | velsn 4603 |
. . . . 5
โข (๐ โ {2} โ ๐ = 2) |
84 | | prodfzo03.3 |
. . . . . . 7
โข (๐ = 2 โ ๐ท = ๐ถ) |
85 | 84 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ = 2) โ ๐ท = ๐ถ) |
86 | | simpr 486 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (0..^3)) โง ๐ท = ๐ถ) โ ๐ท = ๐ถ) |
87 | 12 | adantr 482 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (0..^3)) โง ๐ท = ๐ถ) โ ๐ท โ โ) |
88 | 86, 87 | eqeltrrd 2835 |
. . . . . . . 8
โข (((๐ โง ๐ โ (0..^3)) โง ๐ท = ๐ถ) โ ๐ถ โ โ) |
89 | | 2ex 12235 |
. . . . . . . . . . . 12
โข 2 โ
V |
90 | 89 | tpid3 4735 |
. . . . . . . . . . 11
โข 2 โ
{0, 1, 2} |
91 | 90, 48 | eleqtrri 2833 |
. . . . . . . . . 10
โข 2 โ
(0..^3) |
92 | | eqid 2733 |
. . . . . . . . . 10
โข ๐ถ = ๐ถ |
93 | 84 | eqeq1d 2735 |
. . . . . . . . . . 11
โข (๐ = 2 โ (๐ท = ๐ถ โ ๐ถ = ๐ถ)) |
94 | 93 | rspcev 3580 |
. . . . . . . . . 10
โข ((2
โ (0..^3) โง ๐ถ =
๐ถ) โ โ๐ โ (0..^3)๐ท = ๐ถ) |
95 | 91, 92, 94 | mp2an 691 |
. . . . . . . . 9
โข
โ๐ โ
(0..^3)๐ท = ๐ถ |
96 | 95 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ๐ โ (0..^3)๐ท = ๐ถ) |
97 | 88, 96 | r19.29a 3156 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
98 | 97 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ = 2) โ ๐ถ โ โ) |
99 | 85, 98 | eqeltrd 2834 |
. . . . 5
โข ((๐ โง ๐ = 2) โ ๐ท โ โ) |
100 | 83, 99 | sylan2b 595 |
. . . 4
โข ((๐ โง ๐ โ {2}) โ ๐ท โ โ) |
101 | 82, 100 | fprodcl 15840 |
. . 3
โข (๐ โ โ๐ โ {2}๐ท โ โ) |
102 | 59, 80, 101 | mulassd 11183 |
. 2
โข (๐ โ ((โ๐ โ {0}๐ท ยท โ๐ โ {1}๐ท) ยท โ๐ โ {2}๐ท) = (โ๐ โ {0}๐ท ยท (โ๐ โ {1}๐ท ยท โ๐ โ {2}๐ท))) |
103 | | 0nn0 12433 |
. . . . 5
โข 0 โ
โ0 |
104 | 103 | a1i 11 |
. . . 4
โข (๐ โ 0 โ
โ0) |
105 | 41 | prodsn 15850 |
. . . 4
โข ((0
โ โ0 โง ๐ด โ โ) โ โ๐ โ {0}๐ท = ๐ด) |
106 | 104, 55, 105 | syl2anc 585 |
. . 3
โข (๐ โ โ๐ โ {0}๐ท = ๐ด) |
107 | | 1nn0 12434 |
. . . . . 6
โข 1 โ
โ0 |
108 | 107 | a1i 11 |
. . . . 5
โข (๐ โ 1 โ
โ0) |
109 | 63 | prodsn 15850 |
. . . . 5
โข ((1
โ โ0 โง ๐ต โ โ) โ โ๐ โ {1}๐ท = ๐ต) |
110 | 108, 76, 109 | syl2anc 585 |
. . . 4
โข (๐ โ โ๐ โ {1}๐ท = ๐ต) |
111 | | 2nn0 12435 |
. . . . . 6
โข 2 โ
โ0 |
112 | 111 | a1i 11 |
. . . . 5
โข (๐ โ 2 โ
โ0) |
113 | 84 | prodsn 15850 |
. . . . 5
โข ((2
โ โ0 โง ๐ถ โ โ) โ โ๐ โ {2}๐ท = ๐ถ) |
114 | 112, 97, 113 | syl2anc 585 |
. . . 4
โข (๐ โ โ๐ โ {2}๐ท = ๐ถ) |
115 | 110, 114 | oveq12d 7376 |
. . 3
โข (๐ โ (โ๐ โ {1}๐ท ยท โ๐ โ {2}๐ท) = (๐ต ยท ๐ถ)) |
116 | 106, 115 | oveq12d 7376 |
. 2
โข (๐ โ (โ๐ โ {0}๐ท ยท (โ๐ โ {1}๐ท ยท โ๐ โ {2}๐ท)) = (๐ด ยท (๐ต ยท ๐ถ))) |
117 | 37, 102, 116 | 3eqtrd 2777 |
1
โข (๐ โ โ๐ โ (0..^3)๐ท = (๐ด ยท (๐ต ยท ๐ถ))) |