Metamath Proof Explorer

Theorem div1

Description: A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion div1 
|- ( A e. CC -> ( A / 1 ) = A )

Proof

Step Hyp Ref Expression
1 mulid2 
 |-  ( A e. CC -> ( 1 x. A ) = A )
2 ax-1cn 
 |-  1 e. CC
3 ax-1ne0 
 |-  1 =/= 0
4 2 3 pm3.2i 
 |-  ( 1 e. CC /\ 1 =/= 0 )
5 divmul 
 |-  ( ( A e. CC /\ A e. CC /\ ( 1 e. CC /\ 1 =/= 0 ) ) -> ( ( A / 1 ) = A <-> ( 1 x. A ) = A ) )
6 4 5 mp3an3 
 |-  ( ( A e. CC /\ A e. CC ) -> ( ( A / 1 ) = A <-> ( 1 x. A ) = A ) )
7 6 anidms 
 |-  ( A e. CC -> ( ( A / 1 ) = A <-> ( 1 x. A ) = A ) )
8 1 7 mpbird 
 |-  ( A e. CC -> ( A / 1 ) = A )