Metamath Proof Explorer


Theorem eldioph2b

Description: While Diophantine sets were defined to have a finite number of witness variables consequtively following the observable variables, this is not necessary; they can equivalently be taken to use any witness set ( S \ ( 1 ... N ) ) . For instance, in diophin we use this to take the two input sets to have disjoint witness sets. (Contributed by Stefan O'Rear, 8-Oct-2014)

Ref Expression
Assertion eldioph2b N0SV¬SFin1NSADiophNpmzPolySA=t|u0St=u1Npu=0

Proof

Step Hyp Ref Expression
1 eldiophb ADiophNN0aNbmzPoly1aA=t|d01at=d1Nbd=0
2 simp-5r N0SV¬SFin1NSaNbmzPoly1acVc:1a1-1Sc1N=I1NSV
3 simprr N0SV¬SFin1NSaNbmzPoly1abmzPoly1a
4 3 ad2antrr N0SV¬SFin1NSaNbmzPoly1acVc:1a1-1Sc1N=I1NbmzPoly1a
5 simprl N0SV¬SFin1NSaNbmzPoly1acVc:1a1-1Sc1N=I1Nc:1a1-1S
6 f1f c:1a1-1Sc:1aS
7 5 6 syl N0SV¬SFin1NSaNbmzPoly1acVc:1a1-1Sc1N=I1Nc:1aS
8 mzprename SVbmzPoly1ac:1aSeSbecmzPolyS
9 2 4 7 8 syl3anc N0SV¬SFin1NSaNbmzPoly1acVc:1a1-1Sc1N=I1NeSbecmzPolyS
10 simprr N0SV¬SFin1NSaNbmzPoly1acVc:1a1-1Sc1N=I1Nc1N=I1N
11 diophrw SVc:1a1-1Sc1N=I1Nt|u0St=u1NeSbecu=0=t|d01at=d1Nbd=0
12 11 eqcomd SVc:1a1-1Sc1N=I1Nt|d01at=d1Nbd=0=t|u0St=u1NeSbecu=0
13 2 5 10 12 syl3anc N0SV¬SFin1NSaNbmzPoly1acVc:1a1-1Sc1N=I1Nt|d01at=d1Nbd=0=t|u0St=u1NeSbecu=0
14 fveq1 p=eSbecpu=eSbecu
15 14 eqeq1d p=eSbecpu=0eSbecu=0
16 15 anbi2d p=eSbect=u1Npu=0t=u1NeSbecu=0
17 16 rexbidv p=eSbecu0St=u1Npu=0u0St=u1NeSbecu=0
18 17 abbidv p=eSbect|u0St=u1Npu=0=t|u0St=u1NeSbecu=0
19 18 rspceeqv eSbecmzPolySt|d01at=d1Nbd=0=t|u0St=u1NeSbecu=0pmzPolySt|d01at=d1Nbd=0=t|u0St=u1Npu=0
20 9 13 19 syl2anc N0SV¬SFin1NSaNbmzPoly1acVc:1a1-1Sc1N=I1NpmzPolySt|d01at=d1Nbd=0=t|u0St=u1Npu=0
21 simplll N0SV¬SFin1NSaNbmzPoly1aN0
22 simplrl N0SV¬SFin1NSaNbmzPoly1a¬SFin
23 simplrr N0SV¬SFin1NSaNbmzPoly1a1NS
24 simprl N0SV¬SFin1NSaNbmzPoly1aaN
25 eldioph2lem2 N0¬SFin1NSaNcc:1a1-1Sc1N=I1N
26 21 22 23 24 25 syl22anc N0SV¬SFin1NSaNbmzPoly1acc:1a1-1Sc1N=I1N
27 rexv cVc:1a1-1Sc1N=I1Ncc:1a1-1Sc1N=I1N
28 26 27 sylibr N0SV¬SFin1NSaNbmzPoly1acVc:1a1-1Sc1N=I1N
29 20 28 r19.29a N0SV¬SFin1NSaNbmzPoly1apmzPolySt|d01at=d1Nbd=0=t|u0St=u1Npu=0
30 eqeq1 A=t|d01at=d1Nbd=0A=t|u0St=u1Npu=0t|d01at=d1Nbd=0=t|u0St=u1Npu=0
31 30 rexbidv A=t|d01at=d1Nbd=0pmzPolySA=t|u0St=u1Npu=0pmzPolySt|d01at=d1Nbd=0=t|u0St=u1Npu=0
32 29 31 syl5ibrcom N0SV¬SFin1NSaNbmzPoly1aA=t|d01at=d1Nbd=0pmzPolySA=t|u0St=u1Npu=0
33 32 rexlimdvva N0SV¬SFin1NSaNbmzPoly1aA=t|d01at=d1Nbd=0pmzPolySA=t|u0St=u1Npu=0
34 33 adantld N0SV¬SFin1NSN0aNbmzPoly1aA=t|d01at=d1Nbd=0pmzPolySA=t|u0St=u1Npu=0
35 1 34 syl5bi N0SV¬SFin1NSADiophNpmzPolySA=t|u0St=u1Npu=0
36 simpr N0SV¬SFin1NSpmzPolySA=t|u0St=u1Npu=0A=t|u0St=u1Npu=0
37 simplll N0SV¬SFin1NSpmzPolySN0
38 simpllr N0SV¬SFin1NSpmzPolySSV
39 simplrr N0SV¬SFin1NSpmzPolyS1NS
40 simpr N0SV¬SFin1NSpmzPolySpmzPolyS
41 eldioph2 N0SV1NSpmzPolySt|u0St=u1Npu=0DiophN
42 37 38 39 40 41 syl121anc N0SV¬SFin1NSpmzPolySt|u0St=u1Npu=0DiophN
43 42 adantr N0SV¬SFin1NSpmzPolySA=t|u0St=u1Npu=0t|u0St=u1Npu=0DiophN
44 36 43 eqeltrd N0SV¬SFin1NSpmzPolySA=t|u0St=u1Npu=0ADiophN
45 44 rexlimdva2 N0SV¬SFin1NSpmzPolySA=t|u0St=u1Npu=0ADiophN
46 35 45 impbid N0SV¬SFin1NSADiophNpmzPolySA=t|u0St=u1Npu=0