Metamath Proof Explorer

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 = C + B 2 + C − B 2 2
flt4lem5a.n ⊢ N = C + B 2 − C − B 2 2
flt4lem5a.r ⊢ R = M + N + M − N 2
flt4lem5a.s ⊢ S = M + N − M − N 2
flt4lem5a.a ⊢ φ → A ∈ ℕ
flt4lem5a.b ⊢ φ → B ∈ ℕ
flt4lem5a.c ⊢ φ → C ∈ ℕ
flt4lem5a.1 ⊢ φ → ¬ 2 ∥ A
flt4lem5a.2 ⊢ φ → A gcd C = 1
flt4lem5a.3 ⊢ φ → A 4 + B 4 = C 2
Assertion flt4lem5f ⊢ φ → M gcd B 2 2 = R gcd B 2 4 + S gcd B 2 4

Proof

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