Theorem ltbtwnnq

Description: There exists a number between any two positive fractions. Proposition 9-2.6(i) of Gleason p. 120. (Contributed by NM, 17-Mar-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	ltbtwnnq	⊢ ( 𝐴 <Q 𝐵 ↔ ∃ 𝑥 ( 𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ltrelnq	⊢ <Q ⊆ ( Q × Q )
2	1	brel	⊢ ( 𝐴 <Q 𝐵 → ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) )
3	2	simprd	⊢ ( 𝐴 <Q 𝐵 → 𝐵 ∈ Q )
4		ltexnq	⊢ ( 𝐵 ∈ Q → ( 𝐴 <Q 𝐵 ↔ ∃ 𝑦 ( 𝐴 +Q 𝑦 ) = 𝐵 ) )
5		eleq1	⊢ ( ( 𝐴 +Q 𝑦 ) = 𝐵 → ( ( 𝐴 +Q 𝑦 ) ∈ Q ↔ 𝐵 ∈ Q ) )
6	5	biimparc	⊢ ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑦 ) = 𝐵 ) → ( 𝐴 +Q 𝑦 ) ∈ Q )
7		addnqf	⊢ +Q : ( Q × Q ) ⟶ Q
8	7	fdmi	⊢ dom +Q = ( Q × Q )
9		0nnq	⊢ ¬ ∅ ∈ Q
10	8 9	ndmovrcl	⊢ ( ( 𝐴 +Q 𝑦 ) ∈ Q → ( 𝐴 ∈ Q ∧ 𝑦 ∈ Q ) )
11	6 10	syl	⊢ ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑦 ) = 𝐵 ) → ( 𝐴 ∈ Q ∧ 𝑦 ∈ Q ) )
12	11	simprd	⊢ ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑦 ) = 𝐵 ) → 𝑦 ∈ Q )
13		nsmallnq	⊢ ( 𝑦 ∈ Q → ∃ 𝑧 𝑧 <Q 𝑦 )
14	11	simpld	⊢ ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑦 ) = 𝐵 ) → 𝐴 ∈ Q )
15	1	brel	⊢ ( 𝑧 <Q 𝑦 → ( 𝑧 ∈ Q ∧ 𝑦 ∈ Q ) )
16	15	simpld	⊢ ( 𝑧 <Q 𝑦 → 𝑧 ∈ Q )
17		ltaddnq	⊢ ( ( 𝐴 ∈ Q ∧ 𝑧 ∈ Q ) → 𝐴 <Q ( 𝐴 +Q 𝑧 ) )
18	14 16 17	syl2an	⊢ ( ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑦 ) = 𝐵 ) ∧ 𝑧 <Q 𝑦 ) → 𝐴 <Q ( 𝐴 +Q 𝑧 ) )
19		ltanq	⊢ ( 𝐴 ∈ Q → ( 𝑧 <Q 𝑦 ↔ ( 𝐴 +Q 𝑧 ) <Q ( 𝐴 +Q 𝑦 ) ) )
20	19	biimpa	⊢ ( ( 𝐴 ∈ Q ∧ 𝑧 <Q 𝑦 ) → ( 𝐴 +Q 𝑧 ) <Q ( 𝐴 +Q 𝑦 ) )
21	14 20	sylan	⊢ ( ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑦 ) = 𝐵 ) ∧ 𝑧 <Q 𝑦 ) → ( 𝐴 +Q 𝑧 ) <Q ( 𝐴 +Q 𝑦 ) )
22		simplr	⊢ ( ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑦 ) = 𝐵 ) ∧ 𝑧 <Q 𝑦 ) → ( 𝐴 +Q 𝑦 ) = 𝐵 )
23	21 22	breqtrd	⊢ ( ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑦 ) = 𝐵 ) ∧ 𝑧 <Q 𝑦 ) → ( 𝐴 +Q 𝑧 ) <Q 𝐵 )
24		ovex	⊢ ( 𝐴 +Q 𝑧 ) ∈ V
25		breq2	⊢ ( 𝑥 = ( 𝐴 +Q 𝑧 ) → ( 𝐴 <Q 𝑥 ↔ 𝐴 <Q ( 𝐴 +Q 𝑧 ) ) )
26		breq1	⊢ ( 𝑥 = ( 𝐴 +Q 𝑧 ) → ( 𝑥 <Q 𝐵 ↔ ( 𝐴 +Q 𝑧 ) <Q 𝐵 ) )
27	25 26	anbi12d	⊢ ( 𝑥 = ( 𝐴 +Q 𝑧 ) → ( ( 𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵 ) ↔ ( 𝐴 <Q ( 𝐴 +Q 𝑧 ) ∧ ( 𝐴 +Q 𝑧 ) <Q 𝐵 ) ) )
28	24 27	spcev	⊢ ( ( 𝐴 <Q ( 𝐴 +Q 𝑧 ) ∧ ( 𝐴 +Q 𝑧 ) <Q 𝐵 ) → ∃ 𝑥 ( 𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵 ) )
29	18 23 28	syl2anc	⊢ ( ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑦 ) = 𝐵 ) ∧ 𝑧 <Q 𝑦 ) → ∃ 𝑥 ( 𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵 ) )
30	29	ex	⊢ ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑦 ) = 𝐵 ) → ( 𝑧 <Q 𝑦 → ∃ 𝑥 ( 𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵 ) ) )
31	30	exlimdv	⊢ ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑦 ) = 𝐵 ) → ( ∃ 𝑧 𝑧 <Q 𝑦 → ∃ 𝑥 ( 𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵 ) ) )
32	13 31	syl5	⊢ ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑦 ) = 𝐵 ) → ( 𝑦 ∈ Q → ∃ 𝑥 ( 𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵 ) ) )
33	12 32	mpd	⊢ ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑦 ) = 𝐵 ) → ∃ 𝑥 ( 𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵 ) )
34	33	ex	⊢ ( 𝐵 ∈ Q → ( ( 𝐴 +Q 𝑦 ) = 𝐵 → ∃ 𝑥 ( 𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵 ) ) )
35	34	exlimdv	⊢ ( 𝐵 ∈ Q → ( ∃ 𝑦 ( 𝐴 +Q 𝑦 ) = 𝐵 → ∃ 𝑥 ( 𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵 ) ) )
36	4 35	sylbid	⊢ ( 𝐵 ∈ Q → ( 𝐴 <Q 𝐵 → ∃ 𝑥 ( 𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵 ) ) )
37	3 36	mpcom	⊢ ( 𝐴 <Q 𝐵 → ∃ 𝑥 ( 𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵 ) )
38		ltsonq	⊢ <Q Or Q
39	38 1	sotri	⊢ ( ( 𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵 ) → 𝐴 <Q 𝐵 )
40	39	exlimiv	⊢ ( ∃ 𝑥 ( 𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵 ) → 𝐴 <Q 𝐵 )
41	37 40	impbii	⊢ ( 𝐴 <Q 𝐵 ↔ ∃ 𝑥 ( 𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵 ) )