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=\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	flt4lem5b	$$⊢\phi \to 2\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=B^2$$

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	5	nnsqcld	$$⊢\phi \to A^2\in \mathbb{N}$$
12	6	nnsqcld	$$⊢\phi \to B^2\in \mathbb{N}$$
13		2prm	$$⊢2\in \mathbb{P}$$
14	5	nnzd	$$⊢\phi \to A\in \mathbb{Z}$$
15		prmdvdssq	$$⊢\left(2\in \mathbb{P}\wedge A\in \mathbb{Z}\right)\to \left(2\parallel A\leftrightarrow 2\parallel A^2\right)$$
16	13 14 15	sylancr	$$⊢\phi \to \left(2\parallel A\leftrightarrow 2\parallel A^2\right)$$
17	8 16	mtbid	$$⊢\phi \to \neg 2\parallel A^2$$
18		2nn	$$⊢2\in \mathbb{N}$$
19	18	a1i	$$⊢\phi \to 2\in \mathbb{N}$$
20		rplpwr	$$⊢\left(A\in \mathbb{N}\wedge C\in \mathbb{N}\wedge 2\in \mathbb{N}\right)\to \left(A\gcd C=1\to A^2\gcd C=1\right)$$
21	5 7 19 20	syl3anc	$$⊢\phi \to \left(A\gcd C=1\to A^2\gcd C=1\right)$$
22	9 21	mpd	$$⊢\phi \to A^2\gcd C=1$$
23	5	nncnd	$$⊢\phi \to A\in ℂ$$
24	23	exp4sqsq	$$⊢\phi \to A^4={\left(A^2\right)}^2$$
25	6	nncnd	$$⊢\phi \to B\in ℂ$$
26	25	exp4sqsq	$$⊢\phi \to B^4={\left(B^2\right)}^2$$
27	24 26	oveq12d	$$⊢\phi \to A^4+B^4={\left(A^2\right)}^2+{\left(B^2\right)}^2$$
28	27 10	eqtr3d	$$⊢\phi \to {\left(A^2\right)}^2+{\left(B^2\right)}^2=C^2$$
29	11 12 7 17 22 28	flt4lem1	$$⊢\phi \to \left(\left(A^2\in \mathbb{N}\wedge B^2\in \mathbb{N}\wedge C\in \mathbb{N}\right)\wedge {\left(A^2\right)}^2+{\left(B^2\right)}^2=C^2\wedge \left(A^2\gcd B^2=1\wedge \neg 2\parallel A^2\right)\right)$$
30	1 2	pythagtriplem16	$$⊢\left(\left(A^2\in \mathbb{N}\wedge B^2\in \mathbb{N}\wedge C\in \mathbb{N}\right)\wedge {\left(A^2\right)}^2+{\left(B^2\right)}^2=C^2\wedge \left(A^2\gcd B^2=1\wedge \neg 2\parallel A^2\right)\right)\to B^2=2\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
31	29 30	syl	$$⊢\phi \to B^2=2\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
32	31	eqcomd	$$⊢\phi \to 2\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=B^2$$