Theorem qbtwnre 4650

Description: The rational numbers are dense in RR: any two real numbers have a rational between them. Exercise 6 of [Apostol] p. 28.

Assertion

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

Distinct variable group(s):   x,A   x,B

Proof of Theorem qbtwnre

Step	Hyp	Ref	Expression
1		posdift 4365	. . . 4 |- ((A e. RR /\ B e. RR) -> (A < B <-> 0 < (B - A)))
2		nnreclt 4522	. . . . . . 7 |- (((B - A) e. RR /\ 0 < (B - A)) -> E.y e. NN (1 / y) < (B - A))
3		resubclt 4173	. . . . . . 7 |- ((B e. RR /\ A e. RR) -> (B - A) e. RR)
4	2, 3	sylan 343	. . . . . 6 |- (((B e. RR /\ A e. RR) /\ 0 < (B - A)) -> E.y e. NN (1 / y) < (B - A))
5	4	exp 291	. . . . 5 |- ((B e. RR /\ A e. RR) -> (0 < (B - A) -> E.y e. NN (1 / y) < (B - A)))
6	5	ancoms 334	. . . 4 |- ((A e. RR /\ B e. RR) -> (0 < (B - A) -> E.y e. NN (1 / y) < (B - A)))
7	1, 6	sylbid 178	. . 3 |- ((A e. RR /\ B e. RR) -> (A < B -> E.y e. NN (1 / y) < (B - A)))
8		axmulrcl 4069	. . . . . . . . . . 11 |- ((y e. RR /\ B e. RR) -> (y x. B) e. RR)
9		nnret 4427	. . . . . . . . . . 11 |- (y e. NN -> y e. RR)
10	8, 9	sylan 343	. . . . . . . . . 10 |- ((y e. NN /\ B e. RR) -> (y x. B) e. RR)
11		ax1re 4064	. . . . . . . . . . 11 |- 1 e. RR
12		resubclt 4173	. . . . . . . . . . 11 |- (((y x. B) e. RR /\ 1 e. RR) -> ((y x. B) - 1) e. RR)
13	11, 12	mpan2 519	. . . . . . . . . 10 |- ((y x. B) e. RR -> ((y x. B) - 1) e. RR)
14	10, 13	syl 12	. . . . . . . . 9 |- ((y e. NN /\ B e. RR) -> ((y x. B) - 1) e. RR)
15	14	adantrl 311	. . . . . . . 8 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> ((y x. B) - 1) e. RR)
16		zbtwnre 4619	. . . . . . . 8 |- (((y x. B) - 1) e. RR -> E!z e. ZZ (((y x. B) - 1) <_ z /\ z < (((y x. B) - 1) + 1)))
17		reurex 1337	. . . . . . . 8 |- (E!z e. ZZ (((y x. B) - 1) <_ z /\ z < (((y x. B) - 1) + 1)) -> E.z e. ZZ (((y x. B) - 1) <_ z /\ z < (((y x. B) - 1) + 1)))
18	15, 16, 17	3syl 21	. . . . . . 7 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> E.z e. ZZ (((y x. B) - 1) <_ z /\ z < (((y x. B) - 1) + 1)))
19		znq 4630	. . . . . . . . . . . . . . . 16 |- ((z e. ZZ /\ y e. NN) -> (z / y) e. QQ)
20	19	ancoms 334	. . . . . . . . . . . . . . 15 |- ((y e. NN /\ z e. ZZ) -> (z / y) e. QQ)
21	20	adantlr 310	. . . . . . . . . . . . . 14 |- (((y e. NN /\ (A e. RR /\ B e. RR)) /\ z e. ZZ) -> (z / y) e. QQ)
22	21	a1d 14	. . . . . . . . . . . . 13 |- (((y e. NN /\ (A e. RR /\ B e. RR)) /\ z e. ZZ) -> ((((1 / y) < (B - A) /\ ((y x. B) - 1) <_ z) /\ z < (((y x. B) - 1) + 1)) -> (z / y) e. QQ))
23		subdit 4184	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y e. CC /\ B e. CC /\ A e. CC) -> (y x. (B - A)) = ((y x. B) - (y x. A)))
24		nncnt 4428	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. NN -> y e. CC)
25		recnt 4097	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (B e. RR -> B e. CC)
26		recnt 4097	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A e. RR -> A e. CC)
27	23, 24, 25, 26	syl3an 628	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. NN /\ B e. RR /\ A e. RR) -> (y x. (B - A)) = ((y x. B) - (y x. A)))
28	27	3com23 616	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. NN /\ A e. RR /\ B e. RR) -> (y x. (B - A)) = ((y x. B) - (y x. A)))
29	28	3expb 613	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> (y x. (B - A)) = ((y x. B) - (y x. A)))
30	29	breq2d 2072	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> (1 < (y x. (B - A)) <-> 1 < ((y x. B) - (y x. A))))
31		ltdivmult 4408	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((1 e. RR /\ y e. RR /\ (B - A) e. RR) -> (0 < y -> ((1 / y) < (B - A) <-> 1 < (y x. (B - A)))))
32	11, 31	mp3an1 639	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. RR /\ (B - A) e. RR) -> (0 < y -> ((1 / y) < (B - A) <-> 1 < (y x. (B - A)))))
33	32	exp 291	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. RR -> ((B - A) e. RR -> (0 < y -> ((1 / y) < (B - A) <-> 1 < (y x. (B - A))))))
34	33	com23 32	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. RR -> (0 < y -> ((B - A) e. RR -> ((1 / y) < (B - A) <-> 1 < (y x. (B - A))))))
35		nngt0t 4441	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. NN -> 0 < y)
36	34, 9, 35	sylc 62	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. NN -> ((B - A) e. RR -> ((1 / y) < (B - A) <-> 1 < (y x. (B - A)))))
37	3	ancoms 334	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. RR /\ B e. RR) -> (B - A) e. RR)
38	36, 37	syl5 22	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. NN -> ((A e. RR /\ B e. RR) -> ((1 / y) < (B - A) <-> 1 < (y x. (B - A)))))
39	38	imp 277	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> ((1 / y) < (B - A) <-> 1 < (y x. (B - A))))
40		ltsub13t 4360	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((y x. A) e. RR /\ (y x. B) e. RR /\ 1 e. RR) -> ((y x. A) < ((y x. B) - 1) <-> 1 < ((y x. B) - (y x. A))))
41	11, 40	mp3an3 641	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((y x. A) e. RR /\ (y x. B) e. RR) -> ((y x. A) < ((y x. B) - 1) <-> 1 < ((y x. B) - (y x. A))))
42		axmulrcl 4069	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. RR /\ A e. RR) -> (y x. A) e. RR)
43	41, 42, 8	syl2an 349	. . . . . . . . . . . . . . . . . . . . . 22 |- (((y e. RR /\ A e. RR) /\ (y e. RR /\ B e. RR)) -> ((y x. A) < ((y x. B) - 1) <-> 1 < ((y x. B) - (y x. A))))
44	43	anandis 394	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. RR /\ (A e. RR /\ B e. RR)) -> ((y x. A) < ((y x. B) - 1) <-> 1 < ((y x. B) - (y x. A))))
45	44, 9	sylan 343	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> ((y x. A) < ((y x. B) - 1) <-> 1 < ((y x. B) - (y x. A))))
46	30, 39, 45	3bitr4d 424	. . . . . . . . . . . . . . . . . . 19 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> ((1 / y) < (B - A) <-> (y x. A) < ((y x. B) - 1)))
47	46	adantr 306	. . . . . . . . . . . . . . . . . 18 |- (((y e. NN /\ (A e. RR /\ B e. RR)) /\ z e. RR) -> ((1 / y) < (B - A) <-> (y x. A) < ((y x. B) - 1)))
48	47	anbi1d 469	. . . . . . . . . . . . . . . . 17 |- (((y e. NN /\ (A e. RR /\ B e. RR)) /\ z e. RR) -> (((1 / y) < (B - A) /\ ((y x. B) - 1) <_ z) <-> ((y x. A) < ((y x. B) - 1) /\ ((y x. B) - 1) <_ z)))
49		ltletrt 4290	. . . . . . . . . . . . . . . . . . 19 |- (((y x. A) e. RR /\ ((y x. B) - 1) e. RR /\ z e. RR) -> (((y x. A) < ((y x. B) - 1) /\ ((y x. B) - 1) <_ z) -> (y x. A) < z))
50	49	3expa 612	. . . . . . . . . . . . . . . . . 18 |- ((((y x. A) e. RR /\ ((y x. B) - 1) e. RR) /\ z e. RR) -> (((y x. A) < ((y x. B) - 1) /\ ((y x. B) - 1) <_ z) -> (y x. A) < z))
51	42, 9	sylan 343	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. NN /\ A e. RR) -> (y x. A) e. RR)
52	51	adantrr 312	. . . . . . . . . . . . . . . . . . 19 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> (y x. A) e. RR)
53	52, 15	jca 236	. . . . . . . . . . . . . . . . . 18 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> ((y x. A) e. RR /\ ((y x. B) - 1) e. RR))
54	50, 53	sylan 343	. . . . . . . . . . . . . . . . 17 |- (((y e. NN /\ (A e. RR /\ B e. RR)) /\ z e. RR) -> (((y x. A) < ((y x. B) - 1)