This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 ) )