Step | Hyp | Ref
| Expression |
1 | | pnfxr 11300 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
2 | | icossre 13440 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝐴[,)+∞) ⊆
ℝ) |
3 | 1, 2 | mpan2 689 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ⊆
ℝ) |
4 | 3 | adantr 479 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝐴[,)+∞) ⊆
ℝ) |
5 | | ovolge0 25454 |
. . . . . . 7
⊢ ((𝐴[,)+∞) ⊆ ℝ
→ 0 ≤ (vol*‘(𝐴[,)+∞))) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 0 ≤ (vol*‘(𝐴[,)+∞))) |
7 | | mnflt0 13140 |
. . . . . . 7
⊢ -∞
< 0 |
8 | | mnfxr 11303 |
. . . . . . . 8
⊢ -∞
∈ ℝ* |
9 | | 0xr 11293 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
10 | | ovolcl 25451 |
. . . . . . . . . 10
⊢ ((𝐴[,)+∞) ⊆ ℝ
→ (vol*‘(𝐴[,)+∞)) ∈
ℝ*) |
11 | 3, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
(vol*‘(𝐴[,)+∞))
∈ ℝ*) |
12 | 11 | adantr 479 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) ∈
ℝ*) |
13 | | xrltletr 13171 |
. . . . . . . 8
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ (vol*‘(𝐴[,)+∞)) ∈ ℝ*)
→ ((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐴[,)+∞))) → -∞ <
(vol*‘(𝐴[,)+∞)))) |
14 | 8, 9, 12, 13 | mp3an12i 1461 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐴[,)+∞))) → -∞
< (vol*‘(𝐴[,)+∞)))) |
15 | 7, 14 | mpani 694 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (0 ≤ (vol*‘(𝐴[,)+∞)) → -∞ <
(vol*‘(𝐴[,)+∞)))) |
16 | 6, 15 | mpd 15 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → -∞ < (vol*‘(𝐴[,)+∞))) |
17 | | simpr 483 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) <
+∞) |
18 | | xrrebnd 13182 |
. . . . . 6
⊢
((vol*‘(𝐴[,)+∞)) ∈ ℝ*
→ ((vol*‘(𝐴[,)+∞)) ∈ ℝ ↔
(-∞ < (vol*‘(𝐴[,)+∞)) ∧ (vol*‘(𝐴[,)+∞)) <
+∞))) |
19 | 12, 18 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) ∈ ℝ ↔
(-∞ < (vol*‘(𝐴[,)+∞)) ∧ (vol*‘(𝐴[,)+∞)) <
+∞))) |
20 | 16, 17, 19 | mpbir2and 711 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) ∈
ℝ) |
21 | 20 | ltp1d 12177 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) < ((vol*‘(𝐴[,)+∞)) +
1)) |
22 | | peano2re 11419 |
. . . . 5
⊢
((vol*‘(𝐴[,)+∞)) ∈ ℝ →
((vol*‘(𝐴[,)+∞)) + 1) ∈
ℝ) |
23 | 20, 22 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) + 1) ∈
ℝ) |
24 | | simpl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 𝐴
∈ ℝ) |
25 | 23, 24 | readdcld 11275 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) ∈ ℝ) |
26 | | 0red 11249 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 0 ∈ ℝ) |
27 | 20 | lep1d 12178 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) ≤ ((vol*‘(𝐴[,)+∞)) +
1)) |
28 | 26, 20, 23, 6, 27 | letrd 11403 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 0 ≤ ((vol*‘(𝐴[,)+∞)) + 1)) |
29 | 24, 23 | addge02d 11835 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (0 ≤ ((vol*‘(𝐴[,)+∞)) + 1) ↔ 𝐴 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) |
30 | 28, 29 | mpbid 231 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 𝐴
≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) |
31 | | ovolicc 25496 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) ∈ ℝ ∧ 𝐴 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) = ((((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) − 𝐴)) |
32 | 24, 25, 30, 31 | syl3anc 1368 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) = ((((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) − 𝐴)) |
33 | 23 | recnd 11274 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) + 1) ∈
ℂ) |
34 | 24 | recnd 11274 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 𝐴
∈ ℂ) |
35 | 33, 34 | pncand 11604 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) − 𝐴) = ((vol*‘(𝐴[,)+∞)) + 1)) |
36 | 32, 35 | eqtrd 2765 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) = ((vol*‘(𝐴[,)+∞)) + 1)) |
37 | | elicc2 13424 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧
(((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) ∈ ℝ) → (𝑥 ∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)))) |
38 | 24, 25, 37 | syl2anc 582 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)))) |
39 | 38 | biimpa 475 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) |
40 | 39 | simp1d 1139 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → 𝑥 ∈ ℝ) |
41 | 39 | simp2d 1140 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → 𝐴 ≤ 𝑥) |
42 | | elicopnf 13457 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝑥 ∈ (𝐴[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥))) |
43 | 42 | ad2antrr 724 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → (𝑥 ∈ (𝐴[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥))) |
44 | 40, 41, 43 | mpbir2and 711 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → 𝑥 ∈ (𝐴[,)+∞)) |
45 | 44 | ex 411 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) → 𝑥 ∈ (𝐴[,)+∞))) |
46 | 45 | ssrdv 3982 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ⊆ (𝐴[,)+∞)) |
47 | | ovolss 25458 |
. . . . . 6
⊢ (((𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ⊆ (𝐴[,)+∞) ∧ (𝐴[,)+∞) ⊆ ℝ) →
(vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) ≤ (vol*‘(𝐴[,)+∞))) |
48 | 46, 4, 47 | syl2anc 582 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) ≤ (vol*‘(𝐴[,)+∞))) |
49 | 36, 48 | eqbrtrrd 5173 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) + 1) ≤ (vol*‘(𝐴[,)+∞))) |
50 | 23, 20, 49 | lensymd 11397 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ¬ (vol*‘(𝐴[,)+∞)) < ((vol*‘(𝐴[,)+∞)) +
1)) |
51 | 21, 50 | pm2.65da 815 |
. 2
⊢ (𝐴 ∈ ℝ → ¬
(vol*‘(𝐴[,)+∞))
< +∞) |
52 | | nltpnft 13178 |
. . 3
⊢
((vol*‘(𝐴[,)+∞)) ∈ ℝ*
→ ((vol*‘(𝐴[,)+∞)) = +∞ ↔ ¬
(vol*‘(𝐴[,)+∞))
< +∞)) |
53 | 11, 52 | syl 17 |
. 2
⊢ (𝐴 ∈ ℝ →
((vol*‘(𝐴[,)+∞)) = +∞ ↔ ¬
(vol*‘(𝐴[,)+∞))
< +∞)) |
54 | 51, 53 | mpbird 256 |
1
⊢ (𝐴 ∈ ℝ →
(vol*‘(𝐴[,)+∞))
= +∞) |