Metamath Proof Explorer

Theorem ovollb2

Description: It is often more convenient to do calculations with *closed* coverings rather than open ones; here we show that it makes no difference (compare ovollb ). (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypothesis ovollb2.1 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
Assertion ovollb2 ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) → ( vol* ‘ 𝐴 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 ovollb2.1 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
2 simpr ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) → 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) )
3 ovolficcss ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∪ ran ( [,] ∘ 𝐹 ) ⊆ ℝ )
4 3 adantr ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) → ∪ ran ( [,] ∘ 𝐹 ) ⊆ ℝ )
5 2 4 sstrd ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) → 𝐴 ⊆ ℝ )
6 ovolcl ⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) ∈ ℝ* )
7 5 6 syl ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) → ( vol* ‘ 𝐴 ) ∈ ℝ* )
8 7 adantr ⊢ ( ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ∧ sup ( ran 𝑆 , ℝ* , < ) = +∞ ) → ( vol* ‘ 𝐴 ) ∈ ℝ* )
9 pnfge ⊢ ( ( vol* ‘ 𝐴 ) ∈ ℝ* → ( vol* ‘ 𝐴 ) ≤ +∞ )
10 8 9 syl ⊢ ( ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ∧ sup ( ran 𝑆 , ℝ* , < ) = +∞ ) → ( vol* ‘ 𝐴 ) ≤ +∞ )
11 simpr ⊢ ( ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ∧ sup ( ran 𝑆 , ℝ* , < ) = +∞ ) → sup ( ran 𝑆 , ℝ* , < ) = +∞ )
12 10 11 breqtrrd ⊢ ( ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ∧ sup ( ran 𝑆 , ℝ* , < ) = +∞ ) → ( vol* ‘ 𝐴 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
13 eqid ⊢ ( ( abs ∘ − ) ∘ 𝐹 ) = ( ( abs ∘ − ) ∘ 𝐹 )
14 13 1 ovolsf ⊢ ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
15 14 adantr ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
16 15 frnd ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) → ran 𝑆 ⊆ ( 0 [,) +∞ ) )
17 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
18 16 17 sstrdi ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) → ran 𝑆 ⊆ ℝ )
19 1nn ⊢ 1 ∈ ℕ
20 15 fdmd ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) → dom 𝑆 = ℕ )
21 19 20 eleqtrrid ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) → 1 ∈ dom 𝑆 )
22 21 ne0d ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) → dom 𝑆 ≠ ∅ )
23 dm0rn0 ⊢ ( dom 𝑆 = ∅ ↔ ran 𝑆 = ∅ )
24 23 necon3bii ⊢ ( dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅ )
25 22 24 sylib ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) → ran 𝑆 ≠ ∅ )
26 supxrre2 ⊢ ( ( ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ) → ( sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ↔ sup ( ran 𝑆 , ℝ* , < ) ≠ +∞ ) )
27 18 25 26 syl2anc ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) → ( sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ↔ sup ( ran 𝑆 , ℝ* , < ) ≠ +∞ ) )
28 27 biimpar ⊢ ( ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ∧ sup ( ran 𝑆 , ℝ* , < ) ≠ +∞ ) → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ )
29 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) = ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) )
30 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 2 ↑ 𝑚 ) = ( 2 ↑ 𝑛 ) )
31 30 oveq2d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑚 ) ) = ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑛 ) ) )
32 29 31 oveq12d ⊢ ( 𝑚 = 𝑛 → ( ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑚 ) ) ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑛 ) ) ) )
33 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) = ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) )
34 33 31 oveq12d ⊢ ( 𝑚 = 𝑛 → ( ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑚 ) ) ) = ( ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑛 ) ) ) )
35 32 34 opeq12d ⊢ ( 𝑚 = 𝑛 → ⟨ ( ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ = ⟨ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ⟩ )
36 35 cbvmptv ⊢ ( 𝑚 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ ) = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) − ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑛 ) ) ) , ( ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) + ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑛 ) ) ) ⟩ )
37 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑚 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ ) ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑚 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝐹 ‘ 𝑚 ) ) − ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑚 ) ) ) , ( ( 2nd ‘ ( 𝐹 ‘ 𝑚 ) ) + ( ( 𝑥 / 2 ) / ( 2 ↑ 𝑚 ) ) ) ⟩ ) ) )
38 simplll ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ∧ sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
39 simpllr ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ∧ sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) )
40 simpr ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ∧ sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
41 simplr ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ∧ sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ )
42 1 36 37 38 39 40 41 ovollb2lem ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ∧ sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( vol* ‘ 𝐴 ) ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝑥 ) )
43 42 ralrimiva ⊢ ( ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ∧ sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ) → ∀ 𝑥 ∈ ℝ+ ( vol* ‘ 𝐴 ) ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝑥 ) )
44 xralrple ⊢ ( ( ( vol* ‘ 𝐴 ) ∈ ℝ* ∧ sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ) → ( ( vol* ‘ 𝐴 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ↔ ∀ 𝑥 ∈ ℝ+ ( vol* ‘ 𝐴 ) ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝑥 ) ) )
45 7 44 sylan ⊢ ( ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ∧ sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ) → ( ( vol* ‘ 𝐴 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ↔ ∀ 𝑥 ∈ ℝ+ ( vol* ‘ 𝐴 ) ≤ ( sup ( ran 𝑆 , ℝ* , < ) + 𝑥 ) ) )
46 43 45 mpbird ⊢ ( ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ∧ sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ ) → ( vol* ‘ 𝐴 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
47 28 46 syldan ⊢ ( ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) ∧ sup ( ran 𝑆 , ℝ* , < ) ≠ +∞ ) → ( vol* ‘ 𝐴 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )
48 12 47 pm2.61dane ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( [,] ∘ 𝐹 ) ) → ( vol* ‘ 𝐴 ) ≤ sup ( ran 𝑆 , ℝ* , < ) )