Theorem qinioo

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

	Ref	Expression
Hypotheses	qinioo.a	|- ( ph -> A e. RR* )
	qinioo.b	|- ( ph -> B e. RR* )
Assertion	qinioo	|- ( ph -> ( ( QQ i^i ( A (,) B ) ) = (/) <-> B <_ A ) )

Proof

Step	Hyp	Ref	Expression
1		qinioo.a	|- ( ph -> A e. RR* )
2		qinioo.b	|- ( ph -> B e. RR* )
3		simplr	|- ( ( ( ph /\ ( QQ i^i ( A (,) B ) ) = (/) ) /\ -. B <_ A ) -> ( QQ i^i ( A (,) B ) ) = (/) )
4	1 2	xrltnled	|- ( ph -> ( A < B <-> -. B <_ A ) )
5	4	biimpar	|- ( ( ph /\ -. B <_ A ) -> A < B )
6	1	adantr	|- ( ( ph /\ A < B ) -> A e. RR* )
7	2	adantr	|- ( ( ph /\ A < B ) -> B e. RR* )
8		simpr	|- ( ( ph /\ A < B ) -> A < B )
9		qbtwnxr	|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> E. q e. QQ ( A < q /\ q < B ) )
10	6 7 8 9	syl3anc	|- ( ( ph /\ A < B ) -> E. q e. QQ ( A < q /\ q < B ) )
11	1	ad2antrr	|- ( ( ( ph /\ q e. QQ ) /\ ( A < q /\ q < B ) ) -> A e. RR* )
12	2	ad2antrr	|- ( ( ( ph /\ q e. QQ ) /\ ( A < q /\ q < B ) ) -> B e. RR* )
13		qre	|- ( q e. QQ -> q e. RR )
14	13	ad2antlr	|- ( ( ( ph /\ q e. QQ ) /\ ( A < q /\ q < B ) ) -> q e. RR )
15		simprl	|- ( ( ( ph /\ q e. QQ ) /\ ( A < q /\ q < B ) ) -> A < q )
16		simprr	|- ( ( ( ph /\ q e. QQ ) /\ ( A < q /\ q < B ) ) -> q < B )
17	11 12 14 15 16	eliood	|- ( ( ( ph /\ q e. QQ ) /\ ( A < q /\ q < B ) ) -> q e. ( A (,) B ) )
18	17	ex	|- ( ( ph /\ q e. QQ ) -> ( ( A < q /\ q < B ) -> q e. ( A (,) B ) ) )
19	18	adantlr	|- ( ( ( ph /\ A < B ) /\ q e. QQ ) -> ( ( A < q /\ q < B ) -> q e. ( A (,) B ) ) )
20	19	reximdva	|- ( ( ph /\ A < B ) -> ( E. q e. QQ ( A < q /\ q < B ) -> E. q e. QQ q e. ( A (,) B ) ) )
21	10 20	mpd	|- ( ( ph /\ A < B ) -> E. q e. QQ q e. ( A (,) B ) )
22		inn0	|- ( ( QQ i^i ( A (,) B ) ) =/= (/) <-> E. q e. QQ q e. ( A (,) B ) )
23	21 22	sylibr	|- ( ( ph /\ A < B ) -> ( QQ i^i ( A (,) B ) ) =/= (/) )
24	5 23	syldan	|- ( ( ph /\ -. B <_ A ) -> ( QQ i^i ( A (,) B ) ) =/= (/) )
25	24	neneqd	|- ( ( ph /\ -. B <_ A ) -> -. ( QQ i^i ( A (,) B ) ) = (/) )
26	25	adantlr	|- ( ( ( ph /\ ( QQ i^i ( A (,) B ) ) = (/) ) /\ -. B <_ A ) -> -. ( QQ i^i ( A (,) B ) ) = (/) )
27	3 26	condan	|- ( ( ph /\ ( QQ i^i ( A (,) B ) ) = (/) ) -> B <_ A )
28		ioo0	|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )
29	1 2 28	syl2anc	|- ( ph -> ( ( A (,) B ) = (/) <-> B <_ A ) )
30	29	biimpar	|- ( ( ph /\ B <_ A ) -> ( A (,) B ) = (/) )
31		ineq2	|- ( ( A (,) B ) = (/) -> ( QQ i^i ( A (,) B ) ) = ( QQ i^i (/) ) )
32		in0	|- ( QQ i^i (/) ) = (/)
33	31 32	eqtrdi	|- ( ( A (,) B ) = (/) -> ( QQ i^i ( A (,) B ) ) = (/) )
34	30 33	syl	|- ( ( ph /\ B <_ A ) -> ( QQ i^i ( A (,) B ) ) = (/) )
35	27 34	impbida	|- ( ph -> ( ( QQ i^i ( A (,) B ) ) = (/) <-> B <_ A ) )