Metamath Proof Explorer

Theorem divne0b

Description: The ratio of nonzero numbers is nonzero. (Contributed by NM, 2-Aug-2004) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Step	Hyp	Ref	Expression
1		diveq0	\|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) = 0 <-> A = 0 ) )
2	1	bicomd	\|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A = 0 <-> ( A / B ) = 0 ) )
3	2	necon3bid	\|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A =/= 0 <-> ( A / B ) =/= 0 ) )

Step

Hyp

Ref

Expression

 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) = 0 <-> A = 0 ) )

 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A = 0 <-> ( A / B ) = 0 ) )

 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A =/= 0 <-> ( A / B ) =/= 0 ) )