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 i w 2
2sqlem7.2 Y = z | x y x gcd y = 1 z = x 2 + y 2
Assertion 2sqlem10 A Y B B A B S

Proof

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