Metamath Proof Explorer

Theorem ovolscalem2

Description: Lemma for ovolshft . (Contributed by Mario Carneiro, 22-Mar-2014)

Ref Expression
Hypotheses ovolsca.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
ovolsca.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
ovolsca.3 ⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝐶 · 𝑥 ) ∈ 𝐴 } )
ovolsca.4 ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) ∈ ℝ )
Assertion ovolscalem2 ( 𝜑 → ( vol* ‘ 𝐵 ) ≤ ( ( vol* ‘ 𝐴 ) / 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ovolsca.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 ovolsca.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
3 ovolsca.3 ⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝐶 · 𝑥 ) ∈ 𝐴 } )
4 ovolsca.4 ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) ∈ ℝ )
5 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐴 ⊆ ℝ )
6 4 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
7 rpmulcl ⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) → ( 𝐶 · 𝑦 ) ∈ ℝ+ )
8 2 7 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝐶 · 𝑦 ) ∈ ℝ+ )
9 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) )
10 9 ovolgelb ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐶 · 𝑦 ) ∈ ℝ+ ) → ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑦 ) ) ) )
11 5 6 8 10 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑦 ) ) ) )
12 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑦 ) ) ) ) ) → 𝐴 ⊆ ℝ )
13 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑦 ) ) ) ) ) → 𝐶 ∈ ℝ+ )
14 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑦 ) ) ) ) ) → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝐶 · 𝑥 ) ∈ 𝐴 } )
15 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑦 ) ) ) ) ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
16 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) = ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) )
17 16 oveq1d ⊢ ( 𝑚 = 𝑛 → ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) / 𝐶 ) = ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) / 𝐶 ) )
18 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) = ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) )
19 18 oveq1d ⊢ ( 𝑚 = 𝑛 → ( ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) / 𝐶 ) = ( ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) / 𝐶 ) )
20 17 19 opeq12d ⊢ ( 𝑚 = 𝑛 → ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) / 𝐶 ) , ( ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) / 𝐶 ) ⟩ = ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) / 𝐶 ) ⟩ )
21 20 cbvmptv ⊢ ( 𝑚 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) / 𝐶 ) , ( ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) / 𝐶 ) ⟩ ) = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝑓 ‘ 𝑛 ) ) / 𝐶 ) , ( ( 2nd ‘ ( 𝑓 ‘ 𝑛 ) ) / 𝐶 ) ⟩ )
22 elmapi ⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
23 22 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑦 ) ) ) ) ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
24 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑦 ) ) ) ) ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) )
25 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑦 ) ) ) ) ) → 𝑦 ∈ ℝ+ )
26 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑦 ) ) ) ) ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑦 ) ) )
27 12 13 14 15 9 21 23 24 25 26 ovolscalem1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 · 𝑦 ) ) ) ) ) → ( vol* ‘ 𝐵 ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑦 ) )
28 11 27 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( vol* ‘ 𝐵 ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑦 ) )
29 28 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ( vol* ‘ 𝐵 ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑦 ) )
30 ssrab2 ⊢ { 𝑥 ∈ ℝ ∣ ( 𝐶 · 𝑥 ) ∈ 𝐴 } ⊆ ℝ
31 3 30 eqsstrdi ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
32 ovolcl ⊢ ( 𝐵 ⊆ ℝ → ( vol* ‘ 𝐵 ) ∈ ℝ* )
33 31 32 syl ⊢ ( 𝜑 → ( vol* ‘ 𝐵 ) ∈ ℝ* )
34 4 2 rerpdivcld ⊢ ( 𝜑 → ( ( vol* ‘ 𝐴 ) / 𝐶 ) ∈ ℝ )
35 xralrple ⊢ ( ( ( vol* ‘ 𝐵 ) ∈ ℝ* ∧ ( ( vol* ‘ 𝐴 ) / 𝐶 ) ∈ ℝ ) → ( ( vol* ‘ 𝐵 ) ≤ ( ( vol* ‘ 𝐴 ) / 𝐶 ) ↔ ∀ 𝑦 ∈ ℝ+ ( vol* ‘ 𝐵 ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑦 ) ) )
36 33 34 35 syl2anc ⊢ ( 𝜑 → ( ( vol* ‘ 𝐵 ) ≤ ( ( vol* ‘ 𝐴 ) / 𝐶 ) ↔ ∀ 𝑦 ∈ ℝ+ ( vol* ‘ 𝐵 ) ≤ ( ( ( vol* ‘ 𝐴 ) / 𝐶 ) + 𝑦 ) ) )
37 29 36 mpbird ⊢ ( 𝜑 → ( vol* ‘ 𝐵 ) ≤ ( ( vol* ‘ 𝐴 ) / 𝐶 ) )