Metamath Proof Explorer

Theorem ioorcl2

Description: An open interval with finite volume has real endpoints. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Assertion ioorcl2 ( ( ( 𝐴 (,) 𝐵 ) ≠ ∅ ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( ( 𝐴 (,) 𝐵 ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( 𝐴 (,) 𝐵 ) )
2 elioore ⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) → 𝑧 ∈ ℝ )
3 2 adantr ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 𝑧 ∈ ℝ )
4 peano2re ⊢ ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ → ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ∈ ℝ )
5 4 adantl ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ∈ ℝ )
6 3 5 resubcld ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ∈ ℝ )
7 6 rexrd ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ∈ ℝ* )
8 eliooxr ⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
9 8 adantr ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
10 9 simpld ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 𝐴 ∈ ℝ* )
11 3 rexrd ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 𝑧 ∈ ℝ* )
12 ltp1 ⊢ ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ → ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) < ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) )
13 12 adantl ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) < ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) )
14 0red ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 0 ∈ ℝ )
15 simpr ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ )
16 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
17 ovolge0 ⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ ℝ → 0 ≤ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) )
18 16 17 mp1i ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 0 ≤ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) )
19 lep1 ⊢ ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ → ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ≤ ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) )
20 19 adantl ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ≤ ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) )
21 14 15 5 18 20 letrd ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 0 ≤ ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) )
22 3 5 subge02d ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 0 ≤ ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ↔ ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ≤ 𝑧 ) )
23 21 22 mpbid ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ≤ 𝑧 )
24 ovolioo ⊢ ( ( ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ≤ 𝑧 ) → ( vol* ‘ ( ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) (,) 𝑧 ) ) = ( 𝑧 − ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) )
25 6 3 23 24 syl3anc ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( vol* ‘ ( ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) (,) 𝑧 ) ) = ( 𝑧 − ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) )
26 3 recnd ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 𝑧 ∈ ℂ )
27 5 recnd ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ∈ ℂ )
28 26 27 nncand ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝑧 − ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) = ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) )
29 25 28 eqtrd ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( vol* ‘ ( ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) (,) 𝑧 ) ) = ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) )
30 29 adantr ⊢ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) ∧ 𝐴 ≤ ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) → ( vol* ‘ ( ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) (,) 𝑧 ) ) = ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) )
31 iooss1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) → ( ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) (,) 𝑧 ) ⊆ ( 𝐴 (,) 𝑧 ) )
32 10 31 sylan ⊢ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) ∧ 𝐴 ≤ ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) → ( ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) (,) 𝑧 ) ⊆ ( 𝐴 (,) 𝑧 ) )
33 9 simprd ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 𝐵 ∈ ℝ* )
34 eliooord ⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝑧 ∧ 𝑧 < 𝐵 ) )
35 34 adantr ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝐴 < 𝑧 ∧ 𝑧 < 𝐵 ) )
36 35 simprd ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 𝑧 < 𝐵 )
37 11 33 36 xrltled ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 𝑧 ≤ 𝐵 )
38 iooss2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑧 ≤ 𝐵 ) → ( 𝐴 (,) 𝑧 ) ⊆ ( 𝐴 (,) 𝐵 ) )
39 33 37 38 syl2anc ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝐴 (,) 𝑧 ) ⊆ ( 𝐴 (,) 𝐵 ) )
40 39 adantr ⊢ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) ∧ 𝐴 ≤ ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) → ( 𝐴 (,) 𝑧 ) ⊆ ( 𝐴 (,) 𝐵 ) )
41 32 40 sstrd ⊢ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) ∧ 𝐴 ≤ ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) → ( ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) (,) 𝑧 ) ⊆ ( 𝐴 (,) 𝐵 ) )
42 ovolss ⊢ ( ( ( ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) (,) 𝑧 ) ⊆ ( 𝐴 (,) 𝐵 ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) → ( vol* ‘ ( ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) (,) 𝑧 ) ) ≤ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) )
43 41 16 42 sylancl ⊢ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) ∧ 𝐴 ≤ ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) → ( vol* ‘ ( ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) (,) 𝑧 ) ) ≤ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) )
44 30 43 eqbrtrrd ⊢ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) ∧ 𝐴 ≤ ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) → ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ≤ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) )
45 44 ex ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝐴 ≤ ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) → ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ≤ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ) )
46 10 7 xrlenltd ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝐴 ≤ ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ↔ ¬ ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) < 𝐴 ) )
47 5 15 lenltd ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ≤ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ↔ ¬ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) < ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) )
48 45 46 47 3imtr3d ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( ¬ ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) < 𝐴 → ¬ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) < ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) )
49 13 48 mt4d ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) < 𝐴 )
50 35 simpld ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 𝐴 < 𝑧 )
51 xrre2 ⊢ ( ( ( ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 − ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) < 𝐴 ∧ 𝐴 < 𝑧 ) ) → 𝐴 ∈ ℝ )
52 7 10 11 49 50 51 syl32anc ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 𝐴 ∈ ℝ )
53 3 5 readdcld ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ∈ ℝ )
54 53 rexrd ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ∈ ℝ* )
55 3 5 addge01d ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 0 ≤ ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ↔ 𝑧 ≤ ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) )
56 21 55 mpbid ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 𝑧 ≤ ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) )
57 ovolioo ⊢ ( ( 𝑧 ∈ ℝ ∧ ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ∈ ℝ ∧ 𝑧 ≤ ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) → ( vol* ‘ ( 𝑧 (,) ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) ) = ( ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) − 𝑧 ) )
58 3 53 56 57 syl3anc ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( vol* ‘ ( 𝑧 (,) ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) ) = ( ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) − 𝑧 ) )
59 26 27 pncan2d ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) − 𝑧 ) = ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) )
60 58 59 eqtrd ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( vol* ‘ ( 𝑧 (,) ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) ) = ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) )
61 60 adantr ⊢ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) ∧ ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ≤ 𝐵 ) → ( vol* ‘ ( 𝑧 (,) ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) ) = ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) )
62 iooss2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ≤ 𝐵 ) → ( 𝑧 (,) ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) ⊆ ( 𝑧 (,) 𝐵 ) )
63 33 62 sylan ⊢ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) ∧ ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ≤ 𝐵 ) → ( 𝑧 (,) ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) ⊆ ( 𝑧 (,) 𝐵 ) )
64 10 11 50 xrltled ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 𝐴 ≤ 𝑧 )
65 iooss1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝑧 ) → ( 𝑧 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
66 10 64 65 syl2anc ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝑧 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
67 66 adantr ⊢ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) ∧ ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ≤ 𝐵 ) → ( 𝑧 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
68 63 67 sstrd ⊢ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) ∧ ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ≤ 𝐵 ) → ( 𝑧 (,) ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) ⊆ ( 𝐴 (,) 𝐵 ) )
69 ovolss ⊢ ( ( ( 𝑧 (,) ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) ⊆ ( 𝐴 (,) 𝐵 ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) → ( vol* ‘ ( 𝑧 (,) ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) ) ≤ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) )
70 68 16 69 sylancl ⊢ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) ∧ ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ≤ 𝐵 ) → ( vol* ‘ ( 𝑧 (,) ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) ) ≤ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) )
71 61 70 eqbrtrrd ⊢ ( ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) ∧ ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ≤ 𝐵 ) → ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ≤ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) )
72 71 ex ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ≤ 𝐵 → ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ≤ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ) )
73 54 33 xrlenltd ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ≤ 𝐵 ↔ ¬ 𝐵 < ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) )
74 72 73 47 3imtr3d ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( ¬ 𝐵 < ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) → ¬ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) < ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) )
75 13 74 mt4d ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 𝐵 < ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) )
76 xrre2 ⊢ ( ( ( 𝑧 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ∈ ℝ* ) ∧ ( 𝑧 < 𝐵 ∧ 𝐵 < ( 𝑧 + ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) + 1 ) ) ) ) → 𝐵 ∈ ℝ )
77 11 33 54 36 75 76 syl32anc ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → 𝐵 ∈ ℝ )
78 52 77 jca ⊢ ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
79 78 ex ⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) → ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )
80 79 exlimiv ⊢ ( ∃ 𝑧 𝑧 ∈ ( 𝐴 (,) 𝐵 ) → ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )
81 1 80 sylbi ⊢ ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → ( ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) )
82 81 imp ⊢ ( ( ( 𝐴 (,) 𝐵 ) ≠ ∅ ∧ ( vol* ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )