Metamath Proof Explorer


Theorem jm2.18

Description: Theorem 2.18 of JonesMatijasevic p. 696. Direct relationship of the exponential function to X and Y sequences. (Contributed by Stefan O'Rear, 14-Oct-2014)

Ref Expression
Assertion jm2.18 A 2 K 0 N 0 2 A K - K 2 - 1 A X rm N - A K A Y rm N - K N

Proof

Step Hyp Ref Expression
1 2z 2
2 eluzelz A 2 A
3 2 adantr A 2 K 0 A
4 zmulcl 2 A 2 A
5 1 3 4 sylancr A 2 K 0 2 A
6 nn0z K 0 K
7 6 adantl A 2 K 0 K
8 5 7 zmulcld A 2 K 0 2 A K
9 zsqcl K K 2
10 7 9 syl A 2 K 0 K 2
11 8 10 zsubcld A 2 K 0 2 A K K 2
12 peano2zm 2 A K K 2 2 A K - K 2 - 1
13 11 12 syl A 2 K 0 2 A K - K 2 - 1
14 dvds0 2 A K - K 2 - 1 2 A K - K 2 - 1 0
15 13 14 syl A 2 K 0 2 A K - K 2 - 1 0
16 rmx0 A 2 A X rm 0 = 1
17 16 adantr A 2 K 0 A X rm 0 = 1
18 rmy0 A 2 A Y rm 0 = 0
19 18 adantr A 2 K 0 A Y rm 0 = 0
20 19 oveq2d A 2 K 0 A K A Y rm 0 = A K 0
21 3 7 zsubcld A 2 K 0 A K
22 21 zcnd A 2 K 0 A K
23 22 mul01d A 2 K 0 A K 0 = 0
24 20 23 eqtrd A 2 K 0 A K A Y rm 0 = 0
25 17 24 oveq12d A 2 K 0 A X rm 0 A K A Y rm 0 = 1 0
26 1m0e1 1 0 = 1
27 25 26 syl6eq A 2 K 0 A X rm 0 A K A Y rm 0 = 1
28 nn0cn K 0 K
29 28 adantl A 2 K 0 K
30 29 exp0d A 2 K 0 K 0 = 1
31 27 30 oveq12d A 2 K 0 A X rm 0 - A K A Y rm 0 - K 0 = 1 1
32 1m1e0 1 1 = 0
33 31 32 syl6eq A 2 K 0 A X rm 0 - A K A Y rm 0 - K 0 = 0
34 15 33 breqtrrd A 2 K 0 2 A K - K 2 - 1 A X rm 0 - A K A Y rm 0 - K 0
35 rmx1 A 2 A X rm 1 = A
36 35 adantr A 2 K 0 A X rm 1 = A
37 rmy1 A 2 A Y rm 1 = 1
38 37 adantr A 2 K 0 A Y rm 1 = 1
39 38 oveq2d A 2 K 0 A K A Y rm 1 = A K 1
40 22 mulid1d A 2 K 0 A K 1 = A K
41 39 40 eqtrd A 2 K 0 A K A Y rm 1 = A K
42 36 41 oveq12d A 2 K 0 A X rm 1 A K A Y rm 1 = A A K
43 3 zcnd A 2 K 0 A
44 43 29 nncand A 2 K 0 A A K = K
45 42 44 eqtrd A 2 K 0 A X rm 1 A K A Y rm 1 = K
46 29 exp1d A 2 K 0 K 1 = K
47 45 46 oveq12d A 2 K 0 A X rm 1 - A K A Y rm 1 - K 1 = K K
48 29 subidd A 2 K 0 K K = 0
49 47 48 eqtrd A 2 K 0 A X rm 1 - A K A Y rm 1 - K 1 = 0
50 15 49 breqtrrd A 2 K 0 2 A K - K 2 - 1 A X rm 1 - A K A Y rm 1 - K 1
51 pm3.43 A 2 K 0 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 A 2 K 0 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b A 2 K 0 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b
52 13 adantr A 2 K 0 b 2 A K - K 2 - 1
53 5 adantr A 2 K 0 b 2 A
54 simpll A 2 K 0 b A 2
55 nnz b b
56 55 adantl A 2 K 0 b b
57 frmx X rm : 2 × 0
58 57 fovcl A 2 b A X rm b 0
59 54 56 58 syl2anc A 2 K 0 b A X rm b 0
60 59 nn0zd A 2 K 0 b A X rm b
61 21 adantr A 2 K 0 b A K
62 frmy Y rm : 2 ×
63 62 fovcl A 2 b A Y rm b
64 54 56 63 syl2anc A 2 K 0 b A Y rm b
65 61 64 zmulcld A 2 K 0 b A K A Y rm b
66 60 65 zsubcld A 2 K 0 b A X rm b A K A Y rm b
67 53 66 zmulcld A 2 K 0 b 2 A A X rm b A K A Y rm b
68 peano2zm b b 1
69 56 68 syl A 2 K 0 b b 1
70 57 fovcl A 2 b 1 A X rm b 1 0
71 54 69 70 syl2anc A 2 K 0 b A X rm b 1 0
72 71 nn0zd A 2 K 0 b A X rm b 1
73 62 fovcl A 2 b 1 A Y rm b 1
74 54 69 73 syl2anc A 2 K 0 b A Y rm b 1
75 61 74 zmulcld A 2 K 0 b A K A Y rm b 1
76 72 75 zsubcld A 2 K 0 b A X rm b 1 A K A Y rm b 1
77 67 76 zsubcld A 2 K 0 b 2 A A X rm b A K A Y rm b A X rm b 1 A K A Y rm b 1
78 52 77 jca A 2 K 0 b 2 A K - K 2 - 1 2 A A X rm b A K A Y rm b A X rm b 1 A K A Y rm b 1
79 78 adantr A 2 K 0 b 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K - K 2 - 1 2 A A X rm b A K A Y rm b A X rm b 1 A K A Y rm b 1
80 7 adantr A 2 K 0 b K
81 nnnn0 b b 0
82 81 adantl A 2 K 0 b b 0
83 zexpcl K b 0 K b
84 80 82 83 syl2anc A 2 K 0 b K b
85 53 84 zmulcld A 2 K 0 b 2 A K b
86 nnm1nn0 b b 1 0
87 86 adantl A 2 K 0 b b 1 0
88 zexpcl K b 1 0 K b 1
89 80 87 88 syl2anc A 2 K 0 b K b 1
90 85 89 zsubcld A 2 K 0 b 2 A K b K b 1
91 0z 0
92 zaddcl 0 K 2 0 + K 2
93 91 10 92 sylancr A 2 K 0 0 + K 2
94 93 adantr A 2 K 0 b 0 + K 2
95 89 94 zmulcld A 2 K 0 b K b 1 0 + K 2
96 90 95 jca A 2 K 0 b 2 A K b K b 1 K b 1 0 + K 2
97 96 adantr A 2 K 0 b 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K b K b 1 K b 1 0 + K 2
98 52 67 85 3jca A 2 K 0 b 2 A K - K 2 - 1 2 A A X rm b A K A Y rm b 2 A K b
99 98 adantr A 2 K 0 b 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K - K 2 - 1 2 A A X rm b A K A Y rm b 2 A K b
100 76 89 jca A 2 K 0 b A X rm b 1 A K A Y rm b 1 K b 1
101 100 adantr A 2 K 0 b 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b A X rm b 1 A K A Y rm b 1 K b 1
102 13 5 5 3jca A 2 K 0 2 A K - K 2 - 1 2 A 2 A
103 102 ad2antrr A 2 K 0 b 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K - K 2 - 1 2 A 2 A
104 66 84 jca A 2 K 0 b A X rm b A K A Y rm b K b
105 104 adantr A 2 K 0 b 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b A X rm b A K A Y rm b K b
106 congid 2 A K - K 2 - 1 2 A 2 A K - K 2 - 1 2 A 2 A
107 13 5 106 syl2anc A 2 K 0 2 A K - K 2 - 1 2 A 2 A
108 107 ad2antrr A 2 K 0 b 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K - K 2 - 1 2 A 2 A
109 simpr A 2 K 0 b 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b
110 congmul 2 A K - K 2 - 1 2 A 2 A A X rm b A K A Y rm b K b 2 A K - K 2 - 1 2 A 2 A 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K - K 2 - 1 2 A A X rm b A K A Y rm b 2 A K b
111 103 105 108 109 110 syl112anc A 2 K 0 b 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K - K 2 - 1 2 A A X rm b A K A Y rm b 2 A K b
112 111 adantrl A 2 K 0 b 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K - K 2 - 1 2 A A X rm b A K A Y rm b 2 A K b
113 simprl A 2 K 0 b 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1
114 congsub 2 A K - K 2 - 1 2 A A X rm b A K A Y rm b 2 A K b A X rm b 1 A K A Y rm b 1 K b 1 2 A K - K 2 - 1 2 A A X rm b A K A Y rm b 2 A K b 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 2 A A X rm b A K A Y rm b - A X rm b 1 A K A Y rm b 1 - 2 A K b K b 1
115 99 101 112 113 114 syl112anc A 2 K 0 b 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K - K 2 - 1 2 A A X rm b A K A Y rm b - A X rm b 1 A K A Y rm b 1 - 2 A K b K b 1
116 13 10 zaddcld A 2 K 0 2 A K K 2 - 1 + K 2
117 116 adantr A 2 K 0 b 2 A K K 2 - 1 + K 2
118 congid 2 A K - K 2 - 1 K b 1 2 A K - K 2 - 1 K b 1 K b 1
119 52 89 118 syl2anc A 2 K 0 b 2 A K - K 2 - 1 K b 1 K b 1
120 0zd A 2 K 0 0
121 iddvds 2 A K - K 2 - 1 2 A K - K 2 - 1 2 A K - K 2 - 1
122 13 121 syl A 2 K 0 2 A K - K 2 - 1 2 A K - K 2 - 1
123 13 zcnd A 2 K 0 2 A K - K 2 - 1
124 123 subid1d A 2 K 0 2 A K K 2 - 1 - 0 = 2 A K - K 2 - 1
125 122 124 breqtrrd A 2 K 0 2 A K - K 2 - 1 2 A K K 2 - 1 - 0
126 congid 2 A K - K 2 - 1 K 2 2 A K - K 2 - 1 K 2 K 2
127 13 10 126 syl2anc A 2 K 0 2 A K - K 2 - 1 K 2 K 2
128 congadd 2 A K - K 2 - 1 2 A K - K 2 - 1 0 K 2 K 2 2 A K - K 2 - 1 2 A K K 2 - 1 - 0 2 A K - K 2 - 1 K 2 K 2 2 A K - K 2 - 1 2 A K - K 2 - 1 + K 2 - 0 + K 2
129 13 13 120 10 10 125 127 128 syl322anc A 2 K 0 2 A K - K 2 - 1 2 A K - K 2 - 1 + K 2 - 0 + K 2
130 129 adantr A 2 K 0 b 2 A K - K 2 - 1 2 A K - K 2 - 1 + K 2 - 0 + K 2
131 congmul 2 A K - K 2 - 1 K b 1 K b 1 2 A K K 2 - 1 + K 2 0 + K 2 2 A K - K 2 - 1 K b 1 K b 1 2 A K - K 2 - 1 2 A K - K 2 - 1 + K 2 - 0 + K 2 2 A K - K 2 - 1 K b 1 2 A K K 2 - 1 + K 2 K b 1 0 + K 2
132 52 89 89 117 94 119 130 131 syl322anc A 2 K 0 b 2 A K - K 2 - 1 K b 1 2 A K K 2 - 1 + K 2 K b 1 0 + K 2
133 11 zcnd A 2 K 0 2 A K K 2
134 29 sqcld A 2 K 0 K 2
135 1cnd A 2 K 0 1
136 133 134 135 addsubd A 2 K 0 2 A K K 2 + K 2 - 1 = 2 A K K 2 - 1 + K 2
137 8 zcnd A 2 K 0 2 A K
138 137 134 npcand A 2 K 0 2 A K - K 2 + K 2 = 2 A K
139 138 oveq1d A 2 K 0 2 A K K 2 + K 2 - 1 = 2 A K 1
140 136 139 eqtr3d A 2 K 0 2 A K K 2 - 1 + K 2 = 2 A K 1
141 140 adantr A 2 K 0 b 2 A K K 2 - 1 + K 2 = 2 A K 1
142 141 oveq2d A 2 K 0 b K b 1 2 A K K 2 - 1 + K 2 = K b 1 2 A K 1
143 28 ad2antlr A 2 K 0 b K
144 143 87 expcld A 2 K 0 b K b 1
145 137 adantr A 2 K 0 b 2 A K
146 1cnd A 2 K 0 b 1
147 144 145 146 subdid A 2 K 0 b K b 1 2 A K 1 = K b 1 2 A K K b 1 1
148 5 zcnd A 2 K 0 2 A
149 148 adantr A 2 K 0 b 2 A
150 144 149 143 mul12d A 2 K 0 b K b 1 2 A K = 2 A K b 1 K
151 simpr A 2 K 0 b b
152 expm1t K b K b = K b 1 K
153 143 151 152 syl2anc A 2 K 0 b K b = K b 1 K
154 153 oveq2d A 2 K 0 b 2 A K b = 2 A K b 1 K
155 150 154 eqtr4d A 2 K 0 b K b 1 2 A K = 2 A K b
156 144 mulid1d A 2 K 0 b K b 1 1 = K b 1
157 155 156 oveq12d A 2 K 0 b K b 1 2 A K K b 1 1 = 2 A K b K b 1
158 142 147 157 3eqtrrd A 2 K 0 b 2 A K b K b 1 = K b 1 2 A K K 2 - 1 + K 2
159 158 oveq1d A 2 K 0 b 2 A K b - K b 1 - K b 1 0 + K 2 = K b 1 2 A K K 2 - 1 + K 2 K b 1 0 + K 2
160 132 159 breqtrrd A 2 K 0 b 2 A K - K 2 - 1 2 A K b - K b 1 - K b 1 0 + K 2
161 160 adantr A 2 K 0 b 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K - K 2 - 1 2 A K b - K b 1 - K b 1 0 + K 2
162 congtr 2 A K - K 2 - 1 2 A A X rm b A K A Y rm b A X rm b 1 A K A Y rm b 1 2 A K b K b 1 K b 1 0 + K 2 2 A K - K 2 - 1 2 A A X rm b A K A Y rm b - A X rm b 1 A K A Y rm b 1 - 2 A K b K b 1 2 A K - K 2 - 1 2 A K b - K b 1 - K b 1 0 + K 2 2 A K - K 2 - 1 2 A A X rm b A K A Y rm b - A X rm b 1 A K A Y rm b 1 - K b 1 0 + K 2
163 79 97 115 161 162 syl112anc A 2 K 0 b 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K - K 2 - 1 2 A A X rm b A K A Y rm b - A X rm b 1 A K A Y rm b 1 - K b 1 0 + K 2
164 rmxluc A 2 b A X rm b + 1 = 2 A A X rm b A X rm b 1
165 54 56 164 syl2anc A 2 K 0 b A X rm b + 1 = 2 A A X rm b A X rm b 1
166 rmyluc A 2 b A Y rm b + 1 = 2 A Y rm b A A Y rm b 1
167 54 56 166 syl2anc A 2 K 0 b A Y rm b + 1 = 2 A Y rm b A A Y rm b 1
168 167 oveq2d A 2 K 0 b A K A Y rm b + 1 = A K 2 A Y rm b A A Y rm b 1
169 2 zcnd A 2 A
170 169 ad2antrr A 2 K 0 b A
171 170 143 subcld A 2 K 0 b A K
172 2cn 2
173 63 zcnd A 2 b A Y rm b
174 54 56 173 syl2anc A 2 K 0 b A Y rm b
175 174 170 mulcld A 2 K 0 b A Y rm b A
176 mulcl 2 A Y rm b A 2 A Y rm b A
177 172 175 176 sylancr A 2 K 0 b 2 A Y rm b A
178 73 zcnd A 2 b 1 A Y rm b 1
179 54 69 178 syl2anc A 2 K 0 b A Y rm b 1
180 171 177 179 subdid A 2 K 0 b A K 2 A Y rm b A A Y rm b 1 = A K 2 A Y rm b A A K A Y rm b 1
181 2cnd A 2 K 0 b 2
182 181 174 170 mul12d A 2 K 0 b 2 A Y rm b A = A Y rm b 2 A
183 174 149 mulcomd A 2 K 0 b A Y rm b 2 A = 2 A A Y rm b
184 182 183 eqtrd A 2 K 0 b 2 A Y rm b A = 2 A A Y rm b
185 184 oveq2d A 2 K 0 b A K 2 A Y rm b A = A K 2 A A Y rm b
186 171 149 174 mul12d A 2 K 0 b A K 2 A A Y rm b = 2 A A K A Y rm b
187 185 186 eqtrd A 2 K 0 b A K 2 A Y rm b A = 2 A A K A Y rm b
188 187 oveq1d A 2 K 0 b A K 2 A Y rm b A A K A Y rm b 1 = 2 A A K A Y rm b A K A Y rm b 1
189 168 180 188 3eqtrd A 2 K 0 b A K A Y rm b + 1 = 2 A A K A Y rm b A K A Y rm b 1
190 165 189 oveq12d A 2 K 0 b A X rm b + 1 A K A Y rm b + 1 = 2 A A X rm b - A X rm b 1 - 2 A A K A Y rm b A K A Y rm b 1
191 58 nn0cnd A 2 b A X rm b
192 54 56 191 syl2anc A 2 K 0 b A X rm b
193 149 192 mulcld A 2 K 0 b 2 A A X rm b
194 70 nn0cnd A 2 b 1 A X rm b 1
195 54 69 194 syl2anc A 2 K 0 b A X rm b 1
196 171 174 mulcld A 2 K 0 b A K A Y rm b
197 149 196 mulcld A 2 K 0 b 2 A A K A Y rm b
198 171 179 mulcld A 2 K 0 b A K A Y rm b 1
199 193 195 197 198 sub4d A 2 K 0 b 2 A A X rm b - A X rm b 1 - 2 A A K A Y rm b A K A Y rm b 1 = 2 A A X rm b - 2 A A K A Y rm b - A X rm b 1 A K A Y rm b 1
200 149 192 196 subdid A 2 K 0 b 2 A A X rm b A K A Y rm b = 2 A A X rm b 2 A A K A Y rm b
201 200 eqcomd A 2 K 0 b 2 A A X rm b 2 A A K A Y rm b = 2 A A X rm b A K A Y rm b
202 201 oveq1d A 2 K 0 b 2 A A X rm b - 2 A A K A Y rm b - A X rm b 1 A K A Y rm b 1 = 2 A A X rm b A K A Y rm b A X rm b 1 A K A Y rm b 1
203 190 199 202 3eqtrd A 2 K 0 b A X rm b + 1 A K A Y rm b + 1 = 2 A A X rm b A K A Y rm b A X rm b 1 A K A Y rm b 1
204 143 82 expp1d A 2 K 0 b K b + 1 = K b K
205 nncn b b
206 205 adantl A 2 K 0 b b
207 ax-1cn 1
208 npcan b 1 b - 1 + 1 = b
209 206 207 208 sylancl A 2 K 0 b b - 1 + 1 = b
210 209 oveq2d A 2 K 0 b K b - 1 + 1 = K b
211 143 87 expp1d A 2 K 0 b K b - 1 + 1 = K b 1 K
212 210 211 eqtr3d A 2 K 0 b K b = K b 1 K
213 212 oveq1d A 2 K 0 b K b K = K b 1 K K
214 144 143 143 mulassd A 2 K 0 b K b 1 K K = K b 1 K K
215 134 addid2d A 2 K 0 0 + K 2 = K 2
216 29 sqvald A 2 K 0 K 2 = K K
217 215 216 eqtr2d A 2 K 0 K K = 0 + K 2
218 217 adantr A 2 K 0 b K K = 0 + K 2
219 218 oveq2d A 2 K 0 b K b 1 K K = K b 1 0 + K 2
220 214 219 eqtrd A 2 K 0 b K b 1 K K = K b 1 0 + K 2
221 204 213 220 3eqtrd A 2 K 0 b K b + 1 = K b 1 0 + K 2
222 203 221 oveq12d A 2 K 0 b A X rm b + 1 - A K A Y rm b + 1 - K b + 1 = 2 A A X rm b A K A Y rm b - A X rm b 1 A K A Y rm b 1 - K b 1 0 + K 2
223 222 adantr A 2 K 0 b 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b A X rm b + 1 - A K A Y rm b + 1 - K b + 1 = 2 A A X rm b A K A Y rm b - A X rm b 1 A K A Y rm b 1 - K b 1 0 + K 2
224 163 223 breqtrrd A 2 K 0 b 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K - K 2 - 1 A X rm b + 1 - A K A Y rm b + 1 - K b + 1
225 224 ex A 2 K 0 b 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K - K 2 - 1 A X rm b + 1 - A K A Y rm b + 1 - K b + 1
226 225 expcom b A 2 K 0 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b 2 A K - K 2 - 1 A X rm b + 1 - A K A Y rm b + 1 - K b + 1
227 226 a2d b A 2 K 0 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b A 2 K 0 2 A K - K 2 - 1 A X rm b + 1 - A K A Y rm b + 1 - K b + 1
228 51 227 syl5 b A 2 K 0 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1 A 2 K 0 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b A 2 K 0 2 A K - K 2 - 1 A X rm b + 1 - A K A Y rm b + 1 - K b + 1
229 oveq2 a = 0 A X rm a = A X rm 0
230 oveq2 a = 0 A Y rm a = A Y rm 0
231 230 oveq2d a = 0 A K A Y rm a = A K A Y rm 0
232 229 231 oveq12d a = 0 A X rm a A K A Y rm a = A X rm 0 A K A Y rm 0
233 oveq2 a = 0 K a = K 0
234 232 233 oveq12d a = 0 A X rm a - A K A Y rm a - K a = A X rm 0 - A K A Y rm 0 - K 0
235 234 breq2d a = 0 2 A K - K 2 - 1 A X rm a - A K A Y rm a - K a 2 A K - K 2 - 1 A X rm 0 - A K A Y rm 0 - K 0
236 235 imbi2d a = 0 A 2 K 0 2 A K - K 2 - 1 A X rm a - A K A Y rm a - K a A 2 K 0 2 A K - K 2 - 1 A X rm 0 - A K A Y rm 0 - K 0
237 oveq2 a = 1 A X rm a = A X rm 1
238 oveq2 a = 1 A Y rm a = A Y rm 1
239 238 oveq2d a = 1 A K A Y rm a = A K A Y rm 1
240 237 239 oveq12d a = 1 A X rm a A K A Y rm a = A X rm 1 A K A Y rm 1
241 oveq2 a = 1 K a = K 1
242 240 241 oveq12d a = 1 A X rm a - A K A Y rm a - K a = A X rm 1 - A K A Y rm 1 - K 1
243 242 breq2d a = 1 2 A K - K 2 - 1 A X rm a - A K A Y rm a - K a 2 A K - K 2 - 1 A X rm 1 - A K A Y rm 1 - K 1
244 243 imbi2d a = 1 A 2 K 0 2 A K - K 2 - 1 A X rm a - A K A Y rm a - K a A 2 K 0 2 A K - K 2 - 1 A X rm 1 - A K A Y rm 1 - K 1
245 oveq2 a = b 1 A X rm a = A X rm b 1
246 oveq2 a = b 1 A Y rm a = A Y rm b 1
247 246 oveq2d a = b 1 A K A Y rm a = A K A Y rm b 1
248 245 247 oveq12d a = b 1 A X rm a A K A Y rm a = A X rm b 1 A K A Y rm b 1
249 oveq2 a = b 1 K a = K b 1
250 248 249 oveq12d a = b 1 A X rm a - A K A Y rm a - K a = A X rm b 1 - A K A Y rm b 1 - K b 1
251 250 breq2d a = b 1 2 A K - K 2 - 1 A X rm a - A K A Y rm a - K a 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1
252 251 imbi2d a = b 1 A 2 K 0 2 A K - K 2 - 1 A X rm a - A K A Y rm a - K a A 2 K 0 2 A K - K 2 - 1 A X rm b 1 - A K A Y rm b 1 - K b 1
253 oveq2 a = b A X rm a = A X rm b
254 oveq2 a = b A Y rm a = A Y rm b
255 254 oveq2d a = b A K A Y rm a = A K A Y rm b
256 253 255 oveq12d a = b A X rm a A K A Y rm a = A X rm b A K A Y rm b
257 oveq2 a = b K a = K b
258 256 257 oveq12d a = b A X rm a - A K A Y rm a - K a = A X rm b - A K A Y rm b - K b
259 258 breq2d a = b 2 A K - K 2 - 1 A X rm a - A K A Y rm a - K a 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b
260 259 imbi2d a = b A 2 K 0 2 A K - K 2 - 1 A X rm a - A K A Y rm a - K a A 2 K 0 2 A K - K 2 - 1 A X rm b - A K A Y rm b - K b
261 oveq2 a = b + 1 A X rm a = A X rm b + 1
262 oveq2 a = b + 1 A Y rm a = A Y rm b + 1
263 262 oveq2d a = b + 1 A K A Y rm a = A K A Y rm b + 1
264 261 263 oveq12d a = b + 1 A X rm a A K A Y rm a = A X rm b + 1 A K A Y rm b + 1
265 oveq2 a = b + 1 K a = K b + 1
266 264 265 oveq12d a = b + 1 A X rm a - A K A Y rm a - K a = A X rm b + 1 - A K A Y rm b + 1 - K b + 1
267 266 breq2d a = b + 1 2 A K - K 2 - 1 A X rm a - A K A Y rm a - K a 2 A K - K 2 - 1 A X rm b + 1 - A K A Y rm b + 1 - K b + 1
268 267 imbi2d a = b + 1 A 2 K 0 2 A K - K 2 - 1 A X rm a - A K A Y rm a - K a A 2 K 0 2 A K - K 2 - 1 A X rm b + 1 - A K A Y rm b + 1 - K b + 1
269 oveq2 a = N A X rm a = A X rm N
270 oveq2 a = N A Y rm a = A Y rm N
271 270 oveq2d a = N A K A Y rm a = A K A Y rm N
272 269 271 oveq12d a = N A X rm a A K A Y rm a = A X rm N A K A Y rm N
273 oveq2 a = N K a = K N
274 272 273 oveq12d a = N A X rm a - A K A Y rm a - K a = A X rm N - A K A Y rm N - K N
275 274 breq2d a = N 2 A K - K 2 - 1 A X rm a - A K A Y rm a - K a 2 A K - K 2 - 1 A X rm N - A K A Y rm N - K N
276 275 imbi2d a = N A 2 K 0 2 A K - K 2 - 1 A X rm a - A K A Y rm a - K a A 2 K 0 2 A K - K 2 - 1 A X rm N - A K A Y rm N - K N
277 34 50 228 236 244 252 260 268 276 2nn0ind N 0 A 2 K 0 2 A K - K 2 - 1 A X rm N - A K A Y rm N - K N
278 277 impcom A 2 K 0 N 0 2 A K - K 2 - 1 A X rm N - A K A Y rm N - K N
279 278 3impa A 2 K 0 N 0 2 A K - K 2 - 1 A X rm N - A K A Y rm N - K N