Step | Hyp | Ref
| Expression |
1 | | pnfxr 11267 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
2 | | icossre 13404 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝐴[,)+∞) ⊆
ℝ) |
3 | 1, 2 | mpan2 689 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ⊆
ℝ) |
4 | 3 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝐴[,)+∞) ⊆
ℝ) |
5 | | ovolge0 24997 |
. . . . . . 7
⊢ ((𝐴[,)+∞) ⊆ ℝ
→ 0 ≤ (vol*‘(𝐴[,)+∞))) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 0 ≤ (vol*‘(𝐴[,)+∞))) |
7 | | mnflt0 13104 |
. . . . . . 7
⊢ -∞
< 0 |
8 | | mnfxr 11270 |
. . . . . . . 8
⊢ -∞
∈ ℝ* |
9 | | 0xr 11260 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
10 | | ovolcl 24994 |
. . . . . . . . . 10
⊢ ((𝐴[,)+∞) ⊆ ℝ
→ (vol*‘(𝐴[,)+∞)) ∈
ℝ*) |
11 | 3, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
(vol*‘(𝐴[,)+∞))
∈ ℝ*) |
12 | 11 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) ∈
ℝ*) |
13 | | xrltletr 13135 |
. . . . . . . 8
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ (vol*‘(𝐴[,)+∞)) ∈ ℝ*)
→ ((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐴[,)+∞))) → -∞ <
(vol*‘(𝐴[,)+∞)))) |
14 | 8, 9, 12, 13 | mp3an12i 1465 |
. . . . . . 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 485 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) <
+∞) |
18 | | xrrebnd 13146 |
. . . . . 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 12143 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) < ((vol*‘(𝐴[,)+∞)) +
1)) |
22 | | peano2re 11386 |
. . . . 5
⊢
((vol*‘(𝐴[,)+∞)) ∈ ℝ →
((vol*‘(𝐴[,)+∞)) + 1) ∈
ℝ) |
23 | 20, 22 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) + 1) ∈
ℝ) |
24 | | simpl 483 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 𝐴
∈ ℝ) |
25 | 23, 24 | readdcld 11242 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) ∈ ℝ) |
26 | | 0red 11216 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 0 ∈ ℝ) |
27 | 20 | lep1d 12144 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) ≤ ((vol*‘(𝐴[,)+∞)) +
1)) |
28 | 26, 20, 23, 6, 27 | letrd 11370 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 0 ≤ ((vol*‘(𝐴[,)+∞)) + 1)) |
29 | 24, 23 | addge02d 11802 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (0 ≤ ((vol*‘(𝐴[,)+∞)) + 1) ↔ 𝐴 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) |
30 | 28, 29 | mpbid 231 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 𝐴
≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) |
31 | | ovolicc 25039 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) ∈ ℝ ∧ 𝐴 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) = ((((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) − 𝐴)) |
32 | 24, 25, 30, 31 | syl3anc 1371 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) = ((((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) − 𝐴)) |
33 | 23 | recnd 11241 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) + 1) ∈
ℂ) |
34 | 24 | recnd 11241 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 𝐴
∈ ℂ) |
35 | 33, 34 | pncand 11571 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) − 𝐴) = ((vol*‘(𝐴[,)+∞)) + 1)) |
36 | 32, 35 | eqtrd 2772 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) = ((vol*‘(𝐴[,)+∞)) + 1)) |
37 | | elicc2 13388 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧
(((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) ∈ ℝ) → (𝑥 ∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)))) |
38 | 24, 25, 37 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)))) |
39 | 38 | biimpa 477 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) |
40 | 39 | simp1d 1142 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → 𝑥 ∈ ℝ) |
41 | 39 | simp2d 1143 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → 𝐴 ≤ 𝑥) |
42 | | elicopnf 13421 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝑥 ∈ (𝐴[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥))) |
43 | 42 | ad2antrr 724 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → (𝑥 ∈ (𝐴[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥))) |
44 | 40, 41, 43 | mpbir2and 711 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → 𝑥 ∈ (𝐴[,)+∞)) |
45 | 44 | ex 413 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) → 𝑥 ∈ (𝐴[,)+∞))) |
46 | 45 | ssrdv 3988 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ⊆ (𝐴[,)+∞)) |
47 | | ovolss 25001 |
. . . . . 6
⊢ (((𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ⊆ (𝐴[,)+∞) ∧ (𝐴[,)+∞) ⊆ ℝ) →
(vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) ≤ (vol*‘(𝐴[,)+∞))) |
48 | 46, 4, 47 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) ≤ (vol*‘(𝐴[,)+∞))) |
49 | 36, 48 | eqbrtrrd 5172 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) + 1) ≤ (vol*‘(𝐴[,)+∞))) |
50 | 23, 20, 49 | lensymd 11364 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ¬ (vol*‘(𝐴[,)+∞)) < ((vol*‘(𝐴[,)+∞)) +
1)) |
51 | 21, 50 | pm2.65da 815 |
. 2
⊢ (𝐴 ∈ ℝ → ¬
(vol*‘(𝐴[,)+∞))
< +∞) |
52 | | nltpnft 13142 |
. . 3
⊢
((vol*‘(𝐴[,)+∞)) ∈ ℝ*
→ ((vol*‘(𝐴[,)+∞)) = +∞ ↔ ¬
(vol*‘(𝐴[,)+∞))
< +∞)) |
53 | 11, 52 | syl 17 |
. 2
⊢ (𝐴 ∈ ℝ →
((vol*‘(𝐴[,)+∞)) = +∞ ↔ ¬
(vol*‘(𝐴[,)+∞))
< +∞)) |
54 | 51, 53 | mpbird 256 |
1
⊢ (𝐴 ∈ ℝ →
(vol*‘(𝐴[,)+∞))
= +∞) |