Theorem 4sqlem9

Description: Lemma for 4sq . (Contributed by Mario Carneiro, 15-Jul-2014)

	Ref	Expression
Hypotheses	4sqlem5.2	|- ( ph -> A e. ZZ )
	4sqlem5.3	|- ( ph -> M e. NN )
	4sqlem5.4	|- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )
	4sqlem9.5	|- ( ( ph /\ ps ) -> ( B ^ 2 ) = 0 )
Assertion	4sqlem9	|- ( ( ph /\ ps ) -> ( M ^ 2 ) || ( A ^ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		4sqlem5.2	|- ( ph -> A e. ZZ )
2		4sqlem5.3	|- ( ph -> M e. NN )
3		4sqlem5.4	|- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )
4		4sqlem9.5	|- ( ( ph /\ ps ) -> ( B ^ 2 ) = 0 )
5	1 2 3	4sqlem5	|- ( ph -> ( B e. ZZ /\ ( ( A - B ) / M ) e. ZZ ) )
6	5	simpld	|- ( ph -> B e. ZZ )
7	6	zcnd	|- ( ph -> B e. CC )
8		sqeq0	|- ( B e. CC -> ( ( B ^ 2 ) = 0 <-> B = 0 ) )
9	7 8	syl	|- ( ph -> ( ( B ^ 2 ) = 0 <-> B = 0 ) )
10	9	biimpa	|- ( ( ph /\ ( B ^ 2 ) = 0 ) -> B = 0 )
11	4 10	syldan	|- ( ( ph /\ ps ) -> B = 0 )
12	11	oveq2d	|- ( ( ph /\ ps ) -> ( A - B ) = ( A - 0 ) )
13	1	adantr	|- ( ( ph /\ ps ) -> A e. ZZ )
14	13	zcnd	|- ( ( ph /\ ps ) -> A e. CC )
15	14	subid1d	|- ( ( ph /\ ps ) -> ( A - 0 ) = A )
16	12 15	eqtrd	|- ( ( ph /\ ps ) -> ( A - B ) = A )
17	16	oveq1d	|- ( ( ph /\ ps ) -> ( ( A - B ) / M ) = ( A / M ) )
18	5	simprd	|- ( ph -> ( ( A - B ) / M ) e. ZZ )
19	18	adantr	|- ( ( ph /\ ps ) -> ( ( A - B ) / M ) e. ZZ )
20	17 19	eqeltrrd	|- ( ( ph /\ ps ) -> ( A / M ) e. ZZ )
21	2	nnzd	|- ( ph -> M e. ZZ )
22	2	nnne0d	|- ( ph -> M =/= 0 )
23		dvdsval2	|- ( ( M e. ZZ /\ M =/= 0 /\ A e. ZZ ) -> ( M || A <-> ( A / M ) e. ZZ ) )
24	21 22 1 23	syl3anc	|- ( ph -> ( M || A <-> ( A / M ) e. ZZ ) )
25	24	adantr	|- ( ( ph /\ ps ) -> ( M || A <-> ( A / M ) e. ZZ ) )
26	20 25	mpbird	|- ( ( ph /\ ps ) -> M || A )
27		dvdssq	|- ( ( M e. ZZ /\ A e. ZZ ) -> ( M || A <-> ( M ^ 2 ) || ( A ^ 2 ) ) )
28	21 13 27	syl2an2r	|- ( ( ph /\ ps ) -> ( M || A <-> ( M ^ 2 ) || ( A ^ 2 ) ) )
29	26 28	mpbid	|- ( ( ph /\ ps ) -> ( M ^ 2 ) || ( A ^ 2 ) )