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	bitrid	⊢ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_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* ‘ 𝐴 ) + 𝐵 ) ) )

Metamath Proof Explorer

Theorem ovolgelb

Proof