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 | |
|
flt4lem6.b | |
||
flt4lem6.c | |
||
flt4lem6.1 | |
||
Assertion | flt4lem6 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | flt4lem6.a | |
|
2 | flt4lem6.b | |
|
3 | flt4lem6.c | |
|
4 | flt4lem6.1 | |
|
5 | 2 | nnzd | |
6 | divgcdnn | |
|
7 | 1 5 6 | syl2anc | |
8 | 1 | nnzd | |
9 | divgcdnnr | |
|
10 | 2 8 9 | syl2anc | |
11 | gcdnncl | |
|
12 | 1 2 11 | syl2anc | |
13 | 12 | nncnd | |
14 | 13 | flt4lem | |
15 | 4 14 | oveq12d | |
16 | 1 | nncnd | |
17 | 12 | nnne0d | |
18 | 4nn0 | |
|
19 | 18 | a1i | |
20 | 16 13 17 19 | expdivd | |
21 | 2 | nncnd | |
22 | 21 13 17 19 | expdivd | |
23 | 20 22 | oveq12d | |
24 | 16 19 | expcld | |
25 | 21 19 | expcld | |
26 | 13 19 | expcld | |
27 | 12 19 | nnexpcld | |
28 | 27 | nnne0d | |
29 | 24 25 26 28 | divdird | |
30 | 23 29 | eqtr4d | |
31 | 3 | nncnd | |
32 | 12 | nnsqcld | |
33 | 32 | nncnd | |
34 | 32 | nnne0d | |
35 | 31 33 34 | sqdivd | |
36 | 15 30 35 | 3eqtr4d | |
37 | 7 19 | nnexpcld | |
38 | 10 19 | nnexpcld | |
39 | 37 38 | nnaddcld | |
40 | 39 | nnzd | |
41 | 36 40 | eqeltrrd | |
42 | 3 | nnzd | |
43 | znq | |
|
44 | 42 32 43 | syl2anc | |
45 | 3 | nnred | |
46 | 32 | nnred | |
47 | 3 | nngt0d | |
48 | 32 | nngt0d | |
49 | 45 46 47 48 | divgt0d | |
50 | 41 44 49 | posqsqznn | |
51 | 7 10 50 | 3jca | |
52 | 51 36 | jca | |