Metamath Proof Explorer

Theorem ovolgelb

Description: The outer volume is the greatest lower bound on the sum of all interval coverings of A . (Contributed by Mario Carneiro, 15-Jun-2014)

Ref Expression
Hypothesis ovolgelb.1 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) )
Assertion ovolgelb ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ovolgelb.1 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) )
2 simp2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
3 simp3 ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℝ+ )
4 2 3 ltaddrpd ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( vol* ‘ 𝐴 ) < ( ( vol* ‘ 𝐴 ) + 𝐵 ) )
5 3 rpred ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
6 2 5 readdcld ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ∈ ℝ )
7 2 6 ltnled ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( vol* ‘ 𝐴 ) < ( ( vol* ‘ 𝐴 ) + 𝐵 ) ↔ ¬ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ ( vol* ‘ 𝐴 ) ) )
8 4 7 mpbid ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ¬ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ ( vol* ‘ 𝐴 ) )
9 eqid ⊢ { 𝑦 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } = { 𝑦 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) }
10 9 ovolval ⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) = inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } , ℝ* , < ) )
11 10 3ad2ant1 ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( vol* ‘ 𝐴 ) = inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } , ℝ* , < ) )
12 11 breq2d ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ ( vol* ‘ 𝐴 ) ↔ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } , ℝ* , < ) ) )
13 ssrab2 ⊢ { 𝑦 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } ⊆ ℝ*
14 6 rexrd ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ∈ ℝ* )
15 infxrgelb ⊢ ( ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } ⊆ ℝ* ∧ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ∈ ℝ* ) → ( ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } , ℝ* , < ) ↔ ∀ 𝑥 ∈ { 𝑦 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) )
16 13 14 15 sylancr ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } , ℝ* , < ) ↔ ∀ 𝑥 ∈ { 𝑦 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) )
17 eqeq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ↔ 𝑥 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) )
18 1 rneqi ⊢ ran 𝑆 = ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) )
19 18 supeq1i ⊢ sup ( ran 𝑆 , ℝ* , < ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < )
20 19 eqeq2i ⊢ ( 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ↔ 𝑥 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) )
21 17 20 bitr4di ⊢ ( 𝑦 = 𝑥 → ( 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ↔ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) )
22 21 anbi2d ⊢ ( 𝑦 = 𝑥 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) ) )
23 22 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) ↔ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) ) )
24 23 ralrab ⊢ ( ∀ 𝑥 ∈ { 𝑦 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ↔ ∀ 𝑥 ∈ ℝ* ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) )
25 ralcom ⊢ ( ∀ 𝑥 ∈ ℝ* ∀ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ↔ ∀ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∀ 𝑥 ∈ ℝ* ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) )
26 r19.23v ⊢ ( ∀ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ↔ ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) )
27 26 ralbii ⊢ ( ∀ 𝑥 ∈ ℝ* ∀ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ* ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) )
28 ancomst ⊢ ( ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ↔ ( ( 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) )
29 impexp ⊢ ( ( ( 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ↔ ( 𝑥 = sup ( ran 𝑆 , ℝ* , < ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ) )
30 28 29 bitri ⊢ ( ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ↔ ( 𝑥 = sup ( ran 𝑆 , ℝ* , < ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ) )
31 30 ralbii ⊢ ( ∀ 𝑥 ∈ ℝ* ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ* ( 𝑥 = sup ( ran 𝑆 , ℝ* , < ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ) )
32 elovolmlem ⊢ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ↔ 𝑔 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
33 eqid ⊢ ( ( abs ∘ − ) ∘ 𝑔 ) = ( ( abs ∘ − ) ∘ 𝑔 )
34 33 1 ovolsf ⊢ ( 𝑔 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
35 32 34 sylbi ⊢ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )
36 35 frnd ⊢ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ran 𝑆 ⊆ ( 0 [,) +∞ ) )
37 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
38 36 37 sstrdi ⊢ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ran 𝑆 ⊆ ℝ* )
39 supxrcl ⊢ ( ran 𝑆 ⊆ ℝ* → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* )
40 38 39 syl ⊢ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* )
41 breq2 ⊢ ( 𝑥 = sup ( ran 𝑆 , ℝ* , < ) → ( ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ↔ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) )
42 41 imbi2d ⊢ ( 𝑥 = sup ( ran 𝑆 , ℝ* , < ) → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) ) )
43 42 ceqsralv ⊢ ( sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* → ( ∀ 𝑥 ∈ ℝ* ( 𝑥 = sup ( ran 𝑆 , ℝ* , < ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) ) )
44 40 43 syl ⊢ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( ∀ 𝑥 ∈ ℝ* ( 𝑥 = sup ( ran 𝑆 , ℝ* , < ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) ) )
45 31 44 syl5bb ⊢ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) → ( ∀ 𝑥 ∈ ℝ* ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) ) )
46 45 ralbiia ⊢ ( ∀ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∀ 𝑥 ∈ ℝ* ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ↔ ∀ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) )
47 25 27 46 3bitr3i ⊢ ( ∀ 𝑥 ∈ ℝ* ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑥 = sup ( ran 𝑆 , ℝ* , < ) ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ) ↔ ∀ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) )
48 24 47 bitri ⊢ ( ∀ 𝑥 ∈ { 𝑦 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ 𝑥 ↔ ∀ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) )
49 16 48 bitr2di ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ∀ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) ↔ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } , ℝ* , < ) ) )
50 12 49 bitr4d ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ ( vol* ‘ 𝐴 ) ↔ ∀ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) ) )
51 8 50 mtbid ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ¬ ∀ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) )
52 rexanali ⊢ ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ ¬ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) ↔ ¬ ∀ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) → ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) )
53 51 52 sylibr ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ ¬ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) )
54 xrltnle ⊢ ( ( sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* ∧ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ∈ ℝ* ) → ( sup ( ran 𝑆 , ℝ* , < ) < ( ( vol* ‘ 𝐴 ) + 𝐵 ) ↔ ¬ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) )
55 xrltle ⊢ ( ( sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* ∧ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ∈ ℝ* ) → ( sup ( ran 𝑆 , ℝ* , < ) < ( ( vol* ‘ 𝐴 ) + 𝐵 ) → sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ) )
56 54 55 sylbird ⊢ ( ( sup ( ran 𝑆 , ℝ* , < ) ∈ ℝ* ∧ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ∈ ℝ* ) → ( ¬ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) → sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ) )
57 40 14 56 syl2anr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) → ( ¬ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) → sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ) )
58 57 anim2d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ ¬ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ) ) )
59 58 reximdva ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ ¬ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ≤ sup ( ran 𝑆 , ℝ* , < ) ) → ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ) ) )
60 53 59 mpd ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ sup ( ran 𝑆 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐴 ) + 𝐵 ) ) )