Metamath Proof Explorer

Theorem ovolicopnf

Description: The measure of a right-unbounded interval. (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Assertion ovolicopnf ( 𝐴 ∈ ℝ → ( vol* ‘ ( 𝐴 [,) +∞ ) ) = +∞ )

Proof

Step Hyp Ref Expression
1 pnfxr ⊢ +∞ ∈ ℝ*
2 icossre ⊢ ( ( 𝐴 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 𝐴 [,) +∞ ) ⊆ ℝ )
3 1 2 mpan2 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 [,) +∞ ) ⊆ ℝ )
4 3 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( 𝐴 [,) +∞ ) ⊆ ℝ )
5 ovolge0 ⊢ ( ( 𝐴 [,) +∞ ) ⊆ ℝ → 0 ≤ ( vol* ‘ ( 𝐴 [,) +∞ ) ) )
6 4 5 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → 0 ≤ ( vol* ‘ ( 𝐴 [,) +∞ ) ) )
7 mnflt0 ⊢ -∞ < 0
8 mnfxr ⊢ -∞ ∈ ℝ*
9 0xr ⊢ 0 ∈ ℝ*
10 ovolcl ⊢ ( ( 𝐴 [,) +∞ ) ⊆ ℝ → ( vol* ‘ ( 𝐴 [,) +∞ ) ) ∈ ℝ* )
11 3 10 syl ⊢ ( 𝐴 ∈ ℝ → ( vol* ‘ ( 𝐴 [,) +∞ ) ) ∈ ℝ* )
12 11 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( vol* ‘ ( 𝐴 [,) +∞ ) ) ∈ ℝ* )
13 xrltletr ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) ∈ ℝ* ) → ( ( -∞ < 0 ∧ 0 ≤ ( vol* ‘ ( 𝐴 [,) +∞ ) ) ) → -∞ < ( vol* ‘ ( 𝐴 [,) +∞ ) ) ) )
14 8 9 12 13 mp3an12i ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( ( -∞ < 0 ∧ 0 ≤ ( vol* ‘ ( 𝐴 [,) +∞ ) ) ) → -∞ < ( vol* ‘ ( 𝐴 [,) +∞ ) ) ) )
15 7 14 mpani ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( 0 ≤ ( vol* ‘ ( 𝐴 [,) +∞ ) ) → -∞ < ( vol* ‘ ( 𝐴 [,) +∞ ) ) ) )
16 6 15 mpd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → -∞ < ( vol* ‘ ( 𝐴 [,) +∞ ) ) )
17 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ )
18 xrrebnd ⊢ ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) ∈ ℝ* → ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) ∈ ℝ ↔ ( -∞ < ( vol* ‘ ( 𝐴 [,) +∞ ) ) ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) ) )
19 12 18 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) ∈ ℝ ↔ ( -∞ < ( vol* ‘ ( 𝐴 [,) +∞ ) ) ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) ) )
20 16 17 19 mpbir2and ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( vol* ‘ ( 𝐴 [,) +∞ ) ) ∈ ℝ )
21 20 ltp1d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( vol* ‘ ( 𝐴 [,) +∞ ) ) < ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) )
22 peano2re ⊢ ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) ∈ ℝ → ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) ∈ ℝ )
23 20 22 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) ∈ ℝ )
24 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → 𝐴 ∈ ℝ )
25 23 24 readdcld ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ∈ ℝ )
26 0red ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → 0 ∈ ℝ )
27 20 lep1d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( vol* ‘ ( 𝐴 [,) +∞ ) ) ≤ ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) )
28 26 20 23 6 27 letrd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → 0 ≤ ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) )
29 24 23 addge02d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( 0 ≤ ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) ↔ 𝐴 ≤ ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) )
30 28 29 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → 𝐴 ≤ ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) )
31 ovolicc ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ∈ ℝ ∧ 𝐴 ≤ ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) → ( vol* ‘ ( 𝐴 [,] ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ) = ( ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) − 𝐴 ) )
32 24 25 30 31 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( vol* ‘ ( 𝐴 [,] ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ) = ( ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) − 𝐴 ) )
33 23 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) ∈ ℂ )
34 24 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → 𝐴 ∈ ℂ )
35 33 34 pncand ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) − 𝐴 ) = ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) )
36 32 35 eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( vol* ‘ ( 𝐴 [,] ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ) = ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) )
37 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ) )
38 24 25 37 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( 𝑥 ∈ ( 𝐴 [,] ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ) )
39 38 biimpa ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) ∧ 𝑥 ∈ ( 𝐴 [,] ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) )
40 39 simp1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) ∧ 𝑥 ∈ ( 𝐴 [,] ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ) → 𝑥 ∈ ℝ )
41 39 simp2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) ∧ 𝑥 ∈ ( 𝐴 [,] ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ) → 𝐴 ≤ 𝑥 )
42 elicopnf ⊢ ( 𝐴 ∈ ℝ → ( 𝑥 ∈ ( 𝐴 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) ) )
43 42 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) ∧ 𝑥 ∈ ( 𝐴 [,] ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ) → ( 𝑥 ∈ ( 𝐴 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) ) )
44 40 41 43 mpbir2and ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) ∧ 𝑥 ∈ ( 𝐴 [,] ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ) → 𝑥 ∈ ( 𝐴 [,) +∞ ) )
45 44 ex ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( 𝑥 ∈ ( 𝐴 [,] ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) → 𝑥 ∈ ( 𝐴 [,) +∞ ) ) )
46 45 ssrdv ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( 𝐴 [,] ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ⊆ ( 𝐴 [,) +∞ ) )
47 ovolss ⊢ ( ( ( 𝐴 [,] ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ⊆ ( 𝐴 [,) +∞ ) ∧ ( 𝐴 [,) +∞ ) ⊆ ℝ ) → ( vol* ‘ ( 𝐴 [,] ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ) ≤ ( vol* ‘ ( 𝐴 [,) +∞ ) ) )
48 46 4 47 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( vol* ‘ ( 𝐴 [,] ( ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) + 𝐴 ) ) ) ≤ ( vol* ‘ ( 𝐴 [,) +∞ ) ) )
49 36 48 eqbrtrrd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) ≤ ( vol* ‘ ( 𝐴 [,) +∞ ) ) )
50 23 20 49 lensymd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) → ¬ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) + 1 ) )
51 21 50 pm2.65da ⊢ ( 𝐴 ∈ ℝ → ¬ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ )
52 nltpnft ⊢ ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) ∈ ℝ* → ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) = +∞ ↔ ¬ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) )
53 11 52 syl ⊢ ( 𝐴 ∈ ℝ → ( ( vol* ‘ ( 𝐴 [,) +∞ ) ) = +∞ ↔ ¬ ( vol* ‘ ( 𝐴 [,) +∞ ) ) < +∞ ) )
54 51 53 mpbird ⊢ ( 𝐴 ∈ ℝ → ( vol* ‘ ( 𝐴 [,) +∞ ) ) = +∞ )