Theorem squeeze0

Description: If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006)

	Ref	Expression
Assertion	squeeze0	$$⊢\left(A\in ℝ\wedge 0\le A\wedge \forall x\in ℝ\left(0<x\to A<x\right)\right)\to A=0$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2		leloe	$$⊢\left(0\in ℝ\wedge A\in ℝ\right)\to \left(0\le A\leftrightarrow \left(0<A\vee 0=A\right)\right)$$
3	1 2	mpan	$$⊢A\in ℝ\to \left(0\le A\leftrightarrow \left(0<A\vee 0=A\right)\right)$$
4		breq2	$$⊢x=A\to \left(0<x\leftrightarrow 0<A\right)$$
5		breq2	$$⊢x=A\to \left(A<x\leftrightarrow A<A\right)$$
6	4 5	imbi12d	$$⊢x=A\to \left(\left(0<x\to A<x\right)\leftrightarrow \left(0<A\to A<A\right)\right)$$
7	6	rspcv	$$⊢A\in ℝ\to \left(\forall x\in ℝ\left(0<x\to A<x\right)\to \left(0<A\to A<A\right)\right)$$
8		ltnr	$$⊢A\in ℝ\to \neg A<A$$
9	8	pm2.21d	$$⊢A\in ℝ\to \left(A<A\to A=0\right)$$
10	9	com12	$$⊢A<A\to \left(A\in ℝ\to A=0\right)$$
11	10	imim2i	$$⊢\left(0<A\to A<A\right)\to \left(0<A\to \left(A\in ℝ\to A=0\right)\right)$$
12	11	com13	$$⊢A\in ℝ\to \left(0<A\to \left(\left(0<A\to A<A\right)\to A=0\right)\right)$$
13	7 12	syl5d	$$⊢A\in ℝ\to \left(0<A\to \left(\forall x\in ℝ\left(0<x\to A<x\right)\to A=0\right)\right)$$
14		ax-1	$$⊢A=0\to \left(\forall x\in ℝ\left(0<x\to A<x\right)\to A=0\right)$$
15	14	eqcoms	$$⊢0=A\to \left(\forall x\in ℝ\left(0<x\to A<x\right)\to A=0\right)$$
16	15	a1i	$$⊢A\in ℝ\to \left(0=A\to \left(\forall x\in ℝ\left(0<x\to A<x\right)\to A=0\right)\right)$$
17	13 16	jaod	$$⊢A\in ℝ\to \left(\left(0<A\vee 0=A\right)\to \left(\forall x\in ℝ\left(0<x\to A<x\right)\to A=0\right)\right)$$
18	3 17	sylbid	$$⊢A\in ℝ\to \left(0\le A\to \left(\forall x\in ℝ\left(0<x\to A<x\right)\to A=0\right)\right)$$
19	18	3imp	$$⊢\left(A\in ℝ\wedge 0\le A\wedge \forall x\in ℝ\left(0<x\to A<x\right)\right)\to A=0$$