Metamath Proof Explorer

Theorem ordvdsmul

Description: If an integer divides either of two others, it divides their product. (Contributed by Paul Chapman, 17-Nov-2012) (Proof shortened by Mario Carneiro, 17-Jul-2014)

		Ref	Expression
	Assertion	ordvdsmul	\|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K \|\| M \/ K \|\| N ) -> K \|\| ( M x. N ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvdsmultr1	\|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K \|\| M -> K \|\| ( M x. N ) ) )
2		dvdsmultr2	\|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K \|\| N -> K \|\| ( M x. N ) ) )
3	1 2	jaod	\|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K \|\| M \/ K \|\| N ) -> K \|\| ( M x. N ) ) )

Step

Hyp

Ref

Expression

dvdsmultr1

 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K || M -> K || ( M x. N ) ) )

dvdsmultr2

 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K || N -> K || ( M x. N ) ) )

1 2

jaod

 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M \/ K || N ) -> K || ( M x. N ) ) )