Metamath Proof Explorer


Theorem eqrabdioph

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 N0t1NAmzPoly1Nt1NBmzPoly1Nt01N|A=BDiophN

Proof

Step Hyp Ref Expression
1 nfmpt1 _tt1NA
2 1 nfel1 tt1NAmzPoly1N
3 nfmpt1 _tt1NB
4 3 nfel1 tt1NBmzPoly1N
5 2 4 nfan tt1NAmzPoly1Nt1NBmzPoly1N
6 mzpf t1NAmzPoly1Nt1NA:1N
7 6 ad2antrr t1NAmzPoly1Nt1NBmzPoly1Nt01Nt1NA:1N
8 zex V
9 nn0ssz 0
10 mapss V001N1N
11 8 9 10 mp2an 01N1N
12 11 sseli t01Nt1N
13 12 adantl t1NAmzPoly1Nt1NBmzPoly1Nt01Nt1N
14 mptfcl t1NA:1Nt1NA
15 7 13 14 sylc t1NAmzPoly1Nt1NBmzPoly1Nt01NA
16 15 zcnd t1NAmzPoly1Nt1NBmzPoly1Nt01NA
17 mzpf t1NBmzPoly1Nt1NB:1N
18 17 ad2antlr t1NAmzPoly1Nt1NBmzPoly1Nt01Nt1NB:1N
19 mptfcl t1NB:1Nt1NB
20 18 13 19 sylc t1NAmzPoly1Nt1NBmzPoly1Nt01NB
21 20 zcnd t1NAmzPoly1Nt1NBmzPoly1Nt01NB
22 16 21 subeq0ad t1NAmzPoly1Nt1NBmzPoly1Nt01NAB=0A=B
23 22 bicomd t1NAmzPoly1Nt1NBmzPoly1Nt01NA=BAB=0
24 23 ex t1NAmzPoly1Nt1NBmzPoly1Nt01NA=BAB=0
25 5 24 ralrimi t1NAmzPoly1Nt1NBmzPoly1Nt01NA=BAB=0
26 rabbi t01NA=BAB=0t01N|A=B=t01N|AB=0
27 25 26 sylib t1NAmzPoly1Nt1NBmzPoly1Nt01N|A=B=t01N|AB=0
28 27 3adant1 N0t1NAmzPoly1Nt1NBmzPoly1Nt01N|A=B=t01N|AB=0
29 simp1 N0t1NAmzPoly1Nt1NBmzPoly1NN0
30 mzpsubmpt t1NAmzPoly1Nt1NBmzPoly1Nt1NABmzPoly1N
31 30 3adant1 N0t1NAmzPoly1Nt1NBmzPoly1Nt1NABmzPoly1N
32 eq0rabdioph N0t1NABmzPoly1Nt01N|AB=0DiophN
33 29 31 32 syl2anc N0t1NAmzPoly1Nt1NBmzPoly1Nt01N|AB=0DiophN
34 28 33 eqeltrd N0t1NAmzPoly1Nt1NBmzPoly1Nt01N|A=BDiophN