Metamath Proof Explorer


Theorem 4rexfrabdioph

Description: Diophantine set builder for existential quantifier, explicit substitution, four 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
Assertion 4rexfrabdioph N 0 t 0 1 J | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ Dioph J u 0 1 N | v 0 w 0 x 0 y 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 2sbcrex [˙ a M / v]˙ [˙ a L / w]˙ x 0 y 0 φ x 0 [˙ a M / v]˙ [˙ a L / w]˙ y 0 φ
6 2sbcrex [˙ a M / v]˙ [˙ a L / w]˙ y 0 φ y 0 [˙ a M / v]˙ [˙ a L / w]˙ φ
7 6 rexbii x 0 [˙ a M / v]˙ [˙ a L / w]˙ y 0 φ x 0 y 0 [˙ a M / v]˙ [˙ a L / w]˙ φ
8 5 7 bitri [˙ a M / v]˙ [˙ a L / w]˙ x 0 y 0 φ x 0 y 0 [˙ a M / v]˙ [˙ a L / w]˙ φ
9 8 sbcbii [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ x 0 y 0 φ [˙ a 1 N / u]˙ x 0 y 0 [˙ a M / v]˙ [˙ a L / w]˙ φ
10 sbc2rex [˙ a 1 N / u]˙ x 0 y 0 [˙ a M / v]˙ [˙ a L / w]˙ φ x 0 y 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ
11 9 10 bitri [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ x 0 y 0 φ x 0 y 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ
12 11 rabbii a 0 1 L | [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ x 0 y 0 φ = a 0 1 L | x 0 y 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ
13 nn0p1nn N 0 N + 1
14 1 13 eqeltrid N 0 M
15 14 peano2nnd N 0 M + 1
16 2 15 eqeltrid N 0 L
17 16 nnnn0d N 0 L 0
18 17 adantr N 0 t 0 1 J | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ Dioph J L 0
19 sbcrot3 [˙ a 1 N / u]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ [˙ t K / x]˙ [˙ t J / y]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ
20 sbcrot3 [˙ t J / y]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t J / y]˙ φ
21 20 sbcbii [˙ t K / x]˙ [˙ t J / y]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ [˙ t K / x]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t J / y]˙ φ
22 sbcrot3 [˙ t K / x]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t J / y]˙ φ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
23 21 22 bitri [˙ t K / x]˙ [˙ t J / y]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
24 23 sbcbii [˙ a 1 N / u]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
25 19 24 bitr3i [˙ t K / x]˙ [˙ t J / y]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
26 25 sbcbii [˙ t 1 L / a]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ [˙ t 1 L / a]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
27 reseq1 a = t 1 L a 1 N = t 1 L 1 N
28 27 sbccomieg [˙ t 1 L / a]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t 1 L 1 N / u]˙ [˙ t 1 L / a]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
29 fzssp1 1 N 1 N + 1
30 1 oveq2i 1 M = 1 N + 1
31 29 30 sseqtrri 1 N 1 M
32 fzssp1 1 M 1 M + 1
33 2 oveq2i 1 L = 1 M + 1
34 32 33 sseqtrri 1 M 1 L
35 31 34 sstri 1 N 1 L
36 resabs1 1 N 1 L t 1 L 1 N = t 1 N
37 dfsbcq t 1 L 1 N = t 1 N [˙ t 1 L 1 N / u]˙ [˙ t 1 L / a]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t 1 N / u]˙ [˙ t 1 L / a]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
38 35 36 37 mp2b [˙ t 1 L 1 N / u]˙ [˙ t 1 L / a]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t 1 N / u]˙ [˙ t 1 L / a]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
39 fveq1 a = t 1 L a M = t 1 L M
40 39 sbccomieg [˙ t 1 L / a]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t 1 L M / v]˙ [˙ t 1 L / a]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
41 elfz1end M M 1 M
42 14 41 sylib N 0 M 1 M
43 34 42 sseldi N 0 M 1 L
44 fvres M 1 L t 1 L M = t M
45 dfsbcq t 1 L M = t M [˙ t 1 L M / v]˙ [˙ t 1 L / a]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t M / v]˙ [˙ t 1 L / a]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
46 43 44 45 3syl N 0 [˙ t 1 L M / v]˙ [˙ t 1 L / a]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t M / v]˙ [˙ t 1 L / a]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
47 vex t V
48 47 resex t 1 L V
49 fveq1 a = t 1 L a L = t 1 L L
50 49 sbcco3gw t 1 L V [˙ t 1 L / a]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t 1 L L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
51 48 50 ax-mp [˙ t 1 L / a]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t 1 L L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
52 elfz1end L L 1 L
53 16 52 sylib N 0 L 1 L
54 fvres L 1 L t 1 L L = t L
55 dfsbcq t 1 L L = t L [˙ t 1 L L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
56 53 54 55 3syl N 0 [˙ t 1 L L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
57 51 56 syl5bb N 0 [˙ t 1 L / a]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
58 57 sbcbidv N 0 [˙ t M / v]˙ [˙ t 1 L / a]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
59 46 58 bitrd N 0 [˙ t 1 L M / v]˙ [˙ t 1 L / a]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
60 40 59 syl5bb N 0 [˙ t 1 L / a]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
61 60 sbcbidv N 0 [˙ t 1 N / u]˙ [˙ t 1 L / a]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
62 38 61 syl5bb N 0 [˙ t 1 L 1 N / u]˙ [˙ t 1 L / a]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
63 28 62 syl5bb N 0 [˙ t 1 L / a]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
64 26 63 syl5bb N 0 [˙ t 1 L / a]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
65 64 rabbidv N 0 t 0 1 J | [˙ t 1 L / a]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ = t 0 1 J | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ
66 65 eleq1d N 0 t 0 1 J | [˙ t 1 L / a]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ Dioph J t 0 1 J | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ Dioph J
67 66 biimpar N 0 t 0 1 J | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ Dioph J t 0 1 J | [˙ t 1 L / a]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ Dioph J
68 3 4 2rexfrabdioph L 0 t 0 1 J | [˙ t 1 L / a]˙ [˙ t K / x]˙ [˙ t J / y]˙ [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ Dioph J a 0 1 L | x 0 y 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ Dioph L
69 18 67 68 syl2anc N 0 t 0 1 J | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ Dioph J a 0 1 L | x 0 y 0 [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ φ Dioph L
70 12 69 eqeltrid N 0 t 0 1 J | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ Dioph J a 0 1 L | [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ x 0 y 0 φ Dioph L
71 1 2 2rexfrabdioph N 0 a 0 1 L | [˙ a 1 N / u]˙ [˙ a M / v]˙ [˙ a L / w]˙ x 0 y 0 φ Dioph L u 0 1 N | v 0 w 0 x 0 y 0 φ Dioph N
72 70 71 syldan N 0 t 0 1 J | [˙ t 1 N / u]˙ [˙ t M / v]˙ [˙ t L / w]˙ [˙ t K / x]˙ [˙ t J / y]˙ φ Dioph J u 0 1 N | v 0 w 0 x 0 y 0 φ Dioph N