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 exp4sqsq ⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) = ( ( 𝐴 ↑ 2 ) ↑ 2 ) )
25 6 nncnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
26 25 exp4sqsq ⊢ ( 𝜑 → ( 𝐵 ↑ 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 ) ) )