Step | Hyp | Ref
| Expression |
1 | | nnre 11449 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ) |
2 | 1 | renegcld 10870 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → -𝑗 ∈
ℝ) |
3 | | opelxpi 5445 |
. . . . . . . 8
⊢ ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) →
〈-𝑗, 𝑗〉 ∈ (ℝ ×
ℝ)) |
4 | 2, 1, 3 | syl2anc 576 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ →
〈-𝑗, 𝑗〉 ∈ (ℝ ×
ℝ)) |
5 | 4 | ad2antlr 714 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 〈-𝑗, 𝑗〉 ∈ (ℝ ×
ℝ)) |
6 | | eqid 2778 |
. . . . . 6
⊢ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) = (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) |
7 | 5, 6 | fmptd 6703 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉):𝑋⟶(ℝ ×
ℝ)) |
8 | | reex 10428 |
. . . . . . . . 9
⊢ ℝ
∈ V |
9 | 8, 8 | xpex 7295 |
. . . . . . . 8
⊢ (ℝ
× ℝ) ∈ V |
10 | 9 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (ℝ × ℝ)
∈ V) |
11 | | hoicvrrex.fi |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ Fin) |
12 | | elmapg 8221 |
. . . . . . 7
⊢
(((ℝ × ℝ) ∈ V ∧ 𝑋 ∈ Fin) → ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ ((ℝ × ℝ)
↑𝑚 𝑋) ↔ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉):𝑋⟶(ℝ ×
ℝ))) |
13 | 10, 11, 12 | syl2anc 576 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ ((ℝ × ℝ)
↑𝑚 𝑋) ↔ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉):𝑋⟶(ℝ ×
ℝ))) |
14 | 13 | adantr 473 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ ((ℝ × ℝ)
↑𝑚 𝑋) ↔ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉):𝑋⟶(ℝ ×
ℝ))) |
15 | 7, 14 | mpbird 249 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ ((ℝ × ℝ)
↑𝑚 𝑋)) |
16 | | eqid 2778 |
. . . 4
⊢ (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
17 | 15, 16 | fmptd 6703 |
. . 3
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)):ℕ⟶((ℝ ×
ℝ) ↑𝑚 𝑋)) |
18 | | ovex 7010 |
. . . 4
⊢ ((ℝ
× ℝ) ↑𝑚 𝑋) ∈ V |
19 | | nnex 11448 |
. . . 4
⊢ ℕ
∈ V |
20 | 18, 19 | elmap 8237 |
. . 3
⊢ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ↔
(𝑗 ∈ ℕ ↦
(𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)):ℕ⟶((ℝ ×
ℝ) ↑𝑚 𝑋)) |
21 | 17, 20 | sylibr 226 |
. 2
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ)) |
22 | | hoicvrrex.y |
. . . 4
⊢ (𝜑 → 𝑌 ⊆ (ℝ ↑𝑚
𝑋)) |
23 | | eqid 2778 |
. . . . . 6
⊢ (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) = (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
24 | 23, 11 | hoicvr 42262 |
. . . . 5
⊢ (𝜑 → (ℝ
↑𝑚 𝑋) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
25 | | eqidd 2779 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑘 → 〈-𝑗, 𝑗〉 = 〈-𝑗, 𝑗〉) |
26 | 25 | cbvmptv 5029 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) = (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) |
27 | 26 | mpteq2i 5020 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))) |
29 | 28 | fveq1d 6503 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗) = ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)) |
30 | 29 | coeq2d 5584 |
. . . . . . . 8
⊢ (𝜑 → ([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)) = ([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))) |
31 | 30 | fveq1d 6503 |
. . . . . . 7
⊢ (𝜑 → (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) = (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
32 | 31 | ixpeq2dv 8277 |
. . . . . 6
⊢ (𝜑 → X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
33 | 32 | iuneq2d 4821 |
. . . . 5
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
34 | 24, 33 | sseqtrd 3899 |
. . . 4
⊢ (𝜑 → (ℝ
↑𝑚 𝑋) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
35 | 22, 34 | sstrd 3870 |
. . 3
⊢ (𝜑 → 𝑌 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
36 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
37 | 15 | elexd 3435 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ V) |
38 | 16 | fvmpt2 6607 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ ℕ ∧ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ V) → ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗) = (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
39 | 36, 37, 38 | syl2anc 576 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗) = (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
40 | 39, 5 | fmpt3d 6705 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
41 | 40 | adantr 473 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
42 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
43 | 41, 42 | fvovco 40880 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) = ((1st ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘))[,)(2nd ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘)))) |
44 | 39 | fveq1d 6503 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘) = ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)‘𝑘)) |
45 | 44 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘) = ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)‘𝑘)) |
46 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
47 | | opex 5214 |
. . . . . . . . . . . . . . . . . 18
⊢
〈-𝑗, 𝑗〉 ∈ V |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 〈-𝑗, 𝑗〉 ∈ V) |
49 | 6 | fvmpt2 6607 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ 𝑋 ∧ 〈-𝑗, 𝑗〉 ∈ V) → ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)‘𝑘) = 〈-𝑗, 𝑗〉) |
50 | 46, 48, 49 | syl2anc 576 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)‘𝑘) = 〈-𝑗, 𝑗〉) |
51 | 50 | adantlr 702 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)‘𝑘) = 〈-𝑗, 𝑗〉) |
52 | 45, 51 | eqtrd 2814 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘) = 〈-𝑗, 𝑗〉) |
53 | 52 | fveq2d 6505 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1st ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘)) = (1st ‘〈-𝑗, 𝑗〉)) |
54 | | negex 10686 |
. . . . . . . . . . . . . . 15
⊢ -𝑗 ∈ V |
55 | | vex 3418 |
. . . . . . . . . . . . . . 15
⊢ 𝑗 ∈ V |
56 | 54, 55 | op1st 7511 |
. . . . . . . . . . . . . 14
⊢
(1st ‘〈-𝑗, 𝑗〉) = -𝑗 |
57 | 56 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1st ‘〈-𝑗, 𝑗〉) = -𝑗) |
58 | 53, 57 | eqtrd 2814 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1st ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘)) = -𝑗) |
59 | 52 | fveq2d 6505 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (2nd ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘)) = (2nd ‘〈-𝑗, 𝑗〉)) |
60 | 54, 55 | op2nd 7512 |
. . . . . . . . . . . . . 14
⊢
(2nd ‘〈-𝑗, 𝑗〉) = 𝑗 |
61 | 60 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (2nd ‘〈-𝑗, 𝑗〉) = 𝑗) |
62 | 59, 61 | eqtrd 2814 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (2nd ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘)) = 𝑗) |
63 | 58, 62 | oveq12d 6996 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((1st ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘))[,)(2nd ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘))) = (-𝑗[,)𝑗)) |
64 | 43, 63 | eqtrd 2814 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) = (-𝑗[,)𝑗)) |
65 | 64 | fveq2d 6505 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) = (vol‘(-𝑗[,)𝑗))) |
66 | | volico 41700 |
. . . . . . . . . . . 12
⊢ ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) →
(vol‘(-𝑗[,)𝑗)) = if(-𝑗 < 𝑗, (𝑗 − -𝑗), 0)) |
67 | 2, 1, 66 | syl2anc 576 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ →
(vol‘(-𝑗[,)𝑗)) = if(-𝑗 < 𝑗, (𝑗 − -𝑗), 0)) |
68 | | nnrp 12220 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ+) |
69 | | neglt 40980 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℝ+
→ -𝑗 < 𝑗) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → -𝑗 < 𝑗) |
71 | 70 | iftrued 4359 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → if(-𝑗 < 𝑗, (𝑗 − -𝑗), 0) = (𝑗 − -𝑗)) |
72 | 1 | recnd 10470 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℂ) |
73 | 72, 72 | subnegd 10807 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗 − -𝑗) = (𝑗 + 𝑗)) |
74 | 72 | 2timesd 11693 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) = (𝑗 + 𝑗)) |
75 | 73, 74 | eqtr4d 2817 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → (𝑗 − -𝑗) = (2 · 𝑗)) |
76 | 67, 71, 75 | 3eqtrd 2818 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ →
(vol‘(-𝑗[,)𝑗)) = (2 · 𝑗)) |
77 | 76 | ad2antlr 714 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘(-𝑗[,)𝑗)) = (2 · 𝑗)) |
78 | 65, 77 | eqtrd 2814 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) = (2 · 𝑗)) |
79 | 78 | prodeq2dv 15140 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 (2 · 𝑗)) |
80 | 11 | adantr 473 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin) |
81 | | 2cnd 11521 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 2 ∈
ℂ) |
82 | 72 | adantl 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℂ) |
83 | 81, 82 | mulcld 10462 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · 𝑗) ∈
ℂ) |
84 | | fprodconst 15195 |
. . . . . . . 8
⊢ ((𝑋 ∈ Fin ∧ (2 ·
𝑗) ∈ ℂ) →
∏𝑘 ∈ 𝑋 (2 · 𝑗) = ((2 · 𝑗)↑(♯‘𝑋))) |
85 | 80, 83, 84 | syl2anc 576 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (2 · 𝑗) = ((2 · 𝑗)↑(♯‘𝑋))) |
86 | 79, 85 | eqtrd 2814 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) = ((2 · 𝑗)↑(♯‘𝑋))) |
87 | 86 | mpteq2dva 5023 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋)))) |
88 | 87 | fveq2d 6505 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋))))) |
89 | 19 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℕ ∈
V) |
90 | 68 | ssriv 3864 |
. . . . . . . . . 10
⊢ ℕ
⊆ ℝ+ |
91 | | ioorp 12633 |
. . . . . . . . . . 11
⊢
(0(,)+∞) = ℝ+ |
92 | 91 | eqcomi 2787 |
. . . . . . . . . 10
⊢
ℝ+ = (0(,)+∞) |
93 | 90, 92 | sseqtri 3895 |
. . . . . . . . 9
⊢ ℕ
⊆ (0(,)+∞) |
94 | | ioossicc 12641 |
. . . . . . . . 9
⊢
(0(,)+∞) ⊆ (0[,]+∞) |
95 | 93, 94 | sstri 3869 |
. . . . . . . 8
⊢ ℕ
⊆ (0[,]+∞) |
96 | | 2nn 11516 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
97 | 96 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 2 ∈
ℕ) |
98 | 97, 36 | nnmulcld 11496 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · 𝑗) ∈
ℕ) |
99 | | hashcl 13535 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ Fin →
(♯‘𝑋) ∈
ℕ0) |
100 | 11, 99 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝑋) ∈
ℕ0) |
101 | 100 | adantr 473 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (♯‘𝑋) ∈
ℕ0) |
102 | | nnexpcl 13260 |
. . . . . . . . 9
⊢ (((2
· 𝑗) ∈ ℕ
∧ (♯‘𝑋)
∈ ℕ0) → ((2 · 𝑗)↑(♯‘𝑋)) ∈ ℕ) |
103 | 98, 101, 102 | syl2anc 576 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2 · 𝑗)↑(♯‘𝑋)) ∈
ℕ) |
104 | 95, 103 | sseldi 3858 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2 · 𝑗)↑(♯‘𝑋)) ∈
(0[,]+∞)) |
105 | | eqid 2778 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ ↦ ((2
· 𝑗)↑(♯‘𝑋))) = (𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋))) |
106 | 104, 105 | fmptd 6703 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋))):ℕ⟶(0[,]+∞)) |
107 | 89, 106 | sge0xrcl 42099 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋)))) ∈
ℝ*) |
108 | | pnfxr 10496 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
109 | 108 | a1i 11 |
. . . . . 6
⊢ (𝜑 → +∞ ∈
ℝ*) |
110 | | 1nn 11454 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ |
111 | 95, 110 | sselii 3857 |
. . . . . . . . 9
⊢ 1 ∈
(0[,]+∞) |
112 | 111 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 1 ∈
(0[,]+∞)) |
113 | | eqid 2778 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ ↦ 1) =
(𝑗 ∈ ℕ ↦
1) |
114 | 112, 113 | fmptd 6703 |
. . . . . . 7
⊢ (𝜑 → (𝑗 ∈ ℕ ↦
1):ℕ⟶(0[,]+∞)) |
115 | 89, 114 | sge0xrcl 42099 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ 1)) ∈
ℝ*) |
116 | | nnnfi 13152 |
. . . . . . . . . 10
⊢ ¬
ℕ ∈ Fin |
117 | 116 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ¬ ℕ ∈
Fin) |
118 | | 1rp 12211 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ+ |
119 | 118 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ+) |
120 | 89, 117, 119 | sge0rpcpnf 42135 |
. . . . . . . 8
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ 1)) =
+∞) |
121 | 120 | eqcomd 2784 |
. . . . . . 7
⊢ (𝜑 → +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ 1))) |
122 | 109, 121 | xreqled 41028 |
. . . . . 6
⊢ (𝜑 → +∞ ≤
(Σ^‘(𝑗 ∈ ℕ ↦ 1))) |
123 | | nfv 1873 |
. . . . . . 7
⊢
Ⅎ𝑗𝜑 |
124 | 114 | fvmptelrn 6702 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 1 ∈
(0[,]+∞)) |
125 | 103 | nnge1d 11491 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 1 ≤ ((2 ·
𝑗)↑(♯‘𝑋))) |
126 | 123, 89, 124, 104, 125 | sge0lempt 42124 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ 1)) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋))))) |
127 | 109, 115,
107, 122, 126 | xrletrd 12375 |
. . . . 5
⊢ (𝜑 → +∞ ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋))))) |
128 | 107, 127 | xrgepnfd 41029 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋)))) =
+∞) |
129 | | eqidd 2779 |
. . . 4
⊢ (𝜑 → +∞ =
+∞) |
130 | 88, 128, 129 | 3eqtrrd 2819 |
. . 3
⊢ (𝜑 → +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))))) |
131 | 35, 130 | jca 504 |
. 2
⊢ (𝜑 → (𝑌 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) ∧ +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)))))) |
132 | | nfcv 2932 |
. . . . . . 7
⊢
Ⅎ𝑗𝑖 |
133 | | nfmpt1 5026 |
. . . . . . 7
⊢
Ⅎ𝑗(𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
134 | 132, 133 | nfeq 2943 |
. . . . . 6
⊢
Ⅎ𝑗 𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
135 | | nfcv 2932 |
. . . . . . . . 9
⊢
Ⅎ𝑘𝑖 |
136 | | nfcv 2932 |
. . . . . . . . . 10
⊢
Ⅎ𝑘ℕ |
137 | | nfmpt1 5026 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) |
138 | 136, 137 | nfmpt 5025 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
139 | 135, 138 | nfeq 2943 |
. . . . . . . 8
⊢
Ⅎ𝑘 𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
140 | | fveq1 6500 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → (𝑖‘𝑗) = ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)) |
141 | 140 | coeq2d 5584 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))) |
142 | 141 | fveq1d 6503 |
. . . . . . . . 9
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
143 | 142 | adantr 473 |
. . . . . . . 8
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
144 | 139, 143 | ixpeq2d 40750 |
. . . . . . 7
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
145 | 144 | adantr 473 |
. . . . . 6
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
146 | 134, 145 | iuneq2df 40727 |
. . . . 5
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
147 | 146 | sseq2d 3891 |
. . . 4
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → (𝑌 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ 𝑌 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))) |
148 | 142 | fveq2d 6505 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → (vol‘(([,) ∘
(𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))) |
149 | 148 | a1d 25 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → (𝑘 ∈ 𝑋 → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)))) |
150 | 139, 149 | ralrimi 3166 |
. . . . . . . . 9
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → ∀𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))) |
151 | 150 | adantr 473 |
. . . . . . . 8
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))) |
152 | 151 | prodeq2d 15139 |
. . . . . . 7
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))) |
153 | 134, 152 | mpteq2da 5022 |
. . . . . 6
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)))) |
154 | 153 | fveq2d 6505 |
. . . . 5
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))))) |
155 | 154 | eqeq2d 2788 |
. . . 4
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → (+∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)))))) |
156 | 147, 155 | anbi12d 621 |
. . 3
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → ((𝑌 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ (𝑌 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) ∧ +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))))))) |
157 | 156 | rspcev 3535 |
. 2
⊢ (((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝑌 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) ∧ +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)))))) → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝑌 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
158 | 21, 131, 157 | syl2anc 576 |
1
⊢ (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝑌 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |