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	⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 )
	flt4lem5a.n	⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 )
	flt4lem5a.r	⊢ 𝑅 = ( ( ( √ ‘ ( 𝑀 + 𝑁 ) ) + ( √ ‘ ( 𝑀 − 𝑁 ) ) ) / 2 )
	flt4lem5a.s	⊢ 𝑆 = ( ( ( √ ‘ ( 𝑀 + 𝑁 ) ) − ( √ ‘ ( 𝑀 − 𝑁 ) ) ) / 2 )
	flt4lem5a.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	flt4lem5a.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	flt4lem5a.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
	flt4lem5a.1	⊢ ( 𝜑 → ¬ 2 ∥ 𝐴 )
	flt4lem5a.2	⊢ ( 𝜑 → ( 𝐴 gcd 𝐶 ) = 1 )
	flt4lem5a.3	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( 𝐶 ↑ 2 ) )
Assertion	flt4lem5f	⊢ ( 𝜑 → ( ( 𝑀 gcd ( 𝐵 / 2 ) ) ↑ 2 ) = ( ( ( 𝑅 gcd ( 𝐵 / 2 ) ) ↑ 4 ) + ( ( 𝑆 gcd ( 𝐵 / 2 ) ) ↑ 4 ) ) )

Proof

Step	Hyp	Ref	Expression
1		flt4lem5a.m	⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 )
2		flt4lem5a.n	⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 )
3		flt4lem5a.r	⊢ 𝑅 = ( ( ( √ ‘ ( 𝑀 + 𝑁 ) ) + ( √ ‘ ( 𝑀 − 𝑁 ) ) ) / 2 )
4		flt4lem5a.s	⊢ 𝑆 = ( ( ( √ ‘ ( 𝑀 + 𝑁 ) ) − ( √ ‘ ( 𝑀 − 𝑁 ) ) ) / 2 )
5		flt4lem5a.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
6		flt4lem5a.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
7		flt4lem5a.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
8		flt4lem5a.1	⊢ ( 𝜑 → ¬ 2 ∥ 𝐴 )
9		flt4lem5a.2	⊢ ( 𝜑 → ( 𝐴 gcd 𝐶 ) = 1 )
10		flt4lem5a.3	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( 𝐶 ↑ 2 ) )
11	1 2 3 4 5 6 7 8 9 10	flt4lem5d	⊢ ( 𝜑 → 𝑀 = ( ( 𝑅 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) )
12	1 2 3 4 5 6 7 8 9 10	flt4lem5e	⊢ ( 𝜑 → ( ( ( 𝑅 gcd 𝑆 ) = 1 ∧ ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑀 ) = 1 ) ∧ ( 𝑅 ∈ ℕ ∧ 𝑆 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( ( 𝑀 · ( 𝑅 · 𝑆 ) ) = ( ( 𝐵 / 2 ) ↑ 2 ) ∧ ( 𝐵 / 2 ) ∈ ℕ ) ) )
13	12	simp2d	⊢ ( 𝜑 → ( 𝑅 ∈ ℕ ∧ 𝑆 ∈ ℕ ∧ 𝑀 ∈ ℕ ) )
14	13	simp3d	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
15	13	simp1d	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
16	13	simp2d	⊢ ( 𝜑 → 𝑆 ∈ ℕ )
17	15 16	nnmulcld	⊢ ( 𝜑 → ( 𝑅 · 𝑆 ) ∈ ℕ )
18	12	simp3d	⊢ ( 𝜑 → ( ( 𝑀 · ( 𝑅 · 𝑆 ) ) = ( ( 𝐵 / 2 ) ↑ 2 ) ∧ ( 𝐵 / 2 ) ∈ ℕ ) )
19	18	simprd	⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℕ )
20	14	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
21	15	nnzd	⊢ ( 𝜑 → 𝑅 ∈ ℤ )
22	20 21	gcdcomd	⊢ ( 𝜑 → ( 𝑀 gcd 𝑅 ) = ( 𝑅 gcd 𝑀 ) )
23	12	simp1d	⊢ ( 𝜑 → ( ( 𝑅 gcd 𝑆 ) = 1 ∧ ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑀 ) = 1 ) )
24	23	simp2d	⊢ ( 𝜑 → ( 𝑅 gcd 𝑀 ) = 1 )
25	22 24	eqtrd	⊢ ( 𝜑 → ( 𝑀 gcd 𝑅 ) = 1 )
26	16	nnzd	⊢ ( 𝜑 → 𝑆 ∈ ℤ )
27	20 26	gcdcomd	⊢ ( 𝜑 → ( 𝑀 gcd 𝑆 ) = ( 𝑆 gcd 𝑀 ) )
28	23	simp3d	⊢ ( 𝜑 → ( 𝑆 gcd 𝑀 ) = 1 )
29	27 28	eqtrd	⊢ ( 𝜑 → ( 𝑀 gcd 𝑆 ) = 1 )
30		rpmul	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑆 ∈ ℤ ) → ( ( ( 𝑀 gcd 𝑅 ) = 1 ∧ ( 𝑀 gcd 𝑆 ) = 1 ) → ( 𝑀 gcd ( 𝑅 · 𝑆 ) ) = 1 ) )
31	20 21 26 30	syl3anc	⊢ ( 𝜑 → ( ( ( 𝑀 gcd 𝑅 ) = 1 ∧ ( 𝑀 gcd 𝑆 ) = 1 ) → ( 𝑀 gcd ( 𝑅 · 𝑆 ) ) = 1 ) )
32	25 29 31	mp2and	⊢ ( 𝜑 → ( 𝑀 gcd ( 𝑅 · 𝑆 ) ) = 1 )
33	18	simpld	⊢ ( 𝜑 → ( 𝑀 · ( 𝑅 · 𝑆 ) ) = ( ( 𝐵 / 2 ) ↑ 2 ) )
34	14 17 19 32 33	flt4lem4	⊢ ( 𝜑 → ( 𝑀 = ( ( 𝑀 gcd ( 𝐵 / 2 ) ) ↑ 2 ) ∧ ( 𝑅 · 𝑆 ) = ( ( ( 𝑅 · 𝑆 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) )
35	34	simpld	⊢ ( 𝜑 → 𝑀 = ( ( 𝑀 gcd ( 𝐵 / 2 ) ) ↑ 2 ) )
36	14 16	nnmulcld	⊢ ( 𝜑 → ( 𝑀 · 𝑆 ) ∈ ℕ )
37	36	nnzd	⊢ ( 𝜑 → ( 𝑀 · 𝑆 ) ∈ ℤ )
38	37 21	gcdcomd	⊢ ( 𝜑 → ( ( 𝑀 · 𝑆 ) gcd 𝑅 ) = ( 𝑅 gcd ( 𝑀 · 𝑆 ) ) )
39	23	simp1d	⊢ ( 𝜑 → ( 𝑅 gcd 𝑆 ) = 1 )
40		rpmul	⊢ ( ( 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑆 ∈ ℤ ) → ( ( ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑅 gcd 𝑆 ) = 1 ) → ( 𝑅 gcd ( 𝑀 · 𝑆 ) ) = 1 ) )
41	21 20 26 40	syl3anc	⊢ ( 𝜑 → ( ( ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑅 gcd 𝑆 ) = 1 ) → ( 𝑅 gcd ( 𝑀 · 𝑆 ) ) = 1 ) )
42	24 39 41	mp2and	⊢ ( 𝜑 → ( 𝑅 gcd ( 𝑀 · 𝑆 ) ) = 1 )
43	38 42	eqtrd	⊢ ( 𝜑 → ( ( 𝑀 · 𝑆 ) gcd 𝑅 ) = 1 )
44	14	nncnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
45	16	nncnd	⊢ ( 𝜑 → 𝑆 ∈ ℂ )
46	15	nncnd	⊢ ( 𝜑 → 𝑅 ∈ ℂ )
47	44 45 46	mul32d	⊢ ( 𝜑 → ( ( 𝑀 · 𝑆 ) · 𝑅 ) = ( ( 𝑀 · 𝑅 ) · 𝑆 ) )
48	44 46 45	mulassd	⊢ ( 𝜑 → ( ( 𝑀 · 𝑅 ) · 𝑆 ) = ( 𝑀 · ( 𝑅 · 𝑆 ) ) )
49	48 33	eqtrd	⊢ ( 𝜑 → ( ( 𝑀 · 𝑅 ) · 𝑆 ) = ( ( 𝐵 / 2 ) ↑ 2 ) )
50	47 49	eqtrd	⊢ ( 𝜑 → ( ( 𝑀 · 𝑆 ) · 𝑅 ) = ( ( 𝐵 / 2 ) ↑ 2 ) )
51	36 15 19 43 50	flt4lem4	⊢ ( 𝜑 → ( ( 𝑀 · 𝑆 ) = ( ( ( 𝑀 · 𝑆 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ∧ 𝑅 = ( ( 𝑅 gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) )
52	51	simprd	⊢ ( 𝜑 → 𝑅 = ( ( 𝑅 gcd ( 𝐵 / 2 ) ) ↑ 2 ) )
53	52	oveq1d	⊢ ( 𝜑 → ( 𝑅 ↑ 2 ) = ( ( ( 𝑅 gcd ( 𝐵 / 2 ) ) ↑ 2 ) ↑ 2 ) )
54		gcdnncl	⊢ ( ( 𝑅 ∈ ℕ ∧ ( 𝐵 / 2 ) ∈ ℕ ) → ( 𝑅 gcd ( 𝐵 / 2 ) ) ∈ ℕ )
55	15 19 54	syl2anc	⊢ ( 𝜑 → ( 𝑅 gcd ( 𝐵 / 2 ) ) ∈ ℕ )
56	55	nncnd	⊢ ( 𝜑 → ( 𝑅 gcd ( 𝐵 / 2 ) ) ∈ ℂ )
57	56	flt4lem	⊢ ( 𝜑 → ( ( 𝑅 gcd ( 𝐵 / 2 ) ) ↑ 4 ) = ( ( ( 𝑅 gcd ( 𝐵 / 2 ) ) ↑ 2 ) ↑ 2 ) )
58	53 57	eqtr4d	⊢ ( 𝜑 → ( 𝑅 ↑ 2 ) = ( ( 𝑅 gcd ( 𝐵 / 2 ) ) ↑ 4 ) )
59	14 15	nnmulcld	⊢ ( 𝜑 → ( 𝑀 · 𝑅 ) ∈ ℕ )
60	59	nnzd	⊢ ( 𝜑 → ( 𝑀 · 𝑅 ) ∈ ℤ )
61	60 26	gcdcomd	⊢ ( 𝜑 → ( ( 𝑀 · 𝑅 ) gcd 𝑆 ) = ( 𝑆 gcd ( 𝑀 · 𝑅 ) ) )
62	26 21	gcdcomd	⊢ ( 𝜑 → ( 𝑆 gcd 𝑅 ) = ( 𝑅 gcd 𝑆 ) )
63	62 39	eqtrd	⊢ ( 𝜑 → ( 𝑆 gcd 𝑅 ) = 1 )
64		rpmul	⊢ ( ( 𝑆 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℤ ) → ( ( ( 𝑆 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑅 ) = 1 ) → ( 𝑆 gcd ( 𝑀 · 𝑅 ) ) = 1 ) )
65	26 20 21 64	syl3anc	⊢ ( 𝜑 → ( ( ( 𝑆 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑅 ) = 1 ) → ( 𝑆 gcd ( 𝑀 · 𝑅 ) ) = 1 ) )
66	28 63 65	mp2and	⊢ ( 𝜑 → ( 𝑆 gcd ( 𝑀 · 𝑅 ) ) = 1 )
67	61 66	eqtrd	⊢ ( 𝜑 → ( ( 𝑀 · 𝑅 ) gcd 𝑆 ) = 1 )
68	59 16 19 67 49	flt4lem4	⊢ ( 𝜑 → ( ( 𝑀 · 𝑅 ) = ( ( ( 𝑀 · 𝑅 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ∧ 𝑆 = ( ( 𝑆 gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) )
69	68	simprd	⊢ ( 𝜑 → 𝑆 = ( ( 𝑆 gcd ( 𝐵 / 2 ) ) ↑ 2 ) )
70	69	oveq1d	⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) = ( ( ( 𝑆 gcd ( 𝐵 / 2 ) ) ↑ 2 ) ↑ 2 ) )
71		gcdnncl	⊢ ( ( 𝑆 ∈ ℕ ∧ ( 𝐵 / 2 ) ∈ ℕ ) → ( 𝑆 gcd ( 𝐵 / 2 ) ) ∈ ℕ )
72	16 19 71	syl2anc	⊢ ( 𝜑 → ( 𝑆 gcd ( 𝐵 / 2 ) ) ∈ ℕ )
73	72	nncnd	⊢ ( 𝜑 → ( 𝑆 gcd ( 𝐵 / 2 ) ) ∈ ℂ )
74	73	flt4lem	⊢ ( 𝜑 → ( ( 𝑆 gcd ( 𝐵 / 2 ) ) ↑ 4 ) = ( ( ( 𝑆 gcd ( 𝐵 / 2 ) ) ↑ 2 ) ↑ 2 ) )
75	70 74	eqtr4d	⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) = ( ( 𝑆 gcd ( 𝐵 / 2 ) ) ↑ 4 ) )
76	58 75	oveq12d	⊢ ( 𝜑 → ( ( 𝑅 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) = ( ( ( 𝑅 gcd ( 𝐵 / 2 ) ) ↑ 4 ) + ( ( 𝑆 gcd ( 𝐵 / 2 ) ) ↑ 4 ) ) )
77	11 35 76	3eqtr3d	⊢ ( 𝜑 → ( ( 𝑀 gcd ( 𝐵 / 2 ) ) ↑ 2 ) = ( ( ( 𝑅 gcd ( 𝐵 / 2 ) ) ↑ 4 ) + ( ( 𝑆 gcd ( 𝐵 / 2 ) ) ↑ 4 ) ) )