| Step | Hyp | Ref
| Expression |
| 1 | | pnfxr 11315 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
| 2 | | icossre 13468 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝐴[,)+∞) ⊆
ℝ) |
| 3 | 1, 2 | mpan2 691 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ⊆
ℝ) |
| 4 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝐴[,)+∞) ⊆
ℝ) |
| 5 | | ovolge0 25516 |
. . . . . . 7
⊢ ((𝐴[,)+∞) ⊆ ℝ
→ 0 ≤ (vol*‘(𝐴[,)+∞))) |
| 6 | 4, 5 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 0 ≤ (vol*‘(𝐴[,)+∞))) |
| 7 | | mnflt0 13167 |
. . . . . . 7
⊢ -∞
< 0 |
| 8 | | mnfxr 11318 |
. . . . . . . 8
⊢ -∞
∈ ℝ* |
| 9 | | 0xr 11308 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
| 10 | | ovolcl 25513 |
. . . . . . . . . 10
⊢ ((𝐴[,)+∞) ⊆ ℝ
→ (vol*‘(𝐴[,)+∞)) ∈
ℝ*) |
| 11 | 3, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ →
(vol*‘(𝐴[,)+∞))
∈ ℝ*) |
| 12 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) ∈
ℝ*) |
| 13 | | xrltletr 13199 |
. . . . . . . 8
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ (vol*‘(𝐴[,)+∞)) ∈ ℝ*)
→ ((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐴[,)+∞))) → -∞ <
(vol*‘(𝐴[,)+∞)))) |
| 14 | 8, 9, 12, 13 | mp3an12i 1467 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((-∞ < 0 ∧ 0 ≤ (vol*‘(𝐴[,)+∞))) → -∞
< (vol*‘(𝐴[,)+∞)))) |
| 15 | 7, 14 | mpani 696 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (0 ≤ (vol*‘(𝐴[,)+∞)) → -∞ <
(vol*‘(𝐴[,)+∞)))) |
| 16 | 6, 15 | mpd 15 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → -∞ < (vol*‘(𝐴[,)+∞))) |
| 17 | | simpr 484 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) <
+∞) |
| 18 | | xrrebnd 13210 |
. . . . . 6
⊢
((vol*‘(𝐴[,)+∞)) ∈ ℝ*
→ ((vol*‘(𝐴[,)+∞)) ∈ ℝ ↔
(-∞ < (vol*‘(𝐴[,)+∞)) ∧ (vol*‘(𝐴[,)+∞)) <
+∞))) |
| 19 | 12, 18 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) ∈ ℝ ↔
(-∞ < (vol*‘(𝐴[,)+∞)) ∧ (vol*‘(𝐴[,)+∞)) <
+∞))) |
| 20 | 16, 17, 19 | mpbir2and 713 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) ∈
ℝ) |
| 21 | 20 | ltp1d 12198 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) < ((vol*‘(𝐴[,)+∞)) +
1)) |
| 22 | | peano2re 11434 |
. . . . 5
⊢
((vol*‘(𝐴[,)+∞)) ∈ ℝ →
((vol*‘(𝐴[,)+∞)) + 1) ∈
ℝ) |
| 23 | 20, 22 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) + 1) ∈
ℝ) |
| 24 | | simpl 482 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 𝐴
∈ ℝ) |
| 25 | 23, 24 | readdcld 11290 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) ∈ ℝ) |
| 26 | | 0red 11264 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 0 ∈ ℝ) |
| 27 | 20 | lep1d 12199 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,)+∞)) ≤ ((vol*‘(𝐴[,)+∞)) +
1)) |
| 28 | 26, 20, 23, 6, 27 | letrd 11418 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 0 ≤ ((vol*‘(𝐴[,)+∞)) + 1)) |
| 29 | 24, 23 | addge02d 11852 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (0 ≤ ((vol*‘(𝐴[,)+∞)) + 1) ↔ 𝐴 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) |
| 30 | 28, 29 | mpbid 232 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 𝐴
≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) |
| 31 | | ovolicc 25558 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) ∈ ℝ ∧ 𝐴 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) = ((((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) − 𝐴)) |
| 32 | 24, 25, 30, 31 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) = ((((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) − 𝐴)) |
| 33 | 23 | recnd 11289 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) + 1) ∈
ℂ) |
| 34 | 24 | recnd 11289 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → 𝐴
∈ ℂ) |
| 35 | 33, 34 | pncand 11621 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) − 𝐴) = ((vol*‘(𝐴[,)+∞)) + 1)) |
| 36 | 32, 35 | eqtrd 2777 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) = ((vol*‘(𝐴[,)+∞)) + 1)) |
| 37 | | elicc2 13452 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧
(((vol*‘(𝐴[,)+∞)) + 1) + 𝐴) ∈ ℝ) → (𝑥 ∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)))) |
| 38 | 24, 25, 37 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)))) |
| 39 | 38 | biimpa 476 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ (((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) |
| 40 | 39 | simp1d 1143 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → 𝑥 ∈ ℝ) |
| 41 | 39 | simp2d 1144 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → 𝐴 ≤ 𝑥) |
| 42 | | elicopnf 13485 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝑥 ∈ (𝐴[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥))) |
| 43 | 42 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → (𝑥 ∈ (𝐴[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥))) |
| 44 | 40, 41, 43 | mpbir2and 713 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) ∧ 𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) → 𝑥 ∈ (𝐴[,)+∞)) |
| 45 | 44 | ex 412 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝑥
∈ (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) → 𝑥 ∈ (𝐴[,)+∞))) |
| 46 | 45 | ssrdv 3989 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ⊆ (𝐴[,)+∞)) |
| 47 | | ovolss 25520 |
. . . . . 6
⊢ (((𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴)) ⊆ (𝐴[,)+∞) ∧ (𝐴[,)+∞) ⊆ ℝ) →
(vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) ≤ (vol*‘(𝐴[,)+∞))) |
| 48 | 46, 4, 47 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → (vol*‘(𝐴[,](((vol*‘(𝐴[,)+∞)) + 1) + 𝐴))) ≤ (vol*‘(𝐴[,)+∞))) |
| 49 | 36, 48 | eqbrtrrd 5167 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ((vol*‘(𝐴[,)+∞)) + 1) ≤ (vol*‘(𝐴[,)+∞))) |
| 50 | 23, 20, 49 | lensymd 11412 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧
(vol*‘(𝐴[,)+∞))
< +∞) → ¬ (vol*‘(𝐴[,)+∞)) < ((vol*‘(𝐴[,)+∞)) +
1)) |
| 51 | 21, 50 | pm2.65da 817 |
. 2
⊢ (𝐴 ∈ ℝ → ¬
(vol*‘(𝐴[,)+∞))
< +∞) |
| 52 | | nltpnft 13206 |
. . 3
⊢
((vol*‘(𝐴[,)+∞)) ∈ ℝ*
→ ((vol*‘(𝐴[,)+∞)) = +∞ ↔ ¬
(vol*‘(𝐴[,)+∞))
< +∞)) |
| 53 | 11, 52 | syl 17 |
. 2
⊢ (𝐴 ∈ ℝ →
((vol*‘(𝐴[,)+∞)) = +∞ ↔ ¬
(vol*‘(𝐴[,)+∞))
< +∞)) |
| 54 | 51, 53 | mpbird 257 |
1
⊢ (𝐴 ∈ ℝ →
(vol*‘(𝐴[,)+∞))
= +∞) |