ioorcl2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ioorcl2		Structured version Visualization version GIF version

Theorem ioorcl2 24317

Description: An open interval with finite volume has real endpoints. (Contributed by Mario Carneiro, 26-Mar-2015.)

**Assertion**
Ref	Expression
ioorcl2	⊢ (((𝐴(,)𝐵) ≠ ∅ ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))

Proof of Theorem ioorcl2 Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		n0 4233	. . 3 ⊢ ((𝐴(,)𝐵) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝐴(,)𝐵))
2		elioore 12844	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝐴(,)𝐵) → 𝑧 ∈ ℝ)
3	2	adantr 484	. . . . . . . . 9 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝑧 ∈ ℝ)
4		peano2re 10884	. . . . . . . . . 10 ⊢ ((vol‘(𝐴(,)𝐵)) ∈ ℝ → ((vol‘(𝐴(,)𝐵)) + 1) ∈ ℝ)
5	4	adantl 485	. . . . . . . . 9 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → ((vol‘(𝐴(,)𝐵)) + 1) ∈ ℝ)
6	3, 5	resubcld 11139	. . . . . . . 8 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ)
7	6	rexrd 10762	. . . . . . 7 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ^*)
8		eliooxr 12872	. . . . . . . . 9 ⊢ (𝑧 ∈ (𝐴(,)𝐵) → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*))
9	8	adantr 484	. . . . . . . 8 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ∈ ℝ^ ∧ 𝐵 ∈ ℝ^*))
10	9	simpld 498	. . . . . . 7 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → 𝐴 ∈ ℝ^)
11	3	rexrd 10762	. . . . . . 7 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → 𝑧 ∈ ℝ^)
12		ltp1 11551	. . . . . . . . 9 ⊢ ((vol‘(𝐴(,)𝐵)) ∈ ℝ → (vol‘(𝐴(,)𝐵)) < ((vol*‘(𝐴(,)𝐵)) + 1))
13	12	adantl 485	. . . . . . . 8 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (vol‘(𝐴(,)𝐵)) < ((vol*‘(𝐴(,)𝐵)) + 1))
14		0red 10715	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 0 ∈ ℝ)
15		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (vol‘(𝐴(,)𝐵)) ∈ ℝ)
16		ioossre 12875	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴(,)𝐵) ⊆ ℝ
17		ovolge0 24226	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴(,)𝐵) ⊆ ℝ → 0 ≤ (vol*‘(𝐴(,)𝐵)))
18	16, 17	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → 0 ≤ (vol‘(𝐴(,)𝐵)))
19		lep1 11552	. . . . . . . . . . . . . . . . 17 ⊢ ((vol‘(𝐴(,)𝐵)) ∈ ℝ → (vol‘(𝐴(,)𝐵)) ≤ ((vol*‘(𝐴(,)𝐵)) + 1))
20	19	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (vol‘(𝐴(,)𝐵)) ≤ ((vol*‘(𝐴(,)𝐵)) + 1))
21	14, 15, 5, 18, 20	letrd 10868	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → 0 ≤ ((vol‘(𝐴(,)𝐵)) + 1))
22	3, 5	subge02d 11303	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (0 ≤ ((vol‘(𝐴(,)𝐵)) + 1) ↔ (𝑧 − ((vol*‘(𝐴(,)𝐵)) + 1)) ≤ 𝑧))
23	21, 22	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝑧)
24		ovolioo 24313	. . . . . . . . . . . . . 14 ⊢ (((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝑧) → (vol‘((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧)) = (𝑧 − (𝑧 − ((vol*‘(𝐴(,)𝐵)) + 1))))
25	6, 3, 23, 24	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (vol‘((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧)) = (𝑧 − (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))))
26	3	recnd 10740	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝑧 ∈ ℂ)
27	5	recnd 10740	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → ((vol‘(𝐴(,)𝐵)) + 1) ∈ ℂ)
28	26, 27	nncand 11073	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧 − (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) = ((vol*‘(𝐴(,)𝐵)) + 1))
29	25, 28	eqtrd 2773	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (vol‘((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧)) = ((vol‘(𝐴(,)𝐵)) + 1))
30	29	adantr 484	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ 𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) → (vol‘((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧)) = ((vol*‘(𝐴(,)𝐵)) + 1))
31		iooss1 12849	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) → ((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧) ⊆ (𝐴(,)𝑧))
32	10, 31	sylan 583	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ 𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) → ((𝑧 − ((vol*‘(𝐴(,)𝐵)) + 1))(,)𝑧) ⊆ (𝐴(,)𝑧))
33	9	simprd 499	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → 𝐵 ∈ ℝ^)
34		eliooord 12873	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑧 ∧ 𝑧 < 𝐵))
35	34	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 < 𝑧 ∧ 𝑧 < 𝐵))
36	35	simprd 499	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝑧 < 𝐵)
37	11, 33, 36	xrltled 12619	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝑧 ≤ 𝐵)
38		iooss2 12850	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝑧 ≤ 𝐵) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵))
39	33, 37, 38	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵))
40	39	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ 𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵))
41	32, 40	sstrd 3885	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ 𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) → ((𝑧 − ((vol*‘(𝐴(,)𝐵)) + 1))(,)𝑧) ⊆ (𝐴(,)𝐵))
42		ovolss 24230	. . . . . . . . . . . 12 ⊢ ((((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧) ⊆ (𝐴(,)𝐵) ∧ (𝐴(,)𝐵) ⊆ ℝ) → (vol‘((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧)) ≤ (vol‘(𝐴(,)𝐵)))
43	41, 16, 42	sylancl 589	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ 𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) → (vol‘((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧)) ≤ (vol*‘(𝐴(,)𝐵)))
44	30, 43	eqbrtrrd 5051	. . . . . . . . . 10 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ 𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) → ((vol‘(𝐴(,)𝐵)) + 1) ≤ (vol‘(𝐴(,)𝐵)))
45	44	ex 416	. . . . . . . . 9 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) → ((vol‘(𝐴(,)𝐵)) + 1) ≤ (vol‘(𝐴(,)𝐵))))
46	10, 7	xrlenltd 10778	. . . . . . . . 9 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) ↔ ¬ (𝑧 − ((vol*‘(𝐴(,)𝐵)) + 1)) < 𝐴))
47	5, 15	lenltd 10857	. . . . . . . . 9 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (((vol‘(𝐴(,)𝐵)) + 1) ≤ (vol‘(𝐴(,)𝐵)) ↔ ¬ (vol‘(𝐴(,)𝐵)) < ((vol*‘(𝐴(,)𝐵)) + 1)))
48	45, 46, 47	3imtr3d 296	. . . . . . . 8 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (¬ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) < 𝐴 → ¬ (vol‘(𝐴(,)𝐵)) < ((vol‘(𝐴(,)𝐵)) + 1)))
49	13, 48	mt4d 117	. . . . . . 7 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) < 𝐴)
50	35	simpld 498	. . . . . . 7 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝐴 < 𝑧)
51		xrre2 12639	. . . . . . 7 ⊢ ((((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ^ ∧ 𝐴 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) < 𝐴 ∧ 𝐴 < 𝑧)) → 𝐴 ∈ ℝ)
52	7, 10, 11, 49, 50, 51	syl32anc 1379	. . . . . 6 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝐴 ∈ ℝ)
53	3, 5	readdcld 10741	. . . . . . . 8 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ)
54	53	rexrd 10762	. . . . . . 7 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ^*)
55	3, 5	addge01d 11299	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (0 ≤ ((vol‘(𝐴(,)𝐵)) + 1) ↔ 𝑧 ≤ (𝑧 + ((vol*‘(𝐴(,)𝐵)) + 1))))
56	21, 55	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → 𝑧 ≤ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))
57		ovolioo 24313	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ ∧ 𝑧 ≤ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1))) → (vol‘(𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))) = ((𝑧 + ((vol*‘(𝐴(,)𝐵)) + 1)) − 𝑧))
58	3, 53, 56, 57	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (vol‘(𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))) = ((𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) − 𝑧))
59	26, 27	pncan2d 11070	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → ((𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) − 𝑧) = ((vol*‘(𝐴(,)𝐵)) + 1))
60	58, 59	eqtrd 2773	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (vol‘(𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))) = ((vol‘(𝐴(,)𝐵)) + 1))
61	60	adantr 484	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵) → (vol‘(𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))) = ((vol*‘(𝐴(,)𝐵)) + 1))
62		iooss2 12850	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ^* ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵) → (𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1))) ⊆ (𝑧(,)𝐵))
63	33, 62	sylan 583	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵) → (𝑧(,)(𝑧 + ((vol*‘(𝐴(,)𝐵)) + 1))) ⊆ (𝑧(,)𝐵))
64	10, 11, 50	xrltled 12619	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝐴 ≤ 𝑧)
65		iooss1 12849	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≤ 𝑧) → (𝑧(,)𝐵) ⊆ (𝐴(,)𝐵))
66	10, 64, 65	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧(,)𝐵) ⊆ (𝐴(,)𝐵))
67	66	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵) → (𝑧(,)𝐵) ⊆ (𝐴(,)𝐵))
68	63, 67	sstrd 3885	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵) → (𝑧(,)(𝑧 + ((vol*‘(𝐴(,)𝐵)) + 1))) ⊆ (𝐴(,)𝐵))
69		ovolss 24230	. . . . . . . . . . . 12 ⊢ (((𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1))) ⊆ (𝐴(,)𝐵) ∧ (𝐴(,)𝐵) ⊆ ℝ) → (vol‘(𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))) ≤ (vol‘(𝐴(,)𝐵)))
70	68, 16, 69	sylancl 589	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵) → (vol‘(𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))) ≤ (vol*‘(𝐴(,)𝐵)))
71	61, 70	eqbrtrrd 5051	. . . . . . . . . 10 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵) → ((vol‘(𝐴(,)𝐵)) + 1) ≤ (vol‘(𝐴(,)𝐵)))
72	71	ex 416	. . . . . . . . 9 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → ((𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵 → ((vol‘(𝐴(,)𝐵)) + 1) ≤ (vol‘(𝐴(,)𝐵))))
73	54, 33	xrlenltd 10778	. . . . . . . . 9 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → ((𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵 ↔ ¬ 𝐵 < (𝑧 + ((vol*‘(𝐴(,)𝐵)) + 1))))
74	72, 73, 47	3imtr3d 296	. . . . . . . 8 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (¬ 𝐵 < (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) → ¬ (vol‘(𝐴(,)𝐵)) < ((vol‘(𝐴(,)𝐵)) + 1)))
75	13, 74	mt4d 117	. . . . . . 7 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → 𝐵 < (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))
76		xrre2 12639	. . . . . . 7 ⊢ (((𝑧 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ^) ∧ (𝑧 < 𝐵 ∧ 𝐵 < (𝑧 + ((vol*‘(𝐴(,)𝐵)) + 1)))) → 𝐵 ∈ ℝ)
77	11, 33, 54, 36, 75, 76	syl32anc 1379	. . . . . 6 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝐵 ∈ ℝ)
78	52, 77	jca 515	. . . . 5 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
79	78	ex 416	. . . 4 ⊢ (𝑧 ∈ (𝐴(,)𝐵) → ((vol*‘(𝐴(,)𝐵)) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)))
80	79	exlimiv 1936	. . 3 ⊢ (∃𝑧 𝑧 ∈ (𝐴(,)𝐵) → ((vol*‘(𝐴(,)𝐵)) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)))
81	1, 80	sylbi 220	. 2 ⊢ ((𝐴(,)𝐵) ≠ ∅ → ((vol*‘(𝐴(,)𝐵)) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)))
82	81	imp 410	1 ⊢ (((𝐴(,)𝐵) ≠ ∅ ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 = wceq 1542 ∃wex 1786 ∈ wcel 2113 ≠ wne 2934 ⊆ wss 3841 ∅c0 4209 class class class wbr 5027 ‘cfv 6333 (class class class)co 7164 ℝcr 10607 0cc0 10608 1c1 10609 + caddc 10611 ℝ^*cxr 10745 < clt 10746 ≤ cle 10747 − cmin 10941 (,)cioo 12814 vol*covol 24207

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-rep 5151 ax-sep 5164 ax-nul 5171 ax-pow 5229 ax-pr 5293 ax-un 7473 ax-inf2 9170 ax-cnex 10664 ax-resscn 10665 ax-1cn 10666 ax-icn 10667 ax-addcl 10668 ax-addrcl 10669 ax-mulcl 10670 ax-mulrcl 10671 ax-mulcom 10672 ax-addass 10673 ax-mulass 10674 ax-distr 10675 ax-i2m1 10676 ax-1ne0 10677 ax-1rid 10678 ax-rnegex 10679 ax-rrecex 10680 ax-cnre 10681 ax-pre-lttri 10682 ax-pre-lttrn 10683 ax-pre-ltadd 10684 ax-pre-mulgt0 10685 ax-pre-sup 10686

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-pss 3860 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-tp 4518 df-op 4520 df-uni 4794 df-int 4834 df-iun 4880 df-br 5028 df-opab 5090 df-mpt 5108 df-tr 5134 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-se 5479 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6123 df-ord 6169 df-on 6170 df-lim 6171 df-suc 6172 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-isom 6342 df-riota 7121 df-ov 7167 df-oprab 7168 df-mpo 7169 df-of 7419 df-om 7594 df-1st 7707 df-2nd 7708 df-wrecs 7969 df-recs 8030 df-rdg 8068 df-1o 8124 df-2o 8125 df-er 8313 df-map 8432 df-pm 8433 df-en 8549 df-dom 8550 df-sdom 8551 df-fin 8552 df-fi 8941 df-sup 8972 df-inf 8973 df-oi 9040 df-dju 9396 df-card 9434 df-pnf 10748 df-mnf 10749 df-xr 10750 df-ltxr 10751 df-le 10752 df-sub 10943 df-neg 10944 df-div 11369 df-nn 11710 df-2 11772 df-3 11773 df-n0 11970 df-z 12056 df-uz 12318 df-q 12424 df-rp 12466 df-xneg 12583 df-xadd 12584 df-xmul 12585 df-ioo 12818 df-ico 12820 df-icc 12821 df-fz 12975 df-fzo 13118 df-fl 13246 df-seq 13454 df-exp 13515 df-hash 13776 df-cj 14541 df-re 14542 df-im 14543 df-sqrt 14677 df-abs 14678 df-clim 14928 df-rlim 14929 df-sum 15129 df-rest 16792 df-topgen 16813 df-psmet 20202 df-xmet 20203 df-met 20204 df-bl 20205 df-mopn 20206 df-top 21638 df-topon 21655 df-bases 21690 df-cmp 22131 df-ovol 24209 df-vol 24210

This theorem is referenced by: ioorcl 24322

W3C validator