ovolicc2

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

	Ref	Expression
Hypotheses	ovolicc.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ovolicc.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ovolicc.3	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	ovolicc2.m	⊢ 𝑀 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) }
Assertion	ovolicc2	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ovolicc.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		ovolicc.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		ovolicc.3	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4		ovolicc2.m	⊢ 𝑀 = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) }
5	4	elovolm	⊢ ( 𝑧 ∈ 𝑀 ↔ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) )
6		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) )
7		unieq	⊢ ( 𝑢 = ran ( (,) ∘ 𝑓 ) → ∪ 𝑢 = ∪ ran ( (,) ∘ 𝑓 ) )
8	7	sseq2d	⊢ ( 𝑢 = ran ( (,) ∘ 𝑓 ) → ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 ↔ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) )
9		pweq	⊢ ( 𝑢 = ran ( (,) ∘ 𝑓 ) → 𝒫 𝑢 = 𝒫 ran ( (,) ∘ 𝑓 ) )
10	9	ineq1d	⊢ ( 𝑢 = ran ( (,) ∘ 𝑓 ) → ( 𝒫 𝑢 ∩ Fin ) = ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) )
11	10	rexeqdv	⊢ ( 𝑢 = ran ( (,) ∘ 𝑓 ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ↔ ∃ 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) )
12	8 11	imbi12d	⊢ ( 𝑢 = ran ( (,) ∘ 𝑓 ) → ( ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ↔ ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) → ∃ 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) )
13		eqid	⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
14		eqid	⊢ ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) )
15	13 14	icccmp	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) ) ∈ Comp )
16	1 2 15	syl2anc	⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) ) ∈ Comp )
17		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
18		iccssre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
19	1 2 18	syl2anc	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
20		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
21	20	cmpsub	⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) → ( ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) ) ∈ Comp ↔ ∀ 𝑢 ∈ 𝒫 ( topGen ‘ ran (,) ) ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) )
22	17 19 21	sylancr	⊢ ( 𝜑 → ( ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) ) ∈ Comp ↔ ∀ 𝑢 ∈ 𝒫 ( topGen ‘ ran (,) ) ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) )
23	16 22	mpbid	⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝒫 ( topGen ‘ ran (,) ) ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) )
24	23	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ∀ 𝑢 ∈ 𝒫 ( topGen ‘ ran (,) ) ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) )
25		ioof	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ
26		ffn	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ^* × ℝ^* ) )
27	25 26	ax-mp	⊢ (,) Fn ( ℝ^* × ℝ^* )
28		dffn3	⊢ ( (,) Fn ( ℝ^* × ℝ^* ) ↔ (,) : ( ℝ^* × ℝ^* ) ⟶ ran (,) )
29	27 28	mpbi	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ ran (,)
30		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) )
31		elovolmlem	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ↔ 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
32	30 31	sylib	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
33		inss2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
34		rexpssxrxp	⊢ ( ℝ × ℝ ) ⊆ ( ℝ^* × ℝ^* )
35	33 34	sstri	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ^* × ℝ^* )
36		fss	⊢ ( ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ^* × ℝ^* ) ) → 𝑓 : ℕ ⟶ ( ℝ^* × ℝ^* ) )
37	32 35 36	sylancl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → 𝑓 : ℕ ⟶ ( ℝ^* × ℝ^* ) )
38		fco	⊢ ( ( (,) : ( ℝ^* × ℝ^* ) ⟶ ran (,) ∧ 𝑓 : ℕ ⟶ ( ℝ^* × ℝ^* ) ) → ( (,) ∘ 𝑓 ) : ℕ ⟶ ran (,) )
39	29 37 38	sylancr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → ( (,) ∘ 𝑓 ) : ℕ ⟶ ran (,) )
40	39	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ( (,) ∘ 𝑓 ) : ℕ ⟶ ran (,) )
41	40	frnd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ran ( (,) ∘ 𝑓 ) ⊆ ran (,) )
42		retopbas	⊢ ran (,) ∈ TopBases
43		bastg	⊢ ( ran (,) ∈ TopBases → ran (,) ⊆ ( topGen ‘ ran (,) ) )
44	42 43	ax-mp	⊢ ran (,) ⊆ ( topGen ‘ ran (,) )
45	41 44	sstrdi	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ran ( (,) ∘ 𝑓 ) ⊆ ( topGen ‘ ran (,) ) )
46		fvex	⊢ ( topGen ‘ ran (,) ) ∈ V
47	46	elpw2	⊢ ( ran ( (,) ∘ 𝑓 ) ∈ 𝒫 ( topGen ‘ ran (,) ) ↔ ran ( (,) ∘ 𝑓 ) ⊆ ( topGen ‘ ran (,) ) )
48	45 47	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ran ( (,) ∘ 𝑓 ) ∈ 𝒫 ( topGen ‘ ran (,) ) )
49	12 24 48	rspcdva	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) → ∃ 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) )
50	6 49	mpd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ∃ 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 )
51		simprl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) )
52		elin	⊢ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ↔ ( 𝑣 ∈ 𝒫 ran ( (,) ∘ 𝑓 ) ∧ 𝑣 ∈ Fin ) )
53	51 52	sylib	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( 𝑣 ∈ 𝒫 ran ( (,) ∘ 𝑓 ) ∧ 𝑣 ∈ Fin ) )
54	53	simprd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → 𝑣 ∈ Fin )
55	53	simpld	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → 𝑣 ∈ 𝒫 ran ( (,) ∘ 𝑓 ) )
56	55	elpwid	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → 𝑣 ⊆ ran ( (,) ∘ 𝑓 ) )
57	56	sseld	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( 𝑡 ∈ 𝑣 → 𝑡 ∈ ran ( (,) ∘ 𝑓 ) ) )
58	39	ffnd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → ( (,) ∘ 𝑓 ) Fn ℕ )
59	58	adantr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( (,) ∘ 𝑓 ) Fn ℕ )
60		fvelrnb	⊢ ( ( (,) ∘ 𝑓 ) Fn ℕ → ( 𝑡 ∈ ran ( (,) ∘ 𝑓 ) ↔ ∃ 𝑘 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑘 ) = 𝑡 ) )
61	59 60	syl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( 𝑡 ∈ ran ( (,) ∘ 𝑓 ) ↔ ∃ 𝑘 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑘 ) = 𝑡 ) )
62	57 61	sylibd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( 𝑡 ∈ 𝑣 → ∃ 𝑘 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑘 ) = 𝑡 ) )
63	62	ralrimiv	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ∀ 𝑡 ∈ 𝑣 ∃ 𝑘 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑘 ) = 𝑡 )
64		fveqeq2	⊢ ( 𝑘 = ( 𝑔 ‘ 𝑡 ) → ( ( ( (,) ∘ 𝑓 ) ‘ 𝑘 ) = 𝑡 ↔ ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) )
65	64	ac6sfi	⊢ ( ( 𝑣 ∈ Fin ∧ ∀ 𝑡 ∈ 𝑣 ∃ 𝑘 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑘 ) = 𝑡 ) → ∃ 𝑔 ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) )
66	54 63 65	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ∃ 𝑔 ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) )
67	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → 𝐴 ∈ ℝ )
68	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → 𝐵 ∈ ℝ )
69	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → 𝐴 ≤ 𝐵 )
70		eqid	⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) )
71	32	adantr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
72		simprll	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) )
73		simprlr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 )
74		simprrl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → 𝑔 : 𝑣 ⟶ ℕ )
75		simprrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 )
76		2fveq3	⊢ ( 𝑡 = 𝑥 → ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑥 ) ) )
77		id	⊢ ( 𝑡 = 𝑥 → 𝑡 = 𝑥 )
78	76 77	eqeq12d	⊢ ( 𝑡 = 𝑥 → ( ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ↔ ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑥 ) ) = 𝑥 ) )
79	78	rspccva	⊢ ( ( ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ∧ 𝑥 ∈ 𝑣 ) → ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑥 ) ) = 𝑥 )
80	75 79	sylan	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) ∧ 𝑥 ∈ 𝑣 ) → ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑥 ) ) = 𝑥 )
81		eqid	⊢ { 𝑢 ∈ 𝑣 ∣ ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ } = { 𝑢 ∈ 𝑣 ∣ ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ }
82	67 68 69 70 71 72 73 74 80 81	ovolicc2lem5	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) )
83	82	expr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) )
84	83	exlimdv	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( ∃ 𝑔 ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) )
85	66 84	mpd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) )
86	85	rexlimdvaa	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → ( ∃ 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 → ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) )
87	86	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ( ∃ 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 → ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) )
88	50 87	mpd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) )
89		breq2	⊢ ( 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) → ( ( 𝐵 − 𝐴 ) ≤ 𝑧 ↔ ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) )
90	88 89	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ( 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) → ( 𝐵 − 𝐴 ) ≤ 𝑧 ) )
91	90	expr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) → ( 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) → ( 𝐵 − 𝐴 ) ≤ 𝑧 ) ) )
92	91	impd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → ( ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) → ( 𝐵 − 𝐴 ) ≤ 𝑧 ) )
93	92	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) → ( 𝐵 − 𝐴 ) ≤ 𝑧 ) )
94	5 93	syl5bi	⊢ ( 𝜑 → ( 𝑧 ∈ 𝑀 → ( 𝐵 − 𝐴 ) ≤ 𝑧 ) )
95	94	ralrimiv	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑀 ( 𝐵 − 𝐴 ) ≤ 𝑧 )
96	4	ssrab3	⊢ 𝑀 ⊆ ℝ^*
97	2 1	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
98	97	rexrd	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ^* )
99		infxrgelb	⊢ ( ( 𝑀 ⊆ ℝ^* ∧ ( 𝐵 − 𝐴 ) ∈ ℝ^* ) → ( ( 𝐵 − 𝐴 ) ≤ inf ( 𝑀 , ℝ^* , < ) ↔ ∀ 𝑧 ∈ 𝑀 ( 𝐵 − 𝐴 ) ≤ 𝑧 ) )
100	96 98 99	sylancr	⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) ≤ inf ( 𝑀 , ℝ^* , < ) ↔ ∀ 𝑧 ∈ 𝑀 ( 𝐵 − 𝐴 ) ≤ 𝑧 ) )
101	95 100	mpbird	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ inf ( 𝑀 , ℝ^* , < ) )
102	4	ovolval	⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) = inf ( 𝑀 , ℝ^* , < ) )
103	19 102	syl	⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) = inf ( 𝑀 , ℝ^* , < ) )
104	101 103	breqtrrd	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) )

Metamath Proof Explorer

Theorem ovolicc2

Proof