Step | Hyp | Ref
| Expression |
1 | | pnfxr 10697 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
2 | | icossre 12820 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝐴[,)+∞) ⊆
ℝ) |
3 | 1, 2 | mpan2 689 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ⊆
ℝ) |
4 | 3 | adantr 483 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝐴[,)+∞) ⊆
ℝ) |
5 | | ovolge0 24084 |
. . . . . . 7
⊢ ((𝐴[,)+∞) ⊆ ℝ
→ 0 ≤ (vol*‘(𝐴[,)+∞))) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 0 ≤ (vol*‘(𝐴[,)+∞))) |
7 | | mnflt0 12523 |
. . . . . . 7
⊢ -∞
< 0 |
8 | | mnfxr 10700 |
. . . . . . . 8
⊢ -∞
∈ ℝ* |
9 | | 0xr 10690 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
10 | | ovolcl 24081 |
. . . . . . . . . 10
⊢ ((𝐴[,)+∞) ⊆ ℝ
→ (vol*‘(𝐴[,)+∞)) ∈
ℝ*) |
11 | 3, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
(vol*‘(𝐴[,)+∞))
∈ ℝ*) |
12 | 11 | adantr 483 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) ∈
ℝ*) |
13 | | xrltletr 12553 |
. . . . . . . 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 487 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) <
+∞) |
18 | | xrrebnd 12564 |
. . . . . 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 11572 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) < ((vol*‘(𝐴[,)+∞)) +
1)) |
22 | | peano2re 10815 |
. . . . 5
⊢
((vol*‘(𝐴[,)+∞)) ∈ ℝ →
((vol*‘(𝐴[,)+∞)) + 1) ∈
ℝ) |
23 | 20, 22 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) + 1) ∈
ℝ) |
24 | | simpl 485 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 𝐴
∈ ℝ) |
25 | 23, 24 | readdcld 10672 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) ∈ ℝ) |
26 | | 0red 10646 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 0 ∈ ℝ) |
27 | 20 | lep1d 11573 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) ≤ ((vol*‘(𝐴[,)+∞)) +
1)) |
28 | 26, 20, 23, 6, 27 | letrd 10799 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 0 ≤ ((vol*‘(𝐴[,)+∞)) + 1)) |
29 | 24, 23 | addge02d 11231 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (0 ≤ ((vol*‘(𝐴[,)+∞)) + 1) ↔ 𝐴 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) |
30 | 28, 29 | mpbid 234 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 𝐴
≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) |
31 | | ovolicc 24126 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) ∈ ℝ ∧ 𝐴 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) = ((((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) − 𝐴)) |
32 | 24, 25, 30, 31 | syl3anc 1367 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) = ((((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) − 𝐴)) |
33 | 23 | recnd 10671 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) + 1) ∈
ℂ) |
34 | 24 | recnd 10671 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 𝐴
∈ ℂ) |
35 | 33, 34 | pncand 11000 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) − 𝐴) = ((vol*‘(𝐴[,)+∞)) + 1)) |
36 | 32, 35 | eqtrd 2858 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) = ((vol*‘(𝐴[,)+∞)) + 1)) |
37 | | elicc2 12804 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧
(((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) ∈ ℝ) → (𝑥 ∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)))) |
38 | 24, 25, 37 | syl2anc 586 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)))) |
39 | 38 | biimpa 479 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) |
40 | 39 | simp1d 1138 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → 𝑥 ∈ ℝ) |
41 | 39 | simp2d 1139 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → 𝐴 ≤ 𝑥) |
42 | | elicopnf 12836 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝑥 ∈ (𝐴[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥))) |
43 | 42 | ad2antrr 724 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → (𝑥 ∈ (𝐴[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥))) |
44 | 40, 41, 43 | mpbir2and 711 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → 𝑥 ∈ (𝐴[,)+∞)) |
45 | 44 | ex 415 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) → 𝑥 ∈ (𝐴[,)+∞))) |
46 | 45 | ssrdv 3975 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ⊆ (𝐴[,)+∞)) |
47 | | ovolss 24088 |
. . . . . 6
⊢ (((𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ⊆ (𝐴[,)+∞) ∧ (𝐴[,)+∞) ⊆ ℝ) →
(vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) ≤ (vol*‘(𝐴[,)+∞))) |
48 | 46, 4, 47 | syl2anc 586 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) ≤ (vol*‘(𝐴[,)+∞))) |
49 | 36, 48 | eqbrtrrd 5092 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) + 1) ≤ (vol*‘(𝐴[,)+∞))) |
50 | 23, 20, 49 | lensymd 10793 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ¬ (vol*‘(𝐴[,)+∞)) < ((vol*‘(𝐴[,)+∞)) +
1)) |
51 | 21, 50 | pm2.65da 815 |
. 2
⊢ (𝐴 ∈ ℝ → ¬
(vol*‘(𝐴[,)+∞))
< +∞) |
52 | | nltpnft 12560 |
. . 3
⊢
((vol*‘(𝐴[,)+∞)) ∈ ℝ*
→ ((vol*‘(𝐴[,)+∞)) = +∞ ↔ ¬
(vol*‘(𝐴[,)+∞))
< +∞)) |
53 | 11, 52 | syl 17 |
. 2
⊢ (𝐴 ∈ ℝ →
((vol*‘(𝐴[,)+∞)) = +∞ ↔ ¬
(vol*‘(𝐴[,)+∞))
< +∞)) |
54 | 51, 53 | mpbird 259 |
1
⊢ (𝐴 ∈ ℝ →
(vol*‘(𝐴[,)+∞))
= +∞) |