Proof of Theorem prodfzo03
Step | Hyp | Ref
| Expression |
1 | | fzodisjsn 13280 |
. . . . 5
⊢ ((0..^2)
∩ {2}) = ∅ |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → ((0..^2) ∩ {2}) =
∅) |
3 | | 2p1e3 11972 |
. . . . . . 7
⊢ (2 + 1) =
3 |
4 | 3 | oveq2i 7224 |
. . . . . 6
⊢ (0..^(2 +
1)) = (0..^3) |
5 | | 2eluzge0 12489 |
. . . . . . 7
⊢ 2 ∈
(ℤ≥‘0) |
6 | | fzosplitsn 13350 |
. . . . . . 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 2767 |
. . . . 5
⊢ (0..^3) =
((0..^2) ∪ {2}) |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝜑 → (0..^3) = ((0..^2) ∪
{2})) |
10 | | fzofi 13547 |
. . . . 5
⊢ (0..^3)
∈ Fin |
11 | 10 | a1i 11 |
. . . 4
⊢ (𝜑 → (0..^3) ∈
Fin) |
12 | | prodfzo03.a |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^3)) → 𝐷 ∈ ℂ) |
13 | 2, 9, 11, 12 | fprodsplit 15528 |
. . 3
⊢ (𝜑 → ∏𝑘 ∈ (0..^3)𝐷 = (∏𝑘 ∈ (0..^2)𝐷 · ∏𝑘 ∈ {2}𝐷)) |
14 | | 0ne1 11901 |
. . . . . 6
⊢ 0 ≠
1 |
15 | | disjsn2 4628 |
. . . . . 6
⊢ (0 ≠ 1
→ ({0} ∩ {1}) = ∅) |
16 | 14, 15 | mp1i 13 |
. . . . 5
⊢ (𝜑 → ({0} ∩ {1}) =
∅) |
17 | | fzo0to2pr 13327 |
. . . . . . 7
⊢ (0..^2) =
{0, 1} |
18 | | df-pr 4544 |
. . . . . . 7
⊢ {0, 1} =
({0} ∪ {1}) |
19 | 17, 18 | eqtri 2765 |
. . . . . 6
⊢ (0..^2) =
({0} ∪ {1}) |
20 | 19 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0..^2) = ({0} ∪
{1})) |
21 | | fzofi 13547 |
. . . . . 6
⊢ (0..^2)
∈ Fin |
22 | 21 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0..^2) ∈
Fin) |
23 | | 2z 12209 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
24 | | 3z 12210 |
. . . . . . . . 9
⊢ 3 ∈
ℤ |
25 | | 2re 11904 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
26 | | 3re 11910 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
27 | | 2lt3 12002 |
. . . . . . . . . 10
⊢ 2 <
3 |
28 | 25, 26, 27 | ltleii 10955 |
. . . . . . . . 9
⊢ 2 ≤
3 |
29 | | eluz2 12444 |
. . . . . . . . 9
⊢ (3 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 3 ∈
ℤ ∧ 2 ≤ 3)) |
30 | 23, 24, 28, 29 | mpbir3an 1343 |
. . . . . . . 8
⊢ 3 ∈
(ℤ≥‘2) |
31 | | fzoss2 13270 |
. . . . . . . 8
⊢ (3 ∈
(ℤ≥‘2) → (0..^2) ⊆
(0..^3)) |
32 | 30, 31 | ax-mp 5 |
. . . . . . 7
⊢ (0..^2)
⊆ (0..^3) |
33 | 32 | sseli 3896 |
. . . . . 6
⊢ (𝑘 ∈ (0..^2) → 𝑘 ∈
(0..^3)) |
34 | 33, 12 | sylan2 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^2)) → 𝐷 ∈ ℂ) |
35 | 16, 20, 22, 34 | fprodsplit 15528 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ (0..^2)𝐷 = (∏𝑘 ∈ {0}𝐷 · ∏𝑘 ∈ {1}𝐷)) |
36 | 35 | oveq1d 7228 |
. . 3
⊢ (𝜑 → (∏𝑘 ∈ (0..^2)𝐷 · ∏𝑘 ∈ {2}𝐷) = ((∏𝑘 ∈ {0}𝐷 · ∏𝑘 ∈ {1}𝐷) · ∏𝑘 ∈ {2}𝐷)) |
37 | 13, 36 | eqtrd 2777 |
. 2
⊢ (𝜑 → ∏𝑘 ∈ (0..^3)𝐷 = ((∏𝑘 ∈ {0}𝐷 · ∏𝑘 ∈ {1}𝐷) · ∏𝑘 ∈ {2}𝐷)) |
38 | | snfi 8721 |
. . . . 5
⊢ {0}
∈ Fin |
39 | 38 | a1i 11 |
. . . 4
⊢ (𝜑 → {0} ∈
Fin) |
40 | | velsn 4557 |
. . . . 5
⊢ (𝑘 ∈ {0} ↔ 𝑘 = 0) |
41 | | prodfzo03.1 |
. . . . . . 7
⊢ (𝑘 = 0 → 𝐷 = 𝐴) |
42 | 41 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 0) → 𝐷 = 𝐴) |
43 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0..^3)) ∧ 𝐷 = 𝐴) → 𝐷 = 𝐴) |
44 | 12 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0..^3)) ∧ 𝐷 = 𝐴) → 𝐷 ∈ ℂ) |
45 | 43, 44 | eqeltrrd 2839 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0..^3)) ∧ 𝐷 = 𝐴) → 𝐴 ∈ ℂ) |
46 | | c0ex 10827 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
47 | 46 | tpid1 4684 |
. . . . . . . . . . 11
⊢ 0 ∈
{0, 1, 2} |
48 | | fzo0to3tp 13328 |
. . . . . . . . . . 11
⊢ (0..^3) =
{0, 1, 2} |
49 | 47, 48 | eleqtrri 2837 |
. . . . . . . . . 10
⊢ 0 ∈
(0..^3) |
50 | | eqid 2737 |
. . . . . . . . . 10
⊢ 𝐴 = 𝐴 |
51 | 41 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (𝐷 = 𝐴 ↔ 𝐴 = 𝐴)) |
52 | 51 | rspcev 3537 |
. . . . . . . . . 10
⊢ ((0
∈ (0..^3) ∧ 𝐴 =
𝐴) → ∃𝑘 ∈ (0..^3)𝐷 = 𝐴) |
53 | 49, 50, 52 | mp2an 692 |
. . . . . . . . 9
⊢
∃𝑘 ∈
(0..^3)𝐷 = 𝐴 |
54 | 53 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑘 ∈ (0..^3)𝐷 = 𝐴) |
55 | 45, 54 | r19.29a 3208 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
56 | 55 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 0) → 𝐴 ∈ ℂ) |
57 | 42, 56 | eqeltrd 2838 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 = 0) → 𝐷 ∈ ℂ) |
58 | 40, 57 | sylan2b 597 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ {0}) → 𝐷 ∈ ℂ) |
59 | 39, 58 | fprodcl 15514 |
. . 3
⊢ (𝜑 → ∏𝑘 ∈ {0}𝐷 ∈ ℂ) |
60 | | snfi 8721 |
. . . . 5
⊢ {1}
∈ Fin |
61 | 60 | a1i 11 |
. . . 4
⊢ (𝜑 → {1} ∈
Fin) |
62 | | velsn 4557 |
. . . . 5
⊢ (𝑘 ∈ {1} ↔ 𝑘 = 1) |
63 | | prodfzo03.2 |
. . . . . . 7
⊢ (𝑘 = 1 → 𝐷 = 𝐵) |
64 | 63 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 1) → 𝐷 = 𝐵) |
65 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0..^3)) ∧ 𝐷 = 𝐵) → 𝐷 = 𝐵) |
66 | 12 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0..^3)) ∧ 𝐷 = 𝐵) → 𝐷 ∈ ℂ) |
67 | 65, 66 | eqeltrrd 2839 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0..^3)) ∧ 𝐷 = 𝐵) → 𝐵 ∈ ℂ) |
68 | | 1ex 10829 |
. . . . . . . . . . . 12
⊢ 1 ∈
V |
69 | 68 | tpid2 4686 |
. . . . . . . . . . 11
⊢ 1 ∈
{0, 1, 2} |
70 | 69, 48 | eleqtrri 2837 |
. . . . . . . . . 10
⊢ 1 ∈
(0..^3) |
71 | | eqid 2737 |
. . . . . . . . . 10
⊢ 𝐵 = 𝐵 |
72 | 63 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑘 = 1 → (𝐷 = 𝐵 ↔ 𝐵 = 𝐵)) |
73 | 72 | rspcev 3537 |
. . . . . . . . . 10
⊢ ((1
∈ (0..^3) ∧ 𝐵 =
𝐵) → ∃𝑘 ∈ (0..^3)𝐷 = 𝐵) |
74 | 70, 71, 73 | mp2an 692 |
. . . . . . . . 9
⊢
∃𝑘 ∈
(0..^3)𝐷 = 𝐵 |
75 | 74 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑘 ∈ (0..^3)𝐷 = 𝐵) |
76 | 67, 75 | r19.29a 3208 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) |
77 | 76 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 1) → 𝐵 ∈ ℂ) |
78 | 64, 77 | eqeltrd 2838 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 = 1) → 𝐷 ∈ ℂ) |
79 | 62, 78 | sylan2b 597 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ {1}) → 𝐷 ∈ ℂ) |
80 | 61, 79 | fprodcl 15514 |
. . 3
⊢ (𝜑 → ∏𝑘 ∈ {1}𝐷 ∈ ℂ) |
81 | | snfi 8721 |
. . . . 5
⊢ {2}
∈ Fin |
82 | 81 | a1i 11 |
. . . 4
⊢ (𝜑 → {2} ∈
Fin) |
83 | | velsn 4557 |
. . . . 5
⊢ (𝑘 ∈ {2} ↔ 𝑘 = 2) |
84 | | prodfzo03.3 |
. . . . . . 7
⊢ (𝑘 = 2 → 𝐷 = 𝐶) |
85 | 84 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 2) → 𝐷 = 𝐶) |
86 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0..^3)) ∧ 𝐷 = 𝐶) → 𝐷 = 𝐶) |
87 | 12 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0..^3)) ∧ 𝐷 = 𝐶) → 𝐷 ∈ ℂ) |
88 | 86, 87 | eqeltrrd 2839 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0..^3)) ∧ 𝐷 = 𝐶) → 𝐶 ∈ ℂ) |
89 | | 2ex 11907 |
. . . . . . . . . . . 12
⊢ 2 ∈
V |
90 | 89 | tpid3 4689 |
. . . . . . . . . . 11
⊢ 2 ∈
{0, 1, 2} |
91 | 90, 48 | eleqtrri 2837 |
. . . . . . . . . 10
⊢ 2 ∈
(0..^3) |
92 | | eqid 2737 |
. . . . . . . . . 10
⊢ 𝐶 = 𝐶 |
93 | 84 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑘 = 2 → (𝐷 = 𝐶 ↔ 𝐶 = 𝐶)) |
94 | 93 | rspcev 3537 |
. . . . . . . . . 10
⊢ ((2
∈ (0..^3) ∧ 𝐶 =
𝐶) → ∃𝑘 ∈ (0..^3)𝐷 = 𝐶) |
95 | 91, 92, 94 | mp2an 692 |
. . . . . . . . 9
⊢
∃𝑘 ∈
(0..^3)𝐷 = 𝐶 |
96 | 95 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑘 ∈ (0..^3)𝐷 = 𝐶) |
97 | 88, 96 | r19.29a 3208 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) |
98 | 97 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 2) → 𝐶 ∈ ℂ) |
99 | 85, 98 | eqeltrd 2838 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 = 2) → 𝐷 ∈ ℂ) |
100 | 83, 99 | sylan2b 597 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ {2}) → 𝐷 ∈ ℂ) |
101 | 82, 100 | fprodcl 15514 |
. . 3
⊢ (𝜑 → ∏𝑘 ∈ {2}𝐷 ∈ ℂ) |
102 | 59, 80, 101 | mulassd 10856 |
. 2
⊢ (𝜑 → ((∏𝑘 ∈ {0}𝐷 · ∏𝑘 ∈ {1}𝐷) · ∏𝑘 ∈ {2}𝐷) = (∏𝑘 ∈ {0}𝐷 · (∏𝑘 ∈ {1}𝐷 · ∏𝑘 ∈ {2}𝐷))) |
103 | | 0nn0 12105 |
. . . . 5
⊢ 0 ∈
ℕ0 |
104 | 103 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈
ℕ0) |
105 | 41 | prodsn 15524 |
. . . 4
⊢ ((0
∈ ℕ0 ∧ 𝐴 ∈ ℂ) → ∏𝑘 ∈ {0}𝐷 = 𝐴) |
106 | 104, 55, 105 | syl2anc 587 |
. . 3
⊢ (𝜑 → ∏𝑘 ∈ {0}𝐷 = 𝐴) |
107 | | 1nn0 12106 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
108 | 107 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℕ0) |
109 | 63 | prodsn 15524 |
. . . . 5
⊢ ((1
∈ ℕ0 ∧ 𝐵 ∈ ℂ) → ∏𝑘 ∈ {1}𝐷 = 𝐵) |
110 | 108, 76, 109 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ {1}𝐷 = 𝐵) |
111 | | 2nn0 12107 |
. . . . . 6
⊢ 2 ∈
ℕ0 |
112 | 111 | a1i 11 |
. . . . 5
⊢ (𝜑 → 2 ∈
ℕ0) |
113 | 84 | prodsn 15524 |
. . . . 5
⊢ ((2
∈ ℕ0 ∧ 𝐶 ∈ ℂ) → ∏𝑘 ∈ {2}𝐷 = 𝐶) |
114 | 112, 97, 113 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ∏𝑘 ∈ {2}𝐷 = 𝐶) |
115 | 110, 114 | oveq12d 7231 |
. . 3
⊢ (𝜑 → (∏𝑘 ∈ {1}𝐷 · ∏𝑘 ∈ {2}𝐷) = (𝐵 · 𝐶)) |
116 | 106, 115 | oveq12d 7231 |
. 2
⊢ (𝜑 → (∏𝑘 ∈ {0}𝐷 · (∏𝑘 ∈ {1}𝐷 · ∏𝑘 ∈ {2}𝐷)) = (𝐴 · (𝐵 · 𝐶))) |
117 | 37, 102, 116 | 3eqtrd 2781 |
1
⊢ (𝜑 → ∏𝑘 ∈ (0..^3)𝐷 = (𝐴 · (𝐵 · 𝐶))) |