jm2.18

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

		Ref	Expression
	Assertion	jm2.18	$⊢ (A \in ℤ_{\geq 2} \land K \in ℕ_{0} \land N \in ℕ_{0}) \to (2 A K - K^{2} - 1) ∥ ((A X_{rm} N) - (A - K) (A Y_{rm} N) - K^{N})$

Proof

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

Metamath Proof Explorer

Theorem jm2.18

Proof