| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ovollb2.5 | . . . 4
⊢ (𝜑 → 𝐴 ⊆ ∪ ran
([,] ∘ 𝐹)) | 
| 2 |  | ovollb2.4 | . . . . 5
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) | 
| 3 |  | ovolficcss 25505 | . . . . 5
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ∪ ran ([,] ∘
𝐹) ⊆
ℝ) | 
| 4 | 2, 3 | syl 17 | . . . 4
⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ) | 
| 5 | 1, 4 | sstrd 3993 | . . 3
⊢ (𝜑 → 𝐴 ⊆ ℝ) | 
| 6 |  | ovolcl 25514 | . . 3
⊢ (𝐴 ⊆ ℝ →
(vol*‘𝐴) ∈
ℝ*) | 
| 7 | 5, 6 | syl 17 | . 2
⊢ (𝜑 → (vol*‘𝐴) ∈
ℝ*) | 
| 8 |  | ovolfcl 25502 | . . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) | 
| 9 | 2, 8 | sylan 580 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) | 
| 10 | 9 | simp1d 1142 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ) | 
| 11 |  | ovollb2.6 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈
ℝ+) | 
| 12 | 11 | rphalfcld 13090 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 / 2) ∈
ℝ+) | 
| 13 | 12 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 / 2) ∈
ℝ+) | 
| 14 |  | 2nn 12340 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ | 
| 15 |  | nnnn0 12535 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) | 
| 16 | 15 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) | 
| 17 |  | nnexpcl 14116 | . . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) | 
| 18 | 14, 16, 17 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈
ℕ) | 
| 19 | 18 | nnrpd 13076 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈
ℝ+) | 
| 20 | 13, 19 | rpdivcld 13095 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐵 / 2) / (2↑𝑛)) ∈
ℝ+) | 
| 21 | 20 | rpred 13078 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐵 / 2) / (2↑𝑛)) ∈ ℝ) | 
| 22 | 10, 21 | resubcld 11692 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) − ((𝐵 / 2) / (2↑𝑛))) ∈ ℝ) | 
| 23 | 9 | simp2d 1143 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ) | 
| 24 | 23, 21 | readdcld 11291 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛))) ∈ ℝ) | 
| 25 | 10, 20 | ltsubrpd 13110 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) − ((𝐵 / 2) / (2↑𝑛))) < (1st ‘(𝐹‘𝑛))) | 
| 26 | 9 | simp3d 1144 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) | 
| 27 | 23, 20 | ltaddrpd 13111 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) < ((2nd
‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛)))) | 
| 28 | 10, 23, 24, 26, 27 | lelttrd 11420 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) < ((2nd
‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛)))) | 
| 29 | 22, 10, 24, 25, 28 | lttrd 11423 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) − ((𝐵 / 2) / (2↑𝑛))) < ((2nd ‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛)))) | 
| 30 | 22, 24, 29 | ltled 11410 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) − ((𝐵 / 2) / (2↑𝑛))) ≤ ((2nd ‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛)))) | 
| 31 |  | df-br 5143 | . . . . . . . . 9
⊢
(((1st ‘(𝐹‘𝑛)) − ((𝐵 / 2) / (2↑𝑛))) ≤ ((2nd ‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛))) ↔ 〈((1st
‘(𝐹‘𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛)))〉 ∈ ≤ ) | 
| 32 | 30, 31 | sylib 218 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛)))〉 ∈ ≤ ) | 
| 33 | 22, 24 | opelxpd 5723 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛)))〉 ∈ (ℝ ×
ℝ)) | 
| 34 | 32, 33 | elind 4199 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛)))〉 ∈ ( ≤ ∩ (ℝ
× ℝ))) | 
| 35 |  | ovollb2.2 | . . . . . . 7
⊢ 𝐺 = (𝑛 ∈ ℕ ↦
〈((1st ‘(𝐹‘𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛)))〉) | 
| 36 | 34, 35 | fmptd 7133 | . . . . . 6
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) | 
| 37 |  | eqid 2736 | . . . . . . 7
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) | 
| 38 |  | ovollb2.3 | . . . . . . 7
⊢ 𝑇 = seq1( + , ((abs ∘
− ) ∘ 𝐺)) | 
| 39 | 37, 38 | ovolsf 25508 | . . . . . 6
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞)) | 
| 40 | 36, 39 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞)) | 
| 41 | 40 | frnd 6743 | . . . 4
⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞)) | 
| 42 |  | icossxr 13473 | . . . 4
⊢
(0[,)+∞) ⊆ ℝ* | 
| 43 | 41, 42 | sstrdi 3995 | . . 3
⊢ (𝜑 → ran 𝑇 ⊆
ℝ*) | 
| 44 |  | supxrcl 13358 | . . 3
⊢ (ran
𝑇 ⊆
ℝ* → sup(ran 𝑇, ℝ*, < ) ∈
ℝ*) | 
| 45 | 43, 44 | syl 17 | . 2
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ*) | 
| 46 |  | ovollb2.7 | . . . 4
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ) | 
| 47 | 11 | rpred 13078 | . . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 48 | 46, 47 | readdcld 11291 | . . 3
⊢ (𝜑 → (sup(ran 𝑆, ℝ*, < ) + 𝐵) ∈
ℝ) | 
| 49 | 48 | rexrd 11312 | . 2
⊢ (𝜑 → (sup(ran 𝑆, ℝ*, < ) + 𝐵) ∈
ℝ*) | 
| 50 |  | 2fveq3 6910 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → (1st ‘(𝐹‘𝑛)) = (1st ‘(𝐹‘𝑚))) | 
| 51 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑚 → (2↑𝑛) = (2↑𝑚)) | 
| 52 | 51 | oveq2d 7448 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → ((𝐵 / 2) / (2↑𝑛)) = ((𝐵 / 2) / (2↑𝑚))) | 
| 53 | 50, 52 | oveq12d 7450 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → ((1st ‘(𝐹‘𝑛)) − ((𝐵 / 2) / (2↑𝑛))) = ((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚)))) | 
| 54 |  | 2fveq3 6910 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → (2nd ‘(𝐹‘𝑛)) = (2nd ‘(𝐹‘𝑚))) | 
| 55 | 54, 52 | oveq12d 7450 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → ((2nd ‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛))) = ((2nd ‘(𝐹‘𝑚)) + ((𝐵 / 2) / (2↑𝑚)))) | 
| 56 | 53, 55 | opeq12d 4880 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → 〈((1st ‘(𝐹‘𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹‘𝑛)) + ((𝐵 / 2) / (2↑𝑛)))〉 = 〈((1st
‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝐵 / 2) / (2↑𝑚)))〉) | 
| 57 |  | opex 5468 | . . . . . . . . . . . . . . 15
⊢
〈((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝐵 / 2) / (2↑𝑚)))〉 ∈ V | 
| 58 | 56, 35, 57 | fvmpt 7015 | . . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → (𝐺‘𝑚) = 〈((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝐵 / 2) / (2↑𝑚)))〉) | 
| 59 | 58 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) = 〈((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝐵 / 2) / (2↑𝑚)))〉) | 
| 60 | 59 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (1st
‘(𝐺‘𝑚)) = (1st
‘〈((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝐵 / 2) / (2↑𝑚)))〉)) | 
| 61 |  | ovex 7465 | . . . . . . . . . . . . 13
⊢
((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚))) ∈ V | 
| 62 |  | ovex 7465 | . . . . . . . . . . . . 13
⊢
((2nd ‘(𝐹‘𝑚)) + ((𝐵 / 2) / (2↑𝑚))) ∈ V | 
| 63 | 61, 62 | op1st 8023 | . . . . . . . . . . . 12
⊢
(1st ‘〈((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝐵 / 2) / (2↑𝑚)))〉) = ((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚))) | 
| 64 | 60, 63 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (1st
‘(𝐺‘𝑚)) = ((1st
‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚)))) | 
| 65 |  | ovolfcl 25502 | . . . . . . . . . . . . . 14
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → ((1st
‘(𝐹‘𝑚)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑚)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑚)) ≤ (2nd
‘(𝐹‘𝑚)))) | 
| 66 | 2, 65 | sylan 580 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((1st
‘(𝐹‘𝑚)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑚)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑚)) ≤ (2nd
‘(𝐹‘𝑚)))) | 
| 67 | 66 | simp1d 1142 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (1st
‘(𝐹‘𝑚)) ∈
ℝ) | 
| 68 | 12 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐵 / 2) ∈
ℝ+) | 
| 69 |  | nnnn0 12535 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℕ0) | 
| 70 | 69 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ0) | 
| 71 |  | nnexpcl 14116 | . . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ ∧ 𝑚
∈ ℕ0) → (2↑𝑚) ∈ ℕ) | 
| 72 | 14, 70, 71 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2↑𝑚) ∈
ℕ) | 
| 73 | 72 | nnrpd 13076 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2↑𝑚) ∈
ℝ+) | 
| 74 | 68, 73 | rpdivcld 13095 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝐵 / 2) / (2↑𝑚)) ∈
ℝ+) | 
| 75 | 67, 74 | ltsubrpd 13110 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((1st
‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚))) < (1st ‘(𝐹‘𝑚))) | 
| 76 | 64, 75 | eqbrtrd 5164 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (1st
‘(𝐺‘𝑚)) < (1st
‘(𝐹‘𝑚))) | 
| 77 | 76 | adantlr 715 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑚 ∈ ℕ) → (1st
‘(𝐺‘𝑚)) < (1st
‘(𝐹‘𝑚))) | 
| 78 |  | ovolfcl 25502 | . . . . . . . . . . . . 13
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → ((1st
‘(𝐺‘𝑚)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝑚)) ∈ ℝ ∧ (1st
‘(𝐺‘𝑚)) ≤ (2nd
‘(𝐺‘𝑚)))) | 
| 79 | 36, 78 | sylan 580 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((1st
‘(𝐺‘𝑚)) ∈ ℝ ∧
(2nd ‘(𝐺‘𝑚)) ∈ ℝ ∧ (1st
‘(𝐺‘𝑚)) ≤ (2nd
‘(𝐺‘𝑚)))) | 
| 80 | 79 | simp1d 1142 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (1st
‘(𝐺‘𝑚)) ∈
ℝ) | 
| 81 | 80 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑚 ∈ ℕ) → (1st
‘(𝐺‘𝑚)) ∈
ℝ) | 
| 82 | 67 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑚 ∈ ℕ) → (1st
‘(𝐹‘𝑚)) ∈
ℝ) | 
| 83 | 5 | sselda 3982 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ) | 
| 84 | 83 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ ℝ) | 
| 85 |  | ltletr 11354 | . . . . . . . . . 10
⊢
(((1st ‘(𝐺‘𝑚)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑚)) ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(((1st ‘(𝐺‘𝑚)) < (1st ‘(𝐹‘𝑚)) ∧ (1st ‘(𝐹‘𝑚)) ≤ 𝑧) → (1st ‘(𝐺‘𝑚)) < 𝑧)) | 
| 86 | 81, 82, 84, 85 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑚 ∈ ℕ) → (((1st
‘(𝐺‘𝑚)) < (1st
‘(𝐹‘𝑚)) ∧ (1st
‘(𝐹‘𝑚)) ≤ 𝑧) → (1st ‘(𝐺‘𝑚)) < 𝑧)) | 
| 87 | 77, 86 | mpand 695 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑚 ∈ ℕ) → ((1st
‘(𝐹‘𝑚)) ≤ 𝑧 → (1st ‘(𝐺‘𝑚)) < 𝑧)) | 
| 88 | 66 | simp2d 1143 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2nd
‘(𝐹‘𝑚)) ∈
ℝ) | 
| 89 | 88, 74 | ltaddrpd 13111 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2nd
‘(𝐹‘𝑚)) < ((2nd
‘(𝐹‘𝑚)) + ((𝐵 / 2) / (2↑𝑚)))) | 
| 90 | 59 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2nd
‘(𝐺‘𝑚)) = (2nd
‘〈((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝐵 / 2) / (2↑𝑚)))〉)) | 
| 91 | 61, 62 | op2nd 8024 | . . . . . . . . . . . 12
⊢
(2nd ‘〈((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝐵 / 2) / (2↑𝑚)))〉) = ((2nd ‘(𝐹‘𝑚)) + ((𝐵 / 2) / (2↑𝑚))) | 
| 92 | 90, 91 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2nd
‘(𝐺‘𝑚)) = ((2nd
‘(𝐹‘𝑚)) + ((𝐵 / 2) / (2↑𝑚)))) | 
| 93 | 89, 92 | breqtrrd 5170 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2nd
‘(𝐹‘𝑚)) < (2nd
‘(𝐺‘𝑚))) | 
| 94 | 93 | adantlr 715 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑚 ∈ ℕ) → (2nd
‘(𝐹‘𝑚)) < (2nd
‘(𝐺‘𝑚))) | 
| 95 | 88 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑚 ∈ ℕ) → (2nd
‘(𝐹‘𝑚)) ∈
ℝ) | 
| 96 | 79 | simp2d 1143 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2nd
‘(𝐺‘𝑚)) ∈
ℝ) | 
| 97 | 96 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑚 ∈ ℕ) → (2nd
‘(𝐺‘𝑚)) ∈
ℝ) | 
| 98 |  | lelttr 11352 | . . . . . . . . . 10
⊢ ((𝑧 ∈ ℝ ∧
(2nd ‘(𝐹‘𝑚)) ∈ ℝ ∧ (2nd
‘(𝐺‘𝑚)) ∈ ℝ) →
((𝑧 ≤ (2nd
‘(𝐹‘𝑚)) ∧ (2nd
‘(𝐹‘𝑚)) < (2nd
‘(𝐺‘𝑚))) → 𝑧 < (2nd ‘(𝐺‘𝑚)))) | 
| 99 | 84, 95, 97, 98 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑚 ∈ ℕ) → ((𝑧 ≤ (2nd ‘(𝐹‘𝑚)) ∧ (2nd ‘(𝐹‘𝑚)) < (2nd ‘(𝐺‘𝑚))) → 𝑧 < (2nd ‘(𝐺‘𝑚)))) | 
| 100 | 94, 99 | mpan2d 694 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑚 ∈ ℕ) → (𝑧 ≤ (2nd ‘(𝐹‘𝑚)) → 𝑧 < (2nd ‘(𝐺‘𝑚)))) | 
| 101 | 87, 100 | anim12d 609 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐴) ∧ 𝑚 ∈ ℕ) → (((1st
‘(𝐹‘𝑚)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑚))) → ((1st ‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))))) | 
| 102 | 101 | reximdva 3167 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (∃𝑚 ∈ ℕ ((1st
‘(𝐹‘𝑚)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑚))) → ∃𝑚 ∈ ℕ ((1st
‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))))) | 
| 103 | 102 | ralimdva 3166 | . . . . 5
⊢ (𝜑 → (∀𝑧 ∈ 𝐴 ∃𝑚 ∈ ℕ ((1st
‘(𝐹‘𝑚)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑚))) → ∀𝑧 ∈ 𝐴 ∃𝑚 ∈ ℕ ((1st
‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))))) | 
| 104 |  | ovolficc 25504 | . . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪ ran
([,] ∘ 𝐹) ↔
∀𝑧 ∈ 𝐴 ∃𝑚 ∈ ℕ ((1st
‘(𝐹‘𝑚)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑚))))) | 
| 105 | 5, 2, 104 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝐴 ⊆ ∪ ran
([,] ∘ 𝐹) ↔
∀𝑧 ∈ 𝐴 ∃𝑚 ∈ ℕ ((1st
‘(𝐹‘𝑚)) ≤ 𝑧 ∧ 𝑧 ≤ (2nd ‘(𝐹‘𝑚))))) | 
| 106 |  | ovolfioo 25503 | . . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑧 ∈ 𝐴 ∃𝑚 ∈ ℕ ((1st
‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))))) | 
| 107 | 5, 36, 106 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑧 ∈ 𝐴 ∃𝑚 ∈ ℕ ((1st
‘(𝐺‘𝑚)) < 𝑧 ∧ 𝑧 < (2nd ‘(𝐺‘𝑚))))) | 
| 108 | 103, 105,
107 | 3imtr4d 294 | . . . 4
⊢ (𝜑 → (𝐴 ⊆ ∪ ran
([,] ∘ 𝐹) →
𝐴 ⊆ ∪ ran ((,) ∘ 𝐺))) | 
| 109 | 1, 108 | mpd 15 | . . 3
⊢ (𝜑 → 𝐴 ⊆ ∪ ran
((,) ∘ 𝐺)) | 
| 110 | 38 | ovollb 25515 | . . 3
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran
((,) ∘ 𝐺)) →
(vol*‘𝐴) ≤ sup(ran
𝑇, ℝ*,
< )) | 
| 111 | 36, 109, 110 | syl2anc 584 | . 2
⊢ (𝜑 → (vol*‘𝐴) ≤ sup(ran 𝑇, ℝ*, <
)) | 
| 112 | 38 | fveq1i 6906 | . . . . . . 7
⊢ (𝑇‘𝑘) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘) | 
| 113 |  | fzfid 14015 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin) | 
| 114 |  | rge0ssre 13497 | . . . . . . . . . . 11
⊢
(0[,)+∞) ⊆ ℝ | 
| 115 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) | 
| 116 | 115 | ovolfsf 25507 | . . . . . . . . . . . . . 14
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞)) | 
| 117 | 2, 116 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐹):ℕ⟶(0[,)+∞)) | 
| 118 | 117 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((abs ∘ −
) ∘ 𝐹):ℕ⟶(0[,)+∞)) | 
| 119 |  | elfznn 13594 | . . . . . . . . . . . 12
⊢ (𝑚 ∈ (1...𝑘) → 𝑚 ∈ ℕ) | 
| 120 |  | ffvelcdm 7100 | . . . . . . . . . . . 12
⊢ ((((abs
∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) ∧ 𝑚 ∈ ℕ) → (((abs
∘ − ) ∘ 𝐹)‘𝑚) ∈ (0[,)+∞)) | 
| 121 | 118, 119,
120 | syl2an 596 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘
𝐹)‘𝑚) ∈ (0[,)+∞)) | 
| 122 | 114, 121 | sselid 3980 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘
𝐹)‘𝑚) ∈ ℝ) | 
| 123 | 122 | recnd 11290 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘
𝐹)‘𝑚) ∈ ℂ) | 
| 124 | 11 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐵 ∈
ℝ+) | 
| 125 | 124, 73 | rpdivcld 13095 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐵 / (2↑𝑚)) ∈
ℝ+) | 
| 126 | 125 | rpcnd 13080 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐵 / (2↑𝑚)) ∈ ℂ) | 
| 127 | 119, 126 | sylan2 593 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑘)) → (𝐵 / (2↑𝑚)) ∈ ℂ) | 
| 128 | 127 | adantlr 715 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (𝐵 / (2↑𝑚)) ∈ ℂ) | 
| 129 | 113, 123,
128 | fsumadd 15777 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))) = (Σ𝑚 ∈ (1...𝑘)(((abs ∘ − ) ∘ 𝐹)‘𝑚) + Σ𝑚 ∈ (1...𝑘)(𝐵 / (2↑𝑚)))) | 
| 130 | 37 | ovolfsval 25506 | . . . . . . . . . . . . 13
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑚) = ((2nd ‘(𝐺‘𝑚)) − (1st ‘(𝐺‘𝑚)))) | 
| 131 | 36, 130 | sylan 580 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑚) = ((2nd ‘(𝐺‘𝑚)) − (1st ‘(𝐺‘𝑚)))) | 
| 132 | 88 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2nd
‘(𝐹‘𝑚)) ∈
ℂ) | 
| 133 | 74 | rpcnd 13080 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝐵 / 2) / (2↑𝑚)) ∈ ℂ) | 
| 134 | 67 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (1st
‘(𝐹‘𝑚)) ∈
ℂ) | 
| 135 | 134, 133 | subcld 11621 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((1st
‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚))) ∈ ℂ) | 
| 136 | 132, 133,
135 | addsubassd 11641 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((2nd
‘(𝐹‘𝑚)) + ((𝐵 / 2) / (2↑𝑚))) − ((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚)))) = ((2nd ‘(𝐹‘𝑚)) + (((𝐵 / 2) / (2↑𝑚)) − ((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚)))))) | 
| 137 | 92, 64 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((2nd
‘(𝐺‘𝑚)) − (1st
‘(𝐺‘𝑚))) = (((2nd
‘(𝐹‘𝑚)) + ((𝐵 / 2) / (2↑𝑚))) − ((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚))))) | 
| 138 | 132, 134,
126 | subadd23d 11643 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((2nd
‘(𝐹‘𝑚)) − (1st
‘(𝐹‘𝑚))) + (𝐵 / (2↑𝑚))) = ((2nd ‘(𝐹‘𝑚)) + ((𝐵 / (2↑𝑚)) − (1st ‘(𝐹‘𝑚))))) | 
| 139 | 115 | ovolfsval 25506 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑚) = ((2nd ‘(𝐹‘𝑚)) − (1st ‘(𝐹‘𝑚)))) | 
| 140 | 2, 139 | sylan 580 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑚) = ((2nd ‘(𝐹‘𝑚)) − (1st ‘(𝐹‘𝑚)))) | 
| 141 | 140 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((((abs ∘
− ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))) = (((2nd ‘(𝐹‘𝑚)) − (1st ‘(𝐹‘𝑚))) + (𝐵 / (2↑𝑚)))) | 
| 142 | 133, 134,
133 | subsub3d 11651 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝐵 / 2) / (2↑𝑚)) − ((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚)))) = ((((𝐵 / 2) / (2↑𝑚)) + ((𝐵 / 2) / (2↑𝑚))) − (1st ‘(𝐹‘𝑚)))) | 
| 143 | 68 | rpcnd 13080 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐵 / 2) ∈ ℂ) | 
| 144 | 72 | nncnd 12283 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2↑𝑚) ∈
ℂ) | 
| 145 | 72 | nnne0d 12317 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2↑𝑚) ≠ 0) | 
| 146 | 143, 143,
144, 145 | divdird 12082 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝐵 / 2) + (𝐵 / 2)) / (2↑𝑚)) = (((𝐵 / 2) / (2↑𝑚)) + ((𝐵 / 2) / (2↑𝑚)))) | 
| 147 | 124 | rpcnd 13080 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐵 ∈ ℂ) | 
| 148 | 147 | 2halvesd 12514 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝐵 / 2) + (𝐵 / 2)) = 𝐵) | 
| 149 | 148 | oveq1d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝐵 / 2) + (𝐵 / 2)) / (2↑𝑚)) = (𝐵 / (2↑𝑚))) | 
| 150 | 146, 149 | eqtr3d 2778 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝐵 / 2) / (2↑𝑚)) + ((𝐵 / 2) / (2↑𝑚))) = (𝐵 / (2↑𝑚))) | 
| 151 | 150 | oveq1d 7447 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((((𝐵 / 2) / (2↑𝑚)) + ((𝐵 / 2) / (2↑𝑚))) − (1st ‘(𝐹‘𝑚))) = ((𝐵 / (2↑𝑚)) − (1st ‘(𝐹‘𝑚)))) | 
| 152 | 142, 151 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((𝐵 / 2) / (2↑𝑚)) − ((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚)))) = ((𝐵 / (2↑𝑚)) − (1st ‘(𝐹‘𝑚)))) | 
| 153 | 152 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((2nd
‘(𝐹‘𝑚)) + (((𝐵 / 2) / (2↑𝑚)) − ((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚))))) = ((2nd ‘(𝐹‘𝑚)) + ((𝐵 / (2↑𝑚)) − (1st ‘(𝐹‘𝑚))))) | 
| 154 | 138, 141,
153 | 3eqtr4d 2786 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((((abs ∘
− ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))) = ((2nd ‘(𝐹‘𝑚)) + (((𝐵 / 2) / (2↑𝑚)) − ((1st ‘(𝐹‘𝑚)) − ((𝐵 / 2) / (2↑𝑚)))))) | 
| 155 | 136, 137,
154 | 3eqtr4d 2786 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((2nd
‘(𝐺‘𝑚)) − (1st
‘(𝐺‘𝑚))) = ((((abs ∘ − )
∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚)))) | 
| 156 | 131, 155 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑚) = ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚)))) | 
| 157 | 119, 156 | sylan2 593 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘
𝐺)‘𝑚) = ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚)))) | 
| 158 | 157 | adantlr 715 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘
𝐺)‘𝑚) = ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚)))) | 
| 159 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) | 
| 160 |  | nnuz 12922 | . . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) | 
| 161 | 159, 160 | eleqtrdi 2850 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) | 
| 162 | 123, 128 | addcld 11281 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → ((((abs ∘ − ) ∘
𝐹)‘𝑚) + (𝐵 / (2↑𝑚))) ∈ ℂ) | 
| 163 | 158, 161,
162 | fsumser 15767 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))) = (seq1( + , ((abs ∘ − )
∘ 𝐺))‘𝑘)) | 
| 164 |  | eqidd 2737 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘
𝐹)‘𝑚) = (((abs ∘ − ) ∘ 𝐹)‘𝑚)) | 
| 165 | 164, 161,
123 | fsumser 15767 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(((abs ∘ − ) ∘ 𝐹)‘𝑚) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑘)) | 
| 166 |  | ovollb2.1 | . . . . . . . . . . 11
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) | 
| 167 | 166 | fveq1i 6906 | . . . . . . . . . 10
⊢ (𝑆‘𝑘) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑘) | 
| 168 | 165, 167 | eqtr4di 2794 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(((abs ∘ − ) ∘ 𝐹)‘𝑚) = (𝑆‘𝑘)) | 
| 169 | 11 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐵 ∈
ℝ+) | 
| 170 | 169 | rpcnd 13080 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℂ) | 
| 171 |  | geo2sum 15910 | . . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ∧ 𝐵 ∈ ℂ) →
Σ𝑚 ∈ (1...𝑘)(𝐵 / (2↑𝑚)) = (𝐵 − (𝐵 / (2↑𝑘)))) | 
| 172 | 159, 170,
171 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(𝐵 / (2↑𝑚)) = (𝐵 − (𝐵 / (2↑𝑘)))) | 
| 173 | 168, 172 | oveq12d 7450 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (Σ𝑚 ∈ (1...𝑘)(((abs ∘ − ) ∘ 𝐹)‘𝑚) + Σ𝑚 ∈ (1...𝑘)(𝐵 / (2↑𝑚))) = ((𝑆‘𝑘) + (𝐵 − (𝐵 / (2↑𝑘))))) | 
| 174 | 129, 163,
173 | 3eqtr3d 2784 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , ((abs
∘ − ) ∘ 𝐺))‘𝑘) = ((𝑆‘𝑘) + (𝐵 − (𝐵 / (2↑𝑘))))) | 
| 175 | 112, 174 | eqtrid 2788 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) = ((𝑆‘𝑘) + (𝐵 − (𝐵 / (2↑𝑘))))) | 
| 176 | 115, 166 | ovolsf 25508 | . . . . . . . . . 10
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) | 
| 177 | 2, 176 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞)) | 
| 178 | 177 | ffvelcdmda 7103 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ (0[,)+∞)) | 
| 179 | 114, 178 | sselid 3980 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ℝ) | 
| 180 | 169 | rpred 13078 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℝ) | 
| 181 |  | nnnn0 12535 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) | 
| 182 | 181 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ0) | 
| 183 |  | nnexpcl 14116 | . . . . . . . . . . . 12
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℕ0) → (2↑𝑘) ∈ ℕ) | 
| 184 | 14, 182, 183 | sylancr 587 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2↑𝑘) ∈
ℕ) | 
| 185 | 184 | nnrpd 13076 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2↑𝑘) ∈
ℝ+) | 
| 186 | 169, 185 | rpdivcld 13095 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐵 / (2↑𝑘)) ∈
ℝ+) | 
| 187 | 186 | rpred 13078 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐵 / (2↑𝑘)) ∈ ℝ) | 
| 188 | 180, 187 | resubcld 11692 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐵 − (𝐵 / (2↑𝑘))) ∈ ℝ) | 
| 189 | 46 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < )
∈ ℝ) | 
| 190 | 177 | frnd 6743 | . . . . . . . . . 10
⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞)) | 
| 191 | 190, 42 | sstrdi 3995 | . . . . . . . . 9
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) | 
| 192 | 191 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑆 ⊆
ℝ*) | 
| 193 | 177 | ffnd 6736 | . . . . . . . . 9
⊢ (𝜑 → 𝑆 Fn ℕ) | 
| 194 |  | fnfvelrn 7099 | . . . . . . . . 9
⊢ ((𝑆 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ran 𝑆) | 
| 195 | 193, 194 | sylan 580 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ran 𝑆) | 
| 196 |  | supxrub 13367 | . . . . . . . 8
⊢ ((ran
𝑆 ⊆
ℝ* ∧ (𝑆‘𝑘) ∈ ran 𝑆) → (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, <
)) | 
| 197 | 192, 195,
196 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, <
)) | 
| 198 | 180, 186 | ltsubrpd 13110 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐵 − (𝐵 / (2↑𝑘))) < 𝐵) | 
| 199 | 188, 180,
198 | ltled 11410 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐵 − (𝐵 / (2↑𝑘))) ≤ 𝐵) | 
| 200 | 179, 188,
189, 180, 197, 199 | le2addd 11883 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑆‘𝑘) + (𝐵 − (𝐵 / (2↑𝑘)))) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵)) | 
| 201 | 175, 200 | eqbrtrd 5164 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑇‘𝑘) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵)) | 
| 202 | 201 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵)) | 
| 203 |  | ffn 6735 | . . . . 5
⊢ (𝑇:ℕ⟶(0[,)+∞)
→ 𝑇 Fn
ℕ) | 
| 204 |  | breq1 5145 | . . . . . 6
⊢ (𝑦 = (𝑇‘𝑘) → (𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ↔ (𝑇‘𝑘) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))) | 
| 205 | 204 | ralrn 7107 | . . . . 5
⊢ (𝑇 Fn ℕ →
(∀𝑦 ∈ ran 𝑇 𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ↔ ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))) | 
| 206 | 40, 203, 205 | 3syl 18 | . . . 4
⊢ (𝜑 → (∀𝑦 ∈ ran 𝑇 𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ↔ ∀𝑘 ∈ ℕ (𝑇‘𝑘) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))) | 
| 207 | 202, 206 | mpbird 257 | . . 3
⊢ (𝜑 → ∀𝑦 ∈ ran 𝑇 𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵)) | 
| 208 |  | supxrleub 13369 | . . . 4
⊢ ((ran
𝑇 ⊆
ℝ* ∧ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ∈ ℝ*)
→ (sup(ran 𝑇,
ℝ*, < ) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ↔ ∀𝑦 ∈ ran 𝑇 𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))) | 
| 209 | 43, 49, 208 | syl2anc 584 | . . 3
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) ≤ (sup(ran
𝑆, ℝ*,
< ) + 𝐵) ↔
∀𝑦 ∈ ran 𝑇 𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))) | 
| 210 | 207, 209 | mpbird 257 | . 2
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ (sup(ran
𝑆, ℝ*,
< ) + 𝐵)) | 
| 211 | 7, 45, 49, 111, 210 | xrletrd 13205 | 1
⊢ (𝜑 → (vol*‘𝐴) ≤ (sup(ran 𝑆, ℝ*, < ) +
𝐵)) |