Metamath Proof Explorer

Theorem ovolunlem2

Description: Lemma for ovolun . (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Hypotheses ovolun.a ⊢ ( 𝜑 → ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) )
ovolun.b ⊢ ( 𝜑 → ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) )
ovolun.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
Assertion ovolunlem2 ( 𝜑 → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ovolun.a ⊢ ( 𝜑 → ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) )
2 ovolun.b ⊢ ( 𝜑 → ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) )
3 ovolun.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
4 1 simpld ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
5 1 simprd ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) ∈ ℝ )
6 3 rphalfcld ⊢ ( 𝜑 → ( 𝐶 / 2 ) ∈ ℝ+ )
7 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) )
8 7 ovolgelb ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐶 / 2 ) ∈ ℝ+ ) → ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) )
9 4 5 6 8 syl3anc ⊢ ( 𝜑 → ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) )
10 2 simpld ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
11 2 simprd ⊢ ( 𝜑 → ( vol* ‘ 𝐵 ) ∈ ℝ )
12 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) )
13 12 ovolgelb ⊢ ( ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ∧ ( 𝐶 / 2 ) ∈ ℝ+ ) → ∃ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) )
14 10 11 6 13 syl3anc ⊢ ( 𝜑 → ∃ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) )
15 reeanv ⊢ ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∃ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ∧ ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) ↔ ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ∧ ∃ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) )
16 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ∧ ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) ) → ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) )
17 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ∧ ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) ) → ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) )
18 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ∧ ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) ) → 𝐶 ∈ ℝ+ )
19 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑛 ∈ ℕ ↦ if ( ( 𝑛 / 2 ) ∈ ℕ , ( ℎ ‘ ( 𝑛 / 2 ) ) , ( 𝑔 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) ) ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ ( 𝑛 ∈ ℕ ↦ if ( ( 𝑛 / 2 ) ∈ ℕ , ( ℎ ‘ ( 𝑛 / 2 ) ) , ( 𝑔 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) ) ) )
20 simp2l ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ∧ ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) ) → 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) )
21 simp3ll ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ∧ ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) )
22 simp3lr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ∧ ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) )
23 simp2r ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ∧ ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) ) → ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) )
24 simp3rl ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ∧ ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) ) → 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) )
25 simp3rr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ∧ ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) )
26 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( ( 𝑛 / 2 ) ∈ ℕ , ( ℎ ‘ ( 𝑛 / 2 ) ) , ( 𝑔 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ if ( ( 𝑛 / 2 ) ∈ ℕ , ( ℎ ‘ ( 𝑛 / 2 ) ) , ( 𝑔 ‘ ( ( 𝑛 + 1 ) / 2 ) ) ) )
27 16 17 18 7 12 19 20 21 22 23 24 25 26 ovolunlem1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ∧ ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) )
28 27 3exp ⊢ ( 𝜑 → ( ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) → ( ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ∧ ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ) ) )
29 28 rexlimdvv ⊢ ( 𝜑 → ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∃ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ∧ ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ) )
30 15 29 syl5bir ⊢ ( 𝜑 → ( ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + ( 𝐶 / 2 ) ) ) ∧ ∃ ℎ ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ ℎ ) ∧ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ ℎ ) ) , ℝ* , < ) ≤ ( ( vol* ‘ 𝐵 ) + ( 𝐶 / 2 ) ) ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) ) )
31 9 14 30 mp2and ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝐶 ) )