Metamath Proof Explorer

Theorem ddcan

Description: Cancellation in a double division. (Contributed by Mario Carneiro, 26-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> A e. CC )
2 simprl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> B e. CC )
3 simprr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> B =/= 0 )
4 divcan1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) x. B ) = A )
5 1 2 3 4 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) x. B ) = A )
6 divcl 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) e. CC )
7 1 2 3 6 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A / B ) e. CC )
8 divne0 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A / B ) =/= 0 )
9 divmul 
 |-  ( ( A e. CC /\ B e. CC /\ ( ( A / B ) e. CC /\ ( A / B ) =/= 0 ) ) -> ( ( A / ( A / B ) ) = B <-> ( ( A / B ) x. B ) = A ) )
10 1 2 7 8 9 syl112anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / ( A / B ) ) = B <-> ( ( A / B ) x. B ) = A ) )
11 5 10 mpbird 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A / ( A / B ) ) = B )