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

Theorem jm2.27 26786
 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 26783 and jm2.27c 26785. 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 960 . . . . . . 7 Yrm
2 simpl2 961 . . . . . . 7 Yrm
3 simpl3 962 . . . . . . 7 Yrm
4 simpr 448 . . . . . . 7 Yrm Yrm
5 eqid 2401 . . . . . . 7 Xrm Xrm
6 eqid 2401 . . . . . . 7 Yrm Yrm
7 eqid 2401 . . . . . . 7 Yrm Yrm Yrm Yrm
8 eqid 2401 . . . . . . 7 Xrm Yrm Xrm Yrm
9 eqid 2401 . . . . . . 7 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
10 eqid 2401 . . . . . . 7 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
11 eqid 2401 . . . . . . 7 Xrm Yrm Xrm Yrm Xrm Xrm Yrm Xrm Yrm Xrm
12 eqid 2401 . . . . . . 7 Yrm Yrm Yrm Yrm
131, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12jm2.27c 26785 . . . . . 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 446 . . . . 5 Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm
1514simpld 446 . . . 4 Yrm Xrm Yrm Yrm Xrm Yrm
1614simprd 450 . . . . 5 Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm
1713simprd 450 . . . . . 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 6041 . . . . . . . . . . . 12 Yrm Yrm Yrm Yrm
1918oveq1d 6049 . . . . . . . . . . 11 Yrm Yrm Yrm Yrm
2019eqeq2d 2412 . . . . . . . . . 10 Yrm Yrm Yrm Yrm Yrm Yrm Yrm Yrm
21203anbi2d 1259 . . . . . . . . 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 685 . . . . . . . 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 686 . . . . . . 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 3009 . . . . . 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 2461 . . . . . . . . . 10 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
27263anbi3d 1260 . . . . . . . . 9 Xrm Yrm Xrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm
28 oveq1 6041 . . . . . . . . . . . . . 14 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
2928oveq1d 6049 . . . . . . . . . . . . 13 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3029oveq1d 6049 . . . . . . . . . . . 12 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3130oveq2d 6050 . . . . . . . . . . 11 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3231eqeq1d 2409 . . . . . . . . . 10 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
33 oveq1 6041 . . . . . . . . . . 11 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3433breq2d 4179 . . . . . . . . . 10 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3532, 343anbi13d 1256 . . . . . . . . 9 Xrm Yrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3627, 35anbi12d 692 . . . . . . . 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 6041 . . . . . . . . . . 11 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3837breq2d 4179 . . . . . . . . . 10 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
3938anbi1d 686 . . . . . . . . 9 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
4039anbi1d 686 . . . . . . . 8 Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm
4136, 40anbi12d 692 . . . . . . 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 2684 . . . . . 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 6041 . . . . . . . . . . . . 13 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
4443oveq2d 6050 . . . . . . . . . . . 12 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm
4544oveq2d 6050 . . . . . . . . . . 11 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm
4645eqeq1d 2409 . . . . . . . . . 10 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm
47463anbi1d 1258 . . . . . . . . 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 685 . . . . . . . 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 6041 . . . . . . . . . . 11 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
5049breq2d 4179 . . . . . . . . . 10 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Xrm Yrm Yrm
5150anbi2d 685 . . . . . . . . 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 6041 . . . . . . . . . . 11 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
5352breq2d 4179 . . . . . . . . . 10 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
5453anbi1d 686 . . . . . . . . 9 Xrm Yrm Xrm Yrm Yrm Xrm Yrm Xrm Yrm Yrm
5551, 54anbi12d 692 . . . . . . . 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 692 . . . . . . 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 2684 . . . . . 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