Theorem 4sqlem7

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 ) )
Assertion	4sqlem7	|- ( ph -> ( B ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 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	1 2 3	4sqlem5	|- ( ph -> ( B e. ZZ /\ ( ( A - B ) / M ) e. ZZ ) )
5	4	simpld	|- ( ph -> B e. ZZ )
6	5	zred	|- ( ph -> B e. RR )
7	2	nnrpd	|- ( ph -> M e. RR+ )
8	7	rphalfcld	|- ( ph -> ( M / 2 ) e. RR+ )
9	8	rpred	|- ( ph -> ( M / 2 ) e. RR )
10	1 2 3	4sqlem6	|- ( ph -> ( -u ( M / 2 ) <_ B /\ B < ( M / 2 ) ) )
11	10	simprd	|- ( ph -> B < ( M / 2 ) )
12	6 9 11	ltled	|- ( ph -> B <_ ( M / 2 ) )
13	10	simpld	|- ( ph -> -u ( M / 2 ) <_ B )
14	9 6 13	lenegcon1d	|- ( ph -> -u B <_ ( M / 2 ) )
15	8	rpge0d	|- ( ph -> 0 <_ ( M / 2 ) )
16		lenegsq	|- ( ( B e. RR /\ ( M / 2 ) e. RR /\ 0 <_ ( M / 2 ) ) -> ( ( B <_ ( M / 2 ) /\ -u B <_ ( M / 2 ) ) <-> ( B ^ 2 ) <_ ( ( M / 2 ) ^ 2 ) ) )
17	6 9 15 16	syl3anc	|- ( ph -> ( ( B <_ ( M / 2 ) /\ -u B <_ ( M / 2 ) ) <-> ( B ^ 2 ) <_ ( ( M / 2 ) ^ 2 ) ) )
18	12 14 17	mpbi2and	|- ( ph -> ( B ^ 2 ) <_ ( ( M / 2 ) ^ 2 ) )
19		2cnd	|- ( ph -> 2 e. CC )
20	19	sqvald	|- ( ph -> ( 2 ^ 2 ) = ( 2 x. 2 ) )
21	20	oveq2d	|- ( ph -> ( ( M ^ 2 ) / ( 2 ^ 2 ) ) = ( ( M ^ 2 ) / ( 2 x. 2 ) ) )
22	2	nncnd	|- ( ph -> M e. CC )
23		2ne0	|- 2 =/= 0
24	23	a1i	|- ( ph -> 2 =/= 0 )
25	22 19 24	sqdivd	|- ( ph -> ( ( M / 2 ) ^ 2 ) = ( ( M ^ 2 ) / ( 2 ^ 2 ) ) )
26	22	sqcld	|- ( ph -> ( M ^ 2 ) e. CC )
27	26 19 19 24 24	divdiv1d	|- ( ph -> ( ( ( M ^ 2 ) / 2 ) / 2 ) = ( ( M ^ 2 ) / ( 2 x. 2 ) ) )
28	21 25 27	3eqtr4d	|- ( ph -> ( ( M / 2 ) ^ 2 ) = ( ( ( M ^ 2 ) / 2 ) / 2 ) )
29	18 28	breqtrd	|- ( ph -> ( B ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) )