Metamath Proof Explorer


Theorem flt4lem6

Description: Remove shared factors in a solution to A ^ 4 + B ^ 4 = C ^ 2 . (Contributed by SN, 24-Jul-2024)

Ref Expression
Hypotheses flt4lem6.a φA
flt4lem6.b φB
flt4lem6.c φC
flt4lem6.1 φA4+B4=C2
Assertion flt4lem6 φAAgcdBBAgcdBCAgcdB2AAgcdB4+BAgcdB4=CAgcdB22

Proof

Step Hyp Ref Expression
1 flt4lem6.a φA
2 flt4lem6.b φB
3 flt4lem6.c φC
4 flt4lem6.1 φA4+B4=C2
5 2 nnzd φB
6 divgcdnn ABAAgcdB
7 1 5 6 syl2anc φAAgcdB
8 1 nnzd φA
9 divgcdnnr BABAgcdB
10 2 8 9 syl2anc φBAgcdB
11 gcdnncl ABAgcdB
12 1 2 11 syl2anc φAgcdB
13 12 nncnd φAgcdB
14 13 flt4lem φAgcdB4=AgcdB22
15 4 14 oveq12d φA4+B4AgcdB4=C2AgcdB22
16 1 nncnd φA
17 12 nnne0d φAgcdB0
18 4nn0 40
19 18 a1i φ40
20 16 13 17 19 expdivd φAAgcdB4=A4AgcdB4
21 2 nncnd φB
22 21 13 17 19 expdivd φBAgcdB4=B4AgcdB4
23 20 22 oveq12d φAAgcdB4+BAgcdB4=A4AgcdB4+B4AgcdB4
24 16 19 expcld φA4
25 21 19 expcld φB4
26 13 19 expcld φAgcdB4
27 12 19 nnexpcld φAgcdB4
28 27 nnne0d φAgcdB40
29 24 25 26 28 divdird φA4+B4AgcdB4=A4AgcdB4+B4AgcdB4
30 23 29 eqtr4d φAAgcdB4+BAgcdB4=A4+B4AgcdB4
31 3 nncnd φC
32 12 nnsqcld φAgcdB2
33 32 nncnd φAgcdB2
34 32 nnne0d φAgcdB20
35 31 33 34 sqdivd φCAgcdB22=C2AgcdB22
36 15 30 35 3eqtr4d φAAgcdB4+BAgcdB4=CAgcdB22
37 7 19 nnexpcld φAAgcdB4
38 10 19 nnexpcld φBAgcdB4
39 37 38 nnaddcld φAAgcdB4+BAgcdB4
40 39 nnzd φAAgcdB4+BAgcdB4
41 36 40 eqeltrrd φCAgcdB22
42 3 nnzd φC
43 znq CAgcdB2CAgcdB2
44 42 32 43 syl2anc φCAgcdB2
45 3 nnred φC
46 32 nnred φAgcdB2
47 3 nngt0d φ0<C
48 32 nngt0d φ0<AgcdB2
49 45 46 47 48 divgt0d φ0<CAgcdB2
50 41 44 49 posqsqznn φCAgcdB2
51 7 10 50 3jca φAAgcdBBAgcdBCAgcdB2
52 51 36 jca φAAgcdBBAgcdBCAgcdB2AAgcdB4+BAgcdB4=CAgcdB22