Theorem flt4lem5b

Description: Part 2 of Equation 1 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	flt4lem5b	|- ( ph -> ( 2 x. ( M x. N ) ) = ( B ^ 2 ) )

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	1 2	pythagtriplem16	|- ( ( ( ( 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 ) ) ) -> ( B ^ 2 ) = ( 2 x. ( M x. N ) ) )
31	29 30	syl	|- ( ph -> ( B ^ 2 ) = ( 2 x. ( M x. N ) ) )
32	31	eqcomd	|- ( ph -> ( 2 x. ( M x. N ) ) = ( B ^ 2 ) )