Metamath Proof Explorer


Theorem flt4lem5d

Description: Part 3 of Equation 2 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html . (Contributed by SN, 23-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 flt4lem5d ( 𝜑𝑀 = ( ( 𝑅 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) )

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 5 nnsqcld ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℕ )
12 6 nnsqcld ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℕ )
13 2prm 2 ∈ ℙ
14 5 nnzd ( 𝜑𝐴 ∈ ℤ )
15 prmdvdssq ( ( 2 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 2 ∥ 𝐴 ↔ 2 ∥ ( 𝐴 ↑ 2 ) ) )
16 13 14 15 sylancr ( 𝜑 → ( 2 ∥ 𝐴 ↔ 2 ∥ ( 𝐴 ↑ 2 ) ) )
17 8 16 mtbid ( 𝜑 → ¬ 2 ∥ ( 𝐴 ↑ 2 ) )
18 2nn 2 ∈ ℕ
19 18 a1i ( 𝜑 → 2 ∈ ℕ )
20 rplpwr ( ( 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ ∧ 2 ∈ ℕ ) → ( ( 𝐴 gcd 𝐶 ) = 1 → ( ( 𝐴 ↑ 2 ) gcd 𝐶 ) = 1 ) )
21 5 7 19 20 syl3anc ( 𝜑 → ( ( 𝐴 gcd 𝐶 ) = 1 → ( ( 𝐴 ↑ 2 ) gcd 𝐶 ) = 1 ) )
22 9 21 mpd ( 𝜑 → ( ( 𝐴 ↑ 2 ) gcd 𝐶 ) = 1 )
23 5 nncnd ( 𝜑𝐴 ∈ ℂ )
24 23 flt4lem ( 𝜑 → ( 𝐴 ↑ 4 ) = ( ( 𝐴 ↑ 2 ) ↑ 2 ) )
25 6 nncnd ( 𝜑𝐵 ∈ ℂ )
26 25 flt4lem ( 𝜑 → ( 𝐵 ↑ 4 ) = ( ( 𝐵 ↑ 2 ) ↑ 2 ) )
27 24 26 oveq12d ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) )
28 27 10 eqtr3d ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
29 11 12 7 17 22 28 flt4lem1 ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) )
30 2 pythagtriplem13 ( ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) → 𝑁 ∈ ℕ )
31 29 30 syl ( 𝜑𝑁 ∈ ℕ )
32 1 pythagtriplem11 ( ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) → 𝑀 ∈ ℕ )
33 29 32 syl ( 𝜑𝑀 ∈ ℕ )
34 1 2 3 4 5 6 7 8 9 10 flt4lem5a ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) )
35 31 nnzd ( 𝜑𝑁 ∈ ℤ )
36 14 35 gcdcomd ( 𝜑 → ( 𝐴 gcd 𝑁 ) = ( 𝑁 gcd 𝐴 ) )
37 33 nnzd ( 𝜑𝑀 ∈ ℤ )
38 35 37 gcdcomd ( 𝜑 → ( 𝑁 gcd 𝑀 ) = ( 𝑀 gcd 𝑁 ) )
39 1 2 flt4lem5 ( ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) → ( 𝑀 gcd 𝑁 ) = 1 )
40 29 39 syl ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
41 38 40 eqtrd ( 𝜑 → ( 𝑁 gcd 𝑀 ) = 1 )
42 31 nnsqcld ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℕ )
43 42 nncnd ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℂ )
44 11 nncnd ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
45 43 44 addcomd ( 𝜑 → ( ( 𝑁 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) )
46 45 34 eqtrd ( 𝜑 → ( ( 𝑁 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) )
47 31 5 33 41 46 fltabcoprm ( 𝜑 → ( 𝑁 gcd 𝐴 ) = 1 )
48 36 47 eqtrd ( 𝜑 → ( 𝐴 gcd 𝑁 ) = 1 )
49 3 4 pythagtriplem17 ( ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝑁 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝑀 = ( ( 𝑅 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) )
50 5 31 33 34 48 8 49 syl312anc ( 𝜑𝑀 = ( ( 𝑅 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) )