Step | Hyp | Ref
| Expression |
1 | | pnfxr 11217 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
2 | | icossre 13354 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝐴[,)+∞) ⊆
ℝ) |
3 | 1, 2 | mpan2 690 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ⊆
ℝ) |
4 | 3 | adantr 482 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝐴[,)+∞) ⊆
ℝ) |
5 | | ovolge0 24868 |
. . . . . . 7
⊢ ((𝐴[,)+∞) ⊆ ℝ
→ 0 ≤ (vol*‘(𝐴[,)+∞))) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 0 ≤ (vol*‘(𝐴[,)+∞))) |
7 | | mnflt0 13054 |
. . . . . . 7
⊢ -∞
< 0 |
8 | | mnfxr 11220 |
. . . . . . . 8
⊢ -∞
∈ ℝ* |
9 | | 0xr 11210 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
10 | | ovolcl 24865 |
. . . . . . . . . 10
⊢ ((𝐴[,)+∞) ⊆ ℝ
→ (vol*‘(𝐴[,)+∞)) ∈
ℝ*) |
11 | 3, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
(vol*‘(𝐴[,)+∞))
∈ ℝ*) |
12 | 11 | adantr 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) ∈
ℝ*) |
13 | | xrltletr 13085 |
. . . . . . . 8
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ (vol*‘(𝐴[,)+∞)) ∈ ℝ*)
→ ((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐴[,)+∞))) → -∞ <
(vol*‘(𝐴[,)+∞)))) |
14 | 8, 9, 12, 13 | mp3an12i 1466 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐴[,)+∞))) → -∞
< (vol*‘(𝐴[,)+∞)))) |
15 | 7, 14 | mpani 695 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (0 ≤ (vol*‘(𝐴[,)+∞)) → -∞ <
(vol*‘(𝐴[,)+∞)))) |
16 | 6, 15 | mpd 15 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → -∞ < (vol*‘(𝐴[,)+∞))) |
17 | | simpr 486 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) <
+∞) |
18 | | xrrebnd 13096 |
. . . . . 6
⊢
((vol*‘(𝐴[,)+∞)) ∈ ℝ*
→ ((vol*‘(𝐴[,)+∞)) ∈ ℝ ↔
(-∞ < (vol*‘(𝐴[,)+∞)) ∧ (vol*‘(𝐴[,)+∞)) <
+∞))) |
19 | 12, 18 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) ∈ ℝ ↔
(-∞ < (vol*‘(𝐴[,)+∞)) ∧ (vol*‘(𝐴[,)+∞)) <
+∞))) |
20 | 16, 17, 19 | mpbir2and 712 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) ∈
ℝ) |
21 | 20 | ltp1d 12093 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) < ((vol*‘(𝐴[,)+∞)) +
1)) |
22 | | peano2re 11336 |
. . . . 5
⊢
((vol*‘(𝐴[,)+∞)) ∈ ℝ →
((vol*‘(𝐴[,)+∞)) + 1) ∈
ℝ) |
23 | 20, 22 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) + 1) ∈
ℝ) |
24 | | simpl 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 𝐴
∈ ℝ) |
25 | 23, 24 | readdcld 11192 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) ∈ ℝ) |
26 | | 0red 11166 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 0 ∈ ℝ) |
27 | 20 | lep1d 12094 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) ≤ ((vol*‘(𝐴[,)+∞)) +
1)) |
28 | 26, 20, 23, 6, 27 | letrd 11320 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 0 ≤ ((vol*‘(𝐴[,)+∞)) + 1)) |
29 | 24, 23 | addge02d 11752 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (0 ≤ ((vol*‘(𝐴[,)+∞)) + 1) ↔ 𝐴 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) |
30 | 28, 29 | mpbid 231 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 𝐴
≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) |
31 | | ovolicc 24910 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) ∈ ℝ ∧ 𝐴 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) = ((((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) − 𝐴)) |
32 | 24, 25, 30, 31 | syl3anc 1372 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) = ((((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) − 𝐴)) |
33 | 23 | recnd 11191 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) + 1) ∈
ℂ) |
34 | 24 | recnd 11191 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 𝐴
∈ ℂ) |
35 | 33, 34 | pncand 11521 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) − 𝐴) = ((vol*‘(𝐴[,)+∞)) + 1)) |
36 | 32, 35 | eqtrd 2773 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) = ((vol*‘(𝐴[,)+∞)) + 1)) |
37 | | elicc2 13338 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧
(((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) ∈ ℝ) → (𝑥 ∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)))) |
38 | 24, 25, 37 | syl2anc 585 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)))) |
39 | 38 | biimpa 478 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) |
40 | 39 | simp1d 1143 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → 𝑥 ∈ ℝ) |
41 | 39 | simp2d 1144 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → 𝐴 ≤ 𝑥) |
42 | | elicopnf 13371 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝑥 ∈ (𝐴[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥))) |
43 | 42 | ad2antrr 725 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → (𝑥 ∈ (𝐴[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥))) |
44 | 40, 41, 43 | mpbir2and 712 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → 𝑥 ∈ (𝐴[,)+∞)) |
45 | 44 | ex 414 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) → 𝑥 ∈ (𝐴[,)+∞))) |
46 | 45 | ssrdv 3954 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ⊆ (𝐴[,)+∞)) |
47 | | ovolss 24872 |
. . . . . 6
⊢ (((𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ⊆ (𝐴[,)+∞) ∧ (𝐴[,)+∞) ⊆ ℝ) →
(vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) ≤ (vol*‘(𝐴[,)+∞))) |
48 | 46, 4, 47 | syl2anc 585 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) ≤ (vol*‘(𝐴[,)+∞))) |
49 | 36, 48 | eqbrtrrd 5133 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) + 1) ≤ (vol*‘(𝐴[,)+∞))) |
50 | 23, 20, 49 | lensymd 11314 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ¬ (vol*‘(𝐴[,)+∞)) < ((vol*‘(𝐴[,)+∞)) +
1)) |
51 | 21, 50 | pm2.65da 816 |
. 2
⊢ (𝐴 ∈ ℝ → ¬
(vol*‘(𝐴[,)+∞))
< +∞) |
52 | | nltpnft 13092 |
. . 3
⊢
((vol*‘(𝐴[,)+∞)) ∈ ℝ*
→ ((vol*‘(𝐴[,)+∞)) = +∞ ↔ ¬
(vol*‘(𝐴[,)+∞))
< +∞)) |
53 | 11, 52 | syl 17 |
. 2
⊢ (𝐴 ∈ ℝ →
((vol*‘(𝐴[,)+∞)) = +∞ ↔ ¬
(vol*‘(𝐴[,)+∞))
< +∞)) |
54 | 51, 53 | mpbird 257 |
1
⊢ (𝐴 ∈ ℝ →
(vol*‘(𝐴[,)+∞))
= +∞) |