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* ‘ 𝐴 ) / 𝐶 ) )