Metamath Proof Explorer

Theorem flt4lem5f

Description: Final equation of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html . Given A ^ 4 + B ^ 4 = C ^ 2 , provide a smaller solution. This satisfies the infinite descent condition. (Contributed by SN, 24-Aug-2024)

Ref Expression
Hypotheses flt4lem5a.m 
|- M = ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 )
flt4lem5a.n 
|- N = ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 )
flt4lem5a.r 
|- R = ( ( ( sqrt ` ( M + N ) ) + ( sqrt ` ( M - N ) ) ) / 2 )
flt4lem5a.s 
|- S = ( ( ( sqrt ` ( M + N ) ) - ( sqrt ` ( M - N ) ) ) / 2 )
flt4lem5a.a 
|- ( ph -> A e. NN )
flt4lem5a.b 
|- ( ph -> B e. NN )
flt4lem5a.c 
|- ( ph -> C e. NN )
flt4lem5a.1 
|- ( ph -> -. 2 || A )
flt4lem5a.2 
|- ( ph -> ( A gcd C ) = 1 )
flt4lem5a.3 
|- ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) )
Assertion flt4lem5f 
|- ( ph -> ( ( M gcd ( B / 2 ) ) ^ 2 ) = ( ( ( R gcd ( B / 2 ) ) ^ 4 ) + ( ( S gcd ( B / 2 ) ) ^ 4 ) ) )

Proof

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 ) ) )