Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . 6
⊢ (𝑎 = (𝑇‘𝑏) → (𝑁‘𝑎) = (𝑁‘(𝑇‘𝑏))) |
2 | 1 | fveq2d 6195 |
. . . . 5
⊢ (𝑎 = (𝑇‘𝑏) → (𝐿‘(𝑁‘𝑎)) = (𝐿‘(𝑁‘(𝑇‘𝑏)))) |
3 | | tpfi 8236 |
. . . . . 6
⊢ {0, 1, 2}
∈ Fin |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → {0, 1, 2} ∈
Fin) |
5 | | hgt750lemg.t |
. . . . . 6
⊢ (𝜑 → 𝑇:(0..^3)–1-1-onto→(0..^3)) |
6 | | fzo0to3tp 12554 |
. . . . . . 7
⊢ (0..^3) =
{0, 1, 2} |
7 | | f1oeq23 6130 |
. . . . . . 7
⊢ (((0..^3)
= {0, 1, 2} ∧ (0..^3) = {0, 1, 2}) → (𝑇:(0..^3)–1-1-onto→(0..^3) ↔ 𝑇:{0, 1, 2}–1-1-onto→{0,
1, 2})) |
8 | 6, 6, 7 | mp2an 708 |
. . . . . 6
⊢ (𝑇:(0..^3)–1-1-onto→(0..^3) ↔ 𝑇:{0, 1, 2}–1-1-onto→{0,
1, 2}) |
9 | 5, 8 | sylib 208 |
. . . . 5
⊢ (𝜑 → 𝑇:{0, 1, 2}–1-1-onto→{0,
1, 2}) |
10 | | eqidd 2623 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ {0, 1, 2}) → (𝑇‘𝑏) = (𝑇‘𝑏)) |
11 | | hgt750lemg.l |
. . . . . . . 8
⊢ (𝜑 → 𝐿:ℕ⟶ℝ) |
12 | 11 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ {0, 1, 2}) → 𝐿:ℕ⟶ℝ) |
13 | | hgt750lemg.n |
. . . . . . . . 9
⊢ (𝜑 → 𝑁:(0..^3)⟶ℕ) |
14 | 13 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ {0, 1, 2}) → 𝑁:(0..^3)⟶ℕ) |
15 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ {0, 1, 2}) → 𝑎 ∈ {0, 1, 2}) |
16 | 15, 6 | syl6eleqr 2712 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ {0, 1, 2}) → 𝑎 ∈ (0..^3)) |
17 | 14, 16 | ffvelrnd 6360 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ {0, 1, 2}) → (𝑁‘𝑎) ∈ ℕ) |
18 | 12, 17 | ffvelrnd 6360 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ {0, 1, 2}) → (𝐿‘(𝑁‘𝑎)) ∈ ℝ) |
19 | 18 | recnd 10068 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ {0, 1, 2}) → (𝐿‘(𝑁‘𝑎)) ∈ ℂ) |
20 | 2, 4, 9, 10, 19 | fprodf1o 14676 |
. . . 4
⊢ (𝜑 → ∏𝑎 ∈ {0, 1, 2} (𝐿‘(𝑁‘𝑎)) = ∏𝑏 ∈ {0, 1, 2} (𝐿‘(𝑁‘(𝑇‘𝑏)))) |
21 | | hgt750lemg.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑐 ∈ 𝑅 ↦ (𝑐 ∘ 𝑇)) |
22 | 21 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 = (𝑐 ∈ 𝑅 ↦ (𝑐 ∘ 𝑇))) |
23 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 = 𝑁) → 𝑐 = 𝑁) |
24 | 23 | coeq1d 5283 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 = 𝑁) → (𝑐 ∘ 𝑇) = (𝑁 ∘ 𝑇)) |
25 | | hgt750lemg.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ 𝑅) |
26 | | f1of 6137 |
. . . . . . . . . . . . 13
⊢ (𝑇:(0..^3)–1-1-onto→(0..^3) → 𝑇:(0..^3)⟶(0..^3)) |
27 | 5, 26 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇:(0..^3)⟶(0..^3)) |
28 | | ovexd 6680 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0..^3) ∈
V) |
29 | | fex2 7121 |
. . . . . . . . . . . 12
⊢ ((𝑇:(0..^3)⟶(0..^3) ∧
(0..^3) ∈ V ∧ (0..^3) ∈ V) → 𝑇 ∈ V) |
30 | 27, 28, 28, 29 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ V) |
31 | | coexg 7117 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ 𝑅 ∧ 𝑇 ∈ V) → (𝑁 ∘ 𝑇) ∈ V) |
32 | 25, 30, 31 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 ∘ 𝑇) ∈ V) |
33 | 22, 24, 25, 32 | fvmptd 6288 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝑁) = (𝑁 ∘ 𝑇)) |
34 | 33 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {0, 1, 2}) → (𝐹‘𝑁) = (𝑁 ∘ 𝑇)) |
35 | 34 | fveq1d 6193 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {0, 1, 2}) → ((𝐹‘𝑁)‘𝑏) = ((𝑁 ∘ 𝑇)‘𝑏)) |
36 | | f1ofun 6139 |
. . . . . . . . . 10
⊢ (𝑇:(0..^3)–1-1-onto→(0..^3) → Fun 𝑇) |
37 | 5, 36 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → Fun 𝑇) |
38 | 37 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {0, 1, 2}) → Fun 𝑇) |
39 | | f1odm 6141 |
. . . . . . . . . . 11
⊢ (𝑇:{0, 1, 2}–1-1-onto→{0,
1, 2} → dom 𝑇 = {0, 1,
2}) |
40 | 9, 39 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝑇 = {0, 1, 2}) |
41 | 40 | eleq2d 2687 |
. . . . . . . . 9
⊢ (𝜑 → (𝑏 ∈ dom 𝑇 ↔ 𝑏 ∈ {0, 1, 2})) |
42 | 41 | biimpar 502 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {0, 1, 2}) → 𝑏 ∈ dom 𝑇) |
43 | | fvco 6274 |
. . . . . . . 8
⊢ ((Fun
𝑇 ∧ 𝑏 ∈ dom 𝑇) → ((𝑁 ∘ 𝑇)‘𝑏) = (𝑁‘(𝑇‘𝑏))) |
44 | 38, 42, 43 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {0, 1, 2}) → ((𝑁 ∘ 𝑇)‘𝑏) = (𝑁‘(𝑇‘𝑏))) |
45 | 35, 44 | eqtr2d 2657 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ {0, 1, 2}) → (𝑁‘(𝑇‘𝑏)) = ((𝐹‘𝑁)‘𝑏)) |
46 | 45 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ {0, 1, 2}) → (𝐿‘(𝑁‘(𝑇‘𝑏))) = (𝐿‘((𝐹‘𝑁)‘𝑏))) |
47 | 46 | prodeq2dv 14653 |
. . . 4
⊢ (𝜑 → ∏𝑏 ∈ {0, 1, 2} (𝐿‘(𝑁‘(𝑇‘𝑏))) = ∏𝑏 ∈ {0, 1, 2} (𝐿‘((𝐹‘𝑁)‘𝑏))) |
48 | 20, 47 | eqtr2d 2657 |
. . 3
⊢ (𝜑 → ∏𝑏 ∈ {0, 1, 2} (𝐿‘((𝐹‘𝑁)‘𝑏)) = ∏𝑎 ∈ {0, 1, 2} (𝐿‘(𝑁‘𝑎))) |
49 | | fveq2 6191 |
. . . . 5
⊢ (𝑏 = 0 → ((𝐹‘𝑁)‘𝑏) = ((𝐹‘𝑁)‘0)) |
50 | 49 | fveq2d 6195 |
. . . 4
⊢ (𝑏 = 0 → (𝐿‘((𝐹‘𝑁)‘𝑏)) = (𝐿‘((𝐹‘𝑁)‘0))) |
51 | | fveq2 6191 |
. . . . 5
⊢ (𝑏 = 1 → ((𝐹‘𝑁)‘𝑏) = ((𝐹‘𝑁)‘1)) |
52 | 51 | fveq2d 6195 |
. . . 4
⊢ (𝑏 = 1 → (𝐿‘((𝐹‘𝑁)‘𝑏)) = (𝐿‘((𝐹‘𝑁)‘1))) |
53 | | c0ex 10034 |
. . . . 5
⊢ 0 ∈
V |
54 | 53 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈
V) |
55 | | 1ex 10035 |
. . . . 5
⊢ 1 ∈
V |
56 | 55 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 ∈
V) |
57 | 33 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝑁)‘0) = ((𝑁 ∘ 𝑇)‘0)) |
58 | 53 | tpid1 4303 |
. . . . . . . . . 10
⊢ 0 ∈
{0, 1, 2} |
59 | 58, 40 | syl5eleqr 2708 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ dom 𝑇) |
60 | | fvco 6274 |
. . . . . . . . 9
⊢ ((Fun
𝑇 ∧ 0 ∈ dom 𝑇) → ((𝑁 ∘ 𝑇)‘0) = (𝑁‘(𝑇‘0))) |
61 | 37, 59, 60 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 ∘ 𝑇)‘0) = (𝑁‘(𝑇‘0))) |
62 | 57, 61 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝑁)‘0) = (𝑁‘(𝑇‘0))) |
63 | 58, 6 | eleqtrri 2700 |
. . . . . . . . . 10
⊢ 0 ∈
(0..^3) |
64 | 63 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
(0..^3)) |
65 | 27, 64 | ffvelrnd 6360 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘0) ∈ (0..^3)) |
66 | 13, 65 | ffvelrnd 6360 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘(𝑇‘0)) ∈ ℕ) |
67 | 62, 66 | eqeltrd 2701 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝑁)‘0) ∈ ℕ) |
68 | 11, 67 | ffvelrnd 6360 |
. . . . 5
⊢ (𝜑 → (𝐿‘((𝐹‘𝑁)‘0)) ∈ ℝ) |
69 | 68 | recnd 10068 |
. . . 4
⊢ (𝜑 → (𝐿‘((𝐹‘𝑁)‘0)) ∈ ℂ) |
70 | 33 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝑁)‘1) = ((𝑁 ∘ 𝑇)‘1)) |
71 | 55 | tpid2 4304 |
. . . . . . . . . 10
⊢ 1 ∈
{0, 1, 2} |
72 | 71, 40 | syl5eleqr 2708 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈ dom 𝑇) |
73 | | fvco 6274 |
. . . . . . . . 9
⊢ ((Fun
𝑇 ∧ 1 ∈ dom 𝑇) → ((𝑁 ∘ 𝑇)‘1) = (𝑁‘(𝑇‘1))) |
74 | 37, 72, 73 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 ∘ 𝑇)‘1) = (𝑁‘(𝑇‘1))) |
75 | 70, 74 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝑁)‘1) = (𝑁‘(𝑇‘1))) |
76 | 71, 6 | eleqtrri 2700 |
. . . . . . . . . 10
⊢ 1 ∈
(0..^3) |
77 | 76 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
(0..^3)) |
78 | 27, 77 | ffvelrnd 6360 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘1) ∈ (0..^3)) |
79 | 13, 78 | ffvelrnd 6360 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘(𝑇‘1)) ∈ ℕ) |
80 | 75, 79 | eqeltrd 2701 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝑁)‘1) ∈ ℕ) |
81 | 11, 80 | ffvelrnd 6360 |
. . . . 5
⊢ (𝜑 → (𝐿‘((𝐹‘𝑁)‘1)) ∈ ℝ) |
82 | 81 | recnd 10068 |
. . . 4
⊢ (𝜑 → (𝐿‘((𝐹‘𝑁)‘1)) ∈ ℂ) |
83 | | 0ne1 11088 |
. . . . 5
⊢ 0 ≠
1 |
84 | 83 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ≠ 1) |
85 | | fveq2 6191 |
. . . . 5
⊢ (𝑏 = 2 → ((𝐹‘𝑁)‘𝑏) = ((𝐹‘𝑁)‘2)) |
86 | 85 | fveq2d 6195 |
. . . 4
⊢ (𝑏 = 2 → (𝐿‘((𝐹‘𝑁)‘𝑏)) = (𝐿‘((𝐹‘𝑁)‘2))) |
87 | | 2ex 11092 |
. . . . 5
⊢ 2 ∈
V |
88 | 87 | a1i 11 |
. . . 4
⊢ (𝜑 → 2 ∈
V) |
89 | 33 | fveq1d 6193 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝑁)‘2) = ((𝑁 ∘ 𝑇)‘2)) |
90 | 87 | tpid3 4307 |
. . . . . . . . . 10
⊢ 2 ∈
{0, 1, 2} |
91 | 90, 40 | syl5eleqr 2708 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈ dom 𝑇) |
92 | | fvco 6274 |
. . . . . . . . 9
⊢ ((Fun
𝑇 ∧ 2 ∈ dom 𝑇) → ((𝑁 ∘ 𝑇)‘2) = (𝑁‘(𝑇‘2))) |
93 | 37, 91, 92 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 ∘ 𝑇)‘2) = (𝑁‘(𝑇‘2))) |
94 | 89, 93 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝑁)‘2) = (𝑁‘(𝑇‘2))) |
95 | 90, 6 | eleqtrri 2700 |
. . . . . . . . . 10
⊢ 2 ∈
(0..^3) |
96 | 95 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
(0..^3)) |
97 | 27, 96 | ffvelrnd 6360 |
. . . . . . . 8
⊢ (𝜑 → (𝑇‘2) ∈ (0..^3)) |
98 | 13, 97 | ffvelrnd 6360 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘(𝑇‘2)) ∈ ℕ) |
99 | 94, 98 | eqeltrd 2701 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝑁)‘2) ∈ ℕ) |
100 | 11, 99 | ffvelrnd 6360 |
. . . . 5
⊢ (𝜑 → (𝐿‘((𝐹‘𝑁)‘2)) ∈ ℝ) |
101 | 100 | recnd 10068 |
. . . 4
⊢ (𝜑 → (𝐿‘((𝐹‘𝑁)‘2)) ∈ ℂ) |
102 | | 0ne2 11239 |
. . . . 5
⊢ 0 ≠
2 |
103 | 102 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ≠ 2) |
104 | | 1ne2 11240 |
. . . . 5
⊢ 1 ≠
2 |
105 | 104 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 ≠ 2) |
106 | 50, 52, 54, 56, 69, 82, 84, 86, 88, 101, 103, 105 | prodtp 29573 |
. . 3
⊢ (𝜑 → ∏𝑏 ∈ {0, 1, 2} (𝐿‘((𝐹‘𝑁)‘𝑏)) = (((𝐿‘((𝐹‘𝑁)‘0)) · (𝐿‘((𝐹‘𝑁)‘1))) · (𝐿‘((𝐹‘𝑁)‘2)))) |
107 | | fveq2 6191 |
. . . . 5
⊢ (𝑎 = 0 → (𝑁‘𝑎) = (𝑁‘0)) |
108 | 107 | fveq2d 6195 |
. . . 4
⊢ (𝑎 = 0 → (𝐿‘(𝑁‘𝑎)) = (𝐿‘(𝑁‘0))) |
109 | | fveq2 6191 |
. . . . 5
⊢ (𝑎 = 1 → (𝑁‘𝑎) = (𝑁‘1)) |
110 | 109 | fveq2d 6195 |
. . . 4
⊢ (𝑎 = 1 → (𝐿‘(𝑁‘𝑎)) = (𝐿‘(𝑁‘1))) |
111 | 13, 64 | ffvelrnd 6360 |
. . . . . 6
⊢ (𝜑 → (𝑁‘0) ∈ ℕ) |
112 | 11, 111 | ffvelrnd 6360 |
. . . . 5
⊢ (𝜑 → (𝐿‘(𝑁‘0)) ∈ ℝ) |
113 | 112 | recnd 10068 |
. . . 4
⊢ (𝜑 → (𝐿‘(𝑁‘0)) ∈ ℂ) |
114 | 13, 77 | ffvelrnd 6360 |
. . . . . 6
⊢ (𝜑 → (𝑁‘1) ∈ ℕ) |
115 | 11, 114 | ffvelrnd 6360 |
. . . . 5
⊢ (𝜑 → (𝐿‘(𝑁‘1)) ∈ ℝ) |
116 | 115 | recnd 10068 |
. . . 4
⊢ (𝜑 → (𝐿‘(𝑁‘1)) ∈ ℂ) |
117 | | fveq2 6191 |
. . . . 5
⊢ (𝑎 = 2 → (𝑁‘𝑎) = (𝑁‘2)) |
118 | 117 | fveq2d 6195 |
. . . 4
⊢ (𝑎 = 2 → (𝐿‘(𝑁‘𝑎)) = (𝐿‘(𝑁‘2))) |
119 | 13, 96 | ffvelrnd 6360 |
. . . . . 6
⊢ (𝜑 → (𝑁‘2) ∈ ℕ) |
120 | 11, 119 | ffvelrnd 6360 |
. . . . 5
⊢ (𝜑 → (𝐿‘(𝑁‘2)) ∈ ℝ) |
121 | 120 | recnd 10068 |
. . . 4
⊢ (𝜑 → (𝐿‘(𝑁‘2)) ∈ ℂ) |
122 | 108, 110,
54, 56, 113, 116, 84, 118, 88, 121, 103, 105 | prodtp 29573 |
. . 3
⊢ (𝜑 → ∏𝑎 ∈ {0, 1, 2} (𝐿‘(𝑁‘𝑎)) = (((𝐿‘(𝑁‘0)) · (𝐿‘(𝑁‘1))) · (𝐿‘(𝑁‘2)))) |
123 | 48, 106, 122 | 3eqtr3d 2664 |
. 2
⊢ (𝜑 → (((𝐿‘((𝐹‘𝑁)‘0)) · (𝐿‘((𝐹‘𝑁)‘1))) · (𝐿‘((𝐹‘𝑁)‘2))) = (((𝐿‘(𝑁‘0)) · (𝐿‘(𝑁‘1))) · (𝐿‘(𝑁‘2)))) |
124 | 69, 82, 101 | mulassd 10063 |
. 2
⊢ (𝜑 → (((𝐿‘((𝐹‘𝑁)‘0)) · (𝐿‘((𝐹‘𝑁)‘1))) · (𝐿‘((𝐹‘𝑁)‘2))) = ((𝐿‘((𝐹‘𝑁)‘0)) · ((𝐿‘((𝐹‘𝑁)‘1)) · (𝐿‘((𝐹‘𝑁)‘2))))) |
125 | 113, 116,
121 | mulassd 10063 |
. 2
⊢ (𝜑 → (((𝐿‘(𝑁‘0)) · (𝐿‘(𝑁‘1))) · (𝐿‘(𝑁‘2))) = ((𝐿‘(𝑁‘0)) · ((𝐿‘(𝑁‘1)) · (𝐿‘(𝑁‘2))))) |
126 | 123, 124,
125 | 3eqtr3d 2664 |
1
⊢ (𝜑 → ((𝐿‘((𝐹‘𝑁)‘0)) · ((𝐿‘((𝐹‘𝑁)‘1)) · (𝐿‘((𝐹‘𝑁)‘2)))) = ((𝐿‘(𝑁‘0)) · ((𝐿‘(𝑁‘1)) · (𝐿‘(𝑁‘2))))) |