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	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀ 𝑥 ∈ ℝ ( 0 < 𝑥 → 𝐴 < 𝑥 ) ) → 𝐴 = 0 )

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		leloe	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
3	1 2	mpan	⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
4		breq2	⊢ ( 𝑥 = 𝐴 → ( 0 < 𝑥 ↔ 0 < 𝐴 ) )
5		breq2	⊢ ( 𝑥 = 𝐴 → ( 𝐴 < 𝑥 ↔ 𝐴 < 𝐴 ) )
6	4 5	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 0 < 𝑥 → 𝐴 < 𝑥 ) ↔ ( 0 < 𝐴 → 𝐴 < 𝐴 ) ) )
7	6	rspcv	⊢ ( 𝐴 ∈ ℝ → ( ∀ 𝑥 ∈ ℝ ( 0 < 𝑥 → 𝐴 < 𝑥 ) → ( 0 < 𝐴 → 𝐴 < 𝐴 ) ) )
8		ltnr	⊢ ( 𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴 )
9	8	pm2.21d	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < 𝐴 → 𝐴 = 0 ) )
10	9	com12	⊢ ( 𝐴 < 𝐴 → ( 𝐴 ∈ ℝ → 𝐴 = 0 ) )
11	10	imim2i	⊢ ( ( 0 < 𝐴 → 𝐴 < 𝐴 ) → ( 0 < 𝐴 → ( 𝐴 ∈ ℝ → 𝐴 = 0 ) ) )
12	11	com13	⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 → ( ( 0 < 𝐴 → 𝐴 < 𝐴 ) → 𝐴 = 0 ) ) )
13	7 12	syl5d	⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 → ( ∀ 𝑥 ∈ ℝ ( 0 < 𝑥 → 𝐴 < 𝑥 ) → 𝐴 = 0 ) ) )
14		ax-1	⊢ ( 𝐴 = 0 → ( ∀ 𝑥 ∈ ℝ ( 0 < 𝑥 → 𝐴 < 𝑥 ) → 𝐴 = 0 ) )
15	14	eqcoms	⊢ ( 0 = 𝐴 → ( ∀ 𝑥 ∈ ℝ ( 0 < 𝑥 → 𝐴 < 𝑥 ) → 𝐴 = 0 ) )
16	15	a1i	⊢ ( 𝐴 ∈ ℝ → ( 0 = 𝐴 → ( ∀ 𝑥 ∈ ℝ ( 0 < 𝑥 → 𝐴 < 𝑥 ) → 𝐴 = 0 ) ) )
17	13 16	jaod	⊢ ( 𝐴 ∈ ℝ → ( ( 0 < 𝐴 ∨ 0 = 𝐴 ) → ( ∀ 𝑥 ∈ ℝ ( 0 < 𝑥 → 𝐴 < 𝑥 ) → 𝐴 = 0 ) ) )
18	3 17	sylbid	⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 → ( ∀ 𝑥 ∈ ℝ ( 0 < 𝑥 → 𝐴 < 𝑥 ) → 𝐴 = 0 ) ) )
19	18	3imp	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀ 𝑥 ∈ ℝ ( 0 < 𝑥 → 𝐴 < 𝑥 ) ) → 𝐴 = 0 )