Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  vonicc Structured version   Visualization version   GIF version

Theorem vonicc 43187
 Description: The n-dimensional Lebesgue measure of a closed interval. This is the second statement in Proposition 115G (d) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
Hypotheses
Ref Expression
vonicc.x (𝜑𝑋 ∈ Fin)
vonicc.a (𝜑𝐴:𝑋⟶ℝ)
vonicc.b (𝜑𝐵:𝑋⟶ℝ)
vonicc.i 𝐼 = X𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘))
vonicc.l 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
Assertion
Ref Expression
vonicc (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑘   𝐵,𝑎,𝑏,𝑘   𝑋,𝑎,𝑏,𝑘,𝑥   𝜑,𝑎,𝑏,𝑘,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐼(𝑥,𝑘,𝑎,𝑏)   𝐿(𝑥,𝑘,𝑎,𝑏)

Proof of Theorem vonicc
Dummy variables 𝑖 𝑗 𝑛 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vonicc.l . . . . 5 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
2 vonicc.a . . . . . . 7 (𝜑𝐴:𝑋⟶ℝ)
32adantr 484 . . . . . 6 ((𝜑𝑋 = ∅) → 𝐴:𝑋⟶ℝ)
4 feq2 6484 . . . . . . 7 (𝑋 = ∅ → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ))
54adantl 485 . . . . . 6 ((𝜑𝑋 = ∅) → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ))
63, 5mpbid 235 . . . . 5 ((𝜑𝑋 = ∅) → 𝐴:∅⟶ℝ)
7 vonicc.b . . . . . . 7 (𝜑𝐵:𝑋⟶ℝ)
87adantr 484 . . . . . 6 ((𝜑𝑋 = ∅) → 𝐵:𝑋⟶ℝ)
9 feq2 6484 . . . . . . 7 (𝑋 = ∅ → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ))
109adantl 485 . . . . . 6 ((𝜑𝑋 = ∅) → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ))
118, 10mpbid 235 . . . . 5 ((𝜑𝑋 = ∅) → 𝐵:∅⟶ℝ)
121, 6, 11hoidmv0val 43085 . . . 4 ((𝜑𝑋 = ∅) → (𝐴(𝐿‘∅)𝐵) = 0)
1312eqcomd 2830 . . 3 ((𝜑𝑋 = ∅) → 0 = (𝐴(𝐿‘∅)𝐵))
14 fveq2 6658 . . . . . 6 (𝑋 = ∅ → (voln‘𝑋) = (voln‘∅))
15 vonicc.i . . . . . . . 8 𝐼 = X𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘))
1615a1i 11 . . . . . . 7 (𝑋 = ∅ → 𝐼 = X𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)))
17 ixpeq1 8462 . . . . . . 7 (𝑋 = ∅ → X𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)) = X𝑘 ∈ ∅ ((𝐴𝑘)[,](𝐵𝑘)))
1816, 17eqtrd 2859 . . . . . 6 (𝑋 = ∅ → 𝐼 = X𝑘 ∈ ∅ ((𝐴𝑘)[,](𝐵𝑘)))
1914, 18fveq12d 6665 . . . . 5 (𝑋 = ∅ → ((voln‘𝑋)‘𝐼) = ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴𝑘)[,](𝐵𝑘))))
2019adantl 485 . . . 4 ((𝜑𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴𝑘)[,](𝐵𝑘))))
21 0fin 8737 . . . . . . 7 ∅ ∈ Fin
2221a1i 11 . . . . . 6 ((𝜑𝑋 = ∅) → ∅ ∈ Fin)
23 eqid 2824 . . . . . 6 dom (voln‘∅) = dom (voln‘∅)
2422, 23, 6, 11iccvonmbl 43181 . . . . 5 ((𝜑𝑋 = ∅) → X𝑘 ∈ ∅ ((𝐴𝑘)[,](𝐵𝑘)) ∈ dom (voln‘∅))
2524von0val 43173 . . . 4 ((𝜑𝑋 = ∅) → ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴𝑘)[,](𝐵𝑘))) = 0)
2620, 25eqtrd 2859 . . 3 ((𝜑𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = 0)
27 fveq2 6658 . . . . 5 (𝑋 = ∅ → (𝐿𝑋) = (𝐿‘∅))
2827oveqd 7162 . . . 4 (𝑋 = ∅ → (𝐴(𝐿𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵))
2928adantl 485 . . 3 ((𝜑𝑋 = ∅) → (𝐴(𝐿𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵))
3013, 26, 293eqtr4d 2869 . 2 ((𝜑𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
31 neqne 3022 . . . 4 𝑋 = ∅ → 𝑋 ≠ ∅)
3231adantl 485 . . 3 ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅)
33 nfv 1916 . . . . . . . . 9 𝑘(𝜑𝑋 ≠ ∅)
34 nfra1 3214 . . . . . . . . 9 𝑘𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)
3533, 34nfan 1901 . . . . . . . 8 𝑘((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘))
362ffvelrnda 6839 . . . . . . . . . . . 12 ((𝜑𝑘𝑋) → (𝐴𝑘) ∈ ℝ)
377ffvelrnda 6839 . . . . . . . . . . . 12 ((𝜑𝑘𝑋) → (𝐵𝑘) ∈ ℝ)
38 volico2 43143 . . . . . . . . . . . 12 (((𝐴𝑘) ∈ ℝ ∧ (𝐵𝑘) ∈ ℝ) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = if((𝐴𝑘) ≤ (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0))
3936, 37, 38syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑘𝑋) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = if((𝐴𝑘) ≤ (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0))
4039ad4ant14 751 . . . . . . . . . 10 ((((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) ∧ 𝑘𝑋) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = if((𝐴𝑘) ≤ (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0))
41 rspa 3201 . . . . . . . . . . . 12 ((∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘) ∧ 𝑘𝑋) → (𝐴𝑘) ≤ (𝐵𝑘))
4241iftrued 4457 . . . . . . . . . . 11 ((∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘) ∧ 𝑘𝑋) → if((𝐴𝑘) ≤ (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0) = ((𝐵𝑘) − (𝐴𝑘)))
4342adantll 713 . . . . . . . . . 10 ((((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) ∧ 𝑘𝑋) → if((𝐴𝑘) ≤ (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0) = ((𝐵𝑘) − (𝐴𝑘)))
4440, 43eqtrd 2859 . . . . . . . . 9 ((((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) ∧ 𝑘𝑋) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ((𝐵𝑘) − (𝐴𝑘)))
4544ex 416 . . . . . . . 8 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → (𝑘𝑋 → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ((𝐵𝑘) − (𝐴𝑘))))
4635, 45ralrimi 3211 . . . . . . 7 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ∀𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ((𝐵𝑘) − (𝐴𝑘)))
4746prodeq2d 15272 . . . . . 6 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘𝑋 ((𝐵𝑘) − (𝐴𝑘)))
4847eqcomd 2830 . . . . 5 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ∏𝑘𝑋 ((𝐵𝑘) − (𝐴𝑘)) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
49 fveq2 6658 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝐴𝑘) = (𝐴𝑗))
50 fveq2 6658 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝐵𝑘) = (𝐵𝑗))
5149, 50breq12d 5065 . . . . . . . . 9 (𝑘 = 𝑗 → ((𝐴𝑘) ≤ (𝐵𝑘) ↔ (𝐴𝑗) ≤ (𝐵𝑗)))
5251cbvralvw 3435 . . . . . . . 8 (∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘) ↔ ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗))
5352biimpi 219 . . . . . . 7 (∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘) → ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗))
5453adantl 485 . . . . . 6 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗))
55 vonicc.x . . . . . . . . 9 (𝜑𝑋 ∈ Fin)
5655adantr 484 . . . . . . . 8 ((𝜑𝑋 ≠ ∅) → 𝑋 ∈ Fin)
5756adantr 484 . . . . . . 7 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗)) → 𝑋 ∈ Fin)
582adantr 484 . . . . . . . 8 ((𝜑𝑋 ≠ ∅) → 𝐴:𝑋⟶ℝ)
5958adantr 484 . . . . . . 7 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗)) → 𝐴:𝑋⟶ℝ)
607adantr 484 . . . . . . . 8 ((𝜑𝑋 ≠ ∅) → 𝐵:𝑋⟶ℝ)
6160adantr 484 . . . . . . 7 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗)) → 𝐵:𝑋⟶ℝ)
62 simpr 488 . . . . . . . 8 ((𝜑𝑋 ≠ ∅) → 𝑋 ≠ ∅)
6362adantr 484 . . . . . . 7 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗)) → 𝑋 ≠ ∅)
6452, 41sylanbr 585 . . . . . . . 8 ((∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗) ∧ 𝑘𝑋) → (𝐴𝑘) ≤ (𝐵𝑘))
6564adantll 713 . . . . . . 7 ((((𝜑𝑋 ≠ ∅) ∧ ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗)) ∧ 𝑘𝑋) → (𝐴𝑘) ≤ (𝐵𝑘))
66 fveq2 6658 . . . . . . . . . . 11 (𝑗 = 𝑘 → (𝐵𝑗) = (𝐵𝑘))
6766oveq1d 7160 . . . . . . . . . 10 (𝑗 = 𝑘 → ((𝐵𝑗) + (1 / 𝑚)) = ((𝐵𝑘) + (1 / 𝑚)))
6867cbvmptv 5155 . . . . . . . . 9 (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))) = (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑚)))
6968mpteq2i 5144 . . . . . . . 8 (𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚)))) = (𝑚 ∈ ℕ ↦ (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑚))))
70 oveq2 7153 . . . . . . . . . . 11 (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
7170oveq2d 7161 . . . . . . . . . 10 (𝑚 = 𝑛 → ((𝐵𝑘) + (1 / 𝑚)) = ((𝐵𝑘) + (1 / 𝑛)))
7271mpteq2dv 5148 . . . . . . . . 9 (𝑚 = 𝑛 → (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑚))) = (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑛))))
7372cbvmptv 5155 . . . . . . . 8 (𝑚 ∈ ℕ ↦ (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑚)))) = (𝑛 ∈ ℕ ↦ (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑛))))
7469, 73eqtri 2847 . . . . . . 7 (𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚)))) = (𝑛 ∈ ℕ ↦ (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑛))))
75 fveq2 6658 . . . . . . . . . . 11 (𝑖 = 𝑛 → ((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑖) = ((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑛))
7675fveq1d 6660 . . . . . . . . . 10 (𝑖 = 𝑛 → (((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘) = (((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘))
7776oveq2d 7161 . . . . . . . . 9 (𝑖 = 𝑛 → ((𝐴𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘)) = ((𝐴𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
7877ixpeq2dv 8467 . . . . . . . 8 (𝑖 = 𝑛X𝑘𝑋 ((𝐴𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘)) = X𝑘𝑋 ((𝐴𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
7978cbvmptv 5155 . . . . . . 7 (𝑖 ∈ ℕ ↦ X𝑘𝑋 ((𝐴𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘))) = (𝑛 ∈ ℕ ↦ X𝑘𝑋 ((𝐴𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
8057, 59, 61, 63, 65, 15, 74, 79vonicclem2 43186 . . . . . 6 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗)) → ((voln‘𝑋)‘𝐼) = ∏𝑘𝑋 ((𝐵𝑘) − (𝐴𝑘)))
8154, 80syldan 594 . . . . 5 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ((voln‘𝑋)‘𝐼) = ∏𝑘𝑋 ((𝐵𝑘) − (𝐴𝑘)))
821, 56, 62, 58, 60hoidmvn0val 43086 . . . . . 6 ((𝜑𝑋 ≠ ∅) → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
8382adantr 484 . . . . 5 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
8448, 81, 833eqtr4d 2869 . . . 4 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
85 rexnal 3233 . . . . . . . . . 10 (∃𝑘𝑋 ¬ (𝐴𝑘) ≤ (𝐵𝑘) ↔ ¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘))
8685bicomi 227 . . . . . . . . 9 (¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘) ↔ ∃𝑘𝑋 ¬ (𝐴𝑘) ≤ (𝐵𝑘))
8786biimpi 219 . . . . . . . 8 (¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘) → ∃𝑘𝑋 ¬ (𝐴𝑘) ≤ (𝐵𝑘))
8887adantl 485 . . . . . . 7 ((𝜑 ∧ ¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ∃𝑘𝑋 ¬ (𝐴𝑘) ≤ (𝐵𝑘))
89 simpr 488 . . . . . . . . . . 11 (((𝜑𝑘𝑋) ∧ ¬ (𝐴𝑘) ≤ (𝐵𝑘)) → ¬ (𝐴𝑘) ≤ (𝐵𝑘))
9037adantr 484 . . . . . . . . . . . 12 (((𝜑𝑘𝑋) ∧ ¬ (𝐴𝑘) ≤ (𝐵𝑘)) → (𝐵𝑘) ∈ ℝ)
9136adantr 484 . . . . . . . . . . . 12 (((𝜑𝑘𝑋) ∧ ¬ (𝐴𝑘) ≤ (𝐵𝑘)) → (𝐴𝑘) ∈ ℝ)
9290, 91ltnled 10779 . . . . . . . . . . 11 (((𝜑𝑘𝑋) ∧ ¬ (𝐴𝑘) ≤ (𝐵𝑘)) → ((𝐵𝑘) < (𝐴𝑘) ↔ ¬ (𝐴𝑘) ≤ (𝐵𝑘)))
9389, 92mpbird 260 . . . . . . . . . 10 (((𝜑𝑘𝑋) ∧ ¬ (𝐴𝑘) ≤ (𝐵𝑘)) → (𝐵𝑘) < (𝐴𝑘))
9493ex 416 . . . . . . . . 9 ((𝜑𝑘𝑋) → (¬ (𝐴𝑘) ≤ (𝐵𝑘) → (𝐵𝑘) < (𝐴𝑘)))
9594reximdva 3267 . . . . . . . 8 (𝜑 → (∃𝑘𝑋 ¬ (𝐴𝑘) ≤ (𝐵𝑘) → ∃𝑘𝑋 (𝐵𝑘) < (𝐴𝑘)))
9695adantr 484 . . . . . . 7 ((𝜑 ∧ ¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → (∃𝑘𝑋 ¬ (𝐴𝑘) ≤ (𝐵𝑘) → ∃𝑘𝑋 (𝐵𝑘) < (𝐴𝑘)))
9788, 96mpd 15 . . . . . 6 ((𝜑 ∧ ¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ∃𝑘𝑋 (𝐵𝑘) < (𝐴𝑘))
9897adantlr 714 . . . . 5 (((𝜑𝑋 ≠ ∅) ∧ ¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ∃𝑘𝑋 (𝐵𝑘) < (𝐴𝑘))
99 nfcv 2982 . . . . . . . . 9 𝑘(voln‘𝑋)
100 nfixp1 8472 . . . . . . . . . 10 𝑘X𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘))
10115, 100nfcxfr 2980 . . . . . . . . 9 𝑘𝐼
10299, 101nffv 6668 . . . . . . . 8 𝑘((voln‘𝑋)‘𝐼)
103 nfcv 2982 . . . . . . . . 9 𝑘𝐴
104 nfcv 2982 . . . . . . . . . . . 12 𝑘Fin
105 nfcv 2982 . . . . . . . . . . . . 13 𝑘(ℝ ↑m 𝑥)
106 nfv 1916 . . . . . . . . . . . . . 14 𝑘 𝑥 = ∅
107 nfcv 2982 . . . . . . . . . . . . . 14 𝑘0
108 nfcv 2982 . . . . . . . . . . . . . . 15 𝑘𝑥
109108nfcprod1 15260 . . . . . . . . . . . . . 14 𝑘𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))
110106, 107, 109nfif 4478 . . . . . . . . . . . . 13 𝑘if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))
111105, 105, 110nfmpo 7225 . . . . . . . . . . . 12 𝑘(𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))
112104, 111nfmpt 5149 . . . . . . . . . . 11 𝑘(𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
1131, 112nfcxfr 2980 . . . . . . . . . 10 𝑘𝐿
114 nfcv 2982 . . . . . . . . . 10 𝑘𝑋
115113, 114nffv 6668 . . . . . . . . 9 𝑘(𝐿𝑋)
116 nfcv 2982 . . . . . . . . 9 𝑘𝐵
117103, 115, 116nfov 7175 . . . . . . . 8 𝑘(𝐴(𝐿𝑋)𝐵)
118102, 117nfeq 2995 . . . . . . 7 𝑘((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵)
11955vonmea 43076 . . . . . . . . . . . 12 (𝜑 → (voln‘𝑋) ∈ Meas)
120119mea0 42956 . . . . . . . . . . 11 (𝜑 → ((voln‘𝑋)‘∅) = 0)
1211203ad2ant1 1130 . . . . . . . . . 10 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → ((voln‘𝑋)‘∅) = 0)
12215a1i 11 . . . . . . . . . . . 12 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → 𝐼 = X𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)))
123 simp2 1134 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → 𝑘𝑋)
124 simp3 1135 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → (𝐵𝑘) < (𝐴𝑘))
125 ressxr 10677 . . . . . . . . . . . . . . . . . 18 ℝ ⊆ ℝ*
126125, 36sseldi 3950 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑋) → (𝐴𝑘) ∈ ℝ*)
127125, 37sseldi 3950 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑋) → (𝐵𝑘) ∈ ℝ*)
128 icc0 12779 . . . . . . . . . . . . . . . . 17 (((𝐴𝑘) ∈ ℝ* ∧ (𝐵𝑘) ∈ ℝ*) → (((𝐴𝑘)[,](𝐵𝑘)) = ∅ ↔ (𝐵𝑘) < (𝐴𝑘)))
129126, 127, 128syl2anc 587 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝑋) → (((𝐴𝑘)[,](𝐵𝑘)) = ∅ ↔ (𝐵𝑘) < (𝐴𝑘)))
1301293adant3 1129 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → (((𝐴𝑘)[,](𝐵𝑘)) = ∅ ↔ (𝐵𝑘) < (𝐴𝑘)))
131124, 130mpbird 260 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → ((𝐴𝑘)[,](𝐵𝑘)) = ∅)
132 rspe 3297 . . . . . . . . . . . . . 14 ((𝑘𝑋 ∧ ((𝐴𝑘)[,](𝐵𝑘)) = ∅) → ∃𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)) = ∅)
133123, 131, 132syl2anc 587 . . . . . . . . . . . . 13 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → ∃𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)) = ∅)
134 ixp0 8485 . . . . . . . . . . . . 13 (∃𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)) = ∅ → X𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)) = ∅)
135133, 134syl 17 . . . . . . . . . . . 12 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → X𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)) = ∅)
136122, 135eqtrd 2859 . . . . . . . . . . 11 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → 𝐼 = ∅)
137136fveq2d 6662 . . . . . . . . . 10 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → ((voln‘𝑋)‘𝐼) = ((voln‘𝑋)‘∅))
138 ne0i 4282 . . . . . . . . . . . . . 14 (𝑘𝑋𝑋 ≠ ∅)
139138adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑘𝑋) → 𝑋 ≠ ∅)
140139, 82syldan 594 . . . . . . . . . . . 12 ((𝜑𝑘𝑋) → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
1411403adant3 1129 . . . . . . . . . . 11 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
142 eleq1w 2898 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → (𝑗𝑋𝑘𝑋))
143 fveq2 6658 . . . . . . . . . . . . . . 15 (𝑗 = 𝑘 → (𝐴𝑗) = (𝐴𝑘))
14466, 143breq12d 5065 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → ((𝐵𝑗) < (𝐴𝑗) ↔ (𝐵𝑘) < (𝐴𝑘)))
145142, 1443anbi23d 1436 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) ↔ (𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘))))
146145imbi1d 345 . . . . . . . . . . . 12 (𝑗 = 𝑘 → (((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = 0) ↔ ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = 0)))
147 nfv 1916 . . . . . . . . . . . . 13 𝑘(𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗))
148553ad2ant1 1130 . . . . . . . . . . . . 13 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → 𝑋 ∈ Fin)
149 volicore 43083 . . . . . . . . . . . . . . . 16 (((𝐴𝑘) ∈ ℝ ∧ (𝐵𝑘) ∈ ℝ) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℝ)
15036, 37, 149syl2anc 587 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑋) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℝ)
151150recnd 10661 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑋) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℂ)
1521513ad2antl1 1182 . . . . . . . . . . . . 13 (((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) ∧ 𝑘𝑋) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℂ)
153 simp2 1134 . . . . . . . . . . . . 13 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → 𝑗𝑋)
15449, 50oveq12d 7163 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑗 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑗)[,)(𝐵𝑗)))
155154fveq2d 6662 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑗)[,)(𝐵𝑗))))
156155adantl 485 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑗)[,)(𝐵𝑗))))
1572ffvelrnda 6839 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑋) → (𝐴𝑗) ∈ ℝ)
1587ffvelrnda 6839 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑋) → (𝐵𝑗) ∈ ℝ)
159 volico2 43143 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑗) ∈ ℝ ∧ (𝐵𝑗) ∈ ℝ) → (vol‘((𝐴𝑗)[,)(𝐵𝑗))) = if((𝐴𝑗) ≤ (𝐵𝑗), ((𝐵𝑗) − (𝐴𝑗)), 0))
160157, 158, 159syl2anc 587 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑋) → (vol‘((𝐴𝑗)[,)(𝐵𝑗))) = if((𝐴𝑗) ≤ (𝐵𝑗), ((𝐵𝑗) − (𝐴𝑗)), 0))
1611603adant3 1129 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → (vol‘((𝐴𝑗)[,)(𝐵𝑗))) = if((𝐴𝑗) ≤ (𝐵𝑗), ((𝐵𝑗) − (𝐴𝑗)), 0))
162 simp3 1135 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → (𝐵𝑗) < (𝐴𝑗))
163158, 157ltnled 10779 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑋) → ((𝐵𝑗) < (𝐴𝑗) ↔ ¬ (𝐴𝑗) ≤ (𝐵𝑗)))
1641633adant3 1129 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → ((𝐵𝑗) < (𝐴𝑗) ↔ ¬ (𝐴𝑗) ≤ (𝐵𝑗)))
165162, 164mpbid 235 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → ¬ (𝐴𝑗) ≤ (𝐵𝑗))
166165iffalsed 4460 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → if((𝐴𝑗) ≤ (𝐵𝑗), ((𝐵𝑗) − (𝐴𝑗)), 0) = 0)
167161, 166eqtrd 2859 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → (vol‘((𝐴𝑗)[,)(𝐵𝑗))) = 0)
168167adantr 484 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴𝑗)[,)(𝐵𝑗))) = 0)
169156, 168eqtrd 2859 . . . . . . . . . . . . 13 (((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = 0)
170147, 148, 152, 153, 169fprodeq0g 15344 . . . . . . . . . . . 12 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = 0)
171146, 170chvarvv 2006 . . . . . . . . . . 11 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = 0)
172141, 171eqtrd 2859 . . . . . . . . . 10 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → (𝐴(𝐿𝑋)𝐵) = 0)
173121, 137, 1723eqtr4d 2869 . . . . . . . . 9 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
1741733exp 1116 . . . . . . . 8 (𝜑 → (𝑘𝑋 → ((𝐵𝑘) < (𝐴𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))))
175174adantr 484 . . . . . . 7 ((𝜑𝑋 ≠ ∅) → (𝑘𝑋 → ((𝐵𝑘) < (𝐴𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))))
17633, 118, 175rexlimd 3310 . . . . . 6 ((𝜑𝑋 ≠ ∅) → (∃𝑘𝑋 (𝐵𝑘) < (𝐴𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵)))
177176imp 410 . . . . 5 (((𝜑𝑋 ≠ ∅) ∧ ∃𝑘𝑋 (𝐵𝑘) < (𝐴𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
17898, 177syldan 594 . . . 4 (((𝜑𝑋 ≠ ∅) ∧ ¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
17984, 178pm2.61dan 812 . . 3 ((𝜑𝑋 ≠ ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
18032, 179syldan 594 . 2 ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
18130, 180pm2.61dan 812 1 (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115   ≠ wne 3014  ∀wral 3133  ∃wrex 3134  ∅c0 4275  ifcif 4449   class class class wbr 5052   ↦ cmpt 5132  dom cdm 5542  ⟶wf 6339  ‘cfv 6343  (class class class)co 7145   ∈ cmpo 7147   ↑m cmap 8396  Xcixp 8451  Fincfn 8499  ℂcc 10527  ℝcr 10528  0cc0 10529  1c1 10530   + caddc 10532  ℝ*cxr 10666   < clt 10667   ≤ cle 10668   − cmin 10862   / cdiv 11289  ℕcn 11630  [,)cico 12733  [,]cicc 12734  ∏cprod 15255  volcvol 24063  volncvoln 43040 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7451  ax-inf2 9095  ax-cc 9849  ax-ac2 9877  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4276  df-if 4450  df-pw 4523  df-sn 4550  df-pr 4552  df-tp 4554  df-op 4556  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-disj 5018  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7399  df-om 7571  df-1st 7679  df-2nd 7680  df-supp 7821  df-tpos 7882  df-wrecs 7937  df-recs 7998  df-rdg 8036  df-1o 8092  df-2o 8093  df-oadd 8096  df-omul 8097  df-er 8279  df-map 8398  df-pm 8399  df-ixp 8452  df-en 8500  df-dom 8501  df-sdom 8502  df-fin 8503  df-fsupp 8825  df-fi 8866  df-sup 8897  df-inf 8898  df-oi 8965  df-dju 9321  df-card 9359  df-acn 9362  df-ac 9534  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11693  df-3 11694  df-4 11695  df-5 11696  df-6 11697  df-7 11698  df-8 11699  df-9 11700  df-n0 11891  df-z 11975  df-dec 12092  df-uz 12237  df-q 12342  df-rp 12383  df-xneg 12500  df-xadd 12501  df-xmul 12502  df-ioo 12735  df-ico 12737  df-icc 12738  df-fz 12891  df-fzo 13034  df-fl 13162  df-seq 13370  df-exp 13431  df-hash 13692  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-clim 14841  df-rlim 14842  df-sum 15039  df-prod 15256  df-struct 16481  df-ndx 16482  df-slot 16483  df-base 16485  df-sets 16486  df-ress 16487  df-plusg 16574  df-mulr 16575  df-starv 16576  df-sca 16577  df-vsca 16578  df-ip 16579  df-tset 16580  df-ple 16581  df-ds 16583  df-unif 16584  df-hom 16585  df-cco 16586  df-rest 16692  df-topn 16693  df-0g 16711  df-gsum 16712  df-topgen 16713  df-pt 16714  df-prds 16717  df-pws 16719  df-xrs 16771  df-qtop 16776  df-imas 16777  df-xps 16779  df-mre 16853  df-mrc 16854  df-acs 16856  df-mgm 17848  df-sgrp 17897  df-mnd 17908  df-mhm 17952  df-submnd 17953  df-grp 18102  df-minusg 18103  df-sbg 18104  df-mulg 18221  df-subg 18272  df-ghm 18352  df-cntz 18443  df-cmn 18904  df-abl 18905  df-mgp 19236  df-ur 19248  df-ring 19295  df-cring 19296  df-oppr 19369  df-dvdsr 19387  df-unit 19388  df-invr 19418  df-dvr 19429  df-rnghom 19463  df-drng 19497  df-field 19498  df-subrg 19526  df-abv 19581  df-staf 19609  df-srng 19610  df-lmod 19629  df-lss 19697  df-lmhm 19787  df-lvec 19868  df-sra 19937  df-rgmod 19938  df-psmet 20530  df-xmet 20531  df-met 20532  df-bl 20533  df-mopn 20534  df-cnfld 20539  df-refld 20742  df-phl 20763  df-dsmm 20869  df-frlm 20884  df-top 21495  df-topon 21512  df-topsp 21534  df-bases 21547  df-cn 21828  df-cnp 21829  df-cmp 21988  df-tx 22163  df-hmeo 22356  df-xms 22923  df-ms 22924  df-tms 22925  df-nm 23185  df-ngp 23186  df-tng 23187  df-nrg 23188  df-nlm 23189  df-cncf 23479  df-clm 23664  df-cph 23769  df-tcph 23770  df-rrx 23985  df-ovol 24064  df-vol 24065  df-salg 42814  df-sumge0 42865  df-mea 42952  df-ome 42992  df-caragen 42994  df-ovoln 43039  df-voln 43041 This theorem is referenced by:  vonn0icc  43190
 Copyright terms: Public domain W3C validator