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

Theorem ovolval4lem1 43676
 Description: |- ( ( ph /\ n e. A ) -> ( ( (,) o. G ) 𝑛) = (((,) ∘ 𝐹) n ) ) (Contributed by Glauco Siliprandi, 3-Mar-2021.)
Hypotheses
Ref Expression
ovolval4lem1.f (𝜑𝐹:ℕ⟶(ℝ* × ℝ*))
ovolval4lem1.g 𝐺 = (𝑛 ∈ ℕ ↦ ⟨(1st ‘(𝐹𝑛)), if((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛)), (1st ‘(𝐹𝑛)))⟩)
ovolval4lem1.a 𝐴 = {𝑛 ∈ ℕ ∣ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))}
Assertion
Ref Expression
ovolval4lem1 (𝜑 → ( ran ((,) ∘ 𝐹) = ran ((,) ∘ 𝐺) ∧ (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺))))
Distinct variable groups:   𝐴,𝑛   𝑛,𝐹   𝑛,𝐺   𝜑,𝑛

Proof of Theorem ovolval4lem1
StepHypRef Expression
1 ioof 12879 . . . . . . . 8 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
21a1i 11 . . . . . . 7 (𝜑 → (,):(ℝ* × ℝ*)⟶𝒫 ℝ)
3 ovolval4lem1.f . . . . . . 7 (𝜑𝐹:ℕ⟶(ℝ* × ℝ*))
4 fco 6516 . . . . . . 7 (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
52, 3, 4syl2anc 587 . . . . . 6 (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
65ffnd 6499 . . . . 5 (𝜑 → ((,) ∘ 𝐹) Fn ℕ)
7 fniunfv 6998 . . . . 5 (((,) ∘ 𝐹) Fn ℕ → 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ran ((,) ∘ 𝐹))
86, 7syl 17 . . . 4 (𝜑 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ran ((,) ∘ 𝐹))
98eqcomd 2764 . . 3 (𝜑 ran ((,) ∘ 𝐹) = 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛))
10 ovolval4lem1.a . . . . . . . . 9 𝐴 = {𝑛 ∈ ℕ ∣ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))}
11 ssrab2 3984 . . . . . . . . 9 {𝑛 ∈ ℕ ∣ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))} ⊆ ℕ
1210, 11eqsstri 3926 . . . . . . . 8 𝐴 ⊆ ℕ
13 undif 4378 . . . . . . . 8 (𝐴 ⊆ ℕ ↔ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ)
1412, 13mpbi 233 . . . . . . 7 (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ
1514eqcomi 2767 . . . . . 6 ℕ = (𝐴 ∪ (ℕ ∖ 𝐴))
1615iuneq1i 42116 . . . . 5 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛)
17 iunxun 4981 . . . . 5 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛) = ( 𝑛𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
1816, 17eqtri 2781 . . . 4 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ( 𝑛𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
1918a1i 11 . . 3 (𝜑 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ( 𝑛𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)))
203ffvelrnda 6842 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ (ℝ* × ℝ*))
21 xp1st 7725 . . . . . . . . . . 11 ((𝐹𝑛) ∈ (ℝ* × ℝ*) → (1st ‘(𝐹𝑛)) ∈ ℝ*)
2220, 21syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ*)
23 xp2nd 7726 . . . . . . . . . . . 12 ((𝐹𝑛) ∈ (ℝ* × ℝ*) → (2nd ‘(𝐹𝑛)) ∈ ℝ*)
2420, 23syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ*)
2524, 22ifcld 4466 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → if((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛)), (1st ‘(𝐹𝑛))) ∈ ℝ*)
2622, 25opelxpd 5562 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ⟨(1st ‘(𝐹𝑛)), if((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛)), (1st ‘(𝐹𝑛)))⟩ ∈ (ℝ* × ℝ*))
27 ovolval4lem1.g . . . . . . . . 9 𝐺 = (𝑛 ∈ ℕ ↦ ⟨(1st ‘(𝐹𝑛)), if((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛)), (1st ‘(𝐹𝑛)))⟩)
2826, 27fmptd 6869 . . . . . . . 8 (𝜑𝐺:ℕ⟶(ℝ* × ℝ*))
29 fco 6516 . . . . . . . 8 (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
302, 28, 29syl2anc 587 . . . . . . 7 (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
3130ffnd 6499 . . . . . 6 (𝜑 → ((,) ∘ 𝐺) Fn ℕ)
32 fniunfv 6998 . . . . . 6 (((,) ∘ 𝐺) Fn ℕ → 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ran ((,) ∘ 𝐺))
3331, 32syl 17 . . . . 5 (𝜑 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ran ((,) ∘ 𝐺))
3433eqcomd 2764 . . . 4 (𝜑 ran ((,) ∘ 𝐺) = 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛))
3515iuneq1i 42116 . . . . . 6 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛)
36 iunxun 4981 . . . . . 6 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛) = ( 𝑛𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛))
3735, 36eqtri 2781 . . . . 5 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ( 𝑛𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛))
3837a1i 11 . . . 4 (𝜑 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ( 𝑛𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛)))
3928adantr 484 . . . . . . . 8 ((𝜑𝑛𝐴) → 𝐺:ℕ⟶(ℝ* × ℝ*))
4012sseli 3888 . . . . . . . . 9 (𝑛𝐴𝑛 ∈ ℕ)
4140adantl 485 . . . . . . . 8 ((𝜑𝑛𝐴) → 𝑛 ∈ ℕ)
42 fvco3 6751 . . . . . . . 8 ((𝐺:ℕ⟶(ℝ* × ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺𝑛)))
4339, 41, 42syl2anc 587 . . . . . . 7 ((𝜑𝑛𝐴) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺𝑛)))
443adantr 484 . . . . . . . . 9 ((𝜑𝑛𝐴) → 𝐹:ℕ⟶(ℝ* × ℝ*))
45 fvco3 6751 . . . . . . . . 9 ((𝐹:ℕ⟶(ℝ* × ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹𝑛)))
4644, 41, 45syl2anc 587 . . . . . . . 8 ((𝜑𝑛𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹𝑛)))
47 simpl 486 . . . . . . . . . . 11 ((𝜑𝑛𝐴) → 𝜑)
48 1st2nd2 7732 . . . . . . . . . . . 12 ((𝐹𝑛) ∈ (ℝ* × ℝ*) → (𝐹𝑛) = ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
4920, 48syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
5047, 41, 49syl2anc 587 . . . . . . . . . 10 ((𝜑𝑛𝐴) → (𝐹𝑛) = ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
5127a1i 11 . . . . . . . . . . . . 13 (𝜑𝐺 = (𝑛 ∈ ℕ ↦ ⟨(1st ‘(𝐹𝑛)), if((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛)), (1st ‘(𝐹𝑛)))⟩))
5226elexd 3430 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ⟨(1st ‘(𝐹𝑛)), if((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛)), (1st ‘(𝐹𝑛)))⟩ ∈ V)
5351, 52fvmpt2d 6772 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) = ⟨(1st ‘(𝐹𝑛)), if((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛)), (1st ‘(𝐹𝑛)))⟩)
5447, 41, 53syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑛𝐴) → (𝐺𝑛) = ⟨(1st ‘(𝐹𝑛)), if((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛)), (1st ‘(𝐹𝑛)))⟩)
5510eleq2i 2843 . . . . . . . . . . . . . . . . 17 (𝑛𝐴𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))})
5655biimpi 219 . . . . . . . . . . . . . . . 16 (𝑛𝐴𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))})
57 rabid 3296 . . . . . . . . . . . . . . . 16 (𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))} ↔ (𝑛 ∈ ℕ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
5856, 57sylib 221 . . . . . . . . . . . . . . 15 (𝑛𝐴 → (𝑛 ∈ ℕ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
5958simprd 499 . . . . . . . . . . . . . 14 (𝑛𝐴 → (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)))
6059adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑛𝐴) → (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)))
6160iftrued 4428 . . . . . . . . . . . 12 ((𝜑𝑛𝐴) → if((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛)), (1st ‘(𝐹𝑛))) = (2nd ‘(𝐹𝑛)))
6261opeq2d 4770 . . . . . . . . . . 11 ((𝜑𝑛𝐴) → ⟨(1st ‘(𝐹𝑛)), if((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛)), (1st ‘(𝐹𝑛)))⟩ = ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
63 eqidd 2759 . . . . . . . . . . 11 ((𝜑𝑛𝐴) → ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩ = ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
6454, 62, 633eqtrd 2797 . . . . . . . . . 10 ((𝜑𝑛𝐴) → (𝐺𝑛) = ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
6550, 64eqtr4d 2796 . . . . . . . . 9 ((𝜑𝑛𝐴) → (𝐹𝑛) = (𝐺𝑛))
6665fveq2d 6662 . . . . . . . 8 ((𝜑𝑛𝐴) → ((,)‘(𝐹𝑛)) = ((,)‘(𝐺𝑛)))
6746, 66eqtrd 2793 . . . . . . 7 ((𝜑𝑛𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐺𝑛)))
6843, 67eqtr4d 2796 . . . . . 6 ((𝜑𝑛𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛))
6968iuneq2dv 4907 . . . . 5 (𝜑 𝑛𝐴 (((,) ∘ 𝐺)‘𝑛) = 𝑛𝐴 (((,) ∘ 𝐹)‘𝑛))
7028adantr 484 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → 𝐺:ℕ⟶(ℝ* × ℝ*))
71 eldifi 4032 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ 𝐴) → 𝑛 ∈ ℕ)
7271adantl 485 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → 𝑛 ∈ ℕ)
7370, 72, 42syl2anc 587 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺𝑛)))
74 simpl 486 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → 𝜑)
7574, 72, 53syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐺𝑛) = ⟨(1st ‘(𝐹𝑛)), if((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛)), (1st ‘(𝐹𝑛)))⟩)
7671anim1i 617 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))) → (𝑛 ∈ ℕ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
7776, 57sylibr 237 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))) → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))})
7877, 55sylibr 237 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))) → 𝑛𝐴)
7978adantll 713 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))) → 𝑛𝐴)
80 eldifn 4033 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℕ ∖ 𝐴) → ¬ 𝑛𝐴)
8180ad2antlr 726 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))) → ¬ 𝑛𝐴)
8279, 81pm2.65da 816 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → ¬ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)))
8382iffalsed 4431 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → if((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛)), (1st ‘(𝐹𝑛))) = (1st ‘(𝐹𝑛)))
8483opeq2d 4770 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → ⟨(1st ‘(𝐹𝑛)), if((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛)), (1st ‘(𝐹𝑛)))⟩ = ⟨(1st ‘(𝐹𝑛)), (1st ‘(𝐹𝑛))⟩)
8575, 84eqtrd 2793 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐺𝑛) = ⟨(1st ‘(𝐹𝑛)), (1st ‘(𝐹𝑛))⟩)
8685fveq2d 6662 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐺𝑛)) = ((,)‘⟨(1st ‘(𝐹𝑛)), (1st ‘(𝐹𝑛))⟩))
87 iooid 12807 . . . . . . . . . . . 12 ((1st ‘(𝐹𝑛))(,)(1st ‘(𝐹𝑛))) = ∅
8887eqcomi 2767 . . . . . . . . . . 11 ∅ = ((1st ‘(𝐹𝑛))(,)(1st ‘(𝐹𝑛)))
89 df-ov 7153 . . . . . . . . . . 11 ((1st ‘(𝐹𝑛))(,)(1st ‘(𝐹𝑛))) = ((,)‘⟨(1st ‘(𝐹𝑛)), (1st ‘(𝐹𝑛))⟩)
9088, 89eqtr2i 2782 . . . . . . . . . 10 ((,)‘⟨(1st ‘(𝐹𝑛)), (1st ‘(𝐹𝑛))⟩) = ∅
9190a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘⟨(1st ‘(𝐹𝑛)), (1st ‘(𝐹𝑛))⟩) = ∅)
9273, 86, 913eqtrd 2797 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ∅)
9392iuneq2dv 4907 . . . . . . 7 (𝜑 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = 𝑛 ∈ (ℕ ∖ 𝐴)∅)
94 iun0 4950 . . . . . . . 8 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅
9594a1i 11 . . . . . . 7 (𝜑 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅)
9693, 95eqtrd 2793 . . . . . 6 (𝜑 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∅)
9774, 3syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → 𝐹:ℕ⟶(ℝ* × ℝ*))
9897, 72, 45syl2anc 587 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹𝑛)))
9974, 72, 49syl2anc 587 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐹𝑛) = ⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
10099fveq2d 6662 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐹𝑛)) = ((,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩))
101 df-ov 7153 . . . . . . . . . . 11 ((1st ‘(𝐹𝑛))(,)(2nd ‘(𝐹𝑛))) = ((,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩)
102101a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹𝑛))(,)(2nd ‘(𝐹𝑛))) = ((,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩))
103 simplr 768 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹𝑛)) ≤ (1st ‘(𝐹𝑛))) → 𝑛 ∈ (ℕ ∖ 𝐴))
10472, 22syldan 594 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → (1st ‘(𝐹𝑛)) ∈ ℝ*)
105104adantr 484 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹𝑛)) ≤ (1st ‘(𝐹𝑛))) → (1st ‘(𝐹𝑛)) ∈ ℝ*)
10672, 24syldan 594 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹𝑛)) ∈ ℝ*)
107106adantr 484 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹𝑛)) ≤ (1st ‘(𝐹𝑛))) → (2nd ‘(𝐹𝑛)) ∈ ℝ*)
108 simpr 488 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹𝑛)) ≤ (1st ‘(𝐹𝑛))) → ¬ (2nd ‘(𝐹𝑛)) ≤ (1st ‘(𝐹𝑛)))
109105, 107xrltnled 42385 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹𝑛)) ≤ (1st ‘(𝐹𝑛))) → ((1st ‘(𝐹𝑛)) < (2nd ‘(𝐹𝑛)) ↔ ¬ (2nd ‘(𝐹𝑛)) ≤ (1st ‘(𝐹𝑛))))
110108, 109mpbird 260 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹𝑛)) ≤ (1st ‘(𝐹𝑛))) → (1st ‘(𝐹𝑛)) < (2nd ‘(𝐹𝑛)))
111105, 107, 110xrltled 12584 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹𝑛)) ≤ (1st ‘(𝐹𝑛))) → (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)))
112103, 111, 78syl2anc 587 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹𝑛)) ≤ (1st ‘(𝐹𝑛))) → 𝑛𝐴)
11380ad2antlr 726 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹𝑛)) ≤ (1st ‘(𝐹𝑛))) → ¬ 𝑛𝐴)
114112, 113condan 817 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹𝑛)) ≤ (1st ‘(𝐹𝑛)))
115 ioo0 12804 . . . . . . . . . . . 12 (((1st ‘(𝐹𝑛)) ∈ ℝ* ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ*) → (((1st ‘(𝐹𝑛))(,)(2nd ‘(𝐹𝑛))) = ∅ ↔ (2nd ‘(𝐹𝑛)) ≤ (1st ‘(𝐹𝑛))))
116104, 106, 115syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → (((1st ‘(𝐹𝑛))(,)(2nd ‘(𝐹𝑛))) = ∅ ↔ (2nd ‘(𝐹𝑛)) ≤ (1st ‘(𝐹𝑛))))
117114, 116mpbird 260 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹𝑛))(,)(2nd ‘(𝐹𝑛))) = ∅)
118102, 117eqtr3d 2795 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩) = ∅)
11998, 100, 1183eqtrd 2797 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = ∅)
120119iuneq2dv 4907 . . . . . . 7 (𝜑 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = 𝑛 ∈ (ℕ ∖ 𝐴)∅)
121120, 95eqtrd 2793 . . . . . 6 (𝜑 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∅)
12296, 121eqtr4d 2796 . . . . 5 (𝜑 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
12369, 122uneq12d 4069 . . . 4 (𝜑 → ( 𝑛𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛)) = ( 𝑛𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)))
12434, 38, 1233eqtrrd 2798 . . 3 (𝜑 → ( 𝑛𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)) = ran ((,) ∘ 𝐺))
1259, 19, 1243eqtrd 2797 . 2 (𝜑 ran ((,) ∘ 𝐹) = ran ((,) ∘ 𝐺))
126 volf 24229 . . . . . 6 vol:dom vol⟶(0[,]+∞)
127126a1i 11 . . . . 5 (𝜑 → vol:dom vol⟶(0[,]+∞))
1283adantr 484 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝐹:ℕ⟶(ℝ* × ℝ*))
129 simpr 488 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
130128, 129, 45syl2anc 587 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹𝑛)))
13149fveq2d 6662 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((,)‘(𝐹𝑛)) = ((,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩))
132101eqcomi 2767 . . . . . . . . . . 11 ((,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩) = ((1st ‘(𝐹𝑛))(,)(2nd ‘(𝐹𝑛)))
133132a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((,)‘⟨(1st ‘(𝐹𝑛)), (2nd ‘(𝐹𝑛))⟩) = ((1st ‘(𝐹𝑛))(,)(2nd ‘(𝐹𝑛))))
134130, 131, 1333eqtrd 2797 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((1st ‘(𝐹𝑛))(,)(2nd ‘(𝐹𝑛))))
135 ioombl 24265 . . . . . . . . . 10 ((1st ‘(𝐹𝑛))(,)(2nd ‘(𝐹𝑛))) ∈ dom vol
136135a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛))(,)(2nd ‘(𝐹𝑛))) ∈ dom vol)
137134, 136eqeltrd 2852 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
138137ralrimiva 3113 . . . . . . 7 (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
1396, 138jca 515 . . . . . 6 (𝜑 → (((,) ∘ 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol))
140 ffnfv 6873 . . . . . 6 (((,) ∘ 𝐹):ℕ⟶dom vol ↔ (((,) ∘ 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol))
141139, 140sylibr 237 . . . . 5 (𝜑 → ((,) ∘ 𝐹):ℕ⟶dom vol)
142 fco 6516 . . . . 5 ((vol:dom vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐹):ℕ⟶dom vol) → (vol ∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞))
143127, 141, 142syl2anc 587 . . . 4 (𝜑 → (vol ∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞))
144143ffnd 6499 . . 3 (𝜑 → (vol ∘ ((,) ∘ 𝐹)) Fn ℕ)
14568adantlr 714 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑛𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛))
146137adantr 484 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑛𝐴) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
147145, 146eqeltrd 2852 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑛𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
148 simpll 766 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ ¬ 𝑛𝐴) → 𝜑)
149 eldif 3868 . . . . . . . . . . . . 13 (𝑛 ∈ (ℕ ∖ 𝐴) ↔ (𝑛 ∈ ℕ ∧ ¬ 𝑛𝐴))
150149bicomi 227 . . . . . . . . . . . 12 ((𝑛 ∈ ℕ ∧ ¬ 𝑛𝐴) ↔ 𝑛 ∈ (ℕ ∖ 𝐴))
151150biimpi 219 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ ¬ 𝑛𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴))
152151adantll 713 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ ¬ 𝑛𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴))
153117, 135eqeltrrdi 2861 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → ∅ ∈ dom vol)
15492, 153eqeltrd 2852 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
155148, 152, 154syl2anc 587 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ ¬ 𝑛𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
156147, 155pm2.61dan 812 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
157156ralrimiva 3113 . . . . . . 7 (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
15831, 157jca 515 . . . . . 6 (𝜑 → (((,) ∘ 𝐺) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol))
159 ffnfv 6873 . . . . . 6 (((,) ∘ 𝐺):ℕ⟶dom vol ↔ (((,) ∘ 𝐺) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol))
160158, 159sylibr 237 . . . . 5 (𝜑 → ((,) ∘ 𝐺):ℕ⟶dom vol)
161 fco 6516 . . . . 5 ((vol:dom vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐺):ℕ⟶dom vol) → (vol ∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞))
162127, 160, 161syl2anc 587 . . . 4 (𝜑 → (vol ∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞))
163162ffnd 6499 . . 3 (𝜑 → (vol ∘ ((,) ∘ 𝐺)) Fn ℕ)
164145eqcomd 2764 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑛𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
165119, 92eqtr4d 2796 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
166148, 152, 165syl2anc 587 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ ¬ 𝑛𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
167164, 166pm2.61dan 812 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
168167fveq2d 6662 . . . 4 ((𝜑𝑛 ∈ ℕ) → (vol‘(((,) ∘ 𝐹)‘𝑛)) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
169 fnfun 6434 . . . . . . 7 (((,) ∘ 𝐹) Fn ℕ → Fun ((,) ∘ 𝐹))
1706, 169syl 17 . . . . . 6 (𝜑 → Fun ((,) ∘ 𝐹))
171170adantr 484 . . . . 5 ((𝜑𝑛 ∈ ℕ) → Fun ((,) ∘ 𝐹))
1725fdmd 6508 . . . . . . . 8 (𝜑 → dom ((,) ∘ 𝐹) = ℕ)
173172eqcomd 2764 . . . . . . 7 (𝜑 → ℕ = dom ((,) ∘ 𝐹))
174173adantr 484 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ℕ = dom ((,) ∘ 𝐹))
175129, 174eleqtrd 2854 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐹))
176 fvco 6750 . . . . 5 ((Fun ((,) ∘ 𝐹) ∧ 𝑛 ∈ dom ((,) ∘ 𝐹)) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = (vol‘(((,) ∘ 𝐹)‘𝑛)))
177171, 175, 176syl2anc 587 . . . 4 ((𝜑𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = (vol‘(((,) ∘ 𝐹)‘𝑛)))
178 fnfun 6434 . . . . . . 7 (((,) ∘ 𝐺) Fn ℕ → Fun ((,) ∘ 𝐺))
17931, 178syl 17 . . . . . 6 (𝜑 → Fun ((,) ∘ 𝐺))
180179adantr 484 . . . . 5 ((𝜑𝑛 ∈ ℕ) → Fun ((,) ∘ 𝐺))
18130fdmd 6508 . . . . . . . 8 (𝜑 → dom ((,) ∘ 𝐺) = ℕ)
182181eqcomd 2764 . . . . . . 7 (𝜑 → ℕ = dom ((,) ∘ 𝐺))
183182adantr 484 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ℕ = dom ((,) ∘ 𝐺))
184129, 183eleqtrd 2854 . . . . 5 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐺))
185 fvco 6750 . . . . 5 ((Fun ((,) ∘ 𝐺) ∧ 𝑛 ∈ dom ((,) ∘ 𝐺)) → ((vol ∘ ((,) ∘ 𝐺))‘𝑛) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
186180, 184, 185syl2anc 587 . . . 4 ((𝜑𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐺))‘𝑛) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
187168, 177, 1863eqtr4d 2803 . . 3 ((𝜑𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = ((vol ∘ ((,) ∘ 𝐺))‘𝑛))
188144, 163, 187eqfnfvd 6796 . 2 (𝜑 → (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺)))
189125, 188jca 515 1 (𝜑 → ( ran ((,) ∘ 𝐹) = ran ((,) ∘ 𝐺) ∧ (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3070  {crab 3074  Vcvv 3409   ∖ cdif 3855   ∪ cun 3856   ⊆ wss 3858  ∅c0 4225  ifcif 4420  𝒫 cpw 4494  ⟨cop 4528  ∪ cuni 4798  ∪ ciun 4883   class class class wbr 5032   ↦ cmpt 5112   × cxp 5522  dom cdm 5524  ran crn 5525   ∘ ccom 5528  Fun wfun 6329   Fn wfn 6330  ⟶wf 6331  ‘cfv 6335  (class class class)co 7150  1st c1st 7691  2nd c2nd 7692  ℝcr 10574  0cc0 10575  +∞cpnf 10710  ℝ*cxr 10712   < clt 10713   ≤ cle 10714  ℕcn 11674  (,)cioo 12779  [,]cicc 12782  volcvol 24163 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-inf2 9137  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652  ax-pre-sup 10653 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 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-se 5484  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-isom 6344  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7405  df-om 7580  df-1st 7693  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-2o 8113  df-er 8299  df-map 8418  df-pm 8419  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-sup 8939  df-inf 8940  df-oi 9007  df-dju 9363  df-card 9401  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-div 11336  df-nn 11675  df-2 11737  df-3 11738  df-n0 11935  df-z 12021  df-uz 12283  df-q 12389  df-rp 12431  df-xadd 12549  df-ioo 12783  df-ico 12785  df-icc 12786  df-fz 12940  df-fzo 13083  df-fl 13211  df-seq 13419  df-exp 13480  df-hash 13741  df-cj 14506  df-re 14507  df-im 14508  df-sqrt 14642  df-abs 14643  df-clim 14893  df-rlim 14894  df-sum 15091  df-xmet 20159  df-met 20160  df-ovol 24164  df-vol 24165 This theorem is referenced by:  ovolval4lem2  43677
 Copyright terms: Public domain W3C validator