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		elovolmlem	⊢ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ↔ 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
31	30	bilani	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
32		inss2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
33		rexpssxrxp	⊢ ( ℝ × ℝ ) ⊆ ( ℝ^* × ℝ^* )
34	32 33	sstri	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ^* × ℝ^* )
35		fss	⊢ ( ( 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ^* × ℝ^* ) ) → 𝑓 : ℕ ⟶ ( ℝ^* × ℝ^* ) )
36	31 34 35	sylancl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → 𝑓 : ℕ ⟶ ( ℝ^* × ℝ^* ) )
37		fco	⊢ ( ( (,) : ( ℝ^* × ℝ^* ) ⟶ ran (,) ∧ 𝑓 : ℕ ⟶ ( ℝ^* × ℝ^* ) ) → ( (,) ∘ 𝑓 ) : ℕ ⟶ ran (,) )
38	29 36 37	sylancr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → ( (,) ∘ 𝑓 ) : ℕ ⟶ ran (,) )
39	38	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ( (,) ∘ 𝑓 ) : ℕ ⟶ ran (,) )
40	39	frnd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ran ( (,) ∘ 𝑓 ) ⊆ ran (,) )
41		retopbas	⊢ ran (,) ∈ TopBases
42		bastg	⊢ ( ran (,) ∈ TopBases → ran (,) ⊆ ( topGen ‘ ran (,) ) )
43	41 42	ax-mp	⊢ ran (,) ⊆ ( topGen ‘ ran (,) )
44	40 43	sstrdi	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ran ( (,) ∘ 𝑓 ) ⊆ ( topGen ‘ ran (,) ) )
45		fvex	⊢ ( topGen ‘ ran (,) ) ∈ V
46	45	elpw2	⊢ ( ran ( (,) ∘ 𝑓 ) ∈ 𝒫 ( topGen ‘ ran (,) ) ↔ ran ( (,) ∘ 𝑓 ) ⊆ ( topGen ‘ ran (,) ) )
47	44 46	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ran ( (,) ∘ 𝑓 ) ∈ 𝒫 ( topGen ‘ ran (,) ) )
48	12 24 47	rspcdva	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) → ∃ 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) )
49	6 48	mpd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ∃ 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 )
50		simprl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) )
51		elin	⊢ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ↔ ( 𝑣 ∈ 𝒫 ran ( (,) ∘ 𝑓 ) ∧ 𝑣 ∈ Fin ) )
52	50 51	sylib	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( 𝑣 ∈ 𝒫 ran ( (,) ∘ 𝑓 ) ∧ 𝑣 ∈ Fin ) )
53	52	simprd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → 𝑣 ∈ Fin )
54	52	simpld	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → 𝑣 ∈ 𝒫 ran ( (,) ∘ 𝑓 ) )
55	54	elpwid	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → 𝑣 ⊆ ran ( (,) ∘ 𝑓 ) )
56	55	sseld	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( 𝑡 ∈ 𝑣 → 𝑡 ∈ ran ( (,) ∘ 𝑓 ) ) )
57	38	ffnd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → ( (,) ∘ 𝑓 ) Fn ℕ )
58	57	adantr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( (,) ∘ 𝑓 ) Fn ℕ )
59		fvelrnb	⊢ ( ( (,) ∘ 𝑓 ) Fn ℕ → ( 𝑡 ∈ ran ( (,) ∘ 𝑓 ) ↔ ∃ 𝑘 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑘 ) = 𝑡 ) )
60	58 59	syl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( 𝑡 ∈ ran ( (,) ∘ 𝑓 ) ↔ ∃ 𝑘 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑘 ) = 𝑡 ) )
61	56 60	sylibd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( 𝑡 ∈ 𝑣 → ∃ 𝑘 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑘 ) = 𝑡 ) )
62	61	ralrimiv	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ∀ 𝑡 ∈ 𝑣 ∃ 𝑘 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑘 ) = 𝑡 )
63		fveqeq2	⊢ ( 𝑘 = ( 𝑔 ‘ 𝑡 ) → ( ( ( (,) ∘ 𝑓 ) ‘ 𝑘 ) = 𝑡 ↔ ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) )
64	63	ac6sfi	⊢ ( ( 𝑣 ∈ Fin ∧ ∀ 𝑡 ∈ 𝑣 ∃ 𝑘 ∈ ℕ ( ( (,) ∘ 𝑓 ) ‘ 𝑘 ) = 𝑡 ) → ∃ 𝑔 ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) )
65	53 62 64	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ∃ 𝑔 ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) )
66	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → 𝐴 ∈ ℝ )
67	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → 𝐵 ∈ ℝ )
68	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → 𝐴 ≤ 𝐵 )
69		eqid	⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) )
70	31	adantr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → 𝑓 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
71		simprll	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) )
72		simprlr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 )
73		simprrl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → 𝑔 : 𝑣 ⟶ ℕ )
74		simprrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 )
75		2fveq3	⊢ ( 𝑡 = 𝑥 → ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑥 ) ) )
76		id	⊢ ( 𝑡 = 𝑥 → 𝑡 = 𝑥 )
77	75 76	eqeq12d	⊢ ( 𝑡 = 𝑥 → ( ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ↔ ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑥 ) ) = 𝑥 ) )
78	77	rspccva	⊢ ( ( ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ∧ 𝑥 ∈ 𝑣 ) → ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑥 ) ) = 𝑥 )
79	74 78	sylan	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) ∧ 𝑥 ∈ 𝑣 ) → ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑥 ) ) = 𝑥 )
80		eqid	⊢ { 𝑢 ∈ 𝑣 ∣ ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ } = { 𝑢 ∈ 𝑣 ∣ ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ }
81	66 67 68 69 70 71 72 73 79 80	ovolicc2lem5	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ∧ ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) ) ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) )
82	81	expr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) )
83	82	exlimdv	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( ∃ 𝑔 ( 𝑔 : 𝑣 ⟶ ℕ ∧ ∀ 𝑡 ∈ 𝑣 ( ( (,) ∘ 𝑓 ) ‘ ( 𝑔 ‘ 𝑡 ) ) = 𝑡 ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) )
84	65 83	mpd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) ∧ ( 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 ) ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) )
85	84	rexlimdvaa	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → ( ∃ 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 → ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) )
86	85	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ( ∃ 𝑣 ∈ ( 𝒫 ran ( (,) ∘ 𝑓 ) ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑣 → ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) )
87	49 86	mpd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) )
88		breq2	⊢ ( 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) → ( ( 𝐵 − 𝐴 ) ≤ 𝑧 ↔ ( 𝐵 − 𝐴 ) ≤ sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) )
89	87 88	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ) ) → ( 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) → ( 𝐵 − 𝐴 ) ≤ 𝑧 ) )
90	89	expr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) → ( 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) → ( 𝐵 − 𝐴 ) ≤ 𝑧 ) ) )
91	90	impd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ) → ( ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) → ( 𝐵 − 𝐴 ) ≤ 𝑧 ) )
92	91	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) → ( 𝐵 − 𝐴 ) ≤ 𝑧 ) )
93	5 92	biimtrid	⊢ ( 𝜑 → ( 𝑧 ∈ 𝑀 → ( 𝐵 − 𝐴 ) ≤ 𝑧 ) )
94	93	ralrimiv	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑀 ( 𝐵 − 𝐴 ) ≤ 𝑧 )
95	4	ssrab3	⊢ 𝑀 ⊆ ℝ^*
96	2 1	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
97	96	rexrd	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ^* )
98		infxrgelb	⊢ ( ( 𝑀 ⊆ ℝ^* ∧ ( 𝐵 − 𝐴 ) ∈ ℝ^* ) → ( ( 𝐵 − 𝐴 ) ≤ inf ( 𝑀 , ℝ^* , < ) ↔ ∀ 𝑧 ∈ 𝑀 ( 𝐵 − 𝐴 ) ≤ 𝑧 ) )
99	95 97 98	sylancr	⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) ≤ inf ( 𝑀 , ℝ^* , < ) ↔ ∀ 𝑧 ∈ 𝑀 ( 𝐵 − 𝐴 ) ≤ 𝑧 ) )
100	94 99	mpbird	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ inf ( 𝑀 , ℝ^* , < ) )
101	4	ovolval	⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) = inf ( 𝑀 , ℝ^* , < ) )
102	19 101	syl	⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) = inf ( 𝑀 , ℝ^* , < ) )
103	100 102	breqtrrd	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) )

Metamath Proof Explorer

Theorem ovolicc2

Proof