qinioo

Description: The rational numbers are dense in RR . (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	qinioo.a	$⊢ φ \to A \in ℝ^{*}$
	qinioo.b	$⊢ φ \to B \in ℝ^{*}$
Assertion	qinioo	$⊢ φ \to (ℚ \cap (A, B) = \emptyset \leftrightarrow B \leq A)$

Proof

Step	Hyp	Ref	Expression
1		qinioo.a	$⊢ φ \to A \in ℝ^{*}$
2		qinioo.b	$⊢ φ \to B \in ℝ^{*}$
3		simplr	$⊢ ((φ \land ℚ \cap (A, B) = \emptyset) \land \neg B \leq A) \to ℚ \cap (A, B) = \emptyset$
4	1 2	xrltnled	$⊢ φ \to (A < B \leftrightarrow \neg B \leq A)$
5	4	biimpar	$⊢ (φ \land \neg B \leq A) \to A < B$
6	1	adantr	$⊢ (φ \land A < B) \to A \in ℝ^{*}$
7	2	adantr	$⊢ (φ \land A < B) \to B \in ℝ^{*}$
8		simpr	$⊢ (φ \land A < B) \to A < B$
9		qbtwnxr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to \exists q \in ℚ (A < q \land q < B)$
10	6 7 8 9	syl3anc	$⊢ (φ \land A < B) \to \exists q \in ℚ (A < q \land q < B)$
11	1	ad2antrr	$⊢ ((φ \land q \in ℚ) \land (A < q \land q < B)) \to A \in ℝ^{*}$
12	2	ad2antrr	$⊢ ((φ \land q \in ℚ) \land (A < q \land q < B)) \to B \in ℝ^{*}$
13		qre	$⊢ q \in ℚ \to q \in ℝ$
14	13	ad2antlr	$⊢ ((φ \land q \in ℚ) \land (A < q \land q < B)) \to q \in ℝ$
15		simprl	$⊢ ((φ \land q \in ℚ) \land (A < q \land q < B)) \to A < q$
16		simprr	$⊢ ((φ \land q \in ℚ) \land (A < q \land q < B)) \to q < B$
17	11 12 14 15 16	eliood	$⊢ ((φ \land q \in ℚ) \land (A < q \land q < B)) \to q \in (A, B)$
18	17	ex	$⊢ (φ \land q \in ℚ) \to ((A < q \land q < B) \to q \in (A, B))$
19	18	adantlr	$⊢ ((φ \land A < B) \land q \in ℚ) \to ((A < q \land q < B) \to q \in (A, B))$
20	19	reximdva	$⊢ (φ \land A < B) \to (\exists q \in ℚ (A < q \land q < B) \to \exists q \in ℚ q \in (A, B))$
21	10 20	mpd	$⊢ (φ \land A < B) \to \exists q \in ℚ q \in (A, B)$
22		inn0	$⊢ ℚ \cap (A, B) \neq \emptyset \leftrightarrow \exists q \in ℚ q \in (A, B)$
23	21 22	sylibr	$⊢ (φ \land A < B) \to ℚ \cap (A, B) \neq \emptyset$
24	5 23	syldan	$⊢ (φ \land \neg B \leq A) \to ℚ \cap (A, B) \neq \emptyset$
25	24	neneqd	$⊢ (φ \land \neg B \leq A) \to \neg ℚ \cap (A, B) = \emptyset$
26	25	adantlr	$⊢ ((φ \land ℚ \cap (A, B) = \emptyset) \land \neg B \leq A) \to \neg ℚ \cap (A, B) = \emptyset$
27	3 26	condan	$⊢ (φ \land ℚ \cap (A, B) = \emptyset) \to B \leq A$
28		ioo0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A, B) = \emptyset \leftrightarrow B \leq A)$
29	1 2 28	syl2anc	$⊢ φ \to ((A, B) = \emptyset \leftrightarrow B \leq A)$
30	29	biimpar	$⊢ (φ \land B \leq A) \to (A, B) = \emptyset$
31		ineq2	$⊢ (A, B) = \emptyset \to ℚ \cap (A, B) = ℚ \cap \emptyset$
32		in0	$⊢ ℚ \cap \emptyset = \emptyset$
33	31 32	eqtrdi	$⊢ (A, B) = \emptyset \to ℚ \cap (A, B) = \emptyset$
34	30 33	syl	$⊢ (φ \land B \leq A) \to ℚ \cap (A, B) = \emptyset$
35	27 34	impbida	$⊢ φ \to (ℚ \cap (A, B) = \emptyset \leftrightarrow B \leq A)$

Metamath Proof Explorer

Theorem qinioo

Proof