Metamath Proof Explorer

Theorem jm2.16nn0

Description: Lemma 2.16 of JonesMatijasevic p. 695. This may be regarded as a special case of jm2.15nn0 if rmY is redefined as described in rmyluc . (Contributed by Stefan O'Rear, 1-Oct-2014)

Ref Expression
Assertion jm2.16nn0 ⊢A∈ℤ≥2∧N∈ℕ0→A−1∥AYrmN−N

Proof

Step Hyp Ref Expression
1 eluzelz ⊢A∈ℤ≥2→A∈ℤ
2 peano2zm ⊢A∈ℤ→A−1∈ℤ
3 1 2 syl ⊢A∈ℤ≥2→A−1∈ℤ
4 0z ⊢0∈ℤ
5 congid ⊢A−1∈ℤ∧0∈ℤ→A−1∥0−0
6 3 4 5 sylancl ⊢A∈ℤ≥2→A−1∥0−0
7 rmy0 ⊢A∈ℤ≥2→AYrm0=0
8 7 oveq1d ⊢A∈ℤ≥2→AYrm0−0=0−0
9 6 8 breqtrrd ⊢A∈ℤ≥2→A−1∥AYrm0−0
10 1z ⊢1∈ℤ
11 congid ⊢A−1∈ℤ∧1∈ℤ→A−1∥1−1
12 3 10 11 sylancl ⊢A∈ℤ≥2→A−1∥1−1
13 rmy1 ⊢A∈ℤ≥2→AYrm1=1
14 13 oveq1d ⊢A∈ℤ≥2→AYrm1−1=1−1
15 12 14 breqtrrd ⊢A∈ℤ≥2→A−1∥AYrm1−1
16 pm3.43 ⊢A∈ℤ≥2→A−1∥AYrmb−1−b−1∧A∈ℤ≥2→A−1∥AYrmb−b→A∈ℤ≥2→A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b
17 1 adantl ⊢b∈ℕ∧A∈ℤ≥2→A∈ℤ
18 17 2 syl ⊢b∈ℕ∧A∈ℤ≥2→A−1∈ℤ
19 eluzel2 ⊢A∈ℤ≥2→2∈ℤ
20 19 adantl ⊢b∈ℕ∧A∈ℤ≥2→2∈ℤ
21 simpr ⊢b∈ℕ∧A∈ℤ≥2→A∈ℤ≥2
22 nnz ⊢b∈ℕ→b∈ℤ
23 22 adantr ⊢b∈ℕ∧A∈ℤ≥2→b∈ℤ
24 frmy ⊢Yrm:ℤ≥2×ℤ⟶ℤ
25 24 fovcl ⊢A∈ℤ≥2∧b∈ℤ→AYrmb∈ℤ
26 21 23 25 syl2anc ⊢b∈ℕ∧A∈ℤ≥2→AYrmb∈ℤ
27 26 17 zmulcld ⊢b∈ℕ∧A∈ℤ≥2→AYrmb⁢A∈ℤ
28 20 27 zmulcld ⊢b∈ℕ∧A∈ℤ≥2→2⁢AYrmb⁢A∈ℤ
29 zmulcl ⊢b∈ℤ∧1∈ℤ→b⋅1∈ℤ
30 23 10 29 sylancl ⊢b∈ℕ∧A∈ℤ≥2→b⋅1∈ℤ
31 20 30 zmulcld ⊢b∈ℕ∧A∈ℤ≥2→2⁢b⋅1∈ℤ
32 18 28 31 3jca ⊢b∈ℕ∧A∈ℤ≥2→A−1∈ℤ∧2⁢AYrmb⁢A∈ℤ∧2⁢b⋅1∈ℤ
33 32 3adant3 ⊢b∈ℕ∧A∈ℤ≥2∧A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→A−1∈ℤ∧2⁢AYrmb⁢A∈ℤ∧2⁢b⋅1∈ℤ
34 peano2zm ⊢b∈ℤ→b−1∈ℤ
35 23 34 syl ⊢b∈ℕ∧A∈ℤ≥2→b−1∈ℤ
36 24 fovcl ⊢A∈ℤ≥2∧b−1∈ℤ→AYrmb−1∈ℤ
37 21 35 36 syl2anc ⊢b∈ℕ∧A∈ℤ≥2→AYrmb−1∈ℤ
38 37 35 jca ⊢b∈ℕ∧A∈ℤ≥2→AYrmb−1∈ℤ∧b−1∈ℤ
39 38 3adant3 ⊢b∈ℕ∧A∈ℤ≥2∧A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→AYrmb−1∈ℤ∧b−1∈ℤ
40 18 20 20 3jca ⊢b∈ℕ∧A∈ℤ≥2→A−1∈ℤ∧2∈ℤ∧2∈ℤ
41 40 3adant3 ⊢b∈ℕ∧A∈ℤ≥2∧A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→A−1∈ℤ∧2∈ℤ∧2∈ℤ
42 27 30 jca ⊢b∈ℕ∧A∈ℤ≥2→AYrmb⁢A∈ℤ∧b⋅1∈ℤ
43 42 3adant3 ⊢b∈ℕ∧A∈ℤ≥2∧A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→AYrmb⁢A∈ℤ∧b⋅1∈ℤ
44 congid ⊢A−1∈ℤ∧2∈ℤ→A−1∥2−2
45 18 20 44 syl2anc ⊢b∈ℕ∧A∈ℤ≥2→A−1∥2−2
46 45 3adant3 ⊢b∈ℕ∧A∈ℤ≥2∧A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→A−1∥2−2
47 18 26 23 3jca ⊢b∈ℕ∧A∈ℤ≥2→A−1∈ℤ∧AYrmb∈ℤ∧b∈ℤ
48 47 3adant3 ⊢b∈ℕ∧A∈ℤ≥2∧A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→A−1∈ℤ∧AYrmb∈ℤ∧b∈ℤ
49 17 10 jctir ⊢b∈ℕ∧A∈ℤ≥2→A∈ℤ∧1∈ℤ
50 49 3adant3 ⊢b∈ℕ∧A∈ℤ≥2∧A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→A∈ℤ∧1∈ℤ
51 simp3r ⊢b∈ℕ∧A∈ℤ≥2∧A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→A−1∥AYrmb−b
52 iddvds ⊢A−1∈ℤ→A−1∥A−1
53 18 52 syl ⊢b∈ℕ∧A∈ℤ≥2→A−1∥A−1
54 53 3adant3 ⊢b∈ℕ∧A∈ℤ≥2∧A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→A−1∥A−1
55 congmul ⊢A−1∈ℤ∧AYrmb∈ℤ∧b∈ℤ∧A∈ℤ∧1∈ℤ∧A−1∥AYrmb−b∧A−1∥A−1→A−1∥AYrmb⁢A−b⋅1
56 48 50 51 54 55 syl112anc ⊢b∈ℕ∧A∈ℤ≥2∧A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→A−1∥AYrmb⁢A−b⋅1
57 congmul ⊢A−1∈ℤ∧2∈ℤ∧2∈ℤ∧AYrmb⁢A∈ℤ∧b⋅1∈ℤ∧A−1∥2−2∧A−1∥AYrmb⁢A−b⋅1→A−1∥2⁢AYrmb⁢A−2⁢b⋅1
58 41 43 46 56 57 syl112anc ⊢b∈ℕ∧A∈ℤ≥2∧A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→A−1∥2⁢AYrmb⁢A−2⁢b⋅1
59 simp3l ⊢b∈ℕ∧A∈ℤ≥2∧A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→A−1∥AYrmb−1−b−1
60 congsub ⊢A−1∈ℤ∧2⁢AYrmb⁢A∈ℤ∧2⁢b⋅1∈ℤ∧AYrmb−1∈ℤ∧b−1∈ℤ∧A−1∥2⁢AYrmb⁢A−2⁢b⋅1∧A−1∥AYrmb−1−b−1→A−1∥2⁢AYrmb⁢A-AYrmb−1-2⁢b⋅1−b−1
61 33 39 58 59 60 syl112anc ⊢b∈ℕ∧A∈ℤ≥2∧A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→A−1∥2⁢AYrmb⁢A-AYrmb−1-2⁢b⋅1−b−1
62 rmyluc ⊢A∈ℤ≥2∧b∈ℤ→AYrmb+1=2⁢AYrmb⁢A−AYrmb−1
63 21 23 62 syl2anc ⊢b∈ℕ∧A∈ℤ≥2→AYrmb+1=2⁢AYrmb⁢A−AYrmb−1
64 nncn ⊢b∈ℕ→b∈ℂ
65 64 mulridd ⊢b∈ℕ→b⋅1=b
66 65 oveq2d ⊢b∈ℕ→2⁢b⋅1=2⁢b
67 64 2timesd ⊢b∈ℕ→2⁢b=b+b
68 66 67 eqtrd ⊢b∈ℕ→2⁢b⋅1=b+b
69 68 oveq1d ⊢b∈ℕ→2⁢b⋅1−b−1=b+b-b−1
70 1cnd ⊢b∈ℕ→1∈ℂ
71 64 64 70 pnncand ⊢b∈ℕ→b+b-b−1=b+1
72 69 71 eqtr2d ⊢b∈ℕ→b+1=2⁢b⋅1−b−1
73 72 adantr ⊢b∈ℕ∧A∈ℤ≥2→b+1=2⁢b⋅1−b−1
74 63 73 oveq12d ⊢b∈ℕ∧A∈ℤ≥2→AYrmb+1−b+1=2⁢AYrmb⁢A-AYrmb−1-2⁢b⋅1−b−1
75 74 3adant3 ⊢b∈ℕ∧A∈ℤ≥2∧A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→AYrmb+1−b+1=2⁢AYrmb⁢A-AYrmb−1-2⁢b⋅1−b−1
76 61 75 breqtrrd ⊢b∈ℕ∧A∈ℤ≥2∧A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→A−1∥AYrmb+1−b+1
77 76 3exp ⊢b∈ℕ→A∈ℤ≥2→A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→A−1∥AYrmb+1−b+1
78 77 a2d ⊢b∈ℕ→A∈ℤ≥2→A−1∥AYrmb−1−b−1∧A−1∥AYrmb−b→A∈ℤ≥2→A−1∥AYrmb+1−b+1
79 16 78 syl5 ⊢b∈ℕ→A∈ℤ≥2→A−1∥AYrmb−1−b−1∧A∈ℤ≥2→A−1∥AYrmb−b→A∈ℤ≥2→A−1∥AYrmb+1−b+1
80 oveq2 ⊢a=0→AYrma=AYrm0
81 id ⊢a=0→a=0
82 80 81 oveq12d ⊢a=0→AYrma−a=AYrm0−0
83 82 breq2d ⊢a=0→A−1∥AYrma−a↔A−1∥AYrm0−0
84 83 imbi2d ⊢a=0→A∈ℤ≥2→A−1∥AYrma−a↔A∈ℤ≥2→A−1∥AYrm0−0
85 oveq2 ⊢a=1→AYrma=AYrm1
86 id ⊢a=1→a=1
87 85 86 oveq12d ⊢a=1→AYrma−a=AYrm1−1
88 87 breq2d ⊢a=1→A−1∥AYrma−a↔A−1∥AYrm1−1
89 88 imbi2d ⊢a=1→A∈ℤ≥2→A−1∥AYrma−a↔A∈ℤ≥2→A−1∥AYrm1−1
90 oveq2 ⊢a=b−1→AYrma=AYrmb−1
91 id ⊢a=b−1→a=b−1
92 90 91 oveq12d ⊢a=b−1→AYrma−a=AYrmb−1−b−1
93 92 breq2d ⊢a=b−1→A−1∥AYrma−a↔A−1∥AYrmb−1−b−1
94 93 imbi2d ⊢a=b−1→A∈ℤ≥2→A−1∥AYrma−a↔A∈ℤ≥2→A−1∥AYrmb−1−b−1
95 oveq2 ⊢a=b→AYrma=AYrmb
96 id ⊢a=b→a=b
97 95 96 oveq12d ⊢a=b→AYrma−a=AYrmb−b
98 97 breq2d ⊢a=b→A−1∥AYrma−a↔A−1∥AYrmb−b
99 98 imbi2d ⊢a=b→A∈ℤ≥2→A−1∥AYrma−a↔A∈ℤ≥2→A−1∥AYrmb−b
100 oveq2 ⊢a=b+1→AYrma=AYrmb+1
101 id ⊢a=b+1→a=b+1
102 100 101 oveq12d ⊢a=b+1→AYrma−a=AYrmb+1−b+1
103 102 breq2d ⊢a=b+1→A−1∥AYrma−a↔A−1∥AYrmb+1−b+1
104 103 imbi2d ⊢a=b+1→A∈ℤ≥2→A−1∥AYrma−a↔A∈ℤ≥2→A−1∥AYrmb+1−b+1
105 oveq2 ⊢a=N→AYrma=AYrmN
106 id ⊢a=N→a=N
107 105 106 oveq12d ⊢a=N→AYrma−a=AYrmN−N
108 107 breq2d ⊢a=N→A−1∥AYrma−a↔A−1∥AYrmN−N
109 108 imbi2d ⊢a=N→A∈ℤ≥2→A−1∥AYrma−a↔A∈ℤ≥2→A−1∥AYrmN−N
110 9 15 79 84 89 94 99 104 109 2nn0ind ⊢N∈ℕ0→A∈ℤ≥2→A−1∥AYrmN−N
111 110 impcom ⊢A∈ℤ≥2∧N∈ℕ0→A−1∥AYrmN−N