Metamath Proof Explorer

Theorem recdiv2

Description: Division into a reciprocal. (Contributed by NM, 19-Oct-2007)

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

Step	Hyp	Ref	Expression
1		ax-1cn	\|- 1 e. CC
2		divdiv1	\|- ( ( 1 e. CC /\ ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / A ) / B ) = ( 1 / ( A x. B ) ) )
3	1 2	mp3an1	\|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / A ) / B ) = ( 1 / ( A x. B ) ) )

Step

Hyp

Ref

Expression

 |-  1 e. CC

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

1 2

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