| Step | Hyp | Ref
| Expression |
| 1 | | vonioo.l |
. . . . 5
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
| 2 | | vonioo.a |
. . . . . . 7
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
| 3 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴:𝑋⟶ℝ) |
| 4 | | feq2 6717 |
. . . . . . 7
⊢ (𝑋 = ∅ → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ)) |
| 5 | 4 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ)) |
| 6 | 3, 5 | mpbid 232 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴:∅⟶ℝ) |
| 7 | | vonioo.b |
. . . . . . 7
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
| 8 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:𝑋⟶ℝ) |
| 9 | | feq2 6717 |
. . . . . . 7
⊢ (𝑋 = ∅ → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ)) |
| 10 | 9 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ)) |
| 11 | 8, 10 | mpbid 232 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:∅⟶ℝ) |
| 12 | 1, 6, 11 | hoidmv0val 46598 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘∅)𝐵) = 0) |
| 13 | 12 | eqcomd 2743 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → 0 = (𝐴(𝐿‘∅)𝐵)) |
| 14 | | fveq2 6906 |
. . . . . 6
⊢ (𝑋 = ∅ →
(voln‘𝑋) =
(voln‘∅)) |
| 15 | | vonioo.i |
. . . . . . . 8
⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) |
| 16 | 15 | a1i 11 |
. . . . . . 7
⊢ (𝑋 = ∅ → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘))) |
| 17 | | ixpeq1 8948 |
. . . . . . 7
⊢ (𝑋 = ∅ → X𝑘 ∈
𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) = X𝑘 ∈ ∅ ((𝐴‘𝑘)(,)(𝐵‘𝑘))) |
| 18 | 16, 17 | eqtrd 2777 |
. . . . . 6
⊢ (𝑋 = ∅ → 𝐼 = X𝑘 ∈ ∅ ((𝐴‘𝑘)(,)(𝐵‘𝑘))) |
| 19 | 14, 18 | fveq12d 6913 |
. . . . 5
⊢ (𝑋 = ∅ →
((voln‘𝑋)‘𝐼) =
((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)(,)(𝐵‘𝑘)))) |
| 20 | 19 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = ((voln‘∅)‘X𝑘 ∈
∅ ((𝐴‘𝑘)(,)(𝐵‘𝑘)))) |
| 21 | | 0fi 9082 |
. . . . . . 7
⊢ ∅
∈ Fin |
| 22 | 21 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → ∅ ∈
Fin) |
| 23 | | eqid 2737 |
. . . . . 6
⊢ dom
(voln‘∅) = dom (voln‘∅) |
| 24 | | ressxr 11305 |
. . . . . . . 8
⊢ ℝ
⊆ ℝ* |
| 25 | 24 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 = ∅) → ℝ ⊆
ℝ*) |
| 26 | 6, 25 | fssd 6753 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐴:∅⟶ℝ*) |
| 27 | 11, 25 | fssd 6753 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝐵:∅⟶ℝ*) |
| 28 | 22, 23, 26, 27 | ioovonmbl 46692 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = ∅) → X𝑘 ∈
∅ ((𝐴‘𝑘)(,)(𝐵‘𝑘)) ∈ dom
(voln‘∅)) |
| 29 | 28 | von0val 46686 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) →
((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴‘𝑘)(,)(𝐵‘𝑘))) = 0) |
| 30 | 20, 29 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = 0) |
| 31 | | fveq2 6906 |
. . . . 5
⊢ (𝑋 = ∅ → (𝐿‘𝑋) = (𝐿‘∅)) |
| 32 | 31 | oveqd 7448 |
. . . 4
⊢ (𝑋 = ∅ → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵)) |
| 33 | 32 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → (𝐴(𝐿‘𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵)) |
| 34 | 13, 30, 33 | 3eqtr4d 2787 |
. 2
⊢ ((𝜑 ∧ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) |
| 35 | | neqne 2948 |
. . . 4
⊢ (¬
𝑋 = ∅ → 𝑋 ≠ ∅) |
| 36 | 35 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅) |
| 37 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝜑 ∧ 𝑋 ≠ ∅) |
| 38 | | nfra1 3284 |
. . . . . . . . 9
⊢
Ⅎ𝑘∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘) |
| 39 | 37, 38 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑘((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) |
| 40 | 2 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
| 41 | 7 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
| 42 | | volico 45998 |
. . . . . . . . . . . 12
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) < (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0)) |
| 43 | 40, 41, 42 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) < (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0)) |
| 44 | 43 | ad4ant14 752 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = if((𝐴‘𝑘) < (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0)) |
| 45 | | rspa 3248 |
. . . . . . . . . . . 12
⊢
((∀𝑘 ∈
𝑋 (𝐴‘𝑘) < (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) < (𝐵‘𝑘)) |
| 46 | 45 | iftrued 4533 |
. . . . . . . . . . 11
⊢
((∀𝑘 ∈
𝑋 (𝐴‘𝑘) < (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑋) → if((𝐴‘𝑘) < (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0) = ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 47 | 46 | adantll 714 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → if((𝐴‘𝑘) < (𝐵‘𝑘), ((𝐵‘𝑘) − (𝐴‘𝑘)), 0) = ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 48 | 44, 47 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 49 | 48 | ex 412 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) → (𝑘 ∈ 𝑋 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
| 50 | 39, 49 | ralrimi 3257 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) → ∀𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 51 | 50 | prodeq2d 15957 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 52 | 51 | eqcomd 2743 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) → ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
| 53 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝐴‘𝑘) = (𝐴‘𝑗)) |
| 54 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝐵‘𝑘) = (𝐵‘𝑗)) |
| 55 | 53, 54 | breq12d 5156 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘) < (𝐵‘𝑘) ↔ (𝐴‘𝑗) < (𝐵‘𝑗))) |
| 56 | 55 | cbvralvw 3237 |
. . . . . . . 8
⊢
(∀𝑘 ∈
𝑋 (𝐴‘𝑘) < (𝐵‘𝑘) ↔ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) < (𝐵‘𝑗)) |
| 57 | 56 | biimpi 216 |
. . . . . . 7
⊢
(∀𝑘 ∈
𝑋 (𝐴‘𝑘) < (𝐵‘𝑘) → ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) < (𝐵‘𝑗)) |
| 58 | 57 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) → ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) < (𝐵‘𝑗)) |
| 59 | | vonioo.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ Fin) |
| 60 | 59 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ∈ Fin) |
| 61 | 60 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) < (𝐵‘𝑗)) → 𝑋 ∈ Fin) |
| 62 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐴:𝑋⟶ℝ) |
| 63 | 62 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) < (𝐵‘𝑗)) → 𝐴:𝑋⟶ℝ) |
| 64 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝐵:𝑋⟶ℝ) |
| 65 | 64 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) < (𝐵‘𝑗)) → 𝐵:𝑋⟶ℝ) |
| 66 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → 𝑋 ≠ ∅) |
| 67 | 66 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) < (𝐵‘𝑗)) → 𝑋 ≠ ∅) |
| 68 | 56, 45 | sylanbr 582 |
. . . . . . . 8
⊢
((∀𝑗 ∈
𝑋 (𝐴‘𝑗) < (𝐵‘𝑗) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) < (𝐵‘𝑘)) |
| 69 | 68 | adantll 714 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) < (𝐵‘𝑗)) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) < (𝐵‘𝑘)) |
| 70 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → (𝐴‘𝑗) = (𝐴‘𝑘)) |
| 71 | 70 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → ((𝐴‘𝑗) + (1 / 𝑚)) = ((𝐴‘𝑘) + (1 / 𝑚))) |
| 72 | 71 | cbvmptv 5255 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑚))) |
| 73 | 72 | a1i 11 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑚)))) |
| 74 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛)) |
| 75 | 74 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((𝐴‘𝑘) + (1 / 𝑚)) = ((𝐴‘𝑘) + (1 / 𝑛))) |
| 76 | 75 | mpteq2dv 5244 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛)))) |
| 77 | 73, 76 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛)))) |
| 78 | 77 | cbvmptv 5255 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚)))) = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛)))) |
| 79 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑛X𝑘 ∈
𝑋 ((((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))))‘𝑚)‘𝑘)[,)(𝐵‘𝑘)) |
| 80 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑚𝑋 |
| 81 | | nffvmpt1 6917 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))))‘𝑛) |
| 82 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑚𝑘 |
| 83 | 81, 82 | nffv 6916 |
. . . . . . . . . 10
⊢
Ⅎ𝑚(((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘) |
| 84 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑚[,) |
| 85 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑚(𝐵‘𝑘) |
| 86 | 83, 84, 85 | nfov 7461 |
. . . . . . . . 9
⊢
Ⅎ𝑚((((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) |
| 87 | 80, 86 | nfixpw 8956 |
. . . . . . . 8
⊢
Ⅎ𝑚X𝑘 ∈
𝑋 ((((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) |
| 88 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))))‘𝑚) = ((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))))‘𝑛)) |
| 89 | 88 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))))‘𝑚)‘𝑘) = (((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)) |
| 90 | 89 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))))‘𝑚)‘𝑘)[,)(𝐵‘𝑘)) = ((((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) |
| 91 | 90 | ixpeq2dv 8953 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → X𝑘 ∈ 𝑋 ((((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))))‘𝑚)‘𝑘)[,)(𝐵‘𝑘)) = X𝑘 ∈ 𝑋 ((((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) |
| 92 | 79, 87, 91 | cbvmpt 5253 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ ↦ X𝑘 ∈
𝑋 ((((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))))‘𝑚)‘𝑘)[,)(𝐵‘𝑘))) = (𝑛 ∈ ℕ ↦ X𝑘 ∈
𝑋 ((((𝑚 ∈ ℕ ↦ (𝑗 ∈ 𝑋 ↦ ((𝐴‘𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) |
| 93 | 61, 63, 65, 67, 69, 15, 78, 92 | vonioolem2 46696 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑗 ∈ 𝑋 (𝐴‘𝑗) < (𝐵‘𝑗)) → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 94 | 58, 93 | syldan 591 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 95 | 1, 60, 66, 62, 64 | hoidmvn0val 46599 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
| 96 | 95 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
| 97 | 52, 94, 96 | 3eqtr4d 2787 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) |
| 98 | | rexnal 3100 |
. . . . . . . . . 10
⊢
(∃𝑘 ∈
𝑋 ¬ (𝐴‘𝑘) < (𝐵‘𝑘) ↔ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) |
| 99 | 98 | bicomi 224 |
. . . . . . . . 9
⊢ (¬
∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘) ↔ ∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) < (𝐵‘𝑘)) |
| 100 | 99 | biimpi 216 |
. . . . . . . 8
⊢ (¬
∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘) → ∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) < (𝐵‘𝑘)) |
| 101 | 100 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) < (𝐵‘𝑘)) |
| 102 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) < (𝐵‘𝑘)) → ¬ (𝐴‘𝑘) < (𝐵‘𝑘)) |
| 103 | 41 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) < (𝐵‘𝑘)) → (𝐵‘𝑘) ∈ ℝ) |
| 104 | 40 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) < (𝐵‘𝑘)) → (𝐴‘𝑘) ∈ ℝ) |
| 105 | 103, 104 | lenltd 11407 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) < (𝐵‘𝑘)) → ((𝐵‘𝑘) ≤ (𝐴‘𝑘) ↔ ¬ (𝐴‘𝑘) < (𝐵‘𝑘))) |
| 106 | 102, 105 | mpbird 257 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑋) ∧ ¬ (𝐴‘𝑘) < (𝐵‘𝑘)) → (𝐵‘𝑘) ≤ (𝐴‘𝑘)) |
| 107 | 106 | ex 412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (¬ (𝐴‘𝑘) < (𝐵‘𝑘) → (𝐵‘𝑘) ≤ (𝐴‘𝑘))) |
| 108 | 107 | reximdva 3168 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) < (𝐵‘𝑘) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) ≤ (𝐴‘𝑘))) |
| 109 | 108 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) → (∃𝑘 ∈ 𝑋 ¬ (𝐴‘𝑘) < (𝐵‘𝑘) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) ≤ (𝐴‘𝑘))) |
| 110 | 101, 109 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) ≤ (𝐴‘𝑘)) |
| 111 | 110 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) → ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) ≤ (𝐴‘𝑘)) |
| 112 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑘(voln‘𝑋) |
| 113 | | nfixp1 8958 |
. . . . . . . . . 10
⊢
Ⅎ𝑘X𝑘 ∈
𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) |
| 114 | 15, 113 | nfcxfr 2903 |
. . . . . . . . 9
⊢
Ⅎ𝑘𝐼 |
| 115 | 112, 114 | nffv 6916 |
. . . . . . . 8
⊢
Ⅎ𝑘((voln‘𝑋)‘𝐼) |
| 116 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝐴(𝐿‘𝑋)𝐵) |
| 117 | 115, 116 | nfeq 2919 |
. . . . . . 7
⊢
Ⅎ𝑘((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵) |
| 118 | 59 | vonmea 46589 |
. . . . . . . . . . . 12
⊢ (𝜑 → (voln‘𝑋) ∈ Meas) |
| 119 | 118 | mea0 46469 |
. . . . . . . . . . 11
⊢ (𝜑 → ((voln‘𝑋)‘∅) =
0) |
| 120 | 119 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → ((voln‘𝑋)‘∅) = 0) |
| 121 | 15 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘))) |
| 122 | | simp2 1138 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → 𝑘 ∈ 𝑋) |
| 123 | | simp3 1139 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → (𝐵‘𝑘) ≤ (𝐴‘𝑘)) |
| 124 | 24, 40 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈
ℝ*) |
| 125 | 124 | 3adant3 1133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → (𝐴‘𝑘) ∈
ℝ*) |
| 126 | 24, 41 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈
ℝ*) |
| 127 | 126 | 3adant3 1133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → (𝐵‘𝑘) ∈
ℝ*) |
| 128 | | ioo0 13412 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴‘𝑘) ∈ ℝ* ∧ (𝐵‘𝑘) ∈ ℝ*) → (((𝐴‘𝑘)(,)(𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) ≤ (𝐴‘𝑘))) |
| 129 | 125, 127,
128 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → (((𝐴‘𝑘)(,)(𝐵‘𝑘)) = ∅ ↔ (𝐵‘𝑘) ≤ (𝐴‘𝑘))) |
| 130 | 123, 129 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → ((𝐴‘𝑘)(,)(𝐵‘𝑘)) = ∅) |
| 131 | | rspe 3249 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ 𝑋 ∧ ((𝐴‘𝑘)(,)(𝐵‘𝑘)) = ∅) → ∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) = ∅) |
| 132 | 122, 130,
131 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → ∃𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) = ∅) |
| 133 | | ixp0 8971 |
. . . . . . . . . . . . 13
⊢
(∃𝑘 ∈
𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) = ∅ → X𝑘 ∈
𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) = ∅) |
| 134 | 132, 133 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) = ∅) |
| 135 | 121, 134 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → 𝐼 = ∅) |
| 136 | 135 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = ((voln‘𝑋)‘∅)) |
| 137 | | ne0i 4341 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝑋 → 𝑋 ≠ ∅) |
| 138 | 137 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑋 ≠ ∅) |
| 139 | 138, 95 | syldan 591 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
| 140 | 139 | 3adant3 1133 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘)))) |
| 141 | | eleq1w 2824 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝑋 ↔ 𝑘 ∈ 𝑋)) |
| 142 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑘 → (𝐵‘𝑗) = (𝐵‘𝑘)) |
| 143 | 142, 70 | breq12d 5156 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑘 → ((𝐵‘𝑗) ≤ (𝐴‘𝑗) ↔ (𝐵‘𝑘) ≤ (𝐴‘𝑘))) |
| 144 | 141, 143 | 3anbi23d 1441 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑘 → ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) ↔ (𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)))) |
| 145 | 144 | imbi1d 341 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0) ↔ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0))) |
| 146 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) |
| 147 | 59 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → 𝑋 ∈ Fin) |
| 148 | | volicore 46596 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
| 149 | 40, 41, 148 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
| 150 | 149 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ) |
| 151 | 150 | 3ad2antl1 1186 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ) |
| 152 | | simp2 1138 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → 𝑗 ∈ 𝑋) |
| 153 | 53, 54 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑗)[,)(𝐵‘𝑗))) |
| 154 | 153 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑗 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗)))) |
| 155 | 154 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗)))) |
| 156 | 2 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (𝐴‘𝑗) ∈ ℝ) |
| 157 | 7 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (𝐵‘𝑗) ∈ ℝ) |
| 158 | | volico 45998 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴‘𝑗) ∈ ℝ ∧ (𝐵‘𝑗) ∈ ℝ) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) < (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0)) |
| 159 | 156, 157,
158 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) < (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0)) |
| 160 | 159 | 3adant3 1133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = if((𝐴‘𝑗) < (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0)) |
| 161 | | simp3 1139 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → (𝐵‘𝑗) ≤ (𝐴‘𝑗)) |
| 162 | 157, 156 | lenltd 11407 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋) → ((𝐵‘𝑗) ≤ (𝐴‘𝑗) ↔ ¬ (𝐴‘𝑗) < (𝐵‘𝑗))) |
| 163 | 162 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → ((𝐵‘𝑗) ≤ (𝐴‘𝑗) ↔ ¬ (𝐴‘𝑗) < (𝐵‘𝑗))) |
| 164 | 161, 163 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → ¬ (𝐴‘𝑗) < (𝐵‘𝑗)) |
| 165 | 164 | iffalsed 4536 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → if((𝐴‘𝑗) < (𝐵‘𝑗), ((𝐵‘𝑗) − (𝐴‘𝑗)), 0) = 0) |
| 166 | 160, 165 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = 0) |
| 167 | 166 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑗)[,)(𝐵‘𝑗))) = 0) |
| 168 | 155, 167 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0) |
| 169 | 146, 147,
151, 152, 168 | fprodeq0g 16030 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑋 ∧ (𝐵‘𝑗) ≤ (𝐴‘𝑗)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0) |
| 170 | 145, 169 | chvarvv 1998 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = 0) |
| 171 | 140, 170 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → (𝐴(𝐿‘𝑋)𝐵) = 0) |
| 172 | 120, 136,
171 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋 ∧ (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) |
| 173 | 172 | 3exp 1120 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) ≤ (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)))) |
| 174 | 173 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) ≤ (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)))) |
| 175 | 37, 117, 174 | rexlimd 3266 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (∃𝑘 ∈ 𝑋 (𝐵‘𝑘) ≤ (𝐴‘𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵))) |
| 176 | 175 | imp 406 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ∃𝑘 ∈ 𝑋 (𝐵‘𝑘) ≤ (𝐴‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) |
| 177 | 111, 176 | syldan 591 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ≠ ∅) ∧ ¬ ∀𝑘 ∈ 𝑋 (𝐴‘𝑘) < (𝐵‘𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) |
| 178 | 97, 177 | pm2.61dan 813 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) |
| 179 | 36, 178 | syldan 591 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) |
| 180 | 34, 179 | pm2.61dan 813 |
1
⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿‘𝑋)𝐵)) |