Description: Diophantine set builder for equality of polynomial expressions. Note that the two expressions need not be nonnegative; only variables are so constrained. (Contributed by Stefan O'Rear, 10-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | eqrabdioph | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfmpt1 | |
|
2 | 1 | nfel1 | |
3 | nfmpt1 | |
|
4 | 3 | nfel1 | |
5 | 2 4 | nfan | |
6 | mzpf | |
|
7 | 6 | ad2antrr | |
8 | zex | |
|
9 | nn0ssz | |
|
10 | mapss | |
|
11 | 8 9 10 | mp2an | |
12 | 11 | sseli | |
13 | 12 | adantl | |
14 | mptfcl | |
|
15 | 7 13 14 | sylc | |
16 | 15 | zcnd | |
17 | mzpf | |
|
18 | 17 | ad2antlr | |
19 | mptfcl | |
|
20 | 18 13 19 | sylc | |
21 | 20 | zcnd | |
22 | 16 21 | subeq0ad | |
23 | 22 | bicomd | |
24 | 23 | ex | |
25 | 5 24 | ralrimi | |
26 | rabbi | |
|
27 | 25 26 | sylib | |
28 | 27 | 3adant1 | |
29 | simp1 | |
|
30 | mzpsubmpt | |
|
31 | 30 | 3adant1 | |
32 | eq0rabdioph | |
|
33 | 29 31 32 | syl2anc | |
34 | 28 33 | eqeltrd | |