Theorem qsqueeze

Description: If a nonnegative real is less than any positive rational, it is zero. (Contributed by NM, 6-Feb-2007)

	Ref	Expression
Assertion	qsqueeze	$$⊢\left(A\in ℝ\wedge 0\le A\wedge \forall x\in \mathbb{Q}\left(0<x\to A<x\right)\right)\to A=0$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2		ltnle	$$⊢\left(0\in ℝ\wedge A\in ℝ\right)\to \left(0<A\leftrightarrow \neg A\le 0\right)$$
3	1 2	mpan	$$⊢A\in ℝ\to \left(0<A\leftrightarrow \neg A\le 0\right)$$
4		qbtwnre	$$⊢\left(0\in ℝ\wedge A\in ℝ\wedge 0<A\right)\to \exists x\in \mathbb{Q}\left(0<x\wedge x<A\right)$$
5	1 4	mp3an1	$$⊢\left(A\in ℝ\wedge 0<A\right)\to \exists x\in \mathbb{Q}\left(0<x\wedge x<A\right)$$
6	5	ex	$$⊢A\in ℝ\to \left(0<A\to \exists x\in \mathbb{Q}\left(0<x\wedge x<A\right)\right)$$
7		qre	$$⊢x\in \mathbb{Q}\to x\in ℝ$$
8		ltnsym	$$⊢\left(A\in ℝ\wedge x\in ℝ\right)\to \left(A<x\to \neg x<A\right)$$
9	8	con2d	$$⊢\left(A\in ℝ\wedge x\in ℝ\right)\to \left(x<A\to \neg A<x\right)$$
10	7 9	sylan2	$$⊢\left(A\in ℝ\wedge x\in \mathbb{Q}\right)\to \left(x<A\to \neg A<x\right)$$
11	10	anim2d	$$⊢\left(A\in ℝ\wedge x\in \mathbb{Q}\right)\to \left(\left(0<x\wedge x<A\right)\to \left(0<x\wedge \neg A<x\right)\right)$$
12	11	reximdva	$$⊢A\in ℝ\to \left(\exists x\in \mathbb{Q}\left(0<x\wedge x<A\right)\to \exists x\in \mathbb{Q}\left(0<x\wedge \neg A<x\right)\right)$$
13	6 12	syld	$$⊢A\in ℝ\to \left(0<A\to \exists x\in \mathbb{Q}\left(0<x\wedge \neg A<x\right)\right)$$
14	3 13	sylbird	$$⊢A\in ℝ\to \left(\neg A\le 0\to \exists x\in \mathbb{Q}\left(0<x\wedge \neg A<x\right)\right)$$
15		rexanali	$$⊢\exists x\in \mathbb{Q}\left(0<x\wedge \neg A<x\right)\leftrightarrow \neg \forall x\in \mathbb{Q}\left(0<x\to A<x\right)$$
16	14 15	imbitrdi	$$⊢A\in ℝ\to \left(\neg A\le 0\to \neg \forall x\in \mathbb{Q}\left(0<x\to A<x\right)\right)$$
17	16	con4d	$$⊢A\in ℝ\to \left(\forall x\in \mathbb{Q}\left(0<x\to A<x\right)\to A\le 0\right)$$
18	17	imp	$$⊢\left(A\in ℝ\wedge \forall x\in \mathbb{Q}\left(0<x\to A<x\right)\right)\to A\le 0$$
19	18	3adant2	$$⊢\left(A\in ℝ\wedge 0\le A\wedge \forall x\in \mathbb{Q}\left(0<x\to A<x\right)\right)\to A\le 0$$
20		letri3	$$⊢\left(A\in ℝ\wedge 0\in ℝ\right)\to \left(A=0\leftrightarrow \left(A\le 0\wedge 0\le A\right)\right)$$
21	1 20	mpan2	$$⊢A\in ℝ\to \left(A=0\leftrightarrow \left(A\le 0\wedge 0\le A\right)\right)$$
22	21	rbaibd	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \left(A=0\leftrightarrow A\le 0\right)$$
23	22	3adant3	$$⊢\left(A\in ℝ\wedge 0\le A\wedge \forall x\in \mathbb{Q}\left(0<x\to A<x\right)\right)\to \left(A=0\leftrightarrow A\le 0\right)$$
24	19 23	mpbird	$$⊢\left(A\in ℝ\wedge 0\le A\wedge \forall x\in \mathbb{Q}\left(0<x\to A<x\right)\right)\to A=0$$