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 )