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 25539

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 4293	. . 3 ⊢ ((𝐴(,)𝐵) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝐴(,)𝐵))
2		elioore 13328	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝐴(,)𝐵) → 𝑧 ∈ ℝ)
3	2	adantr 480	. . . . . . . . 9 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝑧 ∈ ℝ)
4		peano2re 11319	. . . . . . . . . 10 ⊢ ((vol‘(𝐴(,)𝐵)) ∈ ℝ → ((vol‘(𝐴(,)𝐵)) + 1) ∈ ℝ)
5	4	adantl 481	. . . . . . . . 9 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → ((vol‘(𝐴(,)𝐵)) + 1) ∈ ℝ)
6	3, 5	resubcld 11578	. . . . . . . 8 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ)
7	6	rexrd 11195	. . . . . . 7 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ^*)
8		eliooxr 13357	. . . . . . . . 9 ⊢ (𝑧 ∈ (𝐴(,)𝐵) → (𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*))
9	8	adantr 480	. . . . . . . 8 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ∈ ℝ^ ∧ 𝐵 ∈ ℝ^*))
10	9	simpld 494	. . . . . . 7 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → 𝐴 ∈ ℝ^)
11	3	rexrd 11195	. . . . . . 7 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → 𝑧 ∈ ℝ^)
12		ltp1 11995	. . . . . . . . 9 ⊢ ((vol‘(𝐴(,)𝐵)) ∈ ℝ → (vol‘(𝐴(,)𝐵)) < ((vol*‘(𝐴(,)𝐵)) + 1))
13	12	adantl 481	. . . . . . . 8 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (vol‘(𝐴(,)𝐵)) < ((vol*‘(𝐴(,)𝐵)) + 1))
14		0red 11147	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 0 ∈ ℝ)
15		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (vol‘(𝐴(,)𝐵)) ∈ ℝ)
16		ioossre 13360	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴(,)𝐵) ⊆ ℝ
17		ovolge0 25448	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴(,)𝐵) ⊆ ℝ → 0 ≤ (vol*‘(𝐴(,)𝐵)))
18	16, 17	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → 0 ≤ (vol‘(𝐴(,)𝐵)))
19		lep1 11996	. . . . . . . . . . . . . . . . 17 ⊢ ((vol‘(𝐴(,)𝐵)) ∈ ℝ → (vol‘(𝐴(,)𝐵)) ≤ ((vol*‘(𝐴(,)𝐵)) + 1))
20	19	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (vol‘(𝐴(,)𝐵)) ≤ ((vol*‘(𝐴(,)𝐵)) + 1))
21	14, 15, 5, 18, 20	letrd 11303	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → 0 ≤ ((vol‘(𝐴(,)𝐵)) + 1))
22	3, 5	subge02d 11742	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (0 ≤ ((vol‘(𝐴(,)𝐵)) + 1) ↔ (𝑧 − ((vol*‘(𝐴(,)𝐵)) + 1)) ≤ 𝑧))
23	21, 22	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝑧)
24		ovolioo 25535	. . . . . . . . . . . . . 14 ⊢ (((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝑧) → (vol‘((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧)) = (𝑧 − (𝑧 − ((vol*‘(𝐴(,)𝐵)) + 1))))
25	6, 3, 23, 24	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (vol‘((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧)) = (𝑧 − (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))))
26	3	recnd 11173	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝑧 ∈ ℂ)
27	5	recnd 11173	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → ((vol‘(𝐴(,)𝐵)) + 1) ∈ ℂ)
28	26, 27	nncand 11510	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧 − (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) = ((vol*‘(𝐴(,)𝐵)) + 1))
29	25, 28	eqtrd 2771	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (vol‘((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧)) = ((vol‘(𝐴(,)𝐵)) + 1))
30	29	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ 𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) → (vol‘((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧)) = ((vol*‘(𝐴(,)𝐵)) + 1))
31		iooss1 13333	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) → ((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧) ⊆ (𝐴(,)𝑧))
32	10, 31	sylan 581	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ 𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) → ((𝑧 − ((vol*‘(𝐴(,)𝐵)) + 1))(,)𝑧) ⊆ (𝐴(,)𝑧))
33	9	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → 𝐵 ∈ ℝ^)
34		eliooord 13358	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ (𝐴(,)𝐵) → (𝐴 < 𝑧 ∧ 𝑧 < 𝐵))
35	34	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 < 𝑧 ∧ 𝑧 < 𝐵))
36	35	simprd 495	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝑧 < 𝐵)
37	11, 33, 36	xrltled 13101	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝑧 ≤ 𝐵)
38		iooss2 13334	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝑧 ≤ 𝐵) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵))
39	33, 37, 38	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵))
40	39	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ 𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵))
41	32, 40	sstrd 3932	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ 𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) → ((𝑧 − ((vol*‘(𝐴(,)𝐵)) + 1))(,)𝑧) ⊆ (𝐴(,)𝐵))
42		ovolss 25452	. . . . . . . . . . . 12 ⊢ ((((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧) ⊆ (𝐴(,)𝐵) ∧ (𝐴(,)𝐵) ⊆ ℝ) → (vol‘((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧)) ≤ (vol‘(𝐴(,)𝐵)))
43	41, 16, 42	sylancl 587	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ 𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) → (vol‘((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))(,)𝑧)) ≤ (vol*‘(𝐴(,)𝐵)))
44	30, 43	eqbrtrrd 5109	. . . . . . . . . 10 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ 𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1))) → ((vol‘(𝐴(,)𝐵)) + 1) ≤ (vol‘(𝐴(,)𝐵)))
45	44	ex 412	. . . . . . . . 9 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) → ((vol‘(𝐴(,)𝐵)) + 1) ≤ (vol‘(𝐴(,)𝐵))))
46	10, 7	xrlenltd 11211	. . . . . . . . 9 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ≤ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) ↔ ¬ (𝑧 − ((vol*‘(𝐴(,)𝐵)) + 1)) < 𝐴))
47	5, 15	lenltd 11292	. . . . . . . . 9 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (((vol‘(𝐴(,)𝐵)) + 1) ≤ (vol‘(𝐴(,)𝐵)) ↔ ¬ (vol‘(𝐴(,)𝐵)) < ((vol*‘(𝐴(,)𝐵)) + 1)))
48	45, 46, 47	3imtr3d 293	. . . . . . . 8 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (¬ (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) < 𝐴 → ¬ (vol‘(𝐴(,)𝐵)) < ((vol‘(𝐴(,)𝐵)) + 1)))
49	13, 48	mt4d 117	. . . . . . 7 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) < 𝐴)
50	35	simpld 494	. . . . . . 7 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝐴 < 𝑧)
51		xrre2 13122	. . . . . . 7 ⊢ ((((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ^ ∧ 𝐴 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧 − ((vol‘(𝐴(,)𝐵)) + 1)) < 𝐴 ∧ 𝐴 < 𝑧)) → 𝐴 ∈ ℝ)
52	7, 10, 11, 49, 50, 51	syl32anc 1381	. . . . . 6 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝐴 ∈ ℝ)
53	3, 5	readdcld 11174	. . . . . . . 8 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ)
54	53	rexrd 11195	. . . . . . 7 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ^*)
55	3, 5	addge01d 11738	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (0 ≤ ((vol‘(𝐴(,)𝐵)) + 1) ↔ 𝑧 ≤ (𝑧 + ((vol*‘(𝐴(,)𝐵)) + 1))))
56	21, 55	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → 𝑧 ≤ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))
57		ovolioo 25535	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ ∧ 𝑧 ≤ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1))) → (vol‘(𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))) = ((𝑧 + ((vol*‘(𝐴(,)𝐵)) + 1)) − 𝑧))
58	3, 53, 56, 57	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (vol‘(𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))) = ((𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) − 𝑧))
59	26, 27	pncan2d 11507	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → ((𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) − 𝑧) = ((vol*‘(𝐴(,)𝐵)) + 1))
60	58, 59	eqtrd 2771	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (vol‘(𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))) = ((vol‘(𝐴(,)𝐵)) + 1))
61	60	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵) → (vol‘(𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))) = ((vol*‘(𝐴(,)𝐵)) + 1))
62		iooss2 13334	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ ℝ^* ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵) → (𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1))) ⊆ (𝑧(,)𝐵))
63	33, 62	sylan 581	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵) → (𝑧(,)(𝑧 + ((vol*‘(𝐴(,)𝐵)) + 1))) ⊆ (𝑧(,)𝐵))
64	10, 11, 50	xrltled 13101	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝐴 ≤ 𝑧)
65		iooss1 13333	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≤ 𝑧) → (𝑧(,)𝐵) ⊆ (𝐴(,)𝐵))
66	10, 64, 65	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝑧(,)𝐵) ⊆ (𝐴(,)𝐵))
67	66	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵) → (𝑧(,)𝐵) ⊆ (𝐴(,)𝐵))
68	63, 67	sstrd 3932	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵) → (𝑧(,)(𝑧 + ((vol*‘(𝐴(,)𝐵)) + 1))) ⊆ (𝐴(,)𝐵))
69		ovolss 25452	. . . . . . . . . . . 12 ⊢ (((𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1))) ⊆ (𝐴(,)𝐵) ∧ (𝐴(,)𝐵) ⊆ ℝ) → (vol‘(𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))) ≤ (vol‘(𝐴(,)𝐵)))
70	68, 16, 69	sylancl 587	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵) → (vol‘(𝑧(,)(𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))) ≤ (vol*‘(𝐴(,)𝐵)))
71	61, 70	eqbrtrrd 5109	. . . . . . . . . 10 ⊢ (((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵) → ((vol‘(𝐴(,)𝐵)) + 1) ≤ (vol‘(𝐴(,)𝐵)))
72	71	ex 412	. . . . . . . . 9 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → ((𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵 → ((vol‘(𝐴(,)𝐵)) + 1) ≤ (vol‘(𝐴(,)𝐵))))
73	54, 33	xrlenltd 11211	. . . . . . . . 9 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → ((𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ≤ 𝐵 ↔ ¬ 𝐵 < (𝑧 + ((vol*‘(𝐴(,)𝐵)) + 1))))
74	72, 73, 47	3imtr3d 293	. . . . . . . 8 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → (¬ 𝐵 < (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) → ¬ (vol‘(𝐴(,)𝐵)) < ((vol‘(𝐴(,)𝐵)) + 1)))
75	13, 74	mt4d 117	. . . . . . 7 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ) → 𝐵 < (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)))
76		xrre2 13122	. . . . . . 7 ⊢ (((𝑧 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑧 + ((vol‘(𝐴(,)𝐵)) + 1)) ∈ ℝ^) ∧ (𝑧 < 𝐵 ∧ 𝐵 < (𝑧 + ((vol*‘(𝐴(,)𝐵)) + 1)))) → 𝐵 ∈ ℝ)
77	11, 33, 54, 36, 75, 76	syl32anc 1381	. . . . . 6 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → 𝐵 ∈ ℝ)
78	52, 77	jca 511	. . . . 5 ⊢ ((𝑧 ∈ (𝐴(,)𝐵) ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
79	78	ex 412	. . . 4 ⊢ (𝑧 ∈ (𝐴(,)𝐵) → ((vol*‘(𝐴(,)𝐵)) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)))
80	79	exlimiv 1932	. . 3 ⊢ (∃𝑧 𝑧 ∈ (𝐴(,)𝐵) → ((vol*‘(𝐴(,)𝐵)) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)))
81	1, 80	sylbi 217	. 2 ⊢ ((𝐴(,)𝐵) ≠ ∅ → ((vol*‘(𝐴(,)𝐵)) ∈ ℝ → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)))
82	81	imp 406	1 ⊢ (((𝐴(,)𝐵) ≠ ∅ ∧ (vol*‘(𝐴(,)𝐵)) ∈ ℝ) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2932 ⊆ wss 3889 ∅c0 4273 class class class wbr 5085 ‘cfv 6498 (class class class)co 7367 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 ℝ^*cxr 11178 < clt 11179 ≤ cle 11180 − cmin 11377 (,)cioo 13298 vol*covol 25429

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-inf2 9562 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-isom 6507 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-of 7631 df-om 7818 df-1st 7942 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-2o 8406 df-er 8643 df-map 8775 df-pm 8776 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-fi 9324 df-sup 9355 df-inf 9356 df-oi 9425 df-dju 9825 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-n0 12438 df-z 12525 df-uz 12789 df-q 12899 df-rp 12943 df-xneg 13063 df-xadd 13064 df-xmul 13065 df-ioo 13302 df-ico 13304 df-icc 13305 df-fz 13462 df-fzo 13609 df-fl 13751 df-seq 13964 df-exp 14024 df-hash 14293 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198 df-clim 15450 df-rlim 15451 df-sum 15649 df-rest 17385 df-topgen 17406 df-psmet 21344 df-xmet 21345 df-met 21346 df-bl 21347 df-mopn 21348 df-top 22859 df-topon 22876 df-bases 22911 df-cmp 23352 df-ovol 25431 df-vol 25432

This theorem is referenced by: ioorcl 25544

W3C validator