Step |
Hyp |
Ref |
Expression |
1 |
|
iccssre |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) |
2 |
1
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) |
3 |
|
ovolcl |
⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ℝ* ) |
4 |
2 3
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ℝ* ) |
5 |
|
simp2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ ) |
6 |
|
simp1 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ ) |
7 |
5 6
|
resubcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 𝐵 − 𝐴 ) ∈ ℝ ) |
8 |
7
|
rexrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 𝐵 − 𝐴 ) ∈ ℝ* ) |
9 |
|
simp3 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 ) |
10 |
|
eqeq1 |
⊢ ( 𝑚 = 𝑛 → ( 𝑚 = 1 ↔ 𝑛 = 1 ) ) |
11 |
10
|
ifbid |
⊢ ( 𝑚 = 𝑛 → if ( 𝑚 = 1 , 〈 𝐴 , 𝐵 〉 , 〈 0 , 0 〉 ) = if ( 𝑛 = 1 , 〈 𝐴 , 𝐵 〉 , 〈 0 , 0 〉 ) ) |
12 |
11
|
cbvmptv |
⊢ ( 𝑚 ∈ ℕ ↦ if ( 𝑚 = 1 , 〈 𝐴 , 𝐵 〉 , 〈 0 , 0 〉 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 = 1 , 〈 𝐴 , 𝐵 〉 , 〈 0 , 0 〉 ) ) |
13 |
6 5 9 12
|
ovolicc1 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) ≤ ( 𝐵 − 𝐴 ) ) |
14 |
|
eqeq1 |
⊢ ( 𝑧 = 𝑦 → ( 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ↔ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ) |
15 |
14
|
anbi2d |
⊢ ( 𝑧 = 𝑦 → ( ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ↔ ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ) ) |
16 |
15
|
rexbidv |
⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ↔ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ) ) |
17 |
16
|
cbvrabv |
⊢ { 𝑧 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } |
18 |
6 5 9 17
|
ovolicc2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 𝐵 − 𝐴 ) ≤ ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) ) |
19 |
4 8 13 18
|
xrletrid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐵 − 𝐴 ) ) |