This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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