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

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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ ( abs ‘ 𝐴 ) < 𝐵 ) → ( 𝐵 − 𝐴 ) ≠ 0 )

Proof

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