Metamath Proof Explorer

Theorem 2sqlem4

Description: Lemma for 2sqlem5 . (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 )
2sqlem4.3 
|- ( ph -> A e. ZZ )
2sqlem4.4 
|- ( ph -> B e. ZZ )
2sqlem4.5 
|- ( ph -> C e. ZZ )
2sqlem4.6 
|- ( ph -> D e. ZZ )
2sqlem4.7 
|- ( ph -> ( N x. P ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
2sqlem4.8 
|- ( ph -> P = ( ( C ^ 2 ) + ( D ^ 2 ) ) )
Assertion 2sqlem4 
|- ( 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 2sqlem4.3 
 |-  ( ph -> A e. ZZ )
5 2sqlem4.4 
 |-  ( ph -> B e. ZZ )
6 2sqlem4.5 
 |-  ( ph -> C e. ZZ )
7 2sqlem4.6 
 |-  ( ph -> D e. ZZ )
8 2sqlem4.7 
 |-  ( ph -> ( N x. P ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
9 2sqlem4.8 
 |-  ( ph -> P = ( ( C ^ 2 ) + ( D ^ 2 ) ) )
10 2 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) + ( A x. D ) ) ) -> N e. NN )
11 3 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) + ( A x. D ) ) ) -> P e. Prime )
12 4 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) + ( A x. D ) ) ) -> A e. ZZ )
13 5 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) + ( A x. D ) ) ) -> B e. ZZ )
14 6 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) + ( A x. D ) ) ) -> C e. ZZ )
15 7 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) + ( A x. D ) ) ) -> D e. ZZ )
16 8 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) + ( A x. D ) ) ) -> ( N x. P ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
17 9 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) + ( A x. D ) ) ) -> P = ( ( C ^ 2 ) + ( D ^ 2 ) ) )
18 simpr 
 |-  ( ( ph /\ P || ( ( C x. B ) + ( A x. D ) ) ) -> P || ( ( C x. B ) + ( A x. D ) ) )
19 1 10 11 12 13 14 15 16 17 18 2sqlem3 
 |-  ( ( ph /\ P || ( ( C x. B ) + ( A x. D ) ) ) -> N e. S )
20 2 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) - ( A x. D ) ) ) -> N e. NN )
21 3 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) - ( A x. D ) ) ) -> P e. Prime )
22 4 znegcld 
 |-  ( ph -> -u A e. ZZ )
23 22 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) - ( A x. D ) ) ) -> -u A e. ZZ )
24 5 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) - ( A x. D ) ) ) -> B e. ZZ )
25 6 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) - ( A x. D ) ) ) -> C e. ZZ )
26 7 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) - ( A x. D ) ) ) -> D e. ZZ )
27 4 zcnd 
 |-  ( ph -> A e. CC )
28 sqneg 
 |-  ( A e. CC -> ( -u A ^ 2 ) = ( A ^ 2 ) )
29 27 28 syl 
 |-  ( ph -> ( -u A ^ 2 ) = ( A ^ 2 ) )
30 29 oveq1d 
 |-  ( ph -> ( ( -u A ^ 2 ) + ( B ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
31 8 30 eqtr4d 
 |-  ( ph -> ( N x. P ) = ( ( -u A ^ 2 ) + ( B ^ 2 ) ) )
32 31 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) - ( A x. D ) ) ) -> ( N x. P ) = ( ( -u A ^ 2 ) + ( B ^ 2 ) ) )
33 9 adantr 
 |-  ( ( ph /\ P || ( ( C x. B ) - ( A x. D ) ) ) -> P = ( ( C ^ 2 ) + ( D ^ 2 ) ) )
34 7 zcnd 
 |-  ( ph -> D e. CC )
35 27 34 mulneg1d 
 |-  ( ph -> ( -u A x. D ) = -u ( A x. D ) )
36 35 oveq2d 
 |-  ( ph -> ( ( C x. B ) + ( -u A x. D ) ) = ( ( C x. B ) + -u ( A x. D ) ) )
37 6 5 zmulcld 
 |-  ( ph -> ( C x. B ) e. ZZ )
