Description: A number divided by itself is one. (Contributed by Thierry Arnoux, 18-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | xdivid | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 /𝑒 𝐴 ) = 1 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexdiv | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 /𝑒 𝐴 ) = ( 𝐴 / 𝐴 ) ) | |
2 | 1 | 3anidm12 | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 /𝑒 𝐴 ) = ( 𝐴 / 𝐴 ) ) |
3 | recn | ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ ) | |
4 | divid | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 / 𝐴 ) = 1 ) | |
5 | 3 4 | sylan | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 / 𝐴 ) = 1 ) |
6 | 2 5 | eqtrd | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 /𝑒 𝐴 ) = 1 ) |