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	$⊢ A <_{𝑸} B \leftrightarrow \exists x (A <_{𝑸} x \land x <_{𝑸} B)$

Proof

Step	Hyp	Ref	Expression
1		ltrelnq	$⊢ <_{𝑸} \subseteq 𝑸 \times 𝑸$
2	1	brel	$⊢ A <_{𝑸} B \to (A \in 𝑸 \land B \in 𝑸)$
3	2	simprd	$⊢ A <_{𝑸} B \to B \in 𝑸$
4		ltexnq	$⊢ B \in 𝑸 \to (A <_{𝑸} B \leftrightarrow \exists y A +_{𝑸} y = B)$
5		eleq1	$⊢ A +_{𝑸} y = B \to (A +_{𝑸} y \in 𝑸 \leftrightarrow B \in 𝑸)$
6	5	biimparc	$⊢ (B \in 𝑸 \land A +_{𝑸} y = B) \to A +_{𝑸} y \in 𝑸$
7		addnqf	$⊢ +_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸$
8	7	fdmi	$⊢ dom +_{𝑸} = 𝑸 \times 𝑸$
9		0nnq	$⊢ \neg \emptyset \in 𝑸$
10	8 9	ndmovrcl	$⊢ A +_{𝑸} y \in 𝑸 \to (A \in 𝑸 \land y \in 𝑸)$
11	6 10	syl	$⊢ (B \in 𝑸 \land A +_{𝑸} y = B) \to (A \in 𝑸 \land y \in 𝑸)$
12	11	simprd	$⊢ (B \in 𝑸 \land A +_{𝑸} y = B) \to y \in 𝑸$
13		nsmallnq	$⊢ y \in 𝑸 \to \exists z z <_{𝑸} y$
14	11	simpld	$⊢ (B \in 𝑸 \land A +_{𝑸} y = B) \to A \in 𝑸$
15	1	brel	$⊢ z <_{𝑸} y \to (z \in 𝑸 \land y \in 𝑸)$
16	15	simpld	$⊢ z <_{𝑸} y \to z \in 𝑸$
17		ltaddnq	$⊢ (A \in 𝑸 \land z \in 𝑸) \to A <_{𝑸} (A +_{𝑸} z)$
18	14 16 17	syl2an	$⊢ ((B \in 𝑸 \land A +_{𝑸} y = B) \land z <_{𝑸} y) \to A <_{𝑸} (A +_{𝑸} z)$
19		ltanq	$⊢ A \in 𝑸 \to (z <_{𝑸} y \leftrightarrow (A +_{𝑸} z) <_{𝑸} (A +_{𝑸} y))$
20	19	biimpa	$⊢ (A \in 𝑸 \land z <_{𝑸} y) \to (A +_{𝑸} z) <_{𝑸} (A +_{𝑸} y)$
21	14 20	sylan	$⊢ ((B \in 𝑸 \land A +_{𝑸} y = B) \land z <_{𝑸} y) \to (A +_{𝑸} z) <_{𝑸} (A +_{𝑸} y)$
22		simplr	$⊢ ((B \in 𝑸 \land A +_{𝑸} y = B) \land z <_{𝑸} y) \to A +_{𝑸} y = B$
23	21 22	breqtrd	$⊢ ((B \in 𝑸 \land A +_{𝑸} y = B) \land z <_{𝑸} y) \to (A +_{𝑸} z) <_{𝑸} B$
24		ovex	$⊢ A +_{𝑸} z \in V$
25		breq2	$⊢ x = A +_{𝑸} z \to (A <_{𝑸} x \leftrightarrow A <_{𝑸} (A +_{𝑸} z))$
26		breq1	$⊢ x = A +_{𝑸} z \to (x <_{𝑸} B \leftrightarrow (A +_{𝑸} z) <_{𝑸} B)$
27	25 26	anbi12d	$⊢ x = A +_{𝑸} z \to ((A <_{𝑸} x \land x <_{𝑸} B) \leftrightarrow (A <_{𝑸} (A +_{𝑸} z) \land (A +_{𝑸} z) <_{𝑸} B))$
28	24 27	spcev	$⊢ (A <_{𝑸} (A +_{𝑸} z) \land (A +_{𝑸} z) <_{𝑸} B) \to \exists x (A <_{𝑸} x \land x <_{𝑸} B)$
29	18 23 28	syl2anc	$⊢ ((B \in 𝑸 \land A +_{𝑸} y = B) \land z <_{𝑸} y) \to \exists x (A <_{𝑸} x \land x <_{𝑸} B)$
30	29	ex	$⊢ (B \in 𝑸 \land A +_{𝑸} y = B) \to (z <_{𝑸} y \to \exists x (A <_{𝑸} x \land x <_{𝑸} B))$
31	30	exlimdv	$⊢ (B \in 𝑸 \land A +_{𝑸} y = B) \to (\exists z z <_{𝑸} y \to \exists x (A <_{𝑸} x \land x <_{𝑸} B))$
32	13 31	syl5	$⊢ (B \in 𝑸 \land A +_{𝑸} y = B) \to (y \in 𝑸 \to \exists x (A <_{𝑸} x \land x <_{𝑸} B))$
33	12 32	mpd	$⊢ (B \in 𝑸 \land A +_{𝑸} y = B) \to \exists x (A <_{𝑸} x \land x <_{𝑸} B)$
34	33	ex	$⊢ B \in 𝑸 \to (A +_{𝑸} y = B \to \exists x (A <_{𝑸} x \land x <_{𝑸} B))$
35	34	exlimdv	$⊢ B \in 𝑸 \to (\exists y A +_{𝑸} y = B \to \exists x (A <_{𝑸} x \land x <_{𝑸} B))$
36	4 35	sylbid	$⊢ B \in 𝑸 \to (A <_{𝑸} B \to \exists x (A <_{𝑸} x \land x <_{𝑸} B))$
37	3 36	mpcom	$⊢ A <_{𝑸} B \to \exists x (A <_{𝑸} x \land x <_{𝑸} B)$
38		ltsonq	$⊢ <_{𝑸} Or 𝑸$
39	38 1	sotri	$⊢ (A <_{𝑸} x \land x <_{𝑸} B) \to A <_{𝑸} B$
40	39	exlimiv	$⊢ \exists x (A <_{𝑸} x \land x <_{𝑸} B) \to A <_{𝑸} B$
41	37 40	impbii	$⊢ A <_{𝑸} B \leftrightarrow \exists x (A <_{𝑸} x \land x <_{𝑸} B)$

Metamath Proof Explorer

Theorem ltbtwnnq

Proof