Theorem qbtwnxr 6279

Description: The rational numbers are dense in RR*: any two extended real numbers have a rational between them.

Assertion

Ref	Expression
qbtwnxr	|- ((A e. RR* /\ B e. RR* /\ A < B) -> E.x e. QQ (A < x /\ x < B))

Distinct variable groups:   x,A   x,B

Proof of Theorem qbtwnxr

Step	Hyp	Ref	Expression
1		qbtwnre 6278	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ A < B) -> E.x e. QQ (A < x /\ x < B))
2	1	3expia 835	. . . . . 6 |- ((A e. RR /\ B e. RR) -> (A < B -> E.x e. QQ (A < x /\ x < B)))
3		peano2re 5436	. . . . . . . . . . 11 |- (A e. RR -> (A + 1) e. RR)
4		ltp1t 5811	. . . . . . . . . . 11 |- (A e. RR -> A < (A + 1))
5		qbtwnre 6278	. . . . . . . . . . 11 |- ((A e. RR /\ (A + 1) e. RR /\ A < (A + 1)) -> E.x e. QQ (A < x /\ x < (A + 1)))
6	3, 4, 5	mpd3an23 918	. . . . . . . . . 10 |- (A e. RR -> E.x e. QQ (A < x /\ x < (A + 1)))
7		ltpnft 5542	. . . . . . . . . . . . . . 15 |- ((A + 1) e. RR -> (A + 1) < +oo)
8	3, 7	syl 10	. . . . . . . . . . . . . 14 |- (A e. RR -> (A + 1) < +oo)
9	8	adantr 389	. . . . . . . . . . . . 13 |- ((A e. RR /\ x e. QQ) -> (A + 1) < +oo)
10		pnfxr 5493	. . . . . . . . . . . . . . 15 |- +oo e. RR*
11		xrlttrt 5553	. . . . . . . . . . . . . . 15 |- ((x e. RR* /\ (A + 1) e. RR* /\ +oo e. RR*) -> ((x < (A + 1) /\ (A + 1) < +oo) -> x < +oo))
12	10, 11	mp3an3 905	. . . . . . . . . . . . . 14 |- ((x e. RR* /\ (A + 1) e. RR*) -> ((x < (A + 1) /\ (A + 1) < +oo) -> x < +oo))
13		qret 6259	. . . . . . . . . . . . . . . 16 |- (x e. QQ -> x e. RR)
14		rexrt 5499	. . . . . . . . . . . . . . . 16 |- (x e. RR -> x e. RR*)
15	13, 14	syl 10	. . . . . . . . . . . . . . 15 |- (x e. QQ -> x e. RR*)
16	15	adantl 388	. . . . . . . . . . . . . 14 |- ((A e. RR /\ x e. QQ) -> x e. RR*)
17		rexrt 5499	. . . . . . . . . . . . . . . 16 |- ((A + 1) e. RR -> (A + 1) e. RR*)
18	3, 17	syl 10	. . . . . . . . . . . . . . 15 |- (A e. RR -> (A + 1) e. RR*)
19	18	adantr 389	. . . . . . . . . . . . . 14 |- ((A e. RR /\ x e. QQ) -> (A + 1) e. RR*)
20	12, 16, 19	sylanc 471	. . . . . . . . . . . . 13 |- ((A e. RR /\ x e. QQ) -> ((x < (A + 1) /\ (A + 1) < +oo) -> x < +oo))
21	9, 20	mpan2d 702	. . . . . . . . . . . 12 |- ((A e. RR /\ x e. QQ) -> (x < (A + 1) -> x < +oo))
22	21	anim2d 561	. . . . . . . . . . 11 |- ((A e. RR /\ x e. QQ) -> ((A < x /\ x < (A + 1)) -> (A < x /\ x < +oo)))
23	22	r19.22dva 1739	. . . . . . . . . 10 |- (A e. RR -> (E.x e. QQ (A < x /\ x < (A + 1)) -> E.x e. QQ (A < x /\ x < +oo)))
24	6, 23	mpd 26	. . . . . . . . 9 |- (A e. RR -> E.x e. QQ (A < x /\ x < +oo))
25	24	adantr 389	. . . . . . . 8 |- ((A e. RR /\ B = +oo) -> E.x e. QQ (A < x /\ x < +oo))
26		breq2 2623	. . . . . . . . . . 11 |- (B = +oo -> (x < B <-> x < +oo))
27	26	anbi2d 616	. . . . . . . . . 10 |- (B = +oo -> ((A < x /\ x < B) <-> (A < x /\ x < +oo)))
28	27	rexbidv 1664	. . . . . . . . 9 |- (B = +oo -> (E.x e. QQ (A < x /\ x < B) <-> E.x e. QQ (A < x /\ x < +oo)))
29	28	adantl 388	. . . . . . . 8 |- ((A e. RR /\ B = +oo) -> (E.x e. QQ (A < x /\ x < B) <-> E.x e. QQ (A < x /\ x < +oo)))
30	25, 29	mpbird 196	. . . . . . 7 |- ((A e. RR /\ B = +oo) -> E.x e. QQ (A < x /\ x < B))
31	30	a1d 12	. . . . . 6 |- ((A e. RR /\ B = +oo) -> (A < B -> E.x e. QQ (A < x /\ x < B)))
32		rexrt 5499	. . . . . . . . . 10 |- (A e. RR -> A e. RR*)
33		nltmnft 5547	. . . . . . . . . 10 |- (A e. RR* -> -. A < -oo)
34	32, 33	syl 10	. . . . . . . . 9 |- (A e. RR -> -. A < -oo)
35	34	adantr 389	. . . . . . . 8 |- ((A e. RR /\ B = -oo) -> -. A < -oo)
36		breq2 2623	. . . . . . . . . 10 |- (B = -oo -> (A < B <-> A < -oo))
37	36	negbid 611	. . . . . . . . 9 |- (B = -oo -> (-. A < B <-> -. A < -oo))
38	37	adantl 388	. . . . . . . 8 |- ((A e. RR /\ B = -oo) -> (-. A < B <-> -. A < -oo))
39	35, 38	mpbird 196	. . . . . . 7 |- ((A e. RR /\ B = -oo) -> -. A < B)
40	39	pm2.21d 78	. . . . . 6 |- ((A e. RR /\ B = -oo) -> (A < B -> E.x e. QQ (A < x /\ x < B)))
41	2, 31, 40	3jaodan 890	. . . . 5 |- ((A e. RR /\ (B e. RR \/ B = +oo \/ B = -oo)) -> (A < B -> E.x e. QQ (A < x /\ x < B)))
42		elxr 5535	. . . . 5 |- (B e. RR* <-> (B e. RR \/ B = +oo \/ B = -oo))
43	41, 42	sylan2b 452	. . . 4 |- ((A e. RR /\ B e. RR*) -> (A < B -> E.x e. QQ (A < x /\ x < B)))
44		pnfnltt 5546	. . . . . . 7 |- (B e. RR* -> -. +oo < B)
45	44	adantl 388	. . . . . 6 |- ((A = +oo /\ B e. RR*) -> -. +oo < B)
46		breq1 2622	. . . . . . . 8 |- (A = +oo -> (A < B <-> +oo < B))
47	46	negbid 611	. . . . . . 7 |- (A = +oo -> (-. A < B <-> -. +oo < B))
48	47	adantr 389	. . . . . 6 |- ((A = +oo /\ B e. RR*) -> (-. A < B <-> -. +oo < B))
49	45, 48	mpbird 196	. . . . 5 |- ((A = +oo /\ B e. RR*) -> -. A < B)
50	49	pm2.21d 78	. . . 4 |- ((A = +oo /\ B e. RR*) -> (A < B -> E.x e. QQ (A < x /\ x < B)))
51		qbtwnre 6278	. . . . . . . . . . 11 |- (((B - 1) e. RR /\ B e. RR /\ (B - 1) < B) -> E.x e. QQ ((B - 1) < x /\ x < B))
52		peano2rem 5442	. . . . . . . . . . 11 |- (B e. RR -> (B - 1) e. RR)
53		id 59	. . . . . . . . . . 11 |- (B e. RR -> B e. RR)
54		ltm1t 5815	. . . . . . . . . . 11 |- (B e. RR -> (B - 1) < B)
55	51, 52, 53, 54	syl3anc 858	. . . . . . . . . 10 |- (B e. RR -> E.x e. QQ ((B - 1) < x /\ x < B))
56		mnfltt 5543	. . . . . . . . . . . . . . 15 |- ((B - 1) e. RR -> -oo < (B - 1))
57	52, 56	syl 10	. . . . . . . . . . . . . 14 |- (B e. RR -> -oo < (B - 1))
58	57	adantr 389	. . . . . . . . . . . . 13 |- ((B e. RR /\ x e. QQ) -> -oo < (B - 1))
59		mnfxr 5494	. . . . . . . . . . . . . . 15 |- -oo e. RR*
60		xrlttrt 5553	. . . . . . . . . . . . . . 15 |- (( -oo e. RR* /\ (B - 1) e. RR* /\ x e. RR*) -> (( -oo < (B - 1) /\ (B - 1) < x) -> -oo < x))
61	59, 60	mp3an1 903	. . . . . . . . . . . . . 14 |- (((B - 1) e. RR* /\ x e. RR*) -> (( -oo < (B - 1) /\ (B - 1) < x) -> -oo < x))
62		rexrt 5499	. . . . . . . . . . . . . . 15 |- ((B - 1) e. RR -> (B - 1) e. RR*)
63	52, 62	syl 10	. . . . . . . . . . . . . 14 |- (B e. RR -> (B - 1) e. RR*)
64	61, 63, 15	syl2an 454	. . . . . . . . . . . . 13 |- ((B e. RR /\ x e. QQ) -> (( -oo < (B - 1) /\ (B - 1) < x) -> -oo < x))
65	58, 64	mpand 701	. . . . . . . . . . . 12 |- ((B e. RR /\ x e. QQ) -> ((B - 1) < x -> -oo < x))
66	65	anim1d 560	. . . . . . . . . . 11 |- ((B e. RR /\ x e. QQ) -> (((B - 1) < x /\ x < B) -> ( -oo < x /\ x < B)))
67	66	r19.22dva 1739	. . . . . . . . . 10 |- (B e. RR -> (E.x e. QQ ((B - 1) < x /\ x < B) -> E.x e. QQ ( -oo < x /\ x < B)))
68	55, 67	mpd 26	. . . . . . . . 9 |- (B e. RR -> E.x e. QQ ( -oo < x /\ x < B))
69	68	adantl 388	. . . . . . . 8 |- ((A = -oo /\ B e. RR) -> E.x e. QQ ( -oo < x /\ x < B))
70		breq1 2622	. . . . . . . . . . 11 |- (A = -oo -> (A < x <-> -oo < x))
71	70	anbi1d 617	. . . . . . . . . 10 |- (A = -oo -> ((A < x /\ x < B) <-> ( -oo < x /\ x < B)))
72	71	rexbidv 1664	. . . . . . . . 9 |- (A = -oo -> (E.x e. QQ (A < x /\ x < B) <-> E.x e. QQ ( -oo < x /\ x < B)))
73	72	adantr 389	. . . . . . . 8 |- ((A = -oo /\ B e. RR) -> (E.x e. QQ (A < x /\ x < B) <-> E.x e. QQ ( -oo < x /\ x < B)))
74	69, 73	mpbird 196	. . . . . . 7 |- ((A = -oo /\ B e. RR) -> E.x e. QQ (A < x /\ x < B))
75	74	a1d 12	. . . . . 6 |- ((A = -oo /\ B e. RR) -> (A < B -> E.x e. QQ (A < x /\ x < B)))
76		1z 6159	. . . . . . . . . 10 |- 1 e. ZZ
77		zqt 6260	. . . . . . . . . 10 |- (1 e. ZZ -> 1 e. QQ)
78	76, 77	ax-mp 7	. . . . . . . . 9 |- 1 e. QQ
79		breq2 2623	. . . . . . . . . . 11 |- (x = 1 -> (A < x <-> A < 1))
80		breq1 2622	. . . . . . . . . . 11 |- (x = 1 -> (x < B <-> 1 < B))
81	79, 80	anbi12d 628	. . . . . . . . . 10 |- (x = 1 -> ((A < x /\ x < B