38 37 zcnd 
 |-  ( ph -> ( C x. B ) e. CC )
39 4 7 zmulcld 
 |-  ( ph -> ( A x. D ) e. ZZ )
40 39 zcnd 
 |-  ( ph -> ( A x. D ) e. CC )
41 38 40 negsubd 
 |-  ( ph -> ( ( C x. B ) + -u ( A x. D ) ) = ( ( C x. B ) - ( A x. D ) ) )
42 36 41 eqtrd 
 |-  ( ph -> ( ( C x. B ) + ( -u A x. D ) ) = ( ( C x. B ) - ( A x. D ) ) )
43 42 breq2d 
 |-  ( ph -> ( P || ( ( C x. B ) + ( -u A x. D ) ) <-> P || ( ( C x. B ) - ( A x. D ) ) ) )
44 43 biimpar 
 |-  ( ( ph /\ P || ( ( C x. B ) - ( A x. D ) ) ) -> P || ( ( C x. B ) + ( -u A x. D ) ) )
45 1 20 21 23 24 25 26 32 33 44 2sqlem3 
 |-  ( ( ph /\ P || ( ( C x. B ) - ( A x. D ) ) ) -> N e. S )
46 prmz 
 |-  ( P e. Prime -> P e. ZZ )
47 3 46 syl 
 |-  ( ph -> P e. ZZ )
48 zsqcl 
 |-  ( C e. ZZ -> ( C ^ 2 ) e. ZZ )
49 6 48 syl 
 |-  ( ph -> ( C ^ 2 ) e. ZZ )
50 2 nnzd 
 |-  ( ph -> N e. ZZ )
51 49 50 zmulcld 
 |-  ( ph -> ( ( C ^ 2 ) x. N ) e. ZZ )
52 zsqcl 
 |-  ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
53 4 52 syl 
 |-  ( ph -> ( A ^ 2 ) e. ZZ )
54 51 53 zsubcld 
 |-  ( ph -> ( ( ( C ^ 2 ) x. N ) - ( A ^ 2 ) ) e. ZZ )
55 dvdsmul1 
 |-  ( ( P e. ZZ /\ ( ( ( C ^ 2 ) x. N ) - ( A ^ 2 ) ) e. ZZ ) -> P || ( P x. ( ( ( C ^ 2 ) x. N ) - ( A ^ 2 ) ) ) )
56 47 54 55 syl2anc 
 |-  ( ph -> P || ( P x. ( ( ( C ^ 2 ) x. N ) - ( A ^ 2 ) ) ) )
57 6 4 zmulcld 
 |-  ( ph -> ( C x. A ) e. ZZ )
58 57 zcnd 
 |-  ( ph -> ( C x. A ) e. CC )
59 58 sqcld 
 |-  ( ph -> ( ( C x. A ) ^ 2 ) e. CC )
60 38 sqcld 
 |-  ( ph -> ( ( C x. B ) ^ 2 ) e. CC )
61 40 sqcld 
 |-  ( ph -> ( ( A x. D ) ^ 2 ) e. CC )
62 59 60 61 pnpcand 
 |-  ( ph -> ( ( ( ( C x. A ) ^ 2 ) + ( ( C x. B ) ^ 2 ) ) - ( ( ( C x. A ) ^ 2 ) + ( ( A x. D ) ^ 2 ) ) ) = ( ( ( C x. B ) ^ 2 ) - ( ( A x. D ) ^ 2 ) ) )
63 6 zcnd 
 |-  ( ph -> C e. CC )
64 63 27 sqmuld 
 |-  ( ph -> ( ( C x. A ) ^ 2 ) = ( ( C ^ 2 ) x. ( A ^ 2 ) ) )
65 5 zcnd 
 |-  ( ph -> B e. CC )
66 63 65 sqmuld 
 |-  ( ph -> ( ( C x. B ) ^ 2 ) = ( ( C ^ 2 ) x. ( B ^ 2 ) ) )
