Metamath Proof Explorer

Theorem 2sqlem10

Description: Lemma for 2sq . Every factor of a "proper" sum of two squares (where the summands are coprime) is a sum of two squares. (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Hypotheses 2sq.1 
|- S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2sqlem7.2 
|- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }
Assertion 2sqlem10 
|- ( ( A e. Y /\ B e. NN /\ B || A ) -> B e. S )

Proof

Step Hyp Ref Expression
1 2sq.1 
 |-  S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2 2sqlem7.2 
 |-  Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }
3 breq1 
 |-  ( b = B -> ( b || a <-> B || a ) )
4 eleq1 
 |-  ( b = B -> ( b e. S <-> B e. S ) )
5 3 4 imbi12d 
 |-  ( b = B -> ( ( b || a -> b e. S ) <-> ( B || a -> B e. S ) ) )
6 5 ralbidv 
 |-  ( b = B -> ( A. a e. Y ( b || a -> b e. S ) <-> A. a e. Y ( B || a -> B e. S ) ) )
7 oveq2 
 |-  ( m = 1 -> ( 1 ... m ) = ( 1 ... 1 ) )
8 7 raleqdv 
 |-  ( m = 1 -> ( A. b e. ( 1 ... m ) A. a e. Y ( b || a -> b e. S ) <-> A. b e. ( 1 ... 1 ) A. a e. Y ( b || a -> b e. S ) ) )
9 oveq2 
 |-  ( m = n -> ( 1 ... m ) = ( 1 ... n ) )
10 9 raleqdv 
 |-  ( m = n -> ( A. b e. ( 1 ... m ) A. a e. Y ( b || a -> b e. S ) <-> A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) ) )
11 oveq2 
 |-  ( m = ( n + 1 ) -> ( 1 ... m ) = ( 1 ... ( n + 1 ) ) )
12 11 raleqdv 
 |-  ( m = ( n + 1 ) -> ( A. b e. ( 1 ... m ) A. a e. Y ( b || a -> b e. S ) <-> A. b e. ( 1 ... ( n + 1 ) ) A. a e. Y ( b || a -> b e. S ) ) )
13 oveq2 
 |-  ( m = B -> ( 1 ... m ) = ( 1 ... B ) )
14 13 raleqdv 
 |-  ( m = B -> ( A. b e. ( 1 ... m ) A. a e. Y ( b || a -> b e. S ) <-> A. b e. ( 1 ... B ) A. a e. Y ( b || a -> b e. S ) ) )
15 elfz1eq 
 |-  ( b e. ( 1 ... 1 ) -> b = 1 )
16 1z 
 |-  1 e. ZZ
17 zgz 
 |-  ( 1 e. ZZ -> 1 e. Z[i] )
18 16 17 ax-mp 
 |-  1 e. Z[i]
19 sq1 
 |-  ( 1 ^ 2 ) = 1
20 19 eqcomi 
 |-  1 = ( 1 ^ 2 )
21 fveq2 
 |-  ( x = 1 -> ( abs ` x ) = ( abs ` 1 ) )
22 abs1 
 |-  ( abs ` 1 ) = 1
23 21 22 eqtrdi 
 |-  ( x = 1 -> ( abs ` x ) = 1 )
24 23 oveq1d 
 |-  ( x = 1 -> ( ( abs ` x ) ^ 2 ) = ( 1 ^ 2 ) )
25 24 rspceeqv 
 |-  ( ( 1 e. Z[i] /\ 1 = ( 1 ^ 2 ) ) -> E. x e. Z[i] 1 = ( ( abs ` x ) ^ 2 ) )
26 18 20 25 mp2an 
 |-  E. x e. Z[i] 1 = ( ( abs ` x ) ^ 2 )
27 1 2sqlem1 
 |-  ( 1 e. S <-> E. x e. Z[i] 1 = ( ( abs ` x ) ^ 2 ) )
28 26 27 mpbir 
 |-  1 e. S
29 15 28 eqeltrdi 
 |-  ( b e. ( 1 ... 1 ) -> b e. S )
30 29 a1d 
 |-  ( b e. ( 1 ... 1 ) -> ( b || a -> b e. S ) )
