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∥AYrmN−BYrmN

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→AYrm0=0
9 rmy0 ⊢B∈ℤ≥2→BYrm0=0
10 8 9 oveqan12d ⊢A∈ℤ≥2∧B∈ℤ≥2→AYrm0−BYrm0=0−0
11 7 10 breqtrrd ⊢A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrm0−BYrm0
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→AYrm1=1
16 rmy1 ⊢B∈ℤ≥2→BYrm1=1
17 15 16 oveqan12d ⊢A∈ℤ≥2∧B∈ℤ≥2→AYrm1−BYrm1=1−1
18 14 17 breqtrrd ⊢A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrm1−BYrm1
19 pm3.43 ⊢A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrmb−1−BYrmb−1∧A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrmb−BYrmb→A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb
20 4 3ad2ant2 ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→A−B∈ℤ
21 2z ⊢2∈ℤ
22 21 a1i ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→2∈ℤ
23 simp2l ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→A∈ℤ≥2
24 nnz ⊢b∈ℕ→b∈ℤ
25 24 3ad2ant1 ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→b∈ℤ
26 frmy ⊢Yrm:ℤ≥2×ℤ⟶ℤ
27 26 fovcl ⊢A∈ℤ≥2∧b∈ℤ→AYrmb∈ℤ
28 23 25 27 syl2anc ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→AYrmb∈ℤ
29 1 adantr ⊢A∈ℤ≥2∧B∈ℤ≥2→A∈ℤ
30 29 3ad2ant2 ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→A∈ℤ
31 28 30 zmulcld ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→AYrmb⁢A∈ℤ
32 22 31 zmulcld ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→2⁢AYrmb⁢A∈ℤ
33 simp2r ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→B∈ℤ≥2
34 26 fovcl ⊢B∈ℤ≥2∧b∈ℤ→BYrmb∈ℤ
35 33 25 34 syl2anc ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→BYrmb∈ℤ
36 2 adantl ⊢A∈ℤ≥2∧B∈ℤ≥2→B∈ℤ
37 36 3ad2ant2 ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→B∈ℤ
38 35 37 zmulcld ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→BYrmb⁢B∈ℤ
39 22 38 zmulcld ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→2⁢BYrmb⁢B∈ℤ
40 peano2zm ⊢b∈ℤ→b−1∈ℤ
41 24 40 syl ⊢b∈ℕ→b−1∈ℤ
42 41 3ad2ant1 ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→b−1∈ℤ
43 26 fovcl ⊢A∈ℤ≥2∧b−1∈ℤ→AYrmb−1∈ℤ
44 23 42 43 syl2anc ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→AYrmb−1∈ℤ
45 26 fovcl ⊢B∈ℤ≥2∧b−1∈ℤ→BYrmb−1∈ℤ
46 33 42 45 syl2anc ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→BYrmb−1∈ℤ
47 congid ⊢A−B∈ℤ∧2∈ℤ→A−B∥2−2
48 20 21 47 sylancl ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→A−B∥2−2
49 simp3r ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→A−B∥AYrmb−BYrmb
50 iddvds ⊢A−B∈ℤ→A−B∥A−B
51 20 50 syl ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→A−B∥A−B
52 congmul ⊢A−B∈ℤ∧AYrmb∈ℤ∧BYrmb∈ℤ∧A∈ℤ∧B∈ℤ∧A−B∥AYrmb−BYrmb∧A−B∥A−B→A−B∥AYrmb⁢A−BYrmb⁢B
53 20 28 35 30 37 49 51 52 syl322anc ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→A−B∥AYrmb⁢A−BYrmb⁢B
54 congmul ⊢A−B∈ℤ∧2∈ℤ∧2∈ℤ∧AYrmb⁢A∈ℤ∧BYrmb⁢B∈ℤ∧A−B∥2−2∧A−B∥AYrmb⁢A−BYrmb⁢B→A−B∥2⁢AYrmb⁢A−2⁢BYrmb⁢B
55 20 22 22 31 38 48 53 54 syl322anc ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→A−B∥2⁢AYrmb⁢A−2⁢BYrmb⁢B
56 simp3l ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→A−B∥AYrmb−1−BYrmb−1
57 congsub ⊢A−B∈ℤ∧2⁢AYrmb⁢A∈ℤ∧2⁢BYrmb⁢B∈ℤ∧AYrmb−1∈ℤ∧BYrmb−1∈ℤ∧A−B∥2⁢AYrmb⁢A−2⁢BYrmb⁢B∧A−B∥AYrmb−1−BYrmb−1→A−B∥2⁢AYrmb⁢A-AYrmb−1-2⁢BYrmb⁢B−BYrmb−1
58 20 32 39 44 46 55 56 57 syl322anc ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→A−B∥2⁢AYrmb⁢A-AYrmb−1-2⁢BYrmb⁢B−BYrmb−1
59 rmyluc ⊢A∈ℤ≥2∧b∈ℤ→AYrmb+1=2⁢AYrmb⁢A−AYrmb−1
60 23 25 59 syl2anc ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→AYrmb+1=2⁢AYrmb⁢A−AYrmb−1
61 rmyluc ⊢B∈ℤ≥2∧b∈ℤ→BYrmb+1=2⁢BYrmb⁢B−BYrmb−1
62 33 25 61 syl2anc ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→BYrmb+1=2⁢BYrmb⁢B−BYrmb−1
63 60 62 oveq12d ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→AYrmb+1−BYrmb+1=2⁢AYrmb⁢A-AYrmb−1-2⁢BYrmb⁢B−BYrmb−1
64 58 63 breqtrrd ⊢b∈ℕ∧A∈ℤ≥2∧B∈ℤ≥2∧A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→A−B∥AYrmb+1−BYrmb+1
65 64 3exp ⊢b∈ℕ→A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→A−B∥AYrmb+1−BYrmb+1
66 65 a2d ⊢b∈ℕ→A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrmb−1−BYrmb−1∧A−B∥AYrmb−BYrmb→A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrmb+1−BYrmb+1
67 19 66 syl5 ⊢b∈ℕ→A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrmb−1−BYrmb−1∧A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrmb−BYrmb→A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrmb+1−BYrmb+1
68 oveq2 ⊢a=0→AYrma=AYrm0
69 oveq2 ⊢a=0→BYrma=BYrm0
70 68 69 oveq12d ⊢a=0→AYrma−BYrma=AYrm0−BYrm0
71 70 breq2d ⊢a=0→A−B∥AYrma−BYrma↔A−B∥AYrm0−BYrm0
72 71 imbi2d ⊢a=0→A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrma−BYrma↔A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrm0−BYrm0
73 oveq2 ⊢a=1→AYrma=AYrm1
74 oveq2 ⊢a=1→BYrma=BYrm1
75 73 74 oveq12d ⊢a=1→AYrma−BYrma=AYrm1−BYrm1
76 75 breq2d ⊢a=1→A−B∥AYrma−BYrma↔A−B∥AYrm1−BYrm1
77 76 imbi2d ⊢a=1→A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrma−BYrma↔A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrm1−BYrm1
78 oveq2 ⊢a=b−1→AYrma=AYrmb−1
79 oveq2 ⊢a=b−1→BYrma=BYrmb−1
80 78 79 oveq12d ⊢a=b−1→AYrma−BYrma=AYrmb−1−BYrmb−1
81 80 breq2d ⊢a=b−1→A−B∥AYrma−BYrma↔A−B∥AYrmb−1−BYrmb−1
82 81 imbi2d ⊢a=b−1→A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrma−BYrma↔A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrmb−1−BYrmb−1
83 oveq2 ⊢a=b→AYrma=AYrmb
84 oveq2 ⊢a=b→BYrma=BYrmb
85 83 84 oveq12d ⊢a=b→AYrma−BYrma=AYrmb−BYrmb
86 85 breq2d ⊢a=b→A−B∥AYrma−BYrma↔A−B∥AYrmb−BYrmb
87 86 imbi2d ⊢a=b→A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrma−BYrma↔A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrmb−BYrmb
88 oveq2 ⊢a=b+1→AYrma=AYrmb+1
89 oveq2 ⊢a=b+1→BYrma=BYrmb+1
90 88 89 oveq12d ⊢a=b+1→AYrma−BYrma=AYrmb+1−BYrmb+1
91 90 breq2d ⊢a=b+1→A−B∥AYrma−BYrma↔A−B∥AYrmb+1−BYrmb+1
92 91 imbi2d ⊢a=b+1→A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrma−BYrma↔A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrmb+1−BYrmb+1
93 oveq2 ⊢a=N→AYrma=AYrmN
94 oveq2 ⊢a=N→BYrma=BYrmN
95 93 94 oveq12d ⊢a=N→AYrma−BYrma=AYrmN−BYrmN
96 95 breq2d ⊢a=N→A−B∥AYrma−BYrma↔A−B∥AYrmN−BYrmN
97 96 imbi2d ⊢a=N→A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrma−BYrma↔A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrmN−BYrmN
98 11 18 67 72 77 82 87 92 97 2nn0ind ⊢N∈ℕ0→A∈ℤ≥2∧B∈ℤ≥2→A−B∥AYrmN−BYrmN
99 98 impcom ⊢A∈ℤ≥2∧B∈ℤ≥2∧N∈ℕ0→A−B∥AYrmN−BYrmN
100 99 3impa ⊢A∈ℤ≥2∧B∈ℤ≥2∧N∈ℕ0→A−B∥AYrmN−BYrmN