qinioo

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

	Ref	Expression
Hypotheses	qinioo.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ^* )
	qinioo.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ^* )
Assertion	qinioo	⊢ ( 𝜑 → ( ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		qinioo.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ^* )
2		qinioo.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ^* )
3		simplr	⊢ ( ( ( 𝜑 ∧ ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ )
4	1 2	xrltnled	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴 ) )
5	4	biimpar	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝐴 ) → 𝐴 < 𝐵 )
6	1	adantr	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ^* )
7	2	adantr	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ^* )
8		simpr	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
9		qbtwnxr	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) → ∃ 𝑞 ∈ ℚ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) )
10	6 7 8 9	syl3anc	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → ∃ 𝑞 ∈ ℚ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) )
11	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℚ ) ∧ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) ) → 𝐴 ∈ ℝ^* )
12	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℚ ) ∧ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) ) → 𝐵 ∈ ℝ^* )
13		qre	⊢ ( 𝑞 ∈ ℚ → 𝑞 ∈ ℝ )
14	13	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℚ ) ∧ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) ) → 𝑞 ∈ ℝ )
15		simprl	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℚ ) ∧ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) ) → 𝐴 < 𝑞 )
16		simprr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℚ ) ∧ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) ) → 𝑞 < 𝐵 )
17	11 12 14 15 16	eliood	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℚ ) ∧ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) ) → 𝑞 ∈ ( 𝐴 (,) 𝐵 ) )
18	17	ex	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ℚ ) → ( ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) → 𝑞 ∈ ( 𝐴 (,) 𝐵 ) ) )
19	18	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 < 𝐵 ) ∧ 𝑞 ∈ ℚ ) → ( ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) → 𝑞 ∈ ( 𝐴 (,) 𝐵 ) ) )
20	19	reximdva	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → ( ∃ 𝑞 ∈ ℚ ( 𝐴 < 𝑞 ∧ 𝑞 < 𝐵 ) → ∃ 𝑞 ∈ ℚ 𝑞 ∈ ( 𝐴 (,) 𝐵 ) ) )
21	10 20	mpd	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → ∃ 𝑞 ∈ ℚ 𝑞 ∈ ( 𝐴 (,) 𝐵 ) )
22		inn0	⊢ ( ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) ≠ ∅ ↔ ∃ 𝑞 ∈ ℚ 𝑞 ∈ ( 𝐴 (,) 𝐵 ) )
23	21 22	sylibr	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) ≠ ∅ )
24	5 23	syldan	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝐴 ) → ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) ≠ ∅ )
25	24	neneqd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ≤ 𝐴 ) → ¬ ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ )
26	25	adantlr	⊢ ( ( ( 𝜑 ∧ ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ ) ∧ ¬ 𝐵 ≤ 𝐴 ) → ¬ ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ )
27	3 26	condan	⊢ ( ( 𝜑 ∧ ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ ) → 𝐵 ≤ 𝐴 )
28		ioo0	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
29	1 2 28	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
30	29	biimpar	⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ( 𝐴 (,) 𝐵 ) = ∅ )
31		ineq2	⊢ ( ( 𝐴 (,) 𝐵 ) = ∅ → ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ( ℚ ∩ ∅ ) )
32		in0	⊢ ( ℚ ∩ ∅ ) = ∅
33	31 32	eqtrdi	⊢ ( ( 𝐴 (,) 𝐵 ) = ∅ → ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ )
34	30 33	syl	⊢ ( ( 𝜑 ∧ 𝐵 ≤ 𝐴 ) → ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ )
35	27 34	impbida	⊢ ( 𝜑 → ( ( ℚ ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )

Metamath Proof Explorer

Theorem qinioo

Proof