Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  jm2.27 Structured version   Unicode version

Theorem jm2.27 31112
 Description: Lemma 2.27 of [JonesMatijasevic] p. 697; rmY is a diophantine relation. 0 was excluded from the range of B and the lower limit of G was imposed because the source proof does not seem to work otherwise; quite possible I'm just missing something. The source proof uses both i and I; i has been changed to j to avoid collision. This theorem is basically nothing but substitution instances, all the work is done in jm2.27a 31109 and jm2.27c 31111. Once Diophantine relations have been defined, the content of the theorem is "rmY is Diophantine" (Contributed by Stefan O'Rear, 4-Oct-2014.)
Assertion
Ref Expression
jm2.27 Yrm
Distinct variable groups:   ,,,,,,,   ,,,,,,,   ,,,,,,,

Proof of Theorem jm2.27
StepHypRef Expression
1 simpl1 999 . . . . . . 7 Yrm
2 simpl2 1000 . . . . . . 7 Yrm
3 simpl3 1001 . . . . . . 7 Yrm
4 simpr 461 . . . . . . 7 Yrm Yrm
5 eqid 2457 . . . . . . 7 Xrm Xrm
6 eqid 2457 . . . . . . 7 Yrm Yrm
7 eqid 2457 . . . . . . 7 Yrm Yrm Yrm Yrm
8 eqid 2457 . . . . . . 7 Xrm Yrm Xrm Yrm
9 eqid 2457 . . . . . . 7 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
10 eqid 2457 . . . . . . 7 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
11 eqid 2457 . . . . . . 7 Xrm Yrm Xrm Yrm Xrm Xrm Yrm Xrm Yrm Xrm
12 eqid 2457 . . . . . . 7 Yrm Yrm Yrm Yrm
131, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12jm2.27c 31111 . . . . . 6 Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
1413simpld 459 . . . . 5 Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm
1514simpld 459 . . . 4 Yrm Xrm Yrm Yrm Xrm Yrm
1614simprd 463 . . . . 5 Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm
1713simprd 463 . . . . . 6 Yrm Yrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
18 oveq1 6303 . . . . . . . . . . . 12 Yrm Yrm Yrm Yrm
1918oveq1d 6311 . . . . . . . . . . 11 Yrm Yrm Yrm Yrm
2019eqeq2d 2471 . . . . . . . . . 10 Yrm Yrm Yrm Yrm Yrm Yrm Yrm Yrm
21203anbi2d 1304 . . . . . . . . 9 Yrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
2221anbi2d 703 . . . . . . . 8 Yrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
2322anbi1d 704 . . . . . . 7 Yrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
2423rspcev 3210 . . . . . 6 Yrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
2517, 24syl 16 . . . . 5 Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
26 eleq1 2529 . . . . . . . . . 10 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
27263anbi3d 1305 . . . . . . . . 9 Xrm Yrm Xrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm
28 oveq1 6303 . . . . . . . . . . . . . 14 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
2928oveq1d 6311 . . . . . . . . . . . . 13 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3029oveq1d 6311 . . . . . . . . . . . 12 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3130oveq2d 6312 . . . . . . . . . . 11 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3231eqeq1d 2459 . . . . . . . . . 10 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
33 oveq1 6303 . . . . . . . . . . 11 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3433breq2d 4468 . . . . . . . . . 10 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3532, 343anbi13d 1301 . . . . . . . . 9 Xrm Yrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3627, 35anbi12d 710 . . . . . . . 8 Xrm Yrm Xrm Yrm Xrm Xrm Yrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
37 oveq1 6303 . . . . . . . . . . 11 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3837breq2d 4468 . . . . . . . . . 10 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3938anbi1d 704 . . . . . . . . 9 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
4039anbi1d 704 . . . . . . . 8 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
4136, 40anbi12d 710 . . . . . . 7 Xrm Yrm Xrm Yrm Xrm Xrm Yrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
4241rexbidv 2968 . . . . . 6 Xrm Yrm Xrm Yrm Xrm Xrm Yrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
43 oveq1 6303 . . . . . . . . . . . . 13 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
4443oveq2d 6312 . . . . . . . . . . . 12 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm
4544oveq2d 6312 . . . . . . . . . . 11 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm
4645eqeq1d 2459 . . . . . . . . . 10 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm
47463anbi1d 1303 . . . . . . . . 9 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
4847anbi2d 703 . . . . . . . 8 Xrm Yrm Xrm Yrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
49 oveq1 6303 . . . . . . . . . . 11 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
5049breq2d 4468 . . . . . . . . . 10 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm
5150anbi2d 703 . . . . . . . . 9 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm
52 oveq1 6303 . . . . . . . . . . 11 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
5352breq2d 4468 . . . . . . . . . 10 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
5453anbi1d 704 . . . . . . . . 9 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
5551, 54anbi12d 710 . . . . . . . 8 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
5648, 55anbi12d 710 . . . . . . 7 Xrm Yrm Xrm Yrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
5756rexbidv 2968 . . . . . 6 Xrm Yrm Xrm Yrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Xrm Yrm Yrm Yrm