# 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 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {K}\in {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left(2{A}{K}-{{K}}^{2}-1\right)\parallel \left(\left({A}{X}_{\mathrm{rm}}{N}\right)-\left({A}-{K}\right)\left({A}{Y}_{\mathrm{rm}}{N}\right)-{{K}}^{{N}}\right)$

### Proof

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