Theorem prmdvdssqOLD

Description: Obsolete version of prmdvdssq as of 21-Aug-2024. (Contributed by Scott Fenton, 8-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	prmdvdssqOLD	|- ( ( P e. Prime /\ M e. ZZ ) -> ( P || M <-> P || ( M ^ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zcn	|- ( M e. ZZ -> M e. CC )
2	1	sqvald	|- ( M e. ZZ -> ( M ^ 2 ) = ( M x. M ) )
3	2	breq2d	|- ( M e. ZZ -> ( P || ( M ^ 2 ) <-> P || ( M x. M ) ) )
4	3	adantl	|- ( ( P e. Prime /\ M e. ZZ ) -> ( P || ( M ^ 2 ) <-> P || ( M x. M ) ) )
5		euclemma	|- ( ( P e. Prime /\ M e. ZZ /\ M e. ZZ ) -> ( P || ( M x. M ) <-> ( P || M \/ P || M ) ) )
6	5	3anidm23	|- ( ( P e. Prime /\ M e. ZZ ) -> ( P || ( M x. M ) <-> ( P || M \/ P || M ) ) )
7		oridm	|- ( ( P || M \/ P || M ) <-> P || M )
8	6 7	bitrdi	|- ( ( P e. Prime /\ M e. ZZ ) -> ( P || ( M x. M ) <-> P || M ) )
9	4 8	bitr2d	|- ( ( P e. Prime /\ M e. ZZ ) -> ( P || M <-> P || ( M ^ 2 ) ) )