31 30 ralrimivw 
 |-  ( b e. ( 1 ... 1 ) -> A. a e. Y ( b || a -> b e. S ) )
32 31 rgen 
 |-  A. b e. ( 1 ... 1 ) A. a e. Y ( b || a -> b e. S )
33 simplr 
 |-  ( ( ( n e. NN /\ A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) ) /\ ( m e. Y /\ ( n + 1 ) || m ) ) -> A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) )
34 nncn 
 |-  ( n e. NN -> n e. CC )
35 34 ad2antrr 
 |-  ( ( ( n e. NN /\ A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) ) /\ ( m e. Y /\ ( n + 1 ) || m ) ) -> n e. CC )
36 ax-1cn 
 |-  1 e. CC
37 pncan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n + 1 ) - 1 ) = n )
38 35 36 37 sylancl 
 |-  ( ( ( n e. NN /\ A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) ) /\ ( m e. Y /\ ( n + 1 ) || m ) ) -> ( ( n + 1 ) - 1 ) = n )
39 38 oveq2d 
 |-  ( ( ( n e. NN /\ A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) ) /\ ( m e. Y /\ ( n + 1 ) || m ) ) -> ( 1 ... ( ( n + 1 ) - 1 ) ) = ( 1 ... n ) )
40 39 raleqdv 
 |-  ( ( ( n e. NN /\ A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) ) /\ ( m e. Y /\ ( n + 1 ) || m ) ) -> ( A. b e. ( 1 ... ( ( n + 1 ) - 1 ) ) A. a e. Y ( b || a -> b e. S ) <-> A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) ) )
41 33 40 mpbird 
 |-  ( ( ( n e. NN /\ A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) ) /\ ( m e. Y /\ ( n + 1 ) || m ) ) -> A. b e. ( 1 ... ( ( n + 1 ) - 1 ) ) A. a e. Y ( b || a -> b e. S ) )
42 simprr 
 |-  ( ( ( n e. NN /\ A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) ) /\ ( m e. Y /\ ( n + 1 ) || m ) ) -> ( n + 1 ) || m )
43 peano2nn 
 |-  ( n e. NN -> ( n + 1 ) e. NN )
44 43 ad2antrr 
 |-  ( ( ( n e. NN /\ A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) ) /\ ( m e. Y /\ ( n + 1 ) || m ) ) -> ( n + 1 ) e. NN )
45 simprl 
 |-  ( ( ( n e. NN /\ A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) ) /\ ( m e. Y /\ ( n + 1 ) || m ) ) -> m e. Y )
46 1 2 41 42 44 45 2sqlem9 
 |-  ( ( ( n e. NN /\ A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) ) /\ ( m e. Y /\ ( n + 1 ) || m ) ) -> ( n + 1 ) e. S )
47 46 expr 
 |-  ( ( ( n e. NN /\ A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) ) /\ m e. Y ) -> ( ( n + 1 ) || m -> ( n + 1 ) e. S ) )
48 47 ralrimiva 
 |-  ( ( n e. NN /\ A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) ) -> A. m e. Y ( ( n + 1 ) || m -> ( n + 1 ) e. S ) )
49 48 ex 
 |-  ( n e. NN -> ( A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) -> A. m e. Y ( ( n + 1 ) || m -> ( n + 1 ) e. S ) ) )
50 breq2 
 |-  ( a = m -> ( ( n + 1 ) || a <-> ( n + 1 ) || m ) )
51 50 imbi1d 
 |-  ( a = m -> ( ( ( n + 1 ) || a -> ( n + 1 ) e. S ) <-> ( ( n + 1 ) || m -> ( n + 1 ) e. S ) ) )
52 51 cbvralvw 
 |-  ( A. a e. Y ( ( n + 1 ) || a -> ( n + 1 ) e. S ) <-> A. m e. Y ( ( n + 1 ) || m -> ( n + 1 ) e. S ) )
53 49 52 syl6ibr 
 |-  ( n e. NN -> ( A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) -> A. a e. Y ( ( n + 1 ) || a -> ( n + 1 ) e. S ) ) )
