| Step | Hyp | Ref
| Expression |
| 1 | | nnre 12273 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ) |
| 2 | 1 | renegcld 11690 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → -𝑗 ∈
ℝ) |
| 3 | | opelxpi 5722 |
. . . . . . . 8
⊢ ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) →
〈-𝑗, 𝑗〉 ∈ (ℝ ×
ℝ)) |
| 4 | 2, 1, 3 | syl2anc 584 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ →
〈-𝑗, 𝑗〉 ∈ (ℝ ×
ℝ)) |
| 5 | 4 | ad2antlr 727 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 〈-𝑗, 𝑗〉 ∈ (ℝ ×
ℝ)) |
| 6 | | eqid 2737 |
. . . . . 6
⊢ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) = (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) |
| 7 | 5, 6 | fmptd 7134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉):𝑋⟶(ℝ ×
ℝ)) |
| 8 | | reex 11246 |
. . . . . . . . 9
⊢ ℝ
∈ V |
| 9 | 8, 8 | xpex 7773 |
. . . . . . . 8
⊢ (ℝ
× ℝ) ∈ V |
| 10 | 9 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (ℝ × ℝ)
∈ V) |
| 11 | | hoicvrrex.fi |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ Fin) |
| 12 | | elmapg 8879 |
. . . . . . 7
⊢
(((ℝ × ℝ) ∈ V ∧ 𝑋 ∈ Fin) → ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ ((ℝ × ℝ)
↑m 𝑋)
↔ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉):𝑋⟶(ℝ ×
ℝ))) |
| 13 | 10, 11, 12 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ ((ℝ × ℝ)
↑m 𝑋)
↔ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉):𝑋⟶(ℝ ×
ℝ))) |
| 14 | 13 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ ((ℝ × ℝ)
↑m 𝑋)
↔ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉):𝑋⟶(ℝ ×
ℝ))) |
| 15 | 7, 14 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ ((ℝ × ℝ)
↑m 𝑋)) |
| 16 | | eqid 2737 |
. . . 4
⊢ (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
| 17 | 15, 16 | fmptd 7134 |
. . 3
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)):ℕ⟶((ℝ ×
ℝ) ↑m 𝑋)) |
| 18 | | ovex 7464 |
. . . 4
⊢ ((ℝ
× ℝ) ↑m 𝑋) ∈ V |
| 19 | | nnex 12272 |
. . . 4
⊢ ℕ
∈ V |
| 20 | 18, 19 | elmap 8911 |
. . 3
⊢ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ↔ (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)):ℕ⟶((ℝ ×
ℝ) ↑m 𝑋)) |
| 21 | 17, 20 | sylibr 234 |
. 2
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) |
| 22 | | hoicvrrex.y |
. . . 4
⊢ (𝜑 → 𝑌 ⊆ (ℝ ↑m 𝑋)) |
| 23 | | eqid 2737 |
. . . . . 6
⊢ (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) = (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
| 24 | 23, 11 | hoicvr 46563 |
. . . . 5
⊢ (𝜑 → (ℝ
↑m 𝑋)
⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
| 25 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑘 → 〈-𝑗, 𝑗〉 = 〈-𝑗, 𝑗〉) |
| 26 | 25 | cbvmptv 5255 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) = (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) |
| 27 | 26 | mpteq2i 5247 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
| 28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))) |
| 29 | 28 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗) = ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)) |
| 30 | 29 | coeq2d 5873 |
. . . . . . . 8
⊢ (𝜑 → ([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)) = ([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))) |
| 31 | 30 | fveq1d 6908 |
. . . . . . 7
⊢ (𝜑 → (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) = (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
| 32 | 31 | ixpeq2dv 8953 |
. . . . . 6
⊢ (𝜑 → X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
| 33 | 32 | iuneq2d 5022 |
. . . . 5
⊢ (𝜑 → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
| 34 | 24, 33 | sseqtrd 4020 |
. . . 4
⊢ (𝜑 → (ℝ
↑m 𝑋)
⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
| 35 | 22, 34 | sstrd 3994 |
. . 3
⊢ (𝜑 → 𝑌 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
| 36 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
| 37 | 15 | elexd 3504 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ V) |
| 38 | 16 | fvmpt2 7027 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ ℕ ∧ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) ∈ V) → ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗) = (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
| 39 | 36, 37, 38 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗) = (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
| 40 | 39, 5 | fmpt3d 7136 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
| 41 | 40 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
| 42 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
| 43 | 41, 42 | fvovco 45198 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) = ((1st ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘))[,)(2nd ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘)))) |
| 44 | 39 | fveq1d 6908 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘) = ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)‘𝑘)) |
| 45 | 44 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘) = ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)‘𝑘)) |
| 46 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
| 47 | | opex 5469 |
. . . . . . . . . . . . . . . . . 18
⊢
〈-𝑗, 𝑗〉 ∈ V |
| 48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 〈-𝑗, 𝑗〉 ∈ V) |
| 49 | 6 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ 𝑋 ∧ 〈-𝑗, 𝑗〉 ∈ V) → ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)‘𝑘) = 〈-𝑗, 𝑗〉) |
| 50 | 46, 48, 49 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)‘𝑘) = 〈-𝑗, 𝑗〉) |
| 51 | 50 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)‘𝑘) = 〈-𝑗, 𝑗〉) |
| 52 | 45, 51 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘) = 〈-𝑗, 𝑗〉) |
| 53 | 52 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1st ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘)) = (1st ‘〈-𝑗, 𝑗〉)) |
| 54 | | negex 11506 |
. . . . . . . . . . . . . . 15
⊢ -𝑗 ∈ V |
| 55 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑗 ∈ V |
| 56 | 54, 55 | op1st 8022 |
. . . . . . . . . . . . . 14
⊢
(1st ‘〈-𝑗, 𝑗〉) = -𝑗 |
| 57 | 56 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1st ‘〈-𝑗, 𝑗〉) = -𝑗) |
| 58 | 53, 57 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1st ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘)) = -𝑗) |
| 59 | 52 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (2nd ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘)) = (2nd ‘〈-𝑗, 𝑗〉)) |
| 60 | 54, 55 | op2nd 8023 |
. . . . . . . . . . . . . 14
⊢
(2nd ‘〈-𝑗, 𝑗〉) = 𝑗 |
| 61 | 60 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (2nd ‘〈-𝑗, 𝑗〉) = 𝑗) |
| 62 | 59, 61 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (2nd ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘)) = 𝑗) |
| 63 | 58, 62 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((1st ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘))[,)(2nd ‘(((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)‘𝑘))) = (-𝑗[,)𝑗)) |
| 64 | 43, 63 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) = (-𝑗[,)𝑗)) |
| 65 | 64 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) = (vol‘(-𝑗[,)𝑗))) |
| 66 | | volico 45998 |
. . . . . . . . . . . 12
⊢ ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) →
(vol‘(-𝑗[,)𝑗)) = if(-𝑗 < 𝑗, (𝑗 − -𝑗), 0)) |
| 67 | 2, 1, 66 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ →
(vol‘(-𝑗[,)𝑗)) = if(-𝑗 < 𝑗, (𝑗 − -𝑗), 0)) |
| 68 | | nnrp 13046 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ+) |
| 69 | | neglt 45296 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℝ+
→ -𝑗 < 𝑗) |
| 70 | 68, 69 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → -𝑗 < 𝑗) |
| 71 | 70 | iftrued 4533 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → if(-𝑗 < 𝑗, (𝑗 − -𝑗), 0) = (𝑗 − -𝑗)) |
| 72 | 1 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℂ) |
| 73 | 72, 72 | subnegd 11627 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (𝑗 − -𝑗) = (𝑗 + 𝑗)) |
| 74 | 72 | 2timesd 12509 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℕ → (2
· 𝑗) = (𝑗 + 𝑗)) |
| 75 | 73, 74 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → (𝑗 − -𝑗) = (2 · 𝑗)) |
| 76 | 67, 71, 75 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ →
(vol‘(-𝑗[,)𝑗)) = (2 · 𝑗)) |
| 77 | 76 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘(-𝑗[,)𝑗)) = (2 · 𝑗)) |
| 78 | 65, 77 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) = (2 · 𝑗)) |
| 79 | 78 | prodeq2dv 15958 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 (2 · 𝑗)) |
| 80 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin) |
| 81 | | 2cnd 12344 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 2 ∈
ℂ) |
| 82 | 72 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℂ) |
| 83 | 81, 82 | mulcld 11281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · 𝑗) ∈
ℂ) |
| 84 | | fprodconst 16014 |
. . . . . . . 8
⊢ ((𝑋 ∈ Fin ∧ (2 ·
𝑗) ∈ ℂ) →
∏𝑘 ∈ 𝑋 (2 · 𝑗) = ((2 · 𝑗)↑(♯‘𝑋))) |
| 85 | 80, 83, 84 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (2 · 𝑗) = ((2 · 𝑗)↑(♯‘𝑋))) |
| 86 | 79, 85 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) = ((2 · 𝑗)↑(♯‘𝑋))) |
| 87 | 86 | mpteq2dva 5242 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋)))) |
| 88 | 87 | fveq2d 6910 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋))))) |
| 89 | 19 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℕ ∈
V) |
| 90 | 68 | ssriv 3987 |
. . . . . . . . . 10
⊢ ℕ
⊆ ℝ+ |
| 91 | | ioorp 13465 |
. . . . . . . . . . 11
⊢
(0(,)+∞) = ℝ+ |
| 92 | 91 | eqcomi 2746 |
. . . . . . . . . 10
⊢
ℝ+ = (0(,)+∞) |
| 93 | 90, 92 | sseqtri 4032 |
. . . . . . . . 9
⊢ ℕ
⊆ (0(,)+∞) |
| 94 | | ioossicc 13473 |
. . . . . . . . 9
⊢
(0(,)+∞) ⊆ (0[,]+∞) |
| 95 | 93, 94 | sstri 3993 |
. . . . . . . 8
⊢ ℕ
⊆ (0[,]+∞) |
| 96 | | 2nn 12339 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
| 97 | 96 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 2 ∈
ℕ) |
| 98 | 97, 36 | nnmulcld 12319 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (2 · 𝑗) ∈
ℕ) |
| 99 | | hashcl 14395 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ Fin →
(♯‘𝑋) ∈
ℕ0) |
| 100 | 11, 99 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝑋) ∈
ℕ0) |
| 101 | 100 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (♯‘𝑋) ∈
ℕ0) |
| 102 | | nnexpcl 14115 |
. . . . . . . . 9
⊢ (((2
· 𝑗) ∈ ℕ
∧ (♯‘𝑋)
∈ ℕ0) → ((2 · 𝑗)↑(♯‘𝑋)) ∈ ℕ) |
| 103 | 98, 101, 102 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2 · 𝑗)↑(♯‘𝑋)) ∈
ℕ) |
| 104 | 95, 103 | sselid 3981 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((2 · 𝑗)↑(♯‘𝑋)) ∈
(0[,]+∞)) |
| 105 | | eqid 2737 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ ↦ ((2
· 𝑗)↑(♯‘𝑋))) = (𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋))) |
| 106 | 104, 105 | fmptd 7134 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋))):ℕ⟶(0[,]+∞)) |
| 107 | 89, 106 | sge0xrcl 46400 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋)))) ∈
ℝ*) |
| 108 | | pnfxr 11315 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
| 109 | 108 | a1i 11 |
. . . . . 6
⊢ (𝜑 → +∞ ∈
ℝ*) |
| 110 | | 1nn 12277 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ |
| 111 | 95, 110 | sselii 3980 |
. . . . . . . . 9
⊢ 1 ∈
(0[,]+∞) |
| 112 | 111 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 1 ∈
(0[,]+∞)) |
| 113 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ ↦ 1) =
(𝑗 ∈ ℕ ↦
1) |
| 114 | 112, 113 | fmptd 7134 |
. . . . . . 7
⊢ (𝜑 → (𝑗 ∈ ℕ ↦
1):ℕ⟶(0[,]+∞)) |
| 115 | 89, 114 | sge0xrcl 46400 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ 1)) ∈
ℝ*) |
| 116 | | nnnfi 14007 |
. . . . . . . . . 10
⊢ ¬
ℕ ∈ Fin |
| 117 | 116 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ¬ ℕ ∈
Fin) |
| 118 | | 1rp 13038 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ+ |
| 119 | 118 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ+) |
| 120 | 89, 117, 119 | sge0rpcpnf 46436 |
. . . . . . . 8
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ 1)) =
+∞) |
| 121 | 120 | eqcomd 2743 |
. . . . . . 7
⊢ (𝜑 → +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ 1))) |
| 122 | 109, 121 | xreqled 45341 |
. . . . . 6
⊢ (𝜑 → +∞ ≤
(Σ^‘(𝑗 ∈ ℕ ↦ 1))) |
| 123 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑗𝜑 |
| 124 | 114 | fvmptelcdm 7133 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 1 ∈
(0[,]+∞)) |
| 125 | 103 | nnge1d 12314 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 1 ≤ ((2 ·
𝑗)↑(♯‘𝑋))) |
| 126 | 123, 89, 124, 104, 125 | sge0lempt 46425 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ 1)) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋))))) |
| 127 | 109, 115,
107, 122, 126 | xrletrd 13204 |
. . . . 5
⊢ (𝜑 → +∞ ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋))))) |
| 128 | 107, 127 | xrgepnfd 45342 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((2 · 𝑗)↑(♯‘𝑋)))) =
+∞) |
| 129 | | eqidd 2738 |
. . . 4
⊢ (𝜑 → +∞ =
+∞) |
| 130 | 88, 128, 129 | 3eqtrrd 2782 |
. . 3
⊢ (𝜑 → +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))))) |
| 131 | 35, 130 | jca 511 |
. 2
⊢ (𝜑 → (𝑌 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) ∧ +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)))))) |
| 132 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑗𝑖 |
| 133 | | nfmpt1 5250 |
. . . . . . 7
⊢
Ⅎ𝑗(𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
| 134 | 132, 133 | nfeq 2919 |
. . . . . 6
⊢
Ⅎ𝑗 𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
| 135 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑘𝑖 |
| 136 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑘ℕ |
| 137 | | nfmpt1 5250 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉) |
| 138 | 136, 137 | nfmpt 5249 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
| 139 | 135, 138 | nfeq 2919 |
. . . . . . . 8
⊢
Ⅎ𝑘 𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) |
| 140 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → (𝑖‘𝑗) = ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗)) |
| 141 | 140 | coeq2d 5873 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))) |
| 142 | 141 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
| 143 | 142 | adantr 480 |
. . . . . . . 8
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
| 144 | 139, 143 | ixpeq2d 45073 |
. . . . . . 7
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
| 145 | 144 | adantr 480 |
. . . . . 6
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
| 146 | 134, 145 | iuneq2df 45052 |
. . . . 5
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)) |
| 147 | 146 | sseq2d 4016 |
. . . 4
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → (𝑌 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ 𝑌 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))) |
| 148 | 142 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → (vol‘(([,) ∘
(𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))) |
| 149 | 148 | a1d 25 |
. . . . . . . . . 10
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → (𝑘 ∈ 𝑋 → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)))) |
| 150 | 139, 149 | ralrimi 3257 |
. . . . . . . . 9
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → ∀𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))) |
| 151 | 150 | adantr 480 |
. . . . . . . 8
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) ∧ 𝑗 ∈ ℕ) → ∀𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))) |
| 152 | 151 | prodeq2d 15957 |
. . . . . . 7
⊢ ((𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))) |
| 153 | 134, 152 | mpteq2da 5240 |
. . . . . 6
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)))) |
| 154 | 153 | fveq2d 6910 |
. . . . 5
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) →
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))))) |
| 155 | 154 | eqeq2d 2748 |
. . . 4
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → (+∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)))))) |
| 156 | 147, 155 | anbi12d 632 |
. . 3
⊢ (𝑖 = (𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) → ((𝑌 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ (𝑌 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) ∧ +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘))))))) |
| 157 | 156 | rspcev 3622 |
. 2
⊢ (((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉)) ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝑌 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘) ∧ +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ ((𝑗 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ 〈-𝑗, 𝑗〉))‘𝑗))‘𝑘)))))) → ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝑌 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
| 158 | 21, 131, 157 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝑌 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |