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 N 0 S V ¬ S Fin 1 N S A Dioph N p mzPoly S A = t | u 0 S t = u 1 N p u = 0

Proof

Step Hyp Ref Expression
1 eldiophb A Dioph N N 0 a N b mzPoly 1 a A = t | d 0 1 a t = d 1 N b d = 0
2 simp-5r N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a c V c : 1 a 1-1 S c 1 N = I 1 N S V
3 simprr N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a b mzPoly 1 a
4 3 ad2antrr N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a c V c : 1 a 1-1 S c 1 N = I 1 N b mzPoly 1 a
5 simprl N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a c V c : 1 a 1-1 S c 1 N = I 1 N c : 1 a 1-1 S
6 f1f c : 1 a 1-1 S c : 1 a S
7 5 6 syl N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a c V c : 1 a 1-1 S c 1 N = I 1 N c : 1 a S
8 mzprename S V b mzPoly 1 a c : 1 a S e S b e c mzPoly S
9 2 4 7 8 syl3anc N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a c V c : 1 a 1-1 S c 1 N = I 1 N e S b e c mzPoly S
10 simprr N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a c V c : 1 a 1-1 S c 1 N = I 1 N c 1 N = I 1 N
11 diophrw S V c : 1 a 1-1 S c 1 N = I 1 N t | u 0 S t = u 1 N e S b e c u = 0 = t | d 0 1 a t = d 1 N b d = 0
12 11 eqcomd S V c : 1 a 1-1 S c 1 N = I 1 N t | d 0 1 a t = d 1 N b d = 0 = t | u 0 S t = u 1 N e S b e c u = 0
13 2 5 10 12 syl3anc N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a c V c : 1 a 1-1 S c 1 N = I 1 N t | d 0 1 a t = d 1 N b d = 0 = t | u 0 S t = u 1 N e S b e c u = 0
14 fveq1 p = e S b e c p u = e S b e c u
15 14 eqeq1d p = e S b e c p u = 0 e S b e c u = 0
16 15 anbi2d p = e S b e c t = u 1 N p u = 0 t = u 1 N e S b e c u = 0
17 16 rexbidv p = e S b e c u 0 S t = u 1 N p u = 0 u 0 S t = u 1 N e S b e c u = 0
18 17 abbidv p = e S b e c t | u 0 S t = u 1 N p u = 0 = t | u 0 S t = u 1 N e S b e c u = 0
19 18 rspceeqv e S b e c mzPoly S t | d 0 1 a t = d 1 N b d = 0 = t | u 0 S t = u 1 N e S b e c u = 0 p mzPoly S t | d 0 1 a t = d 1 N b d = 0 = t | u 0 S t = u 1 N p u = 0
20 9 13 19 syl2anc N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a c V c : 1 a 1-1 S c 1 N = I 1 N p mzPoly S t | d 0 1 a t = d 1 N b d = 0 = t | u 0 S t = u 1 N p u = 0
21 simplll N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a N 0
22 simplrl N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a ¬ S Fin
23 simplrr N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a 1 N S
24 simprl N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a a N
25 eldioph2lem2 N 0 ¬ S Fin 1 N S a N c c : 1 a 1-1 S c 1 N = I 1 N
26 21 22 23 24 25 syl22anc N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a c c : 1 a 1-1 S c 1 N = I 1 N
27 rexv c V c : 1 a 1-1 S c 1 N = I 1 N c c : 1 a 1-1 S c 1 N = I 1 N
28 26 27 sylibr N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a c V c : 1 a 1-1 S c 1 N = I 1 N
29 20 28 r19.29a N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a p mzPoly S t | d 0 1 a t = d 1 N b d = 0 = t | u 0 S t = u 1 N p u = 0
30 eqeq1 A = t | d 0 1 a t = d 1 N b d = 0 A = t | u 0 S t = u 1 N p u = 0 t | d 0 1 a t = d 1 N b d = 0 = t | u 0 S t = u 1 N p u = 0
31 30 rexbidv A = t | d 0 1 a t = d 1 N b d = 0 p mzPoly S A = t | u 0 S t = u 1 N p u = 0 p mzPoly S t | d 0 1 a t = d 1 N b d = 0 = t | u 0 S t = u 1 N p u = 0
32 29 31 syl5ibrcom N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a A = t | d 0 1 a t = d 1 N b d = 0 p mzPoly S A = t | u 0 S t = u 1 N p u = 0
33 32 rexlimdvva N 0 S V ¬ S Fin 1 N S a N b mzPoly 1 a A = t | d 0 1 a t = d 1 N b d = 0 p mzPoly S A = t | u 0 S t = u 1 N p u = 0
34 33 adantld N 0 S V ¬ S Fin 1 N S N 0 a N b mzPoly 1 a A = t | d 0 1 a t = d 1 N b d = 0 p mzPoly S A = t | u 0 S t = u 1 N p u = 0
35 1 34 syl5bi N 0 S V ¬ S Fin 1 N S A Dioph N p mzPoly S A = t | u 0 S t = u 1 N p u = 0
36 simpr N 0 S V ¬ S Fin 1 N S p mzPoly S A = t | u 0 S t = u 1 N p u = 0 A = t | u 0 S t = u 1 N p u = 0
37 simplll N 0 S V ¬ S Fin 1 N S p mzPoly S N 0
38 simpllr N 0 S V ¬ S Fin 1 N S p mzPoly S S V
39 simplrr N 0 S V ¬ S Fin 1 N S p mzPoly S 1 N S
40 simpr N 0 S V ¬ S Fin 1 N S p mzPoly S p mzPoly S
41 eldioph2 N 0 S V 1 N S p mzPoly S t | u 0 S t = u 1 N p u = 0 Dioph N
42 37 38 39 40 41 syl121anc N 0 S V ¬ S Fin 1 N S p mzPoly S t | u 0 S t = u 1 N p u = 0 Dioph N
43 42 adantr N 0 S V ¬ S Fin 1 N S p mzPoly S A = t | u 0 S t = u 1 N p u = 0 t | u 0 S t = u 1 N p u = 0 Dioph N
44 36 43 eqeltrd N 0 S V ¬ S Fin 1 N S p mzPoly S A = t | u 0 S t = u 1 N p u = 0 A Dioph N
45 44 rexlimdva2 N 0 S V ¬ S Fin 1 N S p mzPoly S A = t | u 0 S t = u 1 N p u = 0 A Dioph N
46 35 45 impbid N 0 S V ¬ S Fin 1 N S A Dioph N p mzPoly S A = t | u 0 S t = u 1 N p u = 0