67 64 66 oveq12d 
 |-  ( ph -> ( ( ( C x. A ) ^ 2 ) + ( ( C x. B ) ^ 2 ) ) = ( ( ( C ^ 2 ) x. ( A ^ 2 ) ) + ( ( C ^ 2 ) x. ( B ^ 2 ) ) ) )
68 63 sqcld 
 |-  ( ph -> ( C ^ 2 ) e. CC )
69 53 zcnd 
 |-  ( ph -> ( A ^ 2 ) e. CC )
70 65 sqcld 
 |-  ( ph -> ( B ^ 2 ) e. CC )
71 68 69 70 adddid 
 |-  ( ph -> ( ( C ^ 2 ) x. ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = ( ( ( C ^ 2 ) x. ( A ^ 2 ) ) + ( ( C ^ 2 ) x. ( B ^ 2 ) ) ) )
72 67 71 eqtr4d 
 |-  ( ph -> ( ( ( C x. A ) ^ 2 ) + ( ( C x. B ) ^ 2 ) ) = ( ( C ^ 2 ) x. ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
73 2 nncnd 
 |-  ( ph -> N e. CC )
74 47 zcnd 
 |-  ( ph -> P e. CC )
75 73 74 mulcomd 
 |-  ( ph -> ( N x. P ) = ( P x. N ) )
76 8 75 eqtr3d 
 |-  ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( P x. N ) )
77 76 oveq2d 
 |-  ( ph -> ( ( C ^ 2 ) x. ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = ( ( C ^ 2 ) x. ( P x. N ) ) )
78 68 74 73 mul12d 
 |-  ( ph -> ( ( C ^ 2 ) x. ( P x. N ) ) = ( P x. ( ( C ^ 2 ) x. N ) ) )
79 77 78 eqtrd 
 |-  ( ph -> ( ( C ^ 2 ) x. ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = ( P x. ( ( C ^ 2 ) x. N ) ) )
80 72 79 eqtrd 
 |-  ( ph -> ( ( ( C x. A ) ^ 2 ) + ( ( C x. B ) ^ 2 ) ) = ( P x. ( ( C ^ 2 ) x. N ) ) )
81 27 34 sqmuld 
 |-  ( ph -> ( ( A x. D ) ^ 2 ) = ( ( A ^ 2 ) x. ( D ^ 2 ) ) )
82 34 sqcld 
 |-  ( ph -> ( D ^ 2 ) e. CC )
83 69 82 mulcomd 
 |-  ( ph -> ( ( A ^ 2 ) x. ( D ^ 2 ) ) = ( ( D ^ 2 ) x. ( A ^ 2 ) ) )
84 81 83 eqtrd 
 |-  ( ph -> ( ( A x. D ) ^ 2 ) = ( ( D ^ 2 ) x. ( A ^ 2 ) ) )
85 64 84 oveq12d 
 |-  ( ph -> ( ( ( C x. A ) ^ 2 ) + ( ( A x. D ) ^ 2 ) ) = ( ( ( C ^ 2 ) x. ( A ^ 2 ) ) + ( ( D ^ 2 ) x. ( A ^ 2 ) ) ) )
86 49 zcnd 
 |-  ( ph -> ( C ^ 2 ) e. CC )
87 86 82 69 adddird 
 |-  ( ph -> ( ( ( C ^ 2 ) + ( D ^ 2 ) ) x. ( A ^ 2 ) ) = ( ( ( C ^ 2 ) x. ( A ^ 2 ) ) + ( ( D ^ 2 ) x. ( A ^ 2 ) ) ) )
88 85 87 eqtr4d 
 |-  ( ph -> ( ( ( C x. A ) ^ 2 ) + ( ( A x. D ) ^ 2 ) ) = ( ( ( C ^ 2 ) + ( D ^ 2 ) ) x. ( A ^ 2 ) ) )
89 9 oveq1d 
 |-  ( ph -> ( P x. ( A ^ 2 ) ) = ( ( ( C ^ 2 ) + ( D ^ 2 ) ) x. ( A ^ 2 ) ) )
90 88 89 eqtr4d 
 |-  ( ph -> ( ( ( C x. A ) ^ 2 ) + ( ( A x. D ) ^ 2 ) ) = ( P x. ( A ^ 2 ) ) )
91 80 90 oveq12d 
 |-  ( ph -> ( ( ( ( C x. A ) ^ 2 ) + ( ( C x. B ) ^ 2 ) ) - ( ( ( C x. A ) ^ 2 ) + ( ( A x. D ) ^ 2 ) ) ) = ( ( P x. ( ( C ^ 2 ) x. N ) ) - ( P x. ( A ^ 2 ) ) ) )
92 51 zcnd 
 |-  ( ph -> ( ( C ^ 2 ) x. N ) e. CC )
93 74 92 69 subdid 
 |-  ( ph -> ( P x. ( ( ( C ^ 2 ) x. N ) - ( A ^ 2 ) ) ) = ( ( P x. ( ( C ^ 2 ) x. N ) ) - ( P x. ( A ^ 2 ) ) ) )
94 91 93 eqtr4d 
 |-  ( ph -> ( ( ( ( C x. A ) ^ 2 ) + ( ( C x. B ) ^ 2 ) ) - ( ( ( C x. A ) ^ 2 ) + ( ( A x. D ) ^ 2 ) ) ) = ( P x. ( ( ( C ^ 2 ) x. N ) - ( A ^ 2 ) ) ) )
95 62 94 eqtr3d 
 |-  ( ph -> ( ( ( C x. B ) ^ 2 ) - ( ( A x. D ) ^ 2 ) ) = ( P x. ( ( ( C ^ 2 ) x. N ) - ( A ^ 2 ) ) ) )
96 subsq 
 |-  ( ( ( C x. B ) e. CC /\ ( A x. D ) e. CC ) -> ( ( ( C x. B ) ^ 2 ) - ( ( A x. D ) ^ 2 ) ) = ( ( ( C x. B ) + ( A x. D ) ) x. ( ( C x. B ) - ( A x. D ) ) ) )
97 38 40 96 syl2anc 
 |-  ( ph -> ( ( ( C x. B ) ^ 2 ) - ( ( A x. D ) ^ 2 ) ) = ( ( ( C x. B ) + ( A x. D ) ) x. ( ( C x. B ) - ( A x. D ) ) ) )
98 95 97 eqtr3d 
 |-  ( ph -> ( P x. ( ( ( C ^ 2 ) x. N ) - ( A ^ 2 ) ) ) = ( ( ( C x. B ) + ( A x. D ) ) x. ( ( C x. B ) - ( A x. D ) ) ) )
99 56 98 breqtrd 
 |-  ( ph -> P || ( ( ( C x. B ) + ( A x. D ) ) x. ( ( C x. B ) - ( A x. D ) ) ) )
100 37 39 zaddcld 
 |-  ( ph -> ( ( C x. B ) + ( A x. D ) ) e. ZZ )
101 37 39 zsubcld 
 |-  ( ph -> ( ( C x. B ) - ( A x. D ) ) e. ZZ )
102 euclemma 
 |-  ( ( P e. Prime /\ ( ( C x. B ) + ( A x. D ) ) e. ZZ /\ ( ( C x. B ) - ( A x. D ) ) e. ZZ ) -> ( P || ( ( ( C x. B ) + ( A x. D ) ) x. ( ( C x. B ) - ( A x. D ) ) ) <-> ( P || ( ( C x. B ) + ( A x. D ) ) \/ P || ( ( C x. B ) - ( A x. D ) ) ) ) )
103 3 100 101 102 syl3anc 
 |-  ( ph -> ( P || ( ( ( C x. B ) + ( A x. D ) ) x. ( ( C x. B ) - ( A x. D ) ) ) <-> ( P || ( ( C x. B ) + ( A x. D ) ) \/ P || ( ( C x. B ) - ( A x. D ) ) ) ) )
104 99 103 mpbid 
 |-  ( ph -> ( P || ( ( C x. B ) + ( A x. D ) ) \/ P || ( ( C x. B ) - ( A x. D ) ) ) )
105 19 45 104 mpjaodan 
 |-  ( ph -> N e. S )