MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovolunlem1 Structured version   Visualization version   GIF version

Theorem ovolunlem1 23311
Description: Lemma for ovolun 23313. (Contributed by Mario Carneiro, 12-Jun-2014.)
Hypotheses
Ref Expression
ovolun.a (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))
ovolun.b (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))
ovolun.c (𝜑𝐶 ∈ ℝ+)
ovolun.s 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
ovolun.t 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
ovolun.u 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
ovolun.f1 (𝜑𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ))
ovolun.f2 (𝜑𝐴 ran ((,) ∘ 𝐹))
ovolun.f3 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
ovolun.g1 (𝜑𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ))
ovolun.g2 (𝜑𝐵 ran ((,) ∘ 𝐺))
ovolun.g3 (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
ovolun.h 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))
Assertion
Ref Expression
ovolunlem1 (𝜑 → (vol*‘(𝐴𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
Distinct variable groups:   𝐶,𝑛   𝑛,𝐹   𝐴,𝑛   𝐵,𝑛   𝑛,𝐺   𝜑,𝑛
Allowed substitution hints:   𝑆(𝑛)   𝑇(𝑛)   𝑈(𝑛)   𝐻(𝑛)

Proof of Theorem ovolunlem1
Dummy variables 𝑘 𝑧 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovolun.a . . . . 5 (𝜑 → (𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ))
21simpld 474 . . . 4 (𝜑𝐴 ⊆ ℝ)
3 ovolun.b . . . . 5 (𝜑 → (𝐵 ⊆ ℝ ∧ (vol*‘𝐵) ∈ ℝ))
43simpld 474 . . . 4 (𝜑𝐵 ⊆ ℝ)
52, 4unssd 3822 . . 3 (𝜑 → (𝐴𝐵) ⊆ ℝ)
6 ovolun.g1 . . . . . . . . . . . 12 (𝜑𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ))
7 reex 10065 . . . . . . . . . . . . . . 15 ℝ ∈ V
87, 7xpex 7004 . . . . . . . . . . . . . 14 (ℝ × ℝ) ∈ V
98inex2 4833 . . . . . . . . . . . . 13 ( ≤ ∩ (ℝ × ℝ)) ∈ V
10 nnex 11064 . . . . . . . . . . . . 13 ℕ ∈ V
119, 10elmap 7928 . . . . . . . . . . . 12 (𝐺 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ↔ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
126, 11sylib 208 . . . . . . . . . . 11 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1312adantr 480 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
1413ffvelrnda 6399 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ (𝑛 / 2) ∈ ℕ) → (𝐺‘(𝑛 / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
15 nneo 11499 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
1615adantl 481 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((𝑛 / 2) ∈ ℕ ↔ ¬ ((𝑛 + 1) / 2) ∈ ℕ))
1716con2bid 343 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (((𝑛 + 1) / 2) ∈ ℕ ↔ ¬ (𝑛 / 2) ∈ ℕ))
1817biimpar 501 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → ((𝑛 + 1) / 2) ∈ ℕ)
19 ovolun.f1 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ))
209, 10elmap 7928 . . . . . . . . . . . . 13 (𝐹 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ) ↔ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
2119, 20sylib 208 . . . . . . . . . . . 12 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
2221adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
2322ffvelrnda 6399 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ ((𝑛 + 1) / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
2418, 23syldan 486 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ ¬ (𝑛 / 2) ∈ ℕ) → (𝐹‘((𝑛 + 1) / 2)) ∈ ( ≤ ∩ (ℝ × ℝ)))
2514, 24ifclda 4153 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) ∈ ( ≤ ∩ (ℝ × ℝ)))
26 ovolun.h . . . . . . . 8 𝐻 = (𝑛 ∈ ℕ ↦ if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))))
2725, 26fmptd 6425 . . . . . . 7 (𝜑𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
28 eqid 2651 . . . . . . . 8 ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
29 ovolun.u . . . . . . . 8 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
3028, 29ovolsf 23287 . . . . . . 7 (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
3127, 30syl 17 . . . . . 6 (𝜑𝑈:ℕ⟶(0[,)+∞))
32 rge0ssre 12318 . . . . . 6 (0[,)+∞) ⊆ ℝ
33 fss 6094 . . . . . 6 ((𝑈:ℕ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑈:ℕ⟶ℝ)
3431, 32, 33sylancl 695 . . . . 5 (𝜑𝑈:ℕ⟶ℝ)
35 frn 6091 . . . . 5 (𝑈:ℕ⟶ℝ → ran 𝑈 ⊆ ℝ)
3634, 35syl 17 . . . 4 (𝜑 → ran 𝑈 ⊆ ℝ)
37 1nn 11069 . . . . . . 7 1 ∈ ℕ
38 1z 11445 . . . . . . . . . 10 1 ∈ ℤ
39 seqfn 12853 . . . . . . . . . 10 (1 ∈ ℤ → seq1( + , ((abs ∘ − ) ∘ 𝐻)) Fn (ℤ‘1))
4038, 39mp1i 13 . . . . . . . . 9 (𝜑 → seq1( + , ((abs ∘ − ) ∘ 𝐻)) Fn (ℤ‘1))
4129fneq1i 6023 . . . . . . . . . 10 (𝑈 Fn ℕ ↔ seq1( + , ((abs ∘ − ) ∘ 𝐻)) Fn ℕ)
42 nnuz 11761 . . . . . . . . . . 11 ℕ = (ℤ‘1)
4342fneq2i 6024 . . . . . . . . . 10 (seq1( + , ((abs ∘ − ) ∘ 𝐻)) Fn ℕ ↔ seq1( + , ((abs ∘ − ) ∘ 𝐻)) Fn (ℤ‘1))
4441, 43bitri 264 . . . . . . . . 9 (𝑈 Fn ℕ ↔ seq1( + , ((abs ∘ − ) ∘ 𝐻)) Fn (ℤ‘1))
4540, 44sylibr 224 . . . . . . . 8 (𝜑𝑈 Fn ℕ)
46 fndm 6028 . . . . . . . 8 (𝑈 Fn ℕ → dom 𝑈 = ℕ)
4745, 46syl 17 . . . . . . 7 (𝜑 → dom 𝑈 = ℕ)
4837, 47syl5eleqr 2737 . . . . . 6 (𝜑 → 1 ∈ dom 𝑈)
49 ne0i 3954 . . . . . 6 (1 ∈ dom 𝑈 → dom 𝑈 ≠ ∅)
5048, 49syl 17 . . . . 5 (𝜑 → dom 𝑈 ≠ ∅)
51 dm0rn0 5374 . . . . . 6 (dom 𝑈 = ∅ ↔ ran 𝑈 = ∅)
5251necon3bii 2875 . . . . 5 (dom 𝑈 ≠ ∅ ↔ ran 𝑈 ≠ ∅)
5350, 52sylib 208 . . . 4 (𝜑 → ran 𝑈 ≠ ∅)
541simprd 478 . . . . . . . 8 (𝜑 → (vol*‘𝐴) ∈ ℝ)
553simprd 478 . . . . . . . 8 (𝜑 → (vol*‘𝐵) ∈ ℝ)
5654, 55readdcld 10107 . . . . . . 7 (𝜑 → ((vol*‘𝐴) + (vol*‘𝐵)) ∈ ℝ)
57 ovolun.c . . . . . . . 8 (𝜑𝐶 ∈ ℝ+)
5857rpred 11910 . . . . . . 7 (𝜑𝐶 ∈ ℝ)
5956, 58readdcld 10107 . . . . . 6 (𝜑 → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ)
60 ovolun.s . . . . . . . . 9 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
61 ovolun.t . . . . . . . . 9 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
62 ovolun.f2 . . . . . . . . 9 (𝜑𝐴 ran ((,) ∘ 𝐹))
63 ovolun.f3 . . . . . . . . 9 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 / 2)))
64 ovolun.g2 . . . . . . . . 9 (𝜑𝐵 ran ((,) ∘ 𝐺))
65 ovolun.g3 . . . . . . . . 9 (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐵) + (𝐶 / 2)))
661, 3, 57, 60, 61, 29, 19, 62, 63, 6, 64, 65, 26ovolunlem1a 23310 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑈𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
6766ralrimiva 2995 . . . . . . 7 (𝜑 → ∀𝑘 ∈ ℕ (𝑈𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
68 breq1 4688 . . . . . . . . 9 (𝑧 = (𝑈𝑘) → (𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ↔ (𝑈𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)))
6968ralrn 6402 . . . . . . . 8 (𝑈 Fn ℕ → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ↔ ∀𝑘 ∈ ℕ (𝑈𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)))
7045, 69syl 17 . . . . . . 7 (𝜑 → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ↔ ∀𝑘 ∈ ℕ (𝑈𝑘) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)))
7167, 70mpbird 247 . . . . . 6 (𝜑 → ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
72 breq2 4689 . . . . . . . 8 (𝑘 = (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) → (𝑧𝑘𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)))
7372ralbidv 3015 . . . . . . 7 (𝑘 = (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) → (∀𝑧 ∈ ran 𝑈 𝑧𝑘 ↔ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)))
7473rspcev 3340 . . . . . 6 (((((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ ∧ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)) → ∃𝑘 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧𝑘)
7559, 71, 74syl2anc 694 . . . . 5 (𝜑 → ∃𝑘 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧𝑘)
76 ressxr 10121 . . . . . . 7 ℝ ⊆ ℝ*
7736, 76syl6ss 3648 . . . . . 6 (𝜑 → ran 𝑈 ⊆ ℝ*)
78 supxrbnd2 12190 . . . . . 6 (ran 𝑈 ⊆ ℝ* → (∃𝑘 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧𝑘 ↔ sup(ran 𝑈, ℝ*, < ) < +∞))
7977, 78syl 17 . . . . 5 (𝜑 → (∃𝑘 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧𝑘 ↔ sup(ran 𝑈, ℝ*, < ) < +∞))
8075, 79mpbid 222 . . . 4 (𝜑 → sup(ran 𝑈, ℝ*, < ) < +∞)
81 supxrbnd 12196 . . . 4 ((ran 𝑈 ⊆ ℝ ∧ ran 𝑈 ≠ ∅ ∧ sup(ran 𝑈, ℝ*, < ) < +∞) → sup(ran 𝑈, ℝ*, < ) ∈ ℝ)
8236, 53, 80, 81syl3anc 1366 . . 3 (𝜑 → sup(ran 𝑈, ℝ*, < ) ∈ ℝ)
83 nncn 11066 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
8483adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
85842timesd 11313 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (2 · 𝑚) = (𝑚 + 𝑚))
8685oveq1d 6705 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → ((2 · 𝑚) − 1) = ((𝑚 + 𝑚) − 1))
87 1cnd 10094 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → 1 ∈ ℂ)
8884, 84, 87addsubassd 10450 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → ((𝑚 + 𝑚) − 1) = (𝑚 + (𝑚 − 1)))
8986, 88eqtrd 2685 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((2 · 𝑚) − 1) = (𝑚 + (𝑚 − 1)))
90 simpr 476 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
91 nnm1nn0 11372 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → (𝑚 − 1) ∈ ℕ0)
9291adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝑚 − 1) ∈ ℕ0)
93 nnnn0addcl 11361 . . . . . . . . . . . . 13 ((𝑚 ∈ ℕ ∧ (𝑚 − 1) ∈ ℕ0) → (𝑚 + (𝑚 − 1)) ∈ ℕ)
9490, 92, 93syl2anc 694 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (𝑚 + (𝑚 − 1)) ∈ ℕ)
9589, 94eqeltrd 2730 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → ((2 · 𝑚) − 1) ∈ ℕ)
96 oveq1 6697 . . . . . . . . . . . . . . . 16 (𝑛 = ((2 · 𝑚) − 1) → (𝑛 / 2) = (((2 · 𝑚) − 1) / 2))
9796eleq1d 2715 . . . . . . . . . . . . . . 15 (𝑛 = ((2 · 𝑚) − 1) → ((𝑛 / 2) ∈ ℕ ↔ (((2 · 𝑚) − 1) / 2) ∈ ℕ))
9896fveq2d 6233 . . . . . . . . . . . . . . 15 (𝑛 = ((2 · 𝑚) − 1) → (𝐺‘(𝑛 / 2)) = (𝐺‘(((2 · 𝑚) − 1) / 2)))
99 oveq1 6697 . . . . . . . . . . . . . . . . 17 (𝑛 = ((2 · 𝑚) − 1) → (𝑛 + 1) = (((2 · 𝑚) − 1) + 1))
10099oveq1d 6705 . . . . . . . . . . . . . . . 16 (𝑛 = ((2 · 𝑚) − 1) → ((𝑛 + 1) / 2) = ((((2 · 𝑚) − 1) + 1) / 2))
101100fveq2d 6233 . . . . . . . . . . . . . . 15 (𝑛 = ((2 · 𝑚) − 1) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘((((2 · 𝑚) − 1) + 1) / 2)))
10297, 98, 101ifbieq12d 4146 . . . . . . . . . . . . . 14 (𝑛 = ((2 · 𝑚) − 1) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if((((2 · 𝑚) − 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑚) − 1) / 2)), (𝐹‘((((2 · 𝑚) − 1) + 1) / 2))))
103 fvex 6239 . . . . . . . . . . . . . . 15 (𝐺‘(((2 · 𝑚) − 1) / 2)) ∈ V
104 fvex 6239 . . . . . . . . . . . . . . 15 (𝐹‘((((2 · 𝑚) − 1) + 1) / 2)) ∈ V
105103, 104ifex 4189 . . . . . . . . . . . . . 14 if((((2 · 𝑚) − 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑚) − 1) / 2)), (𝐹‘((((2 · 𝑚) − 1) + 1) / 2))) ∈ V
106102, 26, 105fvmpt 6321 . . . . . . . . . . . . 13 (((2 · 𝑚) − 1) ∈ ℕ → (𝐻‘((2 · 𝑚) − 1)) = if((((2 · 𝑚) − 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑚) − 1) / 2)), (𝐹‘((((2 · 𝑚) − 1) + 1) / 2))))
10795, 106syl 17 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (𝐻‘((2 · 𝑚) − 1)) = if((((2 · 𝑚) − 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑚) − 1) / 2)), (𝐹‘((((2 · 𝑚) − 1) + 1) / 2))))
108 2nn 11223 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℕ
109 nnmulcl 11081 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (2 · 𝑚) ∈ ℕ)
110108, 90, 109sylancr 696 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ ℕ) → (2 · 𝑚) ∈ ℕ)
111110nncnd 11074 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ ℕ) → (2 · 𝑚) ∈ ℂ)
112 ax-1cn 10032 . . . . . . . . . . . . . . . . . 18 1 ∈ ℂ
113 npcan 10328 . . . . . . . . . . . . . . . . . 18 (((2 · 𝑚) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑚) − 1) + 1) = (2 · 𝑚))
114111, 112, 113sylancl 695 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ ℕ) → (((2 · 𝑚) − 1) + 1) = (2 · 𝑚))
115114oveq1d 6705 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ ℕ) → ((((2 · 𝑚) − 1) + 1) / 2) = ((2 · 𝑚) / 2))
116 2cn 11129 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
117 2ne0 11151 . . . . . . . . . . . . . . . . . 18 2 ≠ 0
118 divcan3 10749 . . . . . . . . . . . . . . . . . 18 ((𝑚 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((2 · 𝑚) / 2) = 𝑚)
119116, 117, 118mp3an23 1456 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ ℂ → ((2 · 𝑚) / 2) = 𝑚)
12084, 119syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ ℕ) → ((2 · 𝑚) / 2) = 𝑚)
121115, 120eqtrd 2685 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → ((((2 · 𝑚) − 1) + 1) / 2) = 𝑚)
122121, 90eqeltrd 2730 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → ((((2 · 𝑚) − 1) + 1) / 2) ∈ ℕ)
123 nneo 11499 . . . . . . . . . . . . . . . 16 (((2 · 𝑚) − 1) ∈ ℕ → ((((2 · 𝑚) − 1) / 2) ∈ ℕ ↔ ¬ ((((2 · 𝑚) − 1) + 1) / 2) ∈ ℕ))
12495, 123syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → ((((2 · 𝑚) − 1) / 2) ∈ ℕ ↔ ¬ ((((2 · 𝑚) − 1) + 1) / 2) ∈ ℕ))
125124con2bid 343 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (((((2 · 𝑚) − 1) + 1) / 2) ∈ ℕ ↔ ¬ (((2 · 𝑚) − 1) / 2) ∈ ℕ))
126122, 125mpbid 222 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → ¬ (((2 · 𝑚) − 1) / 2) ∈ ℕ)
127126iffalsed 4130 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → if((((2 · 𝑚) − 1) / 2) ∈ ℕ, (𝐺‘(((2 · 𝑚) − 1) / 2)), (𝐹‘((((2 · 𝑚) − 1) + 1) / 2))) = (𝐹‘((((2 · 𝑚) − 1) + 1) / 2)))
128121fveq2d 6233 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (𝐹‘((((2 · 𝑚) − 1) + 1) / 2)) = (𝐹𝑚))
129107, 127, 1283eqtrd 2689 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝐻‘((2 · 𝑚) − 1)) = (𝐹𝑚))
130 fveq2 6229 . . . . . . . . . . . . 13 (𝑘 = ((2 · 𝑚) − 1) → (𝐻𝑘) = (𝐻‘((2 · 𝑚) − 1)))
131130eqeq1d 2653 . . . . . . . . . . . 12 (𝑘 = ((2 · 𝑚) − 1) → ((𝐻𝑘) = (𝐹𝑚) ↔ (𝐻‘((2 · 𝑚) − 1)) = (𝐹𝑚)))
132131rspcev 3340 . . . . . . . . . . 11 ((((2 · 𝑚) − 1) ∈ ℕ ∧ (𝐻‘((2 · 𝑚) − 1)) = (𝐹𝑚)) → ∃𝑘 ∈ ℕ (𝐻𝑘) = (𝐹𝑚))
13395, 129, 132syl2anc 694 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → ∃𝑘 ∈ ℕ (𝐻𝑘) = (𝐹𝑚))
134 fveq2 6229 . . . . . . . . . . . . . 14 ((𝐻𝑘) = (𝐹𝑚) → (1st ‘(𝐻𝑘)) = (1st ‘(𝐹𝑚)))
135134breq1d 4695 . . . . . . . . . . . . 13 ((𝐻𝑘) = (𝐹𝑚) → ((1st ‘(𝐻𝑘)) < 𝑧 ↔ (1st ‘(𝐹𝑚)) < 𝑧))
136 fveq2 6229 . . . . . . . . . . . . . 14 ((𝐻𝑘) = (𝐹𝑚) → (2nd ‘(𝐻𝑘)) = (2nd ‘(𝐹𝑚)))
137136breq2d 4697 . . . . . . . . . . . . 13 ((𝐻𝑘) = (𝐹𝑚) → (𝑧 < (2nd ‘(𝐻𝑘)) ↔ 𝑧 < (2nd ‘(𝐹𝑚))))
138135, 137anbi12d 747 . . . . . . . . . . . 12 ((𝐻𝑘) = (𝐹𝑚) → (((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘))) ↔ ((1st ‘(𝐹𝑚)) < 𝑧𝑧 < (2nd ‘(𝐹𝑚)))))
139138biimprcd 240 . . . . . . . . . . 11 (((1st ‘(𝐹𝑚)) < 𝑧𝑧 < (2nd ‘(𝐹𝑚))) → ((𝐻𝑘) = (𝐹𝑚) → ((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘)))))
140139reximdv 3045 . . . . . . . . . 10 (((1st ‘(𝐹𝑚)) < 𝑧𝑧 < (2nd ‘(𝐹𝑚))) → (∃𝑘 ∈ ℕ (𝐻𝑘) = (𝐹𝑚) → ∃𝑘 ∈ ℕ ((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘)))))
141133, 140syl5com 31 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (((1st ‘(𝐹𝑚)) < 𝑧𝑧 < (2nd ‘(𝐹𝑚))) → ∃𝑘 ∈ ℕ ((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘)))))
142141rexlimdva 3060 . . . . . . . 8 (𝜑 → (∃𝑚 ∈ ℕ ((1st ‘(𝐹𝑚)) < 𝑧𝑧 < (2nd ‘(𝐹𝑚))) → ∃𝑘 ∈ ℕ ((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘)))))
143142ralimdv 2992 . . . . . . 7 (𝜑 → (∀𝑧𝐴𝑚 ∈ ℕ ((1st ‘(𝐹𝑚)) < 𝑧𝑧 < (2nd ‘(𝐹𝑚))) → ∀𝑧𝐴𝑘 ∈ ℕ ((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘)))))
144 ovolfioo 23282 . . . . . . . 8 ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ran ((,) ∘ 𝐹) ↔ ∀𝑧𝐴𝑚 ∈ ℕ ((1st ‘(𝐹𝑚)) < 𝑧𝑧 < (2nd ‘(𝐹𝑚)))))
1452, 21, 144syl2anc 694 . . . . . . 7 (𝜑 → (𝐴 ran ((,) ∘ 𝐹) ↔ ∀𝑧𝐴𝑚 ∈ ℕ ((1st ‘(𝐹𝑚)) < 𝑧𝑧 < (2nd ‘(𝐹𝑚)))))
146 ovolfioo 23282 . . . . . . . 8 ((𝐴 ⊆ ℝ ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ran ((,) ∘ 𝐻) ↔ ∀𝑧𝐴𝑘 ∈ ℕ ((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘)))))
1472, 27, 146syl2anc 694 . . . . . . 7 (𝜑 → (𝐴 ran ((,) ∘ 𝐻) ↔ ∀𝑧𝐴𝑘 ∈ ℕ ((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘)))))
148143, 145, 1473imtr4d 283 . . . . . 6 (𝜑 → (𝐴 ran ((,) ∘ 𝐹) → 𝐴 ran ((,) ∘ 𝐻)))
14962, 148mpd 15 . . . . 5 (𝜑𝐴 ran ((,) ∘ 𝐻))
150 oveq1 6697 . . . . . . . . . . . . . . . 16 (𝑛 = (2 · 𝑚) → (𝑛 / 2) = ((2 · 𝑚) / 2))
151150eleq1d 2715 . . . . . . . . . . . . . . 15 (𝑛 = (2 · 𝑚) → ((𝑛 / 2) ∈ ℕ ↔ ((2 · 𝑚) / 2) ∈ ℕ))
152150fveq2d 6233 . . . . . . . . . . . . . . 15 (𝑛 = (2 · 𝑚) → (𝐺‘(𝑛 / 2)) = (𝐺‘((2 · 𝑚) / 2)))
153 oveq1 6697 . . . . . . . . . . . . . . . . 17 (𝑛 = (2 · 𝑚) → (𝑛 + 1) = ((2 · 𝑚) + 1))
154153oveq1d 6705 . . . . . . . . . . . . . . . 16 (𝑛 = (2 · 𝑚) → ((𝑛 + 1) / 2) = (((2 · 𝑚) + 1) / 2))
155154fveq2d 6233 . . . . . . . . . . . . . . 15 (𝑛 = (2 · 𝑚) → (𝐹‘((𝑛 + 1) / 2)) = (𝐹‘(((2 · 𝑚) + 1) / 2)))
156151, 152, 155ifbieq12d 4146 . . . . . . . . . . . . . 14 (𝑛 = (2 · 𝑚) → if((𝑛 / 2) ∈ ℕ, (𝐺‘(𝑛 / 2)), (𝐹‘((𝑛 + 1) / 2))) = if(((2 · 𝑚) / 2) ∈ ℕ, (𝐺‘((2 · 𝑚) / 2)), (𝐹‘(((2 · 𝑚) + 1) / 2))))
157 fvex 6239 . . . . . . . . . . . . . . 15 (𝐺‘((2 · 𝑚) / 2)) ∈ V
158 fvex 6239 . . . . . . . . . . . . . . 15 (𝐹‘(((2 · 𝑚) + 1) / 2)) ∈ V
159157, 158ifex 4189 . . . . . . . . . . . . . 14 if(((2 · 𝑚) / 2) ∈ ℕ, (𝐺‘((2 · 𝑚) / 2)), (𝐹‘(((2 · 𝑚) + 1) / 2))) ∈ V
160156, 26, 159fvmpt 6321 . . . . . . . . . . . . 13 ((2 · 𝑚) ∈ ℕ → (𝐻‘(2 · 𝑚)) = if(((2 · 𝑚) / 2) ∈ ℕ, (𝐺‘((2 · 𝑚) / 2)), (𝐹‘(((2 · 𝑚) + 1) / 2))))
161110, 160syl 17 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (𝐻‘(2 · 𝑚)) = if(((2 · 𝑚) / 2) ∈ ℕ, (𝐺‘((2 · 𝑚) / 2)), (𝐹‘(((2 · 𝑚) + 1) / 2))))
162120, 90eqeltrd 2730 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → ((2 · 𝑚) / 2) ∈ ℕ)
163162iftrued 4127 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → if(((2 · 𝑚) / 2) ∈ ℕ, (𝐺‘((2 · 𝑚) / 2)), (𝐹‘(((2 · 𝑚) + 1) / 2))) = (𝐺‘((2 · 𝑚) / 2)))
164120fveq2d 6233 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (𝐺‘((2 · 𝑚) / 2)) = (𝐺𝑚))
165161, 163, 1643eqtrd 2689 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝐻‘(2 · 𝑚)) = (𝐺𝑚))
166 fveq2 6229 . . . . . . . . . . . . 13 (𝑘 = (2 · 𝑚) → (𝐻𝑘) = (𝐻‘(2 · 𝑚)))
167166eqeq1d 2653 . . . . . . . . . . . 12 (𝑘 = (2 · 𝑚) → ((𝐻𝑘) = (𝐺𝑚) ↔ (𝐻‘(2 · 𝑚)) = (𝐺𝑚)))
168167rspcev 3340 . . . . . . . . . . 11 (((2 · 𝑚) ∈ ℕ ∧ (𝐻‘(2 · 𝑚)) = (𝐺𝑚)) → ∃𝑘 ∈ ℕ (𝐻𝑘) = (𝐺𝑚))
169110, 165, 168syl2anc 694 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → ∃𝑘 ∈ ℕ (𝐻𝑘) = (𝐺𝑚))
170 fveq2 6229 . . . . . . . . . . . . . 14 ((𝐻𝑘) = (𝐺𝑚) → (1st ‘(𝐻𝑘)) = (1st ‘(𝐺𝑚)))
171170breq1d 4695 . . . . . . . . . . . . 13 ((𝐻𝑘) = (𝐺𝑚) → ((1st ‘(𝐻𝑘)) < 𝑧 ↔ (1st ‘(𝐺𝑚)) < 𝑧))
172 fveq2 6229 . . . . . . . . . . . . . 14 ((𝐻𝑘) = (𝐺𝑚) → (2nd ‘(𝐻𝑘)) = (2nd ‘(𝐺𝑚)))
173172breq2d 4697 . . . . . . . . . . . . 13 ((𝐻𝑘) = (𝐺𝑚) → (𝑧 < (2nd ‘(𝐻𝑘)) ↔ 𝑧 < (2nd ‘(𝐺𝑚))))
174171, 173anbi12d 747 . . . . . . . . . . . 12 ((𝐻𝑘) = (𝐺𝑚) → (((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘))) ↔ ((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚)))))
175174biimprcd 240 . . . . . . . . . . 11 (((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚))) → ((𝐻𝑘) = (𝐺𝑚) → ((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘)))))
176175reximdv 3045 . . . . . . . . . 10 (((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚))) → (∃𝑘 ∈ ℕ (𝐻𝑘) = (𝐺𝑚) → ∃𝑘 ∈ ℕ ((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘)))))
177169, 176syl5com 31 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ) → (((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚))) → ∃𝑘 ∈ ℕ ((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘)))))
178177rexlimdva 3060 . . . . . . . 8 (𝜑 → (∃𝑚 ∈ ℕ ((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚))) → ∃𝑘 ∈ ℕ ((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘)))))
179178ralimdv 2992 . . . . . . 7 (𝜑 → (∀𝑧𝐵𝑚 ∈ ℕ ((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚))) → ∀𝑧𝐵𝑘 ∈ ℕ ((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘)))))
180 ovolfioo 23282 . . . . . . . 8 ((𝐵 ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐵 ran ((,) ∘ 𝐺) ↔ ∀𝑧𝐵𝑚 ∈ ℕ ((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚)))))
1814, 12, 180syl2anc 694 . . . . . . 7 (𝜑 → (𝐵 ran ((,) ∘ 𝐺) ↔ ∀𝑧𝐵𝑚 ∈ ℕ ((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚)))))
182 ovolfioo 23282 . . . . . . . 8 ((𝐵 ⊆ ℝ ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐵 ran ((,) ∘ 𝐻) ↔ ∀𝑧𝐵𝑘 ∈ ℕ ((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘)))))
1834, 27, 182syl2anc 694 . . . . . . 7 (𝜑 → (𝐵 ran ((,) ∘ 𝐻) ↔ ∀𝑧𝐵𝑘 ∈ ℕ ((1st ‘(𝐻𝑘)) < 𝑧𝑧 < (2nd ‘(𝐻𝑘)))))
184179, 181, 1833imtr4d 283 . . . . . 6 (𝜑 → (𝐵 ran ((,) ∘ 𝐺) → 𝐵 ran ((,) ∘ 𝐻)))
18564, 184mpd 15 . . . . 5 (𝜑𝐵 ran ((,) ∘ 𝐻))
186149, 185unssd 3822 . . . 4 (𝜑 → (𝐴𝐵) ⊆ ran ((,) ∘ 𝐻))
18729ovollb 23293 . . . 4 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐴𝐵) ⊆ ran ((,) ∘ 𝐻)) → (vol*‘(𝐴𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
18827, 186, 187syl2anc 694 . . 3 (𝜑 → (vol*‘(𝐴𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
189 ovollecl 23297 . . 3 (((𝐴𝐵) ⊆ ℝ ∧ sup(ran 𝑈, ℝ*, < ) ∈ ℝ ∧ (vol*‘(𝐴𝐵)) ≤ sup(ran 𝑈, ℝ*, < )) → (vol*‘(𝐴𝐵)) ∈ ℝ)
1905, 82, 188, 189syl3anc 1366 . 2 (𝜑 → (vol*‘(𝐴𝐵)) ∈ ℝ)
19159rexrd 10127 . . . 4 (𝜑 → (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ*)
192 supxrleub 12194 . . . 4 ((ran 𝑈 ⊆ ℝ* ∧ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ∈ ℝ*) → (sup(ran 𝑈, ℝ*, < ) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ↔ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)))
19377, 191, 192syl2anc 694 . . 3 (𝜑 → (sup(ran 𝑈, ℝ*, < ) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶) ↔ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶)))
19471, 193mpbird 247 . 2 (𝜑 → sup(ran 𝑈, ℝ*, < ) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
195190, 82, 59, 188, 194letrd 10232 1 (𝜑 → (vol*‘(𝐴𝐵)) ≤ (((vol*‘𝐴) + (vol*‘𝐵)) + 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  cun 3605  cin 3606  wss 3607  c0 3948  ifcif 4119   cuni 4468   class class class wbr 4685  cmpt 4762   × cxp 5141  dom cdm 5143  ran crn 5144  ccom 5147   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  1st c1st 7208  2nd c2nd 7209  𝑚 cmap 7899  supcsup 8387  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  +∞cpnf 10109  *cxr 10111   < clt 10112  cle 10113  cmin 10304   / cdiv 10722  cn 11058  2c2 11108  0cn0 11330  cz 11415  cuz 11725  +crp 11870  (,)cioo 12213  [,)cico 12215  seqcseq 12841  abscabs 14018  vol*covol 23277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-sup 8389  df-inf 8390  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-ioo 12217  df-ico 12219  df-fz 12365  df-fl 12633  df-seq 12842  df-exp 12901  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-ovol 23279
This theorem is referenced by:  ovolunlem2  23312
  Copyright terms: Public domain W3C validator