Metamath Proof Explorer

Theorem divid

Description: A number divided by itself is one. (Contributed by NM, 1-Aug-2004) (Proof shortened by SN, 9-Jul-2025)

Ref Expression
Assertion divid 
|- ( ( A e. CC /\ A =/= 0 ) -> ( A / A ) = 1 )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  A = A
2 diveq1 
 |-  ( ( A e. CC /\ A e. CC /\ A =/= 0 ) -> ( ( A / A ) = 1 <-> A = A ) )
3 1 2 mpbiri 
 |-  ( ( A e. CC /\ A e. CC /\ A =/= 0 ) -> ( A / A ) = 1 )
4 3 3anidm12 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( A / A ) = 1 )