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 ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( ( 2 · 𝐴 ) · 𝐾 ) − ( 𝐾 ↑ 2 ) ) − 1 ) ∥ ( ( ( 𝐴 Xrm 𝑁 ) − ( ( 𝐴 − 𝐾 ) · ( 𝐴 Yrm 𝑁 ) ) ) − ( 𝐾 ↑ 𝑁 ) ) )

Proof

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