Metamath Proof Explorer


Theorem 7rexfrabdioph

Description: Diophantine set builder for existential quantifier, explicit substitution, seven variables. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses rexfrabdioph.1 M = N + 1
rexfrabdioph.2 L = M + 1
rexfrabdioph.3 K = L + 1
rexfrabdioph.4 J = K + 1
rexfrabdioph.5 I = J + 1
rexfrabdioph.6 H = I + 1
rexfrabdioph.7 G = H + 1
Assertion 7rexfrabdioph N 0 t 0 1 G | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ Dioph G u 0 1 N | v 0 w 0 x 0 y 0 z 0 p 0 q 0 φ Dioph N

Proof

Step Hyp Ref Expression
1 rexfrabdioph.1 M = N + 1
2 rexfrabdioph.2 L = M + 1
3 rexfrabdioph.3 K = L + 1
4 rexfrabdioph.4 J = K + 1
5 rexfrabdioph.5 I = J + 1
6 rexfrabdioph.6 H = I + 1
7 rexfrabdioph.7 G = H + 1
8 sbc2rex [˙ a M / v]˙ w 0 x 0 y 0 z 0 p 0 q 0 φ w 0 x 0 [˙ a M / v]˙ y 0 z 0 p 0 q 0 φ
9 sbc4rex [˙ a M / v]˙ y 0 z 0 p 0 q 0 φ y 0 z 0 p 0 q 0 [˙ a M / v]˙ φ
10 9 2rexbii w 0 x 0 [˙ a M / v]˙ y 0 z 0 p 0 q 0 φ w 0 x 0 y 0 z 0 p 0 q 0 [˙ a M / v]˙ φ
11 8 10 bitri [˙ a M / v]˙ w 0 x 0 y 0 z 0 p 0 q 0 φ w 0 x 0 y 0 z 0 p 0 q 0 [˙ a M / v]˙ φ
12 11 sbcbii [˙ a 1 N / u]˙ [˙ a M / v]˙ w 0 x 0 y 0 z 0 p 0 q 0 φ [˙ a 1 N / u]˙ w 0 x 0 y 0 z 0 p 0 q 0 [˙ a M / v]˙ φ
13 sbc2rex [˙ a 1 N / u]˙ w 0 x 0 y 0 z 0 p 0 q 0 [˙ a M / v]˙ φ w 0 x 0 [˙ a 1 N / u]˙ y 0 z 0 p 0 q 0 [˙ a M / v]˙ φ
14 sbc4rex [˙ a 1 N / u]˙ y 0 z 0 p 0 q 0 [˙ a M / v]˙ φ y 0 z 0 p 0 q 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
15 14 2rexbii w 0 x 0 [˙ a 1 N / u]˙ y 0 z 0 p 0 q 0 [˙ a M / v]˙ φ w 0 x 0 y 0 z 0 p 0 q 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
16 12 13 15 3bitri [˙ a 1 N / u]˙ [˙ a M / v]˙ w 0 x 0 y 0 z 0 p 0 q 0 φ w 0 x 0 y 0 z 0 p 0 q 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
17 16 rabbii a 0 1 M | [˙ a 1 N / u]˙ [˙ a M / v]˙ w 0 x 0 y 0 z 0 p 0 q 0 φ = a 0 1 M | w 0 x 0 y 0 z 0 p 0 q 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
18 nn0p1nn N 0 N + 1
19 1 18 eqeltrid N 0 M
20 19 nnnn0d N 0 M 0
21 20 adantr N 0 t 0 1 G | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ Dioph G M 0
22 sbcrot3 [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t L / w]˙ [˙ t K / x]˙ [˙ a M / v]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
23 22 sbcbii [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ a 1 N / u]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ a M / v]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
24 sbcrot3 [˙ a 1 N / u]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ a M / v]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t L / w]˙ [˙ t K / x]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
25 sbcrot5 [˙ a M / v]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ [˙ a M / v]˙ φ
26 25 sbcbii [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ a 1 N / u]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ [˙ a M / v]˙ φ
27 sbcrot5 [˙ a 1 N / u]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ [˙ a M / v]˙ φ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
28 26 27 bitri [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
29 28 sbcbii [˙ t K / x]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
30 29 sbcbii [˙ t L / w]˙ [˙ t K / x]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
31 23 24 30 3bitri [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
32 31 sbcbii [˙ t 1 M / a]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t 1 M / a]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ
33 reseq1 a = t 1 M a 1 N = t 1 M 1 N
34 33 sbccomieg [˙ t 1 M / a]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t 1 M 1 N / u]˙ [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
35 fzssp1 1 N 1 N + 1
36 1 oveq2i 1 M = 1 N + 1
37 35 36 sseqtrri 1 N 1 M
38 resabs1 1 N 1 M t 1 M 1 N = t 1 N
39 dfsbcq t 1 M 1 N = t 1 N [˙ t 1 M 1 N / u]˙ [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t 1 N / u]˙ [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
40 37 38 39 mp2b [˙ t 1 M 1 N / u]˙ [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t 1 N / u]˙ [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
41 vex t V
42 41 resex t 1 M V
43 fveq1 a = t 1 M a M = t 1 M M
44 43 sbcco3gw t 1 M V [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t 1 M M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
45 42 44 ax-mp [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t 1 M M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
46 elfz1end M M 1 M
47 19 46 sylib N 0 M 1 M
48 fvres M 1 M t 1 M M = t M
49 dfsbcq t 1 M M = t M [˙ t 1 M M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
50 47 48 49 3syl N 0 [˙ t 1 M M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
51 45 50 syl5bb N 0 [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
52 51 sbcbidv N 0 [˙ t 1 N / u]˙ [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
53 40 52 syl5bb N 0 [˙ t 1 M 1 N / u]˙ [˙ t 1 M / a]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
54 34 53 syl5bb N 0 [˙ t 1 M / a]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
55 32 54 bitr3id N 0 [˙ t 1 M / a]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
56 55 rabbidv N 0 t 0 1 G | [˙ t 1 M / a]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ = t 0 1 G | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ
57 56 eleq1d N 0 t 0 1 G | [˙ t 1 M / a]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ Dioph G t 0 1 G | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ Dioph G
58 57 biimpar N 0 t 0 1 G | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ Dioph G t 0 1 G | [˙ t 1 M / a]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ Dioph G
59 2 3 4 5 6 7 6rexfrabdioph M 0 t 0 1 G | [˙ t 1 M / a]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ φ Dioph G a 0 1 M | w 0 x 0 y 0 z 0 p 0 q 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ φ Dioph M
60 21 58 59 syl2anc N 0 t 0 1 G | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ Dioph G a 0 1 M | w 0 x 0 y 0 z 0 p 0 q 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ φ Dioph M
61 17 60 eqeltrid N 0 t 0 1 G | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ Dioph G a 0 1 M | [˙ a 1 N / u]˙ [˙ a M / v]˙ w 0 x 0 y 0 z 0 p 0 q 0 φ Dioph M
62 1 rexfrabdioph N 0 a 0 1 M | [˙ a 1 N / u]˙ [˙ a M / v]˙ w 0 x 0 y 0 z 0 p 0 q 0 φ Dioph M u 0 1 N | v 0 w 0 x 0 y 0 z 0 p 0 q 0 φ Dioph N
63 61 62 syldan N 0 t 0 1 G | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ t I / z]˙ [˙ t H / p]˙ [˙ t G / q]˙ φ Dioph G u 0 1 N | v 0 w 0 x 0 y 0 z 0 p 0 q 0 φ Dioph N