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

Theorem vonicc 42844
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 481 . . . . . 6 ((𝜑𝑋 = ∅) → 𝐴:𝑋⟶ℝ)
4 feq2 6489 . . . . . . 7 (𝑋 = ∅ → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ))
54adantl 482 . . . . . 6 ((𝜑𝑋 = ∅) → (𝐴:𝑋⟶ℝ ↔ 𝐴:∅⟶ℝ))
63, 5mpbid 233 . . . . 5 ((𝜑𝑋 = ∅) → 𝐴:∅⟶ℝ)
7 vonicc.b . . . . . . 7 (𝜑𝐵:𝑋⟶ℝ)
87adantr 481 . . . . . 6 ((𝜑𝑋 = ∅) → 𝐵:𝑋⟶ℝ)
9 feq2 6489 . . . . . . 7 (𝑋 = ∅ → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ))
109adantl 482 . . . . . 6 ((𝜑𝑋 = ∅) → (𝐵:𝑋⟶ℝ ↔ 𝐵:∅⟶ℝ))
118, 10mpbid 233 . . . . 5 ((𝜑𝑋 = ∅) → 𝐵:∅⟶ℝ)
121, 6, 11hoidmv0val 42742 . . . 4 ((𝜑𝑋 = ∅) → (𝐴(𝐿‘∅)𝐵) = 0)
1312eqcomd 2824 . . 3 ((𝜑𝑋 = ∅) → 0 = (𝐴(𝐿‘∅)𝐵))
14 fveq2 6663 . . . . . 6 (𝑋 = ∅ → (voln‘𝑋) = (voln‘∅))
15 vonicc.i . . . . . . . 8 𝐼 = X𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘))
1615a1i 11 . . . . . . 7 (𝑋 = ∅ → 𝐼 = X𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)))
17 ixpeq1 8460 . . . . . . 7 (𝑋 = ∅ → X𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)) = X𝑘 ∈ ∅ ((𝐴𝑘)[,](𝐵𝑘)))
1816, 17eqtrd 2853 . . . . . 6 (𝑋 = ∅ → 𝐼 = X𝑘 ∈ ∅ ((𝐴𝑘)[,](𝐵𝑘)))
1914, 18fveq12d 6670 . . . . 5 (𝑋 = ∅ → ((voln‘𝑋)‘𝐼) = ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴𝑘)[,](𝐵𝑘))))
2019adantl 482 . . . 4 ((𝜑𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴𝑘)[,](𝐵𝑘))))
21 0fin 8734 . . . . . . 7 ∅ ∈ Fin
2221a1i 11 . . . . . 6 ((𝜑𝑋 = ∅) → ∅ ∈ Fin)
23 eqid 2818 . . . . . 6 dom (voln‘∅) = dom (voln‘∅)
2422, 23, 6, 11iccvonmbl 42838 . . . . 5 ((𝜑𝑋 = ∅) → X𝑘 ∈ ∅ ((𝐴𝑘)[,](𝐵𝑘)) ∈ dom (voln‘∅))
2524von0val 42830 . . . 4 ((𝜑𝑋 = ∅) → ((voln‘∅)‘X𝑘 ∈ ∅ ((𝐴𝑘)[,](𝐵𝑘))) = 0)
2620, 25eqtrd 2853 . . 3 ((𝜑𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = 0)
27 fveq2 6663 . . . . 5 (𝑋 = ∅ → (𝐿𝑋) = (𝐿‘∅))
2827oveqd 7162 . . . 4 (𝑋 = ∅ → (𝐴(𝐿𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵))
2928adantl 482 . . 3 ((𝜑𝑋 = ∅) → (𝐴(𝐿𝑋)𝐵) = (𝐴(𝐿‘∅)𝐵))
3013, 26, 293eqtr4d 2863 . 2 ((𝜑𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
31 neqne 3021 . . . 4 𝑋 = ∅ → 𝑋 ≠ ∅)
3231adantl 482 . . 3 ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅)
33 nfv 1906 . . . . . . . . 9 𝑘(𝜑𝑋 ≠ ∅)
34 nfra1 3216 . . . . . . . . 9 𝑘𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)
3533, 34nfan 1891 . . . . . . . 8 𝑘((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘))
362ffvelrnda 6843 . . . . . . . . . . . 12 ((𝜑𝑘𝑋) → (𝐴𝑘) ∈ ℝ)
377ffvelrnda 6843 . . . . . . . . . . . 12 ((𝜑𝑘𝑋) → (𝐵𝑘) ∈ ℝ)
38 volico2 42800 . . . . . . . . . . . 12 (((𝐴𝑘) ∈ ℝ ∧ (𝐵𝑘) ∈ ℝ) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = if((𝐴𝑘) ≤ (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0))
3936, 37, 38syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑘𝑋) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = if((𝐴𝑘) ≤ (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0))
4039ad4ant14 748 . . . . . . . . . 10 ((((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) ∧ 𝑘𝑋) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = if((𝐴𝑘) ≤ (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0))
41 rspa 3203 . . . . . . . . . . . 12 ((∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘) ∧ 𝑘𝑋) → (𝐴𝑘) ≤ (𝐵𝑘))
4241iftrued 4471 . . . . . . . . . . 11 ((∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘) ∧ 𝑘𝑋) → if((𝐴𝑘) ≤ (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0) = ((𝐵𝑘) − (𝐴𝑘)))
4342adantll 710 . . . . . . . . . 10 ((((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) ∧ 𝑘𝑋) → if((𝐴𝑘) ≤ (𝐵𝑘), ((𝐵𝑘) − (𝐴𝑘)), 0) = ((𝐵𝑘) − (𝐴𝑘)))
4440, 43eqtrd 2853 . . . . . . . . 9 ((((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) ∧ 𝑘𝑋) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ((𝐵𝑘) − (𝐴𝑘)))
4544ex 413 . . . . . . . 8 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → (𝑘𝑋 → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ((𝐵𝑘) − (𝐴𝑘))))
4635, 45ralrimi 3213 . . . . . . 7 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ∀𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ((𝐵𝑘) − (𝐴𝑘)))
4746prodeq2d 15264 . . . . . 6 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘𝑋 ((𝐵𝑘) − (𝐴𝑘)))
4847eqcomd 2824 . . . . 5 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ∏𝑘𝑋 ((𝐵𝑘) − (𝐴𝑘)) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
49 fveq2 6663 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝐴𝑘) = (𝐴𝑗))
50 fveq2 6663 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝐵𝑘) = (𝐵𝑗))
5149, 50breq12d 5070 . . . . . . . . 9 (𝑘 = 𝑗 → ((𝐴𝑘) ≤ (𝐵𝑘) ↔ (𝐴𝑗) ≤ (𝐵𝑗)))
5251cbvralv 3450 . . . . . . . 8 (∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘) ↔ ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗))
5352biimpi 217 . . . . . . 7 (∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘) → ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗))
5453adantl 482 . . . . . 6 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗))
55 vonicc.x . . . . . . . . 9 (𝜑𝑋 ∈ Fin)
5655adantr 481 . . . . . . . 8 ((𝜑𝑋 ≠ ∅) → 𝑋 ∈ Fin)
5756adantr 481 . . . . . . 7 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗)) → 𝑋 ∈ Fin)
582adantr 481 . . . . . . . 8 ((𝜑𝑋 ≠ ∅) → 𝐴:𝑋⟶ℝ)
5958adantr 481 . . . . . . 7 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗)) → 𝐴:𝑋⟶ℝ)
607adantr 481 . . . . . . . 8 ((𝜑𝑋 ≠ ∅) → 𝐵:𝑋⟶ℝ)
6160adantr 481 . . . . . . 7 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗)) → 𝐵:𝑋⟶ℝ)
62 simpr 485 . . . . . . . 8 ((𝜑𝑋 ≠ ∅) → 𝑋 ≠ ∅)
6362adantr 481 . . . . . . 7 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗)) → 𝑋 ≠ ∅)
6452, 41sylanbr 582 . . . . . . . 8 ((∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗) ∧ 𝑘𝑋) → (𝐴𝑘) ≤ (𝐵𝑘))
6564adantll 710 . . . . . . 7 ((((𝜑𝑋 ≠ ∅) ∧ ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗)) ∧ 𝑘𝑋) → (𝐴𝑘) ≤ (𝐵𝑘))
66 fveq2 6663 . . . . . . . . . . 11 (𝑗 = 𝑘 → (𝐵𝑗) = (𝐵𝑘))
6766oveq1d 7160 . . . . . . . . . 10 (𝑗 = 𝑘 → ((𝐵𝑗) + (1 / 𝑚)) = ((𝐵𝑘) + (1 / 𝑚)))
6867cbvmptv 5160 . . . . . . . . 9 (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))) = (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑚)))
6968mpteq2i 5149 . . . . . . . 8 (𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚)))) = (𝑚 ∈ ℕ ↦ (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑚))))
70 oveq2 7153 . . . . . . . . . . 11 (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
7170oveq2d 7161 . . . . . . . . . 10 (𝑚 = 𝑛 → ((𝐵𝑘) + (1 / 𝑚)) = ((𝐵𝑘) + (1 / 𝑛)))
7271mpteq2dv 5153 . . . . . . . . 9 (𝑚 = 𝑛 → (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑚))) = (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑛))))
7372cbvmptv 5160 . . . . . . . 8 (𝑚 ∈ ℕ ↦ (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑚)))) = (𝑛 ∈ ℕ ↦ (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑛))))
7469, 73eqtri 2841 . . . . . . 7 (𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚)))) = (𝑛 ∈ ℕ ↦ (𝑘𝑋 ↦ ((𝐵𝑘) + (1 / 𝑛))))
75 fveq2 6663 . . . . . . . . . . 11 (𝑖 = 𝑛 → ((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑖) = ((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑛))
7675fveq1d 6665 . . . . . . . . . 10 (𝑖 = 𝑛 → (((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘) = (((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘))
7776oveq2d 7161 . . . . . . . . 9 (𝑖 = 𝑛 → ((𝐴𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘)) = ((𝐴𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
7877ixpeq2dv 8465 . . . . . . . 8 (𝑖 = 𝑛X𝑘𝑋 ((𝐴𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘)) = X𝑘𝑋 ((𝐴𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
7978cbvmptv 5160 . . . . . . 7 (𝑖 ∈ ℕ ↦ X𝑘𝑋 ((𝐴𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑖)‘𝑘))) = (𝑛 ∈ ℕ ↦ X𝑘𝑋 ((𝐴𝑘)[,)(((𝑚 ∈ ℕ ↦ (𝑗𝑋 ↦ ((𝐵𝑗) + (1 / 𝑚))))‘𝑛)‘𝑘)))
8057, 59, 61, 63, 65, 15, 74, 79vonicclem2 42843 . . . . . 6 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑗𝑋 (𝐴𝑗) ≤ (𝐵𝑗)) → ((voln‘𝑋)‘𝐼) = ∏𝑘𝑋 ((𝐵𝑘) − (𝐴𝑘)))
8154, 80syldan 591 . . . . 5 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ((voln‘𝑋)‘𝐼) = ∏𝑘𝑋 ((𝐵𝑘) − (𝐴𝑘)))
821, 56, 62, 58, 60hoidmvn0val 42743 . . . . . 6 ((𝜑𝑋 ≠ ∅) → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
8382adantr 481 . . . . 5 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
8448, 81, 833eqtr4d 2863 . . . 4 (((𝜑𝑋 ≠ ∅) ∧ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
85 rexnal 3235 . . . . . . . . . 10 (∃𝑘𝑋 ¬ (𝐴𝑘) ≤ (𝐵𝑘) ↔ ¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘))
8685bicomi 225 . . . . . . . . 9 (¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘) ↔ ∃𝑘𝑋 ¬ (𝐴𝑘) ≤ (𝐵𝑘))
8786biimpi 217 . . . . . . . 8 (¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘) → ∃𝑘𝑋 ¬ (𝐴𝑘) ≤ (𝐵𝑘))
8887adantl 482 . . . . . . 7 ((𝜑 ∧ ¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ∃𝑘𝑋 ¬ (𝐴𝑘) ≤ (𝐵𝑘))
89 simpr 485 . . . . . . . . . . 11 (((𝜑𝑘𝑋) ∧ ¬ (𝐴𝑘) ≤ (𝐵𝑘)) → ¬ (𝐴𝑘) ≤ (𝐵𝑘))
9037adantr 481 . . . . . . . . . . . 12 (((𝜑𝑘𝑋) ∧ ¬ (𝐴𝑘) ≤ (𝐵𝑘)) → (𝐵𝑘) ∈ ℝ)
9136adantr 481 . . . . . . . . . . . 12 (((𝜑𝑘𝑋) ∧ ¬ (𝐴𝑘) ≤ (𝐵𝑘)) → (𝐴𝑘) ∈ ℝ)
9290, 91ltnled 10775 . . . . . . . . . . 11 (((𝜑𝑘𝑋) ∧ ¬ (𝐴𝑘) ≤ (𝐵𝑘)) → ((𝐵𝑘) < (𝐴𝑘) ↔ ¬ (𝐴𝑘) ≤ (𝐵𝑘)))
9389, 92mpbird 258 . . . . . . . . . 10 (((𝜑𝑘𝑋) ∧ ¬ (𝐴𝑘) ≤ (𝐵𝑘)) → (𝐵𝑘) < (𝐴𝑘))
9493ex 413 . . . . . . . . 9 ((𝜑𝑘𝑋) → (¬ (𝐴𝑘) ≤ (𝐵𝑘) → (𝐵𝑘) < (𝐴𝑘)))
9594reximdva 3271 . . . . . . . 8 (𝜑 → (∃𝑘𝑋 ¬ (𝐴𝑘) ≤ (𝐵𝑘) → ∃𝑘𝑋 (𝐵𝑘) < (𝐴𝑘)))
9695adantr 481 . . . . . . 7 ((𝜑 ∧ ¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → (∃𝑘𝑋 ¬ (𝐴𝑘) ≤ (𝐵𝑘) → ∃𝑘𝑋 (𝐵𝑘) < (𝐴𝑘)))
9788, 96mpd 15 . . . . . 6 ((𝜑 ∧ ¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ∃𝑘𝑋 (𝐵𝑘) < (𝐴𝑘))
9897adantlr 711 . . . . 5 (((𝜑𝑋 ≠ ∅) ∧ ¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ∃𝑘𝑋 (𝐵𝑘) < (𝐴𝑘))
99 nfcv 2974 . . . . . . . . 9 𝑘(voln‘𝑋)
100 nfixp1 8470 . . . . . . . . . 10 𝑘X𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘))
10115, 100nfcxfr 2972 . . . . . . . . 9 𝑘𝐼
10299, 101nffv 6673 . . . . . . . 8 𝑘((voln‘𝑋)‘𝐼)
103 nfcv 2974 . . . . . . . . 9 𝑘𝐴
104 nfcv 2974 . . . . . . . . . . . 12 𝑘Fin
105 nfcv 2974 . . . . . . . . . . . . 13 𝑘(ℝ ↑m 𝑥)
106 nfv 1906 . . . . . . . . . . . . . 14 𝑘 𝑥 = ∅
107 nfcv 2974 . . . . . . . . . . . . . 14 𝑘0
108 nfcv 2974 . . . . . . . . . . . . . . 15 𝑘𝑥
109108nfcprod1 15252 . . . . . . . . . . . . . 14 𝑘𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))
110106, 107, 109nfif 4492 . . . . . . . . . . . . 13 𝑘if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))
111105, 105, 110nfmpo 7225 . . . . . . . . . . . 12 𝑘(𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘)))))
112104, 111nfmpt 5154 . . . . . . . . . . 11 𝑘(𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘𝑥 (vol‘((𝑎𝑘)[,)(𝑏𝑘))))))
1131, 112nfcxfr 2972 . . . . . . . . . 10 𝑘𝐿
114 nfcv 2974 . . . . . . . . . 10 𝑘𝑋
115113, 114nffv 6673 . . . . . . . . 9 𝑘(𝐿𝑋)
116 nfcv 2974 . . . . . . . . 9 𝑘𝐵
117103, 115, 116nfov 7175 . . . . . . . 8 𝑘(𝐴(𝐿𝑋)𝐵)
118102, 117nfeq 2988 . . . . . . 7 𝑘((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵)
11955vonmea 42733 . . . . . . . . . . . 12 (𝜑 → (voln‘𝑋) ∈ Meas)
120119mea0 42613 . . . . . . . . . . 11 (𝜑 → ((voln‘𝑋)‘∅) = 0)
1211203ad2ant1 1125 . . . . . . . . . 10 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → ((voln‘𝑋)‘∅) = 0)
12215a1i 11 . . . . . . . . . . . 12 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → 𝐼 = X𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)))
123 simp2 1129 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → 𝑘𝑋)
124 simp3 1130 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → (𝐵𝑘) < (𝐴𝑘))
125 ressxr 10673 . . . . . . . . . . . . . . . . . 18 ℝ ⊆ ℝ*
126125, 36sseldi 3962 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑋) → (𝐴𝑘) ∈ ℝ*)
127125, 37sseldi 3962 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑋) → (𝐵𝑘) ∈ ℝ*)
128 icc0 12774 . . . . . . . . . . . . . . . . 17 (((𝐴𝑘) ∈ ℝ* ∧ (𝐵𝑘) ∈ ℝ*) → (((𝐴𝑘)[,](𝐵𝑘)) = ∅ ↔ (𝐵𝑘) < (𝐴𝑘)))
129126, 127, 128syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝑋) → (((𝐴𝑘)[,](𝐵𝑘)) = ∅ ↔ (𝐵𝑘) < (𝐴𝑘)))
1301293adant3 1124 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → (((𝐴𝑘)[,](𝐵𝑘)) = ∅ ↔ (𝐵𝑘) < (𝐴𝑘)))
131124, 130mpbird 258 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → ((𝐴𝑘)[,](𝐵𝑘)) = ∅)
132 rspe 3301 . . . . . . . . . . . . . 14 ((𝑘𝑋 ∧ ((𝐴𝑘)[,](𝐵𝑘)) = ∅) → ∃𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)) = ∅)
133123, 131, 132syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → ∃𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)) = ∅)
134 ixp0 8483 . . . . . . . . . . . . 13 (∃𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)) = ∅ → X𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)) = ∅)
135133, 134syl 17 . . . . . . . . . . . 12 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → X𝑘𝑋 ((𝐴𝑘)[,](𝐵𝑘)) = ∅)
136122, 135eqtrd 2853 . . . . . . . . . . 11 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → 𝐼 = ∅)
137136fveq2d 6667 . . . . . . . . . 10 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → ((voln‘𝑋)‘𝐼) = ((voln‘𝑋)‘∅))
138 ne0i 4297 . . . . . . . . . . . . . 14 (𝑘𝑋𝑋 ≠ ∅)
139138adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑘𝑋) → 𝑋 ≠ ∅)
140139, 82syldan 591 . . . . . . . . . . . 12 ((𝜑𝑘𝑋) → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
1411403adant3 1124 . . . . . . . . . . 11 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
142 eleq1w 2892 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → (𝑗𝑋𝑘𝑋))
143 fveq2 6663 . . . . . . . . . . . . . . 15 (𝑗 = 𝑘 → (𝐴𝑗) = (𝐴𝑘))
14466, 143breq12d 5070 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → ((𝐵𝑗) < (𝐴𝑗) ↔ (𝐵𝑘) < (𝐴𝑘)))
145142, 1443anbi23d 1430 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) ↔ (𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘))))
146145imbi1d 343 . . . . . . . . . . . 12 (𝑗 = 𝑘 → (((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = 0) ↔ ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = 0)))
147 nfv 1906 . . . . . . . . . . . . 13 𝑘(𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗))
148553ad2ant1 1125 . . . . . . . . . . . . 13 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → 𝑋 ∈ Fin)
149 volicore 42740 . . . . . . . . . . . . . . . 16 (((𝐴𝑘) ∈ ℝ ∧ (𝐵𝑘) ∈ ℝ) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℝ)
15036, 37, 149syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑋) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℝ)
151150recnd 10657 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑋) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℂ)
1521513ad2antl1 1177 . . . . . . . . . . . . 13 (((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) ∧ 𝑘𝑋) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℂ)
153 simp2 1129 . . . . . . . . . . . . 13 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → 𝑗𝑋)
15449, 50oveq12d 7163 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑗 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝑗)[,)(𝐵𝑗)))
155154fveq2d 6667 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑗)[,)(𝐵𝑗))))
156155adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑗)[,)(𝐵𝑗))))
1572ffvelrnda 6843 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑋) → (𝐴𝑗) ∈ ℝ)
1587ffvelrnda 6843 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑋) → (𝐵𝑗) ∈ ℝ)
159 volico2 42800 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑗) ∈ ℝ ∧ (𝐵𝑗) ∈ ℝ) → (vol‘((𝐴𝑗)[,)(𝐵𝑗))) = if((𝐴𝑗) ≤ (𝐵𝑗), ((𝐵𝑗) − (𝐴𝑗)), 0))
160157, 158, 159syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑋) → (vol‘((𝐴𝑗)[,)(𝐵𝑗))) = if((𝐴𝑗) ≤ (𝐵𝑗), ((𝐵𝑗) − (𝐴𝑗)), 0))
1611603adant3 1124 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → (vol‘((𝐴𝑗)[,)(𝐵𝑗))) = if((𝐴𝑗) ≤ (𝐵𝑗), ((𝐵𝑗) − (𝐴𝑗)), 0))
162 simp3 1130 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → (𝐵𝑗) < (𝐴𝑗))
163158, 157ltnled 10775 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗𝑋) → ((𝐵𝑗) < (𝐴𝑗) ↔ ¬ (𝐴𝑗) ≤ (𝐵𝑗)))
1641633adant3 1124 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → ((𝐵𝑗) < (𝐴𝑗) ↔ ¬ (𝐴𝑗) ≤ (𝐵𝑗)))
165162, 164mpbid 233 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → ¬ (𝐴𝑗) ≤ (𝐵𝑗))
166165iffalsed 4474 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → if((𝐴𝑗) ≤ (𝐵𝑗), ((𝐵𝑗) − (𝐴𝑗)), 0) = 0)
167161, 166eqtrd 2853 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → (vol‘((𝐴𝑗)[,)(𝐵𝑗))) = 0)
168167adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴𝑗)[,)(𝐵𝑗))) = 0)
169156, 168eqtrd 2853 . . . . . . . . . . . . 13 (((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) ∧ 𝑘 = 𝑗) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = 0)
170147, 148, 152, 153, 169fprodeq0g 15336 . . . . . . . . . . . 12 ((𝜑𝑗𝑋 ∧ (𝐵𝑗) < (𝐴𝑗)) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = 0)
171146, 170chvarv 2405 . . . . . . . . . . 11 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = 0)
172141, 171eqtrd 2853 . . . . . . . . . 10 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → (𝐴(𝐿𝑋)𝐵) = 0)
173121, 137, 1723eqtr4d 2863 . . . . . . . . 9 ((𝜑𝑘𝑋 ∧ (𝐵𝑘) < (𝐴𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
1741733exp 1111 . . . . . . . 8 (𝜑 → (𝑘𝑋 → ((𝐵𝑘) < (𝐴𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))))
175174adantr 481 . . . . . . 7 ((𝜑𝑋 ≠ ∅) → (𝑘𝑋 → ((𝐵𝑘) < (𝐴𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))))
17633, 118, 175rexlimd 3314 . . . . . 6 ((𝜑𝑋 ≠ ∅) → (∃𝑘𝑋 (𝐵𝑘) < (𝐴𝑘) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵)))
177176imp 407 . . . . 5 (((𝜑𝑋 ≠ ∅) ∧ ∃𝑘𝑋 (𝐵𝑘) < (𝐴𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
17898, 177syldan 591 . . . 4 (((𝜑𝑋 ≠ ∅) ∧ ¬ ∀𝑘𝑋 (𝐴𝑘) ≤ (𝐵𝑘)) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
17984, 178pm2.61dan 809 . . 3 ((𝜑𝑋 ≠ ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
18032, 179syldan 591 . 2 ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
18130, 180pm2.61dan 809 1 (𝜑 → ((voln‘𝑋)‘𝐼) = (𝐴(𝐿𝑋)𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  wne 3013  wral 3135  wrex 3136  c0 4288  ifcif 4463   class class class wbr 5057  cmpt 5137  dom cdm 5548  wf 6344  cfv 6348  (class class class)co 7145  cmpo 7147  m cmap 8395  Xcixp 8449  Fincfn 8497  cc 10523  cr 10524  0cc0 10525  1c1 10526   + caddc 10528  *cxr 10662   < clt 10663  cle 10664  cmin 10858   / cdiv 11285  cn 11626  [,)cico 12728  [,]cicc 12729  cprod 15247  volcvol 23991  volncvoln 42697
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-13 2381  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092  ax-cc 9845  ax-ac2 9873  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603  ax-addf 10604  ax-mulf 10605
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-disj 5023  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7570  df-1st 7678  df-2nd 7679  df-supp 7820  df-tpos 7881  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-omul 8096  df-er 8278  df-map 8397  df-pm 8398  df-ixp 8450  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-acn 9359  df-ac 9530  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ico 12732  df-icc 12733  df-fz 12881  df-fzo 13022  df-fl 13150  df-seq 13358  df-exp 13418  df-hash 13679  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-clim 14833  df-rlim 14834  df-sum 15031  df-prod 15248  df-struct 16473  df-ndx 16474  df-slot 16475  df-base 16477  df-sets 16478  df-ress 16479  df-plusg 16566  df-mulr 16567  df-starv 16568  df-sca 16569  df-vsca 16570  df-ip 16571  df-tset 16572  df-ple 16573  df-ds 16575  df-unif 16576  df-hom 16577  df-cco 16578  df-rest 16684  df-topn 16685  df-0g 16703  df-gsum 16704  df-topgen 16705  df-pt 16706  df-prds 16709  df-pws 16711  df-xrs 16763  df-qtop 16768  df-imas 16769  df-xps 16771  df-mre 16845  df-mrc 16846  df-acs 16848  df-mgm 17840  df-sgrp 17889  df-mnd 17900  df-mhm 17944  df-submnd 17945  df-grp 18044  df-minusg 18045  df-sbg 18046  df-mulg 18163  df-subg 18214  df-ghm 18294  df-cntz 18385  df-cmn 18837  df-abl 18838  df-mgp 19169  df-ur 19181  df-ring 19228  df-cring 19229  df-oppr 19302  df-dvdsr 19320  df-unit 19321  df-invr 19351  df-dvr 19362  df-rnghom 19396  df-drng 19433  df-field 19434  df-subrg 19462  df-abv 19517  df-staf 19545  df-srng 19546  df-lmod 19565  df-lss 19633  df-lmhm 19723  df-lvec 19804  df-sra 19873  df-rgmod 19874  df-psmet 20465  df-xmet 20466  df-met 20467  df-bl 20468  df-mopn 20469  df-cnfld 20474  df-refld 20677  df-phl 20698  df-dsmm 20804  df-frlm 20819  df-top 21430  df-topon 21447  df-topsp 21469  df-bases 21482  df-cn 21763  df-cnp 21764  df-cmp 21923  df-tx 22098  df-hmeo 22291  df-xms 22857  df-ms 22858  df-tms 22859  df-nm 23119  df-ngp 23120  df-tng 23121  df-nrg 23122  df-nlm 23123  df-cncf 23413  df-clm 23594  df-cph 23699  df-tcph 23700  df-rrx 23915  df-ovol 23992  df-vol 23993  df-salg 42471  df-sumge0 42522  df-mea 42609  df-ome 42649  df-caragen 42651  df-ovoln 42696  df-voln 42698
This theorem is referenced by:  vonn0icc  42847
  Copyright terms: Public domain W3C validator