Metamath Proof Explorer


Theorem flt4lem5c

Description: Part 2 of Equation 2 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 flt4lem5c φ N = 2 R S

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 2 pythagtriplem13 A 2 B 2 C A 2 2 + B 2 2 = C 2 A 2 gcd B 2 = 1 ¬ 2 A 2 N
31 29 30 syl φ N
32 1 pythagtriplem11 A 2 B 2 C A 2 2 + B 2 2 = C 2 A 2 gcd B 2 = 1 ¬ 2 A 2 M
33 29 32 syl φ M
34 1 2 3 4 5 6 7 8 9 10 flt4lem5a φ A 2 + N 2 = M 2
35 31 nnzd φ N
36 14 35 gcdcomd φ A gcd N = N gcd A
37 33 nnzd φ M
38 35 37 gcdcomd φ N gcd M = M gcd N
39 1 2 flt4lem5 A 2 B 2 C A 2 2 + B 2 2 = C 2 A 2 gcd B 2 = 1 ¬ 2 A 2 M gcd N = 1
40 29 39 syl φ M gcd N = 1
41 38 40 eqtrd φ N gcd M = 1
42 31 nnsqcld φ N 2
43 42 nncnd φ N 2
44 11 nncnd φ A 2
45 43 44 addcomd φ N 2 + A 2 = A 2 + N 2
46 45 34 eqtrd φ N 2 + A 2 = M 2
47 31 5 33 41 46 fltabcoprm φ N gcd A = 1
48 36 47 eqtrd φ A gcd N = 1
49 3 4 pythagtriplem16 A N M A 2 + N 2 = M 2 A gcd N = 1 ¬ 2 A N = 2 R S
50 5 31 33 34 48 8 49 syl312anc φ N = 2 R S