This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem flt4lem5b

Description: Part 2 of Equation 1 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html . (Contributed by SN, 22-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 flt4lem5b ⊢ φ → 2 ⁢ M ⋅ N = B 2

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 5 nnsqcld ⊢ φ → A 2 ∈ ℕ
12 6 nnsqcld ⊢ φ → B 2 ∈ ℕ
13 2prm ⊢ 2 ∈ ℙ
14 5 nnzd ⊢ φ → A ∈ ℤ
15 prmdvdssq ⊢ 2 ∈ ℙ ∧ A ∈ ℤ → 2 ∥ A ↔ 2 ∥ A 2
16 13 14 15 sylancr ⊢ φ → 2 ∥ A ↔ 2 ∥ A 2
17 8 16 mtbid ⊢ φ → ¬ 2 ∥ A 2
18 2nn ⊢ 2 ∈ ℕ
19 18 a1i ⊢ φ → 2 ∈ ℕ
20 rplpwr ⊢ A ∈ ℕ ∧ C ∈ ℕ ∧ 2 ∈ ℕ → A gcd C = 1 → A 2 gcd C = 1
21 5 7 19 20 syl3anc ⊢ φ → A gcd C = 1 → A 2 gcd C = 1
22 9 21 mpd ⊢ φ → A 2 gcd C = 1
23 5 nncnd ⊢ φ → A ∈ ℂ
24 23 flt4lem ⊢ φ → A 4 = A 2 2
25 6 nncnd ⊢ φ → B ∈ ℂ
26 25 flt4lem ⊢ φ → B 4 = B 2 2
27 24 26 oveq12d ⊢ φ → A 4 + B 4 = A 2 2 + B 2 2
28 27 10 eqtr3d ⊢ φ → A 2 2 + B 2 2 = C 2
29 11 12 7 17 22 28 flt4lem1 ⊢ φ → A 2 ∈ ℕ ∧ B 2 ∈ ℕ ∧ C ∈ ℕ ∧ A 2 2 + B 2 2 = C 2 ∧ A 2 gcd B 2 = 1 ∧ ¬ 2 ∥ A 2
30 1 2 pythagtriplem16 ⊢ A 2 ∈ ℕ ∧ B 2 ∈ ℕ ∧ C ∈ ℕ ∧ A 2 2 + B 2 2 = C 2 ∧ A 2 gcd B 2 = 1 ∧ ¬ 2 ∥ A 2 → B 2 = 2 ⁢ M ⋅ N
31 29 30 syl ⊢ φ → B 2 = 2 ⁢ M ⋅ N
32 31 eqcomd ⊢ φ → 2 ⁢ M ⋅ N = B 2