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