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

Metamath Proof Explorer

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 )