| Step |
Hyp |
Ref |
Expression |
| 1 |
|
flt4lem5a.m |
|- M = ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) |
| 2 |
|
flt4lem5a.n |
|- N = ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 ) |
| 3 |
|
flt4lem5a.r |
|- R = ( ( ( sqrt ` ( M + N ) ) + ( sqrt ` ( M - N ) ) ) / 2 ) |
| 4 |
|
flt4lem5a.s |
|- S = ( ( ( sqrt ` ( M + N ) ) - ( sqrt ` ( M - N ) ) ) / 2 ) |
| 5 |
|
flt4lem5a.a |
|- ( ph -> A e. NN ) |
| 6 |
|
flt4lem5a.b |
|- ( ph -> B e. NN ) |
| 7 |
|
flt4lem5a.c |
|- ( ph -> C e. NN ) |
| 8 |
|
flt4lem5a.1 |
|- ( ph -> -. 2 || A ) |
| 9 |
|
flt4lem5a.2 |
|- ( ph -> ( A gcd C ) = 1 ) |
| 10 |
|
flt4lem5a.3 |
|- ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) ) |
| 11 |
1 2 3 4 5 6 7 8 9 10
|
flt4lem5d |
|- ( ph -> M = ( ( R ^ 2 ) + ( S ^ 2 ) ) ) |
| 12 |
1 2 3 4 5 6 7 8 9 10
|
flt4lem5e |
|- ( ph -> ( ( ( R gcd S ) = 1 /\ ( R gcd M ) = 1 /\ ( S gcd M ) = 1 ) /\ ( R e. NN /\ S e. NN /\ M e. NN ) /\ ( ( M x. ( R x. S ) ) = ( ( B / 2 ) ^ 2 ) /\ ( B / 2 ) e. NN ) ) ) |
| 13 |
12
|
simp2d |
|- ( ph -> ( R e. NN /\ S e. NN /\ M e. NN ) ) |
| 14 |
13
|
simp3d |
|- ( ph -> M e. NN ) |
| 15 |
13
|
simp1d |
|- ( ph -> R e. NN ) |
| 16 |
13
|
simp2d |
|- ( ph -> S e. NN ) |
| 17 |
15 16
|
nnmulcld |
|- ( ph -> ( R x. S ) e. NN ) |
| 18 |
12
|
simp3d |
|- ( ph -> ( ( M x. ( R x. S ) ) = ( ( B / 2 ) ^ 2 ) /\ ( B / 2 ) e. NN ) ) |
| 19 |
18
|
simprd |
|- ( ph -> ( B / 2 ) e. NN ) |
| 20 |
14
|
nnzd |
|- ( ph -> M e. ZZ ) |
| 21 |
15
|
nnzd |
|- ( ph -> R e. ZZ ) |
| 22 |
20 21
|
gcdcomd |
|- ( ph -> ( M gcd R ) = ( R gcd M ) ) |
| 23 |
12
|
simp1d |
|- ( ph -> ( ( R gcd S ) = 1 /\ ( R gcd M ) = 1 /\ ( S gcd M ) = 1 ) ) |
| 24 |
23
|
simp2d |
|- ( ph -> ( R gcd M ) = 1 ) |
| 25 |
22 24
|
eqtrd |
|- ( ph -> ( M gcd R ) = 1 ) |
| 26 |
16
|
nnzd |
|- ( ph -> S e. ZZ ) |
| 27 |
20 26
|
gcdcomd |
|- ( ph -> ( M gcd S ) = ( S gcd M ) ) |
| 28 |
23
|
simp3d |
|- ( ph -> ( S gcd M ) = 1 ) |
| 29 |
27 28
|
eqtrd |
|- ( ph -> ( M gcd S ) = 1 ) |
| 30 |
|
rpmul |
|- ( ( M e. ZZ /\ R e. ZZ /\ S e. ZZ ) -> ( ( ( M gcd R ) = 1 /\ ( M gcd S ) = 1 ) -> ( M gcd ( R x. S ) ) = 1 ) ) |
| 31 |
20 21 26 30
|
syl3anc |
|- ( ph -> ( ( ( M gcd R ) = 1 /\ ( M gcd S ) = 1 ) -> ( M gcd ( R x. S ) ) = 1 ) ) |
| 32 |
25 29 31
|
mp2and |
|- ( ph -> ( M gcd ( R x. S ) ) = 1 ) |
| 33 |
18
|
simpld |
|- ( ph -> ( M x. ( R x. S ) ) = ( ( B / 2 ) ^ 2 ) ) |
| 34 |
14 17 19 32 33
|
flt4lem4 |
|- ( ph -> ( M = ( ( M gcd ( B / 2 ) ) ^ 2 ) /\ ( R x. S ) = ( ( ( R x. S ) gcd ( B / 2 ) ) ^ 2 ) ) ) |
| 35 |
34
|
simpld |
|- ( ph -> M = ( ( M gcd ( B / 2 ) ) ^ 2 ) ) |
| 36 |
14 16
|
nnmulcld |
|- ( ph -> ( M x. S ) e. NN ) |
| 37 |
36
|
nnzd |
|- ( ph -> ( M x. S ) e. ZZ ) |
| 38 |
37 21
|
gcdcomd |
|- ( ph -> ( ( M x. S ) gcd R ) = ( R gcd ( M x. S ) ) ) |
| 39 |
23
|
simp1d |
|- ( ph -> ( R gcd S ) = 1 ) |
| 40 |
|
rpmul |
|- ( ( R e. ZZ /\ M e. ZZ /\ S e. ZZ ) -> ( ( ( R gcd M ) = 1 /\ ( R gcd S ) = 1 ) -> ( R gcd ( M x. S ) ) = 1 ) ) |
| 41 |
21 20 26 40
|
syl3anc |
|- ( ph -> ( ( ( R gcd M ) = 1 /\ ( R gcd S ) = 1 ) -> ( R gcd ( M x. S ) ) = 1 ) ) |
| 42 |
24 39 41
|
mp2and |
|- ( ph -> ( R gcd ( M x. S ) ) = 1 ) |
| 43 |
38 42
|
eqtrd |
|- ( ph -> ( ( M x. S ) gcd R ) = 1 ) |
| 44 |
14
|
nncnd |
|- ( ph -> M e. CC ) |
| 45 |
16
|
nncnd |
|- ( ph -> S e. CC ) |
| 46 |
15
|
nncnd |
|- ( ph -> R e. CC ) |
| 47 |
44 45 46
|
mul32d |
|- ( ph -> ( ( M x. S ) x. R ) = ( ( M x. R ) x. S ) ) |
| 48 |
44 46 45
|
mulassd |
|- ( ph -> ( ( M x. R ) x. S ) = ( M x. ( R x. S ) ) ) |
| 49 |
48 33
|
eqtrd |
|- ( ph -> ( ( M x. R ) x. S ) = ( ( B / 2 ) ^ 2 ) ) |
| 50 |
47 49
|
eqtrd |
|- ( ph -> ( ( M x. S ) x. R ) = ( ( B / 2 ) ^ 2 ) ) |
| 51 |
36 15 19 43 50
|
flt4lem4 |
|- ( ph -> ( ( M x. S ) = ( ( ( M x. S ) gcd ( B / 2 ) ) ^ 2 ) /\ R = ( ( R gcd ( B / 2 ) ) ^ 2 ) ) ) |
| 52 |
51
|
simprd |
|- ( ph -> R = ( ( R gcd ( B / 2 ) ) ^ 2 ) ) |
| 53 |
52
|
oveq1d |
|- ( ph -> ( R ^ 2 ) = ( ( ( R gcd ( B / 2 ) ) ^ 2 ) ^ 2 ) ) |
| 54 |
|
gcdnncl |
|- ( ( R e. NN /\ ( B / 2 ) e. NN ) -> ( R gcd ( B / 2 ) ) e. NN ) |
| 55 |
15 19 54
|
syl2anc |
|- ( ph -> ( R gcd ( B / 2 ) ) e. NN ) |
| 56 |
55
|
nncnd |
|- ( ph -> ( R gcd ( B / 2 ) ) e. CC ) |
| 57 |
56
|
flt4lem |
|- ( ph -> ( ( R gcd ( B / 2 ) ) ^ 4 ) = ( ( ( R gcd ( B / 2 ) ) ^ 2 ) ^ 2 ) ) |
| 58 |
53 57
|
eqtr4d |
|- ( ph -> ( R ^ 2 ) = ( ( R gcd ( B / 2 ) ) ^ 4 ) ) |
| 59 |
14 15
|
nnmulcld |
|- ( ph -> ( M x. R ) e. NN ) |
| 60 |
59
|
nnzd |
|- ( ph -> ( M x. R ) e. ZZ ) |
| 61 |
60 26
|
gcdcomd |
|- ( ph -> ( ( M x. R ) gcd S ) = ( S gcd ( M x. R ) ) ) |
| 62 |
26 21
|
gcdcomd |
|- ( ph -> ( S gcd R ) = ( R gcd S ) ) |
| 63 |
62 39
|
eqtrd |
|- ( ph -> ( S gcd R ) = 1 ) |
| 64 |
|
rpmul |
|- ( ( S e. ZZ /\ M e. ZZ /\ R e. ZZ ) -> ( ( ( S gcd M ) = 1 /\ ( S gcd R ) = 1 ) -> ( S gcd ( M x. R ) ) = 1 ) ) |
| 65 |
26 20 21 64
|
syl3anc |
|- ( ph -> ( ( ( S gcd M ) = 1 /\ ( S gcd R ) = 1 ) -> ( S gcd ( M x. R ) ) = 1 ) ) |
| 66 |
28 63 65
|
mp2and |
|- ( ph -> ( S gcd ( M x. R ) ) = 1 ) |
| 67 |
61 66
|
eqtrd |
|- ( ph -> ( ( M x. R ) gcd S ) = 1 ) |
| 68 |
59 16 19 67 49
|
flt4lem4 |
|- ( ph -> ( ( M x. R ) = ( ( ( M x. R ) gcd ( B / 2 ) ) ^ 2 ) /\ S = ( ( S gcd ( B / 2 ) ) ^ 2 ) ) ) |
| 69 |
68
|
simprd |
|- ( ph -> S = ( ( S gcd ( B / 2 ) ) ^ 2 ) ) |
| 70 |
69
|
oveq1d |
|- ( ph -> ( S ^ 2 ) = ( ( ( S gcd ( B / 2 ) ) ^ 2 ) ^ 2 ) ) |
| 71 |
|
gcdnncl |
|- ( ( S e. NN /\ ( B / 2 ) e. NN ) -> ( S gcd ( B / 2 ) ) e. NN ) |
| 72 |
16 19 71
|
syl2anc |
|- ( ph -> ( S gcd ( B / 2 ) ) e. NN ) |
| 73 |
72
|
nncnd |
|- ( ph -> ( S gcd ( B / 2 ) ) e. CC ) |
| 74 |
73
|
flt4lem |
|- ( ph -> ( ( S gcd ( B / 2 ) ) ^ 4 ) = ( ( ( S gcd ( B / 2 ) ) ^ 2 ) ^ 2 ) ) |
| 75 |
70 74
|
eqtr4d |
|- ( ph -> ( S ^ 2 ) = ( ( S gcd ( B / 2 ) ) ^ 4 ) ) |
| 76 |
58 75
|
oveq12d |
|- ( ph -> ( ( R ^ 2 ) + ( S ^ 2 ) ) = ( ( ( R gcd ( B / 2 ) ) ^ 4 ) + ( ( S gcd ( B / 2 ) ) ^ 4 ) ) ) |
| 77 |
11 35 76
|
3eqtr3d |
|- ( ph -> ( ( M gcd ( B / 2 ) ) ^ 2 ) = ( ( ( R gcd ( B / 2 ) ) ^ 4 ) + ( ( S gcd ( B / 2 ) ) ^ 4 ) ) ) |