Metamath Proof Explorer

Theorem abssubne0

Description: If the absolute value of a complex number is less than a real, its difference from the real is nonzero. (Contributed by NM, 2-Nov-2007) (Proof shortened by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion abssubne0 ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ A < B → B − A ≠ 0

Proof

Step Hyp Ref Expression
1 simplr ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ A < B → B ∈ ℝ
2 1 recnd ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ A < B → B ∈ ℂ
3 simpll ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ A < B → A ∈ ℂ
4 abscl ⊢ A ∈ ℂ → A ∈ ℝ
5 3 4 syl ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ A < B → A ∈ ℝ
6 abscl ⊢ B ∈ ℂ → B ∈ ℝ
7 2 6 syl ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ A < B → B ∈ ℝ
8 simpr ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ A < B → A < B
9 leabs ⊢ B ∈ ℝ → B ≤ B
10 1 9 syl ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ A < B → B ≤ B
11 5 1 7 8 10 ltletrd ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ A < B → A < B
12 5 11 gtned ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ A < B → B ≠ A
13 fveq2 ⊢ B = A → B = A
14 13 necon3i ⊢ B ≠ A → B ≠ A
15 12 14 syl ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ A < B → B ≠ A
16 2 3 15 subne0d ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ A < B → B − A ≠ 0
17 16 3impa ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ A < B → B − A ≠ 0