Metamath Proof Explorer


Theorem jm2.15nn0

Description: Lemma 2.15 of JonesMatijasevic p. 695. rmY is a polynomial for fixed N, so has the expected congruence property. (Contributed by Stefan O'Rear, 1-Oct-2014)

Ref Expression
Assertion jm2.15nn0 A 2 B 2 N 0 A B A Y rm N B Y rm N

Proof

Step Hyp Ref Expression
1 eluzelz A 2 A
2 eluzelz B 2 B
3 zsubcl A B A B
4 1 2 3 syl2an A 2 B 2 A B
5 0z 0
6 congid A B 0 A B 0 0
7 4 5 6 sylancl A 2 B 2 A B 0 0
8 rmy0 A 2 A Y rm 0 = 0
9 rmy0 B 2 B Y rm 0 = 0
10 8 9 oveqan12d A 2 B 2 A Y rm 0 B Y rm 0 = 0 0
11 7 10 breqtrrd A 2 B 2 A B A Y rm 0 B Y rm 0
12 1z 1
13 congid A B 1 A B 1 1
14 4 12 13 sylancl A 2 B 2 A B 1 1
15 rmy1 A 2 A Y rm 1 = 1
16 rmy1 B 2 B Y rm 1 = 1
17 15 16 oveqan12d A 2 B 2 A Y rm 1 B Y rm 1 = 1 1
18 14 17 breqtrrd A 2 B 2 A B A Y rm 1 B Y rm 1
19 pm3.43 A 2 B 2 A B A Y rm b 1 B Y rm b 1 A 2 B 2 A B A Y rm b B Y rm b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b
20 4 3ad2ant2 b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A B
21 2z 2
22 21 a1i b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b 2
23 simp2l b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A 2
24 nnz b b
25 24 3ad2ant1 b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b b
26 frmy Y rm : 2 ×
27 26 fovcl A 2 b A Y rm b
28 23 25 27 syl2anc b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A Y rm b
29 1 adantr A 2 B 2 A
30 29 3ad2ant2 b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A
31 28 30 zmulcld b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A Y rm b A
32 22 31 zmulcld b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b 2 A Y rm b A
33 simp2r b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b B 2
34 26 fovcl B 2 b B Y rm b
35 33 25 34 syl2anc b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b B Y rm b
36 2 adantl A 2 B 2 B
37 36 3ad2ant2 b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b B
38 35 37 zmulcld b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b B Y rm b B
39 22 38 zmulcld b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b 2 B Y rm b B
40 peano2zm b b 1
41 24 40 syl b b 1
42 41 3ad2ant1 b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b b 1
43 26 fovcl A 2 b 1 A Y rm b 1
44 23 42 43 syl2anc b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A Y rm b 1
45 26 fovcl B 2 b 1 B Y rm b 1
46 33 42 45 syl2anc b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b B Y rm b 1
47 congid A B 2 A B 2 2
48 20 21 47 sylancl b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A B 2 2
49 simp3r b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A B A Y rm b B Y rm b
50 iddvds A B A B A B
51 20 50 syl b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A B A B
52 congmul A B A Y rm b B Y rm b A B A B A Y rm b B Y rm b A B A B A B A Y rm b A B Y rm b B
53 20 28 35 30 37 49 51 52 syl322anc b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A B A Y rm b A B Y rm b B
54 congmul A B 2 2 A Y rm b A B Y rm b B A B 2 2 A B A Y rm b A B Y rm b B A B 2 A Y rm b A 2 B Y rm b B
55 20 22 22 31 38 48 53 54 syl322anc b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A B 2 A Y rm b A 2 B Y rm b B
56 simp3l b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A B A Y rm b 1 B Y rm b 1
57 congsub A B 2 A Y rm b A 2 B Y rm b B A Y rm b 1 B Y rm b 1 A B 2 A Y rm b A 2 B Y rm b B A B A Y rm b 1 B Y rm b 1 A B 2 A Y rm b A - A Y rm b 1 - 2 B Y rm b B B Y rm b 1
58 20 32 39 44 46 55 56 57 syl322anc b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A B 2 A Y rm b A - A Y rm b 1 - 2 B Y rm b B B Y rm b 1
59 rmyluc A 2 b A Y rm b + 1 = 2 A Y rm b A A Y rm b 1
60 23 25 59 syl2anc b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A Y rm b + 1 = 2 A Y rm b A A Y rm b 1
61 rmyluc B 2 b B Y rm b + 1 = 2 B Y rm b B B Y rm b 1
62 33 25 61 syl2anc b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b B Y rm b + 1 = 2 B Y rm b B B Y rm b 1
63 60 62 oveq12d b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A Y rm b + 1 B Y rm b + 1 = 2 A Y rm b A - A Y rm b 1 - 2 B Y rm b B B Y rm b 1
64 58 63 breqtrrd b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A B A Y rm b + 1 B Y rm b + 1
65 64 3exp b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A B A Y rm b + 1 B Y rm b + 1
66 65 a2d b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A B A Y rm b B Y rm b A 2 B 2 A B A Y rm b + 1 B Y rm b + 1
67 19 66 syl5 b A 2 B 2 A B A Y rm b 1 B Y rm b 1 A 2 B 2 A B A Y rm b B Y rm b A 2 B 2 A B A Y rm b + 1 B Y rm b + 1
68 oveq2 a = 0 A Y rm a = A Y rm 0
69 oveq2 a = 0 B Y rm a = B Y rm 0
70 68 69 oveq12d a = 0 A Y rm a B Y rm a = A Y rm 0 B Y rm 0
71 70 breq2d a = 0 A B A Y rm a B Y rm a A B A Y rm 0 B Y rm 0
72 71 imbi2d a = 0 A 2 B 2 A B A Y rm a B Y rm a A 2 B 2 A B A Y rm 0 B Y rm 0
73 oveq2 a = 1 A Y rm a = A Y rm 1
74 oveq2 a = 1 B Y rm a = B Y rm 1
75 73 74 oveq12d a = 1 A Y rm a B Y rm a = A Y rm 1 B Y rm 1
76 75 breq2d a = 1 A B A Y rm a B Y rm a A B A Y rm 1 B Y rm 1
77 76 imbi2d a = 1 A 2 B 2 A B A Y rm a B Y rm a A 2 B 2 A B A Y rm 1 B Y rm 1
78 oveq2 a = b 1 A Y rm a = A Y rm b 1
79 oveq2 a = b 1 B Y rm a = B Y rm b 1
80 78 79 oveq12d a = b 1 A Y rm a B Y rm a = A Y rm b 1 B Y rm b 1
81 80 breq2d a = b 1 A B A Y rm a B Y rm a A B A Y rm b 1 B Y rm b 1
82 81 imbi2d a = b 1 A 2 B 2 A B A Y rm a B Y rm a A 2 B 2 A B A Y rm b 1 B Y rm b 1
83 oveq2 a = b A Y rm a = A Y rm b
84 oveq2 a = b B Y rm a = B Y rm b
85 83 84 oveq12d a = b A Y rm a B Y rm a = A Y rm b B Y rm b
86 85 breq2d a = b A B A Y rm a B Y rm a A B A Y rm b B Y rm b
87 86 imbi2d a = b A 2 B 2 A B A Y rm a B Y rm a A 2 B 2 A B A Y rm b B Y rm b
88 oveq2 a = b + 1 A Y rm a = A Y rm b + 1
89 oveq2 a = b + 1 B Y rm a = B Y rm b + 1
90 88 89 oveq12d a = b + 1 A Y rm a B Y rm a = A Y rm b + 1 B Y rm b + 1
91 90 breq2d a = b + 1 A B A Y rm a B Y rm a A B A Y rm b + 1 B Y rm b + 1
92 91 imbi2d a = b + 1 A 2 B 2 A B A Y rm a B Y rm a A 2 B 2 A B A Y rm b + 1 B Y rm b + 1
93 oveq2 a = N A Y rm a = A Y rm N
94 oveq2 a = N B Y rm a = B Y rm N
95 93 94 oveq12d a = N A Y rm a B Y rm a = A Y rm N B Y rm N
96 95 breq2d a = N A B A Y rm a B Y rm a A B A Y rm N B Y rm N
97 96 imbi2d a = N A 2 B 2 A B A Y rm a B Y rm a A 2 B 2 A B A Y rm N B Y rm N
98 11 18 67 72 77 82 87 92 97 2nn0ind N 0 A 2 B 2 A B A Y rm N B Y rm N
99 98 impcom A 2 B 2 N 0 A B A Y rm N B Y rm N
100 99 3impa A 2 B 2 N 0 A B A Y rm N B Y rm N