Metamath Proof Explorer


Theorem div1d

Description: A number divided by 1 is itself. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypothesis div1d.1 ( 𝜑𝐴 ∈ ℂ )
Assertion div1d ( 𝜑 → ( 𝐴 / 1 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 div1d.1 ( 𝜑𝐴 ∈ ℂ )
2 div1 ( 𝐴 ∈ ℂ → ( 𝐴 / 1 ) = 𝐴 )
3 1 2 syl ( 𝜑 → ( 𝐴 / 1 ) = 𝐴 )