| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnex 12272 | . . . 4
⊢ ℕ
∈ V | 
| 2 | 1 | a1i 11 | . . 3
⊢ (𝜑 → ℕ ∈
V) | 
| 3 |  | sge0hsphoire.l | . . . . . 6
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) | 
| 4 |  | sge0hsphoire.w | . . . . . . . 8
⊢ 𝑊 = (𝑌 ∪ {𝑍}) | 
| 5 |  | sge0hsphoire.f | . . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ Fin) | 
| 6 |  | snfi 9083 | . . . . . . . . . 10
⊢ {𝑍} ∈ Fin | 
| 7 | 6 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → {𝑍} ∈ Fin) | 
| 8 |  | unfi 9211 | . . . . . . . . 9
⊢ ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin) | 
| 9 | 5, 7, 8 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin) | 
| 10 | 4, 9 | eqeltrid 2845 | . . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Fin) | 
| 11 | 10 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin) | 
| 12 |  | sge0hsphoire.c | . . . . . . . 8
⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑m
𝑊)) | 
| 13 | 12 | ffvelcdmda 7104 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑m 𝑊)) | 
| 14 |  | elmapi 8889 | . . . . . . 7
⊢ ((𝐶‘𝑗) ∈ (ℝ ↑m 𝑊) → (𝐶‘𝑗):𝑊⟶ℝ) | 
| 15 | 13, 14 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑊⟶ℝ) | 
| 16 |  | sge0hsphoire.h | . . . . . . . 8
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) | 
| 17 |  | eleq1w 2824 | . . . . . . . . . . . 12
⊢ (𝑗 = ℎ → (𝑗 ∈ 𝑌 ↔ ℎ ∈ 𝑌)) | 
| 18 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑗 = ℎ → (𝑐‘𝑗) = (𝑐‘ℎ)) | 
| 19 | 18 | breq1d 5153 | . . . . . . . . . . . . 13
⊢ (𝑗 = ℎ → ((𝑐‘𝑗) ≤ 𝑥 ↔ (𝑐‘ℎ) ≤ 𝑥)) | 
| 20 | 19, 18 | ifbieq1d 4550 | . . . . . . . . . . . 12
⊢ (𝑗 = ℎ → if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥) = if((𝑐‘ℎ) ≤ 𝑥, (𝑐‘ℎ), 𝑥)) | 
| 21 | 17, 18, 20 | ifbieq12d 4554 | . . . . . . . . . . 11
⊢ (𝑗 = ℎ → if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)) = if(ℎ ∈ 𝑌, (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑥, (𝑐‘ℎ), 𝑥))) | 
| 22 | 21 | cbvmptv 5255 | . . . . . . . . . 10
⊢ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))) = (ℎ ∈ 𝑊 ↦ if(ℎ ∈ 𝑌, (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑥, (𝑐‘ℎ), 𝑥))) | 
| 23 | 22 | mpteq2i 5247 | . . . . . . . . 9
⊢ (𝑐 ∈ (ℝ
↑m 𝑊)
↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))) = (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (ℎ ∈ 𝑊 ↦ if(ℎ ∈ 𝑌, (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑥, (𝑐‘ℎ), 𝑥)))) | 
| 24 | 23 | mpteq2i 5247 | . . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ
↑m 𝑊)
↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (ℎ ∈ 𝑊 ↦ if(ℎ ∈ 𝑌, (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑥, (𝑐‘ℎ), 𝑥))))) | 
| 25 | 16, 24 | eqtri 2765 | . . . . . . 7
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (ℎ ∈ 𝑊 ↦ if(ℎ ∈ 𝑌, (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑥, (𝑐‘ℎ), 𝑥))))) | 
| 26 |  | sge0hsphoire.s | . . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℝ) | 
| 27 | 26 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ) | 
| 28 |  | sge0hsphoire.d | . . . . . . . . 9
⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑m
𝑊)) | 
| 29 | 28 | ffvelcdmda 7104 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑m 𝑊)) | 
| 30 |  | elmapi 8889 | . . . . . . . 8
⊢ ((𝐷‘𝑗) ∈ (ℝ ↑m 𝑊) → (𝐷‘𝑗):𝑊⟶ℝ) | 
| 31 | 29, 30 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑊⟶ℝ) | 
| 32 | 25, 27, 11, 31 | hsphoif 46591 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑆)‘(𝐷‘𝑗)):𝑊⟶ℝ) | 
| 33 | 3, 11, 15, 32 | hoidmvcl 46597 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) | 
| 34 |  | eqid 2737 | . . . . 5
⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) | 
| 35 | 33, 34 | fmptd 7134 | . . . 4
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))):ℕ⟶(0[,)+∞)) | 
| 36 |  | icossicc 13476 | . . . . 5
⊢
(0[,)+∞) ⊆ (0[,]+∞) | 
| 37 | 36 | a1i 11 | . . . 4
⊢ (𝜑 → (0[,)+∞) ⊆
(0[,]+∞)) | 
| 38 | 35, 37 | fssd 6753 | . . 3
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))):ℕ⟶(0[,]+∞)) | 
| 39 | 2, 38 | sge0cl 46396 | . 2
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ (0[,]+∞)) | 
| 40 | 2, 38 | sge0xrcl 46400 | . . 3
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈
ℝ*) | 
| 41 |  | pnfxr 11315 | . . . 4
⊢ +∞
∈ ℝ* | 
| 42 | 41 | a1i 11 | . . 3
⊢ (𝜑 → +∞ ∈
ℝ*) | 
| 43 |  | sge0hsphoire.r | . . . . 5
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) | 
| 44 | 43 | rexrd 11311 | . . . 4
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈
ℝ*) | 
| 45 |  | nfv 1914 | . . . . 5
⊢
Ⅎ𝑗𝜑 | 
| 46 | 36, 33 | sselid 3981 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) | 
| 47 | 3, 11, 15, 31 | hoidmvcl 46597 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) ∈ (0[,)+∞)) | 
| 48 | 36, 47 | sselid 3981 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) ∈ (0[,]+∞)) | 
| 49 |  | sge0hsphoire.z | . . . . . . 7
⊢ (𝜑 → 𝑍 ∈ (𝑊 ∖ 𝑌)) | 
| 50 | 49 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊 ∖ 𝑌)) | 
| 51 | 3, 11, 50, 4, 27, 25, 15, 31 | hsphoidmvle 46601 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))) | 
| 52 | 45, 2, 46, 48, 51 | sge0lempt 46425 | . . . 4
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) | 
| 53 | 43 | ltpnfd 13163 | . . . 4
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) < +∞) | 
| 54 | 40, 44, 42, 52, 53 | xrlelttrd 13202 | . . 3
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) < +∞) | 
| 55 | 40, 42, 54 | xrltned 45368 | . 2
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ≠ +∞) | 
| 56 |  | ge0xrre 45544 | . 2
⊢
(((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ (0[,]+∞) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ≠ +∞) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ) | 
| 57 | 39, 55, 56 | syl2anc 584 | 1
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ) |