54 ovex 
 |-  ( n + 1 ) e. _V
55 breq1 
 |-  ( b = ( n + 1 ) -> ( b || a <-> ( n + 1 ) || a ) )
56 eleq1 
 |-  ( b = ( n + 1 ) -> ( b e. S <-> ( n + 1 ) e. S ) )
57 55 56 imbi12d 
 |-  ( b = ( n + 1 ) -> ( ( b || a -> b e. S ) <-> ( ( n + 1 ) || a -> ( n + 1 ) e. S ) ) )
58 57 ralbidv 
 |-  ( b = ( n + 1 ) -> ( A. a e. Y ( b || a -> b e. S ) <-> A. a e. Y ( ( n + 1 ) || a -> ( n + 1 ) e. S ) ) )
59 54 58 ralsn 
 |-  ( A. b e. { ( n + 1 ) } A. a e. Y ( b || a -> b e. S ) <-> A. a e. Y ( ( n + 1 ) || a -> ( n + 1 ) e. S ) )
60 53 59 syl6ibr 
 |-  ( n e. NN -> ( A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) -> A. b e. { ( n + 1 ) } A. a e. Y ( b || a -> b e. S ) ) )
61 60 ancld 
 |-  ( n e. NN -> ( A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) -> ( A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) /\ A. b e. { ( n + 1 ) } A. a e. Y ( b || a -> b e. S ) ) ) )
62 elnnuz 
 |-  ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
63 fzsuc 
 |-  ( n e. ( ZZ>= ` 1 ) -> ( 1 ... ( n + 1 ) ) = ( ( 1 ... n ) u. { ( n + 1 ) } ) )
64 62 63 sylbi 
 |-  ( n e. NN -> ( 1 ... ( n + 1 ) ) = ( ( 1 ... n ) u. { ( n + 1 ) } ) )
65 64 raleqdv 
 |-  ( n e. NN -> ( A. b e. ( 1 ... ( n + 1 ) ) A. a e. Y ( b || a -> b e. S ) <-> A. b e. ( ( 1 ... n ) u. { ( n + 1 ) } ) A. a e. Y ( b || a -> b e. S ) ) )
66 ralunb 
 |-  ( A. b e. ( ( 1 ... n ) u. { ( n + 1 ) } ) A. a e. Y ( b || a -> b e. S ) <-> ( A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) /\ A. b e. { ( n + 1 ) } A. a e. Y ( b || a -> b e. S ) ) )
67 65 66 bitrdi 
 |-  ( n e. NN -> ( A. b e. ( 1 ... ( n + 1 ) ) A. a e. Y ( b || a -> b e. S ) <-> ( A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) /\ A. b e. { ( n + 1 ) } A. a e. Y ( b || a -> b e. S ) ) ) )
68 61 67 sylibrd 
 |-  ( n e. NN -> ( A. b e. ( 1 ... n ) A. a e. Y ( b || a -> b e. S ) -> A. b e. ( 1 ... ( n + 1 ) ) A. a e. Y ( b || a -> b e. S ) ) )
69 8 10 12 14 32 68 nnind 
 |-  ( B e. NN -> A. b e. ( 1 ... B ) A. a e. Y ( b || a -> b e. S ) )
70 elfz1end 
 |-  ( B e. NN <-> B e. ( 1 ... B ) )
71 70 biimpi 
 |-  ( B e. NN -> B e. ( 1 ... B ) )
72 6 69 71 rspcdva 
 |-  ( B e. NN -> A. a e. Y ( B || a -> B e. S ) )
73 breq2 
 |-  ( a = A -> ( B || a <-> B || A ) )
74 73 imbi1d 
 |-  ( a = A -> ( ( B || a -> B e. S ) <-> ( B || A -> B e. S ) ) )
75 74 rspcv 
 |-  ( A e. Y -> ( A. a e. Y ( B || a -> B e. S ) -> ( B || A -> B e. S ) ) )
76 72 75 syl5 
 |-  ( A e. Y -> ( B e. NN -> ( B || A -> B e. S ) ) )
77 76 3imp 
 |-  ( ( A e. Y /\ B e. NN /\ B || A ) -> B e. S )