Theorem qbtwnre 6224

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 groups:   x,A   x,B

Proof of Theorem qbtwnre

Step	Hyp	Ref	Expression
1		posdift 5635	. . . 4 |- ((A e. RR /\ B e. RR) -> (A < B <-> 0 < (B - A)))
2		nnreclt 6027	. . . . . . 7 |- (((B - A) e. RR /\ 0 < (B - A)) -> E.y e. NN (1 / y) < (B - A))
3		resubclt 5418	. . . . . . 7 |- ((B e. RR /\ A e. RR) -> (B - A) e. RR)
4	2, 3	sylan 448	. . . . . 6 |- (((B e. RR /\ A e. RR) /\ 0 < (B - A)) -> E.y e. NN (1 / y) < (B - A))
5	4	ex 373	. . . . 5 |- ((B e. RR /\ A e. RR) -> (0 < (B - A) -> E.y e. NN (1 / y) < (B - A)))
6	5	ancoms 436	. . . 4 |- ((A e. RR /\ B e. RR) -> (0 < (B - A) -> E.y e. NN (1 / y) < (B - A)))
7	1, 6	sylbid 203	. . 3 |- ((A e. RR /\ B e. RR) -> (A < B -> E.y e. NN (1 / y) < (B - A)))
8		axmulrcl 5254	. . . . . . . . . 10 |- ((y e. RR /\ B e. RR) -> (y x. B) e. RR)
9		nnret 5885	. . . . . . . . . 10 |- (y e. NN -> y e. RR)
10	8, 9	sylan 448	. . . . . . . . 9 |- ((y e. NN /\ B e. RR) -> (y x. B) e. RR)
11		peano2rem 5422	. . . . . . . . 9 |- ((y x. B) e. RR -> ((y x. B) - 1) e. RR)
12	10, 11	syl 10	. . . . . . . 8 |- ((y e. NN /\ B e. RR) -> ((y x. B) - 1) e. RR)
13	12	adantrl 394	. . . . . . 7 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> ((y x. B) - 1) e. RR)
14		zbtwnre 6177	. . . . . . 7 |- (((y x. B) - 1) e. RR -> E!z e. ZZ (((y x. B) - 1) <_ z /\ z < (((y x. B) - 1) + 1)))
15		reurex 1924	. . . . . . 7 |- (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)))
16	13, 14, 15	3syl 20	. . . . . 6 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> E.z e. ZZ (((y x. B) - 1) <_ z /\ z < (((y x. B) - 1) + 1)))
17		subdit 5407	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. CC /\ B e. CC /\ A e. CC) -> (y x. (B - A)) = ((y x. B) - (y x. A)))
18		nncnt 5886	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. NN -> y e. CC)
19		recnt 5293	. . . . . . . . . . . . . . . . . . . . . . 23 |- (B e. RR -> B e. CC)
20		recnt 5293	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A e. RR -> A e. CC)
21	17, 18, 19, 20	syl3an 867	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. NN /\ B e. RR /\ A e. RR) -> (y x. (B - A)) = ((y x. B) - (y x. A)))
22	21	3com23 838	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. NN /\ A e. RR /\ B e. RR) -> (y x. (B - A)) = ((y x. B) - (y x. A)))
23	22	3expb 833	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> (y x. (B - A)) = ((y x. B) - (y x. A)))
24	23	breq2d 2625	. . . . . . . . . . . . . . . . . . 19 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> (1 < (y x. (B - A)) <-> 1 < ((y x. B) - (y x. A))))
25		1re 5415	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 1 e. RR
26		ltdivmult 5827	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((1 e. RR /\ y e. RR /\ (B - A) e. RR) /\ 0 < y) -> ((1 / y) < (B - A) <-> 1 < (y x. (B - A))))
27	25, 26	mp3anl1 908	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((y e. RR /\ (B - A) e. RR) /\ 0 < y) -> ((1 / y) < (B - A) <-> 1 < (y x. (B - A))))
28	27	exp31 376	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. RR -> ((B - A) e. RR -> (0 < y -> ((1 / y) < (B - A) <-> 1 < (y x. (B - A))))))
29	28	com23 32	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. RR -> (0 < y -> ((B - A) e. RR -> ((1 / y) < (B - A) <-> 1 < (y x. (B - A))))))
30		nngt0t 5902	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. NN -> 0 < y)
31	29, 9, 30	sylc 68	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. NN -> ((B - A) e. RR -> ((1 / y) < (B - A) <-> 1 < (y x. (B - A)))))
32	3	ancoms 436	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. RR /\ B e. RR) -> (B - A) e. RR)
33	31, 32	syl5 21	. . . . . . . . . . . . . . . . . . . 20 |- (y e. NN -> ((A e. RR /\ B e. RR) -> ((1 / y) < (B - A) <-> 1 < (y x. (B - A)))))
34	33	imp 350	. . . . . . . . . . . . . . . . . . 19 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> ((1 / y) < (B - A) <-> 1 < (y x. (B - A))))
35		ltsub13t 5624	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((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))))
36	25, 35	mp3an3 903	. . . . . . . . . . . . . . . . . . . . . 22 |- (((y x. A) e. RR /\ (y x. B) e. RR) -> ((y x. A) < ((y x. B) - 1) <-> 1 < ((y x. B) - (y x. A))))
37		axmulrcl 5254	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. RR /\ A e. RR) -> (y x. A) e. RR)
38	36, 37, 8	syl2an 454	. . . . . . . . . . . . . . . . . . . . 21 |- (((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))))
39	38	anandis 512	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. RR /\ (A e. RR /\ B e. RR)) -> ((y x. A) < ((y x. B) - 1) <-> 1 < ((y x. B) - (y x. A))))
40	39, 9	sylan 448	. . . . . . . . . . . . . . . . . . 19 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> ((y x. A) < ((y x. B) - 1) <-> 1 < ((y x. B) - (y x. A))))
41	24, 34, 40	3bitr4d 549	. . . . . . . . . . . . . . . . . 18 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> ((1 / y) < (B - A) <-> (y x. A) < ((y x. B) - 1)))
42	41	adantr 389	. . . . . . . . . . . . . . . . 17 |- (((y e. NN /\ (A e. RR /\ B e. RR)) /\ z e. RR) -> ((1 / y) < (B - A) <-> (y x. A) < ((y x. B) - 1)))
43	42	anbi1d 616	. . . . . . . . . . . . . . . 16 |- (((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)))
44		ltletrt 5505	. . . . . . . . . . . . . . . . . 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))
45	44	3expa 832	. . . . . . . . . . . . . . . . 17 |- ((((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))
46	37, 9	sylan 448	. . . . . . . . . . . . . . . . . . 19 |- ((y e. NN /\ A e. RR) -> (y x. A) e. RR)
47	46	adantrr 395	. . . . . . . . . . . . . . . . . 18 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> (y x. A) e. RR)
48	47, 13	jca 288	. . . . . . . . . . . . . . . . 17 |- ((y e. NN /\ (A e. RR /\ B e. RR)) -> ((y x. A) e. RR /\ ((y x. B) - 1) e. RR))
49	45, 48	sylan 448	. . . . . . . . . . . . . . . 16 |- (((y e. NN /\ (A e. RR /\ B e. RR)) /\ z e. RR) -> (((y x. A) < ((y x. B) - 1) /\ ((y x. B) - 1) <_ z) -> (y x. A) < z))
50	43, 49	sylbid 203	. . . . . . . . . . . . . . 15 |- (((y e. NN /\ (A e. RR /\ B e. RR)) /\ z e. RR) -> (((1 / y) < (B - A) /\ ((y x. B) - 1) <_ z) -> (y x. A) < z))
51		ltmuldiv2t 5826	. . . . . . . . . . . . . . . . . . . . 21 |- (((y e. RR /\ A e. RR /\ z e. RR) /\ 0 < y) -> ((y x. A) < z <-> A < (z / y)))
52	51	3exp1 848	. . . . . . . . . . . . . . . . . . . 20 |- (y e. RR -> (A