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 ⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 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 ) ) )