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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldiophb | |
|
2 | simp-5r | |
|
3 | simprr | |
|
4 | 3 | ad2antrr | |
5 | simprl | |
|
6 | f1f | |
|
7 | 5 6 | syl | |
8 | mzprename | |
|
9 | 2 4 7 8 | syl3anc | |
10 | simprr | |
|
11 | diophrw | |
|
12 | 11 | eqcomd | |
13 | 2 5 10 12 | syl3anc | |
14 | fveq1 | |
|
15 | 14 | eqeq1d | |
16 | 15 | anbi2d | |
17 | 16 | rexbidv | |
18 | 17 | abbidv | |
19 | 18 | rspceeqv | |
20 | 9 13 19 | syl2anc | |
21 | simplll | |
|
22 | simplrl | |
|
23 | simplrr | |
|
24 | simprl | |
|
25 | eldioph2lem2 | |
|
26 | 21 22 23 24 25 | syl22anc | |
27 | rexv | |
|
28 | 26 27 | sylibr | |
29 | 20 28 | r19.29a | |
30 | eqeq1 | |
|
31 | 30 | rexbidv | |
32 | 29 31 | syl5ibrcom | |
33 | 32 | rexlimdvva | |
34 | 33 | adantld | |
35 | 1 34 | syl5bi | |
36 | simpr | |
|
37 | simplll | |
|
38 | simpllr | |
|
39 | simplrr | |
|
40 | simpr | |
|
41 | eldioph2 | |
|
42 | 37 38 39 40 41 | syl121anc | |
43 | 42 | adantr | |
44 | 36 43 | eqeltrd | |
45 | 44 | rexlimdva2 | |
46 | 35 45 | impbid | |