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=\frac{\sqrt{C+B^2}+\sqrt{C-B^2}}{2}$$
	flt4lem5a.n	$$⊢N=\frac{\sqrt{C+B^2}-\sqrt{C-B^2}}{2}$$
	flt4lem5a.r	$$⊢R=\frac{\sqrt{M+N}+\sqrt{M-N}}{2}$$
	flt4lem5a.s	$$⊢S=\frac{\sqrt{M+N}-\sqrt{M-N}}{2}$$
	flt4lem5a.a	$$⊢\phi \to A\in \mathbb{N}$$
	flt4lem5a.b	$$⊢\phi \to B\in \mathbb{N}$$
	flt4lem5a.c	$$⊢\phi \to C\in \mathbb{N}$$
	flt4lem5a.1	$$⊢\phi \to \neg 2\parallel A$$
	flt4lem5a.2	$$⊢\phi \to A\gcd C=1$$
	flt4lem5a.3	$$⊢\phi \to A^4+B^4=C^2$$
Assertion	flt4lem5f	$$⊢\phi \to {\left(M\gcd \left(\frac{B}{2}\right)\right)}^2={\left(R\gcd \left(\frac{B}{2}\right)\right)}^4+{\left(S\gcd \left(\frac{B}{2}\right)\right)}^4$$

Proof

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