Metamath Proof Explorer

Theorem 2sqlem5

Description: Lemma for 2sq . If a number that is a sum of two squares is divisible by a prime that is a sum of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypotheses 2sq.1 
|- S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2sqlem5.1 
|- ( ph -> N e. NN )
2sqlem5.2 
|- ( ph -> P e. Prime )
2sqlem5.3 
|- ( ph -> ( N x. P ) e. S )
2sqlem5.4 
|- ( ph -> P e. S )
Assertion 2sqlem5 
|- ( ph -> N e. S )

Proof

Step Hyp Ref Expression
1 2sq.1 
 |-  S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2 2sqlem5.1 
 |-  ( ph -> N e. NN )
3 2sqlem5.2 
 |-  ( ph -> P e. Prime )
4 2sqlem5.3 
 |-  ( ph -> ( N x. P ) e. S )
5 2sqlem5.4 
 |-  ( ph -> P e. S )
6 1 2sqlem2 
 |-  ( P e. S <-> E. p e. ZZ E. q e. ZZ P = ( ( p ^ 2 ) + ( q ^ 2 ) ) )
7 5 6 sylib 
 |-  ( ph -> E. p e. ZZ E. q e. ZZ P = ( ( p ^ 2 ) + ( q ^ 2 ) ) )
8 1 2sqlem2 
 |-  ( ( N x. P ) e. S <-> E. x e. ZZ E. y e. ZZ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
9 4 8 sylib 
 |-  ( ph -> E. x e. ZZ E. y e. ZZ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
10 reeanv 
 |-  ( E. p e. ZZ E. x e. ZZ ( E. q e. ZZ P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ E. y e. ZZ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> ( E. p e. ZZ E. q e. ZZ P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ E. x e. ZZ E. y e. ZZ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
11 reeanv 
 |-  ( E. q e. ZZ E. y e. ZZ ( P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> ( E. q e. ZZ P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ E. y e. ZZ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
12 2 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ZZ /\ x e. ZZ ) ) /\ ( ( q e. ZZ /\ y e. ZZ ) /\ ( P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) -> N e. NN )
13 3 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ZZ /\ x e. ZZ ) ) /\ ( ( q e. ZZ /\ y e. ZZ ) /\ ( P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) -> P e. Prime )
14 simplrr 
 |-  ( ( ( ph /\ ( p e. ZZ /\ x e. ZZ ) ) /\ ( ( q e. ZZ /\ y e. ZZ ) /\ ( P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) -> x e. ZZ )
15 simprlr 
 |-  ( ( ( ph /\ ( p e. ZZ /\ x e. ZZ ) ) /\ ( ( q e. ZZ /\ y e. ZZ ) /\ ( P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) -> y e. ZZ )
16 simplrl 
 |-  ( ( ( ph /\ ( p e. ZZ /\ x e. ZZ ) ) /\ ( ( q e. ZZ /\ y e. ZZ ) /\ ( P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) -> p e. ZZ )
17 simprll 
 |-  ( ( ( ph /\ ( p e. ZZ /\ x e. ZZ ) ) /\ ( ( q e. ZZ /\ y e. ZZ ) /\ ( P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) -> q e. ZZ )
18 simprrr 
 |-  ( ( ( ph /\ ( p e. ZZ /\ x e. ZZ ) ) /\ ( ( q e. ZZ /\ y e. ZZ ) /\ ( P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) -> ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
19 simprrl 
 |-  ( ( ( ph /\ ( p e. ZZ /\ x e. ZZ ) ) /\ ( ( q e. ZZ /\ y e. ZZ ) /\ ( P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) -> P = ( ( p ^ 2 ) + ( q ^ 2 ) ) )
20 1 12 13 14 15 16 17 18 19 2sqlem4 
 |-  ( ( ( ph /\ ( p e. ZZ /\ x e. ZZ ) ) /\ ( ( q e. ZZ /\ y e. ZZ ) /\ ( P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) ) -> N e. S )
21 20 expr 
 |-  ( ( ( ph /\ ( p e. ZZ /\ x e. ZZ ) ) /\ ( q e. ZZ /\ y e. ZZ ) ) -> ( ( P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> N e. S ) )
22 21 rexlimdvva 
 |-  ( ( ph /\ ( p e. ZZ /\ x e. ZZ ) ) -> ( E. q e. ZZ E. y e. ZZ ( P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> N e. S ) )
23 11 22 syl5bir 
 |-  ( ( ph /\ ( p e. ZZ /\ x e. ZZ ) ) -> ( ( E. q e. ZZ P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ E. y e. ZZ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> N e. S ) )
24 23 rexlimdvva 
 |-  ( ph -> ( E. p e. ZZ E. x e. ZZ ( E. q e. ZZ P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ E. y e. ZZ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> N e. S ) )
25 10 24 syl5bir 
 |-  ( ph -> ( ( E. p e. ZZ E. q e. ZZ P = ( ( p ^ 2 ) + ( q ^ 2 ) ) /\ E. x e. ZZ E. y e. ZZ ( N x. P ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> N e. S ) )
26 7 9 25 mp2and 
 |-  ( ph -> N e. S )