Metamath Proof Explorer


Theorem flt4lem5c

Description: Part 2 of Equation 2 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html . (Contributed by SN, 22-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 flt4lem5c
|- ( ph -> N = ( 2 x. ( R x. S ) ) )

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 5 nnsqcld
 |-  ( ph -> ( A ^ 2 ) e. NN )
12 6 nnsqcld
 |-  ( ph -> ( B ^ 2 ) e. NN )
13 2prm
 |-  2 e. Prime
14 5 nnzd
 |-  ( ph -> A e. ZZ )
15 prmdvdssq
 |-  ( ( 2 e. Prime /\ A e. ZZ ) -> ( 2 || A <-> 2 || ( A ^ 2 ) ) )
16 13 14 15 sylancr
 |-  ( ph -> ( 2 || A <-> 2 || ( A ^ 2 ) ) )
17 8 16 mtbid
 |-  ( ph -> -. 2 || ( A ^ 2 ) )
18 2nn
 |-  2 e. NN
19 18 a1i
 |-  ( ph -> 2 e. NN )
20 rplpwr
 |-  ( ( A e. NN /\ C e. NN /\ 2 e. NN ) -> ( ( A gcd C ) = 1 -> ( ( A ^ 2 ) gcd C ) = 1 ) )
21 5 7 19 20 syl3anc
 |-  ( ph -> ( ( A gcd C ) = 1 -> ( ( A ^ 2 ) gcd C ) = 1 ) )
22 9 21 mpd
 |-  ( ph -> ( ( A ^ 2 ) gcd C ) = 1 )
23 5 nncnd
 |-  ( ph -> A e. CC )
24 23 flt4lem
 |-  ( ph -> ( A ^ 4 ) = ( ( A ^ 2 ) ^ 2 ) )
25 6 nncnd
 |-  ( ph -> B e. CC )
26 25 flt4lem
 |-  ( ph -> ( B ^ 4 ) = ( ( B ^ 2 ) ^ 2 ) )
27 24 26 oveq12d
 |-  ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( ( ( A ^ 2 ) ^ 2 ) + ( ( B ^ 2 ) ^ 2 ) ) )
28 27 10 eqtr3d
 |-  ( ph -> ( ( ( A ^ 2 ) ^ 2 ) + ( ( B ^ 2 ) ^ 2 ) ) = ( C ^ 2 ) )
29 11 12 7 17 22 28 flt4lem1
 |-  ( ph -> ( ( ( A ^ 2 ) e. NN /\ ( B ^ 2 ) e. NN /\ C e. NN ) /\ ( ( ( A ^ 2 ) ^ 2 ) + ( ( B ^ 2 ) ^ 2 ) ) = ( C ^ 2 ) /\ ( ( ( A ^ 2 ) gcd ( B ^ 2 ) ) = 1 /\ -. 2 || ( A ^ 2 ) ) ) )
30 2 pythagtriplem13
 |-  ( ( ( ( A ^ 2 ) e. NN /\ ( B ^ 2 ) e. NN /\ C e. NN ) /\ ( ( ( A ^ 2 ) ^ 2 ) + ( ( B ^ 2 ) ^ 2 ) ) = ( C ^ 2 ) /\ ( ( ( A ^ 2 ) gcd ( B ^ 2 ) ) = 1 /\ -. 2 || ( A ^ 2 ) ) ) -> N e. NN )
31 29 30 syl
 |-  ( ph -> N e. NN )
32 1 pythagtriplem11
 |-  ( ( ( ( A ^ 2 ) e. NN /\ ( B ^ 2 ) e. NN /\ C e. NN ) /\ ( ( ( A ^ 2 ) ^ 2 ) + ( ( B ^ 2 ) ^ 2 ) ) = ( C ^ 2 ) /\ ( ( ( A ^ 2 ) gcd ( B ^ 2 ) ) = 1 /\ -. 2 || ( A ^ 2 ) ) ) -> M e. NN )
33 29 32 syl
 |-  ( ph -> M e. NN )
34 1 2 3 4 5 6 7 8 9 10 flt4lem5a
 |-  ( ph -> ( ( A ^ 2 ) + ( N ^ 2 ) ) = ( M ^ 2 ) )
35 31 nnzd
 |-  ( ph -> N e. ZZ )
36 14 35 gcdcomd
 |-  ( ph -> ( A gcd N ) = ( N gcd A ) )
37 33 nnzd
 |-  ( ph -> M e. ZZ )
38 35 37 gcdcomd
 |-  ( ph -> ( N gcd M ) = ( M gcd N ) )
39 1 2 flt4lem5
 |-  ( ( ( ( A ^ 2 ) e. NN /\ ( B ^ 2 ) e. NN /\ C e. NN ) /\ ( ( ( A ^ 2 ) ^ 2 ) + ( ( B ^ 2 ) ^ 2 ) ) = ( C ^ 2 ) /\ ( ( ( A ^ 2 ) gcd ( B ^ 2 ) ) = 1 /\ -. 2 || ( A ^ 2 ) ) ) -> ( M gcd N ) = 1 )
40 29 39 syl
 |-  ( ph -> ( M gcd N ) = 1 )
41 38 40 eqtrd
 |-  ( ph -> ( N gcd M ) = 1 )
42 31 nnsqcld
 |-  ( ph -> ( N ^ 2 ) e. NN )
43 42 nncnd
 |-  ( ph -> ( N ^ 2 ) e. CC )
44 11 nncnd
 |-  ( ph -> ( A ^ 2 ) e. CC )
45 43 44 addcomd
 |-  ( ph -> ( ( N ^ 2 ) + ( A ^ 2 ) ) = ( ( A ^ 2 ) + ( N ^ 2 ) ) )
46 45 34 eqtrd
 |-  ( ph -> ( ( N ^ 2 ) + ( A ^ 2 ) ) = ( M ^ 2 ) )
47 31 5 33 41 46 fltabcoprm
 |-  ( ph -> ( N gcd A ) = 1 )
48 36 47 eqtrd
 |-  ( ph -> ( A gcd N ) = 1 )
49 3 4 pythagtriplem16
 |-  ( ( ( A e. NN /\ N e. NN /\ M e. NN ) /\ ( ( A ^ 2 ) + ( N ^ 2 ) ) = ( M ^ 2 ) /\ ( ( A gcd N ) = 1 /\ -. 2 || A ) ) -> N = ( 2 x. ( R x. S ) ) )
50 5 31 33 34 48 8 49 syl312anc
 |-  ( ph -> N = ( 2 x. ( R x. S ) ) )