| Step |
Hyp |
Ref |
Expression |
| 1 |
|
flt4lem3.a |
|- ( ph -> A e. NN ) |
| 2 |
|
flt4lem3.b |
|- ( ph -> B e. NN ) |
| 3 |
|
flt4lem3.c |
|- ( ph -> C e. NN ) |
| 4 |
|
flt4lem3.1 |
|- ( ph -> 2 || A ) |
| 5 |
|
flt4lem3.2 |
|- ( ph -> ( A gcd C ) = 1 ) |
| 6 |
|
flt4lem3.3 |
|- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) |
| 7 |
3
|
nnzd |
|- ( ph -> C e. ZZ ) |
| 8 |
1
|
nnzd |
|- ( ph -> A e. ZZ ) |
| 9 |
7 8
|
zaddcld |
|- ( ph -> ( C + A ) e. ZZ ) |
| 10 |
7 8
|
zsubcld |
|- ( ph -> ( C - A ) e. ZZ ) |
| 11 |
9 10
|
gcdcomd |
|- ( ph -> ( ( C + A ) gcd ( C - A ) ) = ( ( C - A ) gcd ( C + A ) ) ) |
| 12 |
1 2 3 4 5 6
|
flt4lem2 |
|- ( ph -> -. 2 || B ) |
| 13 |
|
2nn0 |
|- 2 e. NN0 |
| 14 |
13
|
a1i |
|- ( ph -> 2 e. NN0 ) |
| 15 |
1 2 3 5 6
|
fltabcoprm |
|- ( ph -> ( A gcd B ) = 1 ) |
| 16 |
1 2 3 14 6 15
|
fltbccoprm |
|- ( ph -> ( B gcd C ) = 1 ) |
| 17 |
2
|
nnsqcld |
|- ( ph -> ( B ^ 2 ) e. NN ) |
| 18 |
17
|
nncnd |
|- ( ph -> ( B ^ 2 ) e. CC ) |
| 19 |
1
|
nnsqcld |
|- ( ph -> ( A ^ 2 ) e. NN ) |
| 20 |
19
|
nncnd |
|- ( ph -> ( A ^ 2 ) e. CC ) |
| 21 |
18 20
|
addcomd |
|- ( ph -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) ) |
| 22 |
21 6
|
eqtrd |
|- ( ph -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) ) |
| 23 |
2 1 3 12 16 22
|
flt4lem1 |
|- ( ph -> ( ( B e. NN /\ A e. NN /\ C e. NN ) /\ ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) /\ ( ( B gcd A ) = 1 /\ -. 2 || B ) ) ) |
| 24 |
|
pythagtriplem4 |
|- ( ( ( B e. NN /\ A e. NN /\ C e. NN ) /\ ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( C ^ 2 ) /\ ( ( B gcd A ) = 1 /\ -. 2 || B ) ) -> ( ( C - A ) gcd ( C + A ) ) = 1 ) |
| 25 |
23 24
|
syl |
|- ( ph -> ( ( C - A ) gcd ( C + A ) ) = 1 ) |
| 26 |
11 25
|
eqtrd |
|- ( ph -> ( ( C + A ) gcd ( C - A ) ) = 1 ) |