Metamath Proof Explorer


Theorem ovolicc

Description: The measure of a closed interval. (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Assertion ovolicc ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵 ) → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐵𝐴 ) )

Proof

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* ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐵𝐴 ) )