Step |
Hyp |
Ref |
Expression |
1 |
|
2sqcoprm.1 |
|- ( ph -> P e. Prime ) |
2 |
|
2sqcoprm.2 |
|- ( ph -> A e. ZZ ) |
3 |
|
2sqcoprm.3 |
|- ( ph -> B e. ZZ ) |
4 |
|
2sqcoprm.4 |
|- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = P ) |
5 |
1 2 3 4
|
2sqn0 |
|- ( ph -> A =/= 0 ) |
6 |
2 3
|
gcdcld |
|- ( ph -> ( A gcd B ) e. NN0 ) |
7 |
6
|
adantr |
|- ( ( ph /\ A =/= 0 ) -> ( A gcd B ) e. NN0 ) |
8 |
2
|
adantr |
|- ( ( ph /\ A =/= 0 ) -> A e. ZZ ) |
9 |
3
|
adantr |
|- ( ( ph /\ A =/= 0 ) -> B e. ZZ ) |
10 |
|
simpr |
|- ( ( ph /\ A =/= 0 ) -> A =/= 0 ) |
11 |
10
|
neneqd |
|- ( ( ph /\ A =/= 0 ) -> -. A = 0 ) |
12 |
11
|
intnanrd |
|- ( ( ph /\ A =/= 0 ) -> -. ( A = 0 /\ B = 0 ) ) |
13 |
|
gcdn0cl |
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( A gcd B ) e. NN ) |
14 |
8 9 12 13
|
syl21anc |
|- ( ( ph /\ A =/= 0 ) -> ( A gcd B ) e. NN ) |
15 |
14
|
nnsqcld |
|- ( ( ph /\ A =/= 0 ) -> ( ( A gcd B ) ^ 2 ) e. NN ) |
16 |
6
|
nn0zd |
|- ( ph -> ( A gcd B ) e. ZZ ) |
17 |
|
sqnprm |
|- ( ( A gcd B ) e. ZZ -> -. ( ( A gcd B ) ^ 2 ) e. Prime ) |
18 |
16 17
|
syl |
|- ( ph -> -. ( ( A gcd B ) ^ 2 ) e. Prime ) |
19 |
|
zsqcl |
|- ( ( A gcd B ) e. ZZ -> ( ( A gcd B ) ^ 2 ) e. ZZ ) |
20 |
16 19
|
syl |
|- ( ph -> ( ( A gcd B ) ^ 2 ) e. ZZ ) |
21 |
|
zsqcl |
|- ( A e. ZZ -> ( A ^ 2 ) e. ZZ ) |
22 |
2 21
|
syl |
|- ( ph -> ( A ^ 2 ) e. ZZ ) |
23 |
|
zsqcl |
|- ( B e. ZZ -> ( B ^ 2 ) e. ZZ ) |
24 |
3 23
|
syl |
|- ( ph -> ( B ^ 2 ) e. ZZ ) |
25 |
|
gcddvds |
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) ) |
26 |
2 3 25
|
syl2anc |
|- ( ph -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) ) |
27 |
26
|
simpld |
|- ( ph -> ( A gcd B ) || A ) |
28 |
|
dvdssqim |
|- ( ( ( A gcd B ) e. ZZ /\ A e. ZZ ) -> ( ( A gcd B ) || A -> ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) ) ) |
29 |
28
|
imp |
|- ( ( ( ( A gcd B ) e. ZZ /\ A e. ZZ ) /\ ( A gcd B ) || A ) -> ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) ) |
30 |
16 2 27 29
|
syl21anc |
|- ( ph -> ( ( A gcd B ) ^ 2 ) || ( A ^ 2 ) ) |
31 |
26
|
simprd |
|- ( ph -> ( A gcd B ) || B ) |
32 |
|
dvdssqim |
|- ( ( ( A gcd B ) e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || B -> ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) ) |
33 |
32
|
imp |
|- ( ( ( ( A gcd B ) e. ZZ /\ B e. ZZ ) /\ ( A gcd B ) || B ) -> ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) |
34 |
16 3 31 33
|
syl21anc |
|- ( ph -> ( ( A gcd B ) ^ 2 ) || ( B ^ 2 ) ) |
35 |
20 22 24 30 34
|
dvds2addd |
|- ( ph -> ( ( A gcd B ) ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) ) |
36 |
35 4
|
breqtrd |
|- ( ph -> ( ( A gcd B ) ^ 2 ) || P ) |
37 |
36
|
adantr |
|- ( ( ph /\ ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) ) -> ( ( A gcd B ) ^ 2 ) || P ) |
38 |
|
simpr |
|- ( ( ph /\ ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) ) -> ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) ) |
39 |
1
|
adantr |
|- ( ( ph /\ ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) ) -> P e. Prime ) |
40 |
|
dvdsprm |
|- ( ( ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( ( ( A gcd B ) ^ 2 ) || P <-> ( ( A gcd B ) ^ 2 ) = P ) ) |
41 |
38 39 40
|
syl2anc |
|- ( ( ph /\ ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) ) -> ( ( ( A gcd B ) ^ 2 ) || P <-> ( ( A gcd B ) ^ 2 ) = P ) ) |
42 |
37 41
|
mpbid |
|- ( ( ph /\ ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) ) -> ( ( A gcd B ) ^ 2 ) = P ) |
43 |
42 39
|
eqeltrd |
|- ( ( ph /\ ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) ) -> ( ( A gcd B ) ^ 2 ) e. Prime ) |
44 |
18 43
|
mtand |
|- ( ph -> -. ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) ) |
45 |
|
eluz2b3 |
|- ( ( ( A gcd B ) ^ 2 ) e. ( ZZ>= ` 2 ) <-> ( ( ( A gcd B ) ^ 2 ) e. NN /\ ( ( A gcd B ) ^ 2 ) =/= 1 ) ) |
46 |
44 45
|
sylnib |
|- ( ph -> -. ( ( ( A gcd B ) ^ 2 ) e. NN /\ ( ( A gcd B ) ^ 2 ) =/= 1 ) ) |
47 |
|
imnan |
|- ( ( ( ( A gcd B ) ^ 2 ) e. NN -> -. ( ( A gcd B ) ^ 2 ) =/= 1 ) <-> -. ( ( ( A gcd B ) ^ 2 ) e. NN /\ ( ( A gcd B ) ^ 2 ) =/= 1 ) ) |
48 |
46 47
|
sylibr |
|- ( ph -> ( ( ( A gcd B ) ^ 2 ) e. NN -> -. ( ( A gcd B ) ^ 2 ) =/= 1 ) ) |
49 |
48
|
adantr |
|- ( ( ph /\ A =/= 0 ) -> ( ( ( A gcd B ) ^ 2 ) e. NN -> -. ( ( A gcd B ) ^ 2 ) =/= 1 ) ) |
50 |
15 49
|
mpd |
|- ( ( ph /\ A =/= 0 ) -> -. ( ( A gcd B ) ^ 2 ) =/= 1 ) |
51 |
|
df-ne |
|- ( ( ( A gcd B ) ^ 2 ) =/= 1 <-> -. ( ( A gcd B ) ^ 2 ) = 1 ) |
52 |
50 51
|
sylnib |
|- ( ( ph /\ A =/= 0 ) -> -. -. ( ( A gcd B ) ^ 2 ) = 1 ) |
53 |
52
|
notnotrd |
|- ( ( ph /\ A =/= 0 ) -> ( ( A gcd B ) ^ 2 ) = 1 ) |
54 |
|
nn0sqeq1 |
|- ( ( ( A gcd B ) e. NN0 /\ ( ( A gcd B ) ^ 2 ) = 1 ) -> ( A gcd B ) = 1 ) |
55 |
7 53 54
|
syl2anc |
|- ( ( ph /\ A =/= 0 ) -> ( A gcd B ) = 1 ) |
56 |
5 55
|
mpdan |
|- ( ph -> ( A gcd B ) = 1 ) |