jm2.15nn0

Description: Lemma 2.15 of JonesMatijasevic p. 695. rmY is a polynomial for fixed N, so has the expected congruence property. (Contributed by Stefan O'Rear, 1-Oct-2014)

		Ref	Expression
	Assertion	jm2.15nn0	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to (A - B) ∥ ((A Y_{rm} N) - (B Y_{rm} N))$

Proof

Step	Hyp	Ref	Expression
1		eluzelz	$⊢ A \in ℤ_{\geq 2} \to A \in ℤ$
2		eluzelz	$⊢ B \in ℤ_{\geq 2} \to B \in ℤ$
3		zsubcl	$⊢ (A \in ℤ \land B \in ℤ) \to A - B \in ℤ$
4	1 2 3	syl2an	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to A - B \in ℤ$
5		0z	$⊢ 0 \in ℤ$
6		congid	$⊢ (A - B \in ℤ \land 0 \in ℤ) \to (A - B) ∥ (0 - 0)$
7	4 5 6	sylancl	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ (0 - 0)$
8		rmy0	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} 0 = 0$
9		rmy0	$⊢ B \in ℤ_{\geq 2} \to B Y_{rm} 0 = 0$
10	8 9	oveqan12d	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A Y_{rm} 0) - (B Y_{rm} 0) = 0 - 0$
11	7 10	breqtrrd	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} 0) - (B Y_{rm} 0))$
12		1z	$⊢ 1 \in ℤ$
13		congid	$⊢ (A - B \in ℤ \land 1 \in ℤ) \to (A - B) ∥ (1 - 1)$
14	4 12 13	sylancl	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ (1 - 1)$
15		rmy1	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} 1 = 1$
16		rmy1	$⊢ B \in ℤ_{\geq 2} \to B Y_{rm} 1 = 1$
17	15 16	oveqan12d	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A Y_{rm} 1) - (B Y_{rm} 1) = 1 - 1$
18	14 17	breqtrrd	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} 1) - (B Y_{rm} 1))$
19		pm3.43	$⊢ (((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1)))) \land ((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to ((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b))))$
20	4	3ad2ant2	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to A - B \in ℤ$
21		2z	$⊢ 2 \in ℤ$
22	21	a1i	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to 2 \in ℤ$
23		simp2l	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to A \in ℤ_{\geq 2}$
24		nnz	$⊢ b \in ℕ \to b \in ℤ$
25	24	3ad2ant1	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to b \in ℤ$
26		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
27	26	fovcl	$⊢ (A \in ℤ_{\geq 2} \land b \in ℤ) \to A Y_{rm} b \in ℤ$
28	23 25 27	syl2anc	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to A Y_{rm} b \in ℤ$
29	1	adantr	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to A \in ℤ$
30	29	3ad2ant2	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to A \in ℤ$
31	28 30	zmulcld	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to (A Y_{rm} b) A \in ℤ$
32	22 31	zmulcld	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to 2 (A Y_{rm} b) A \in ℤ$
33		simp2r	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to B \in ℤ_{\geq 2}$
34	26	fovcl	$⊢ (B \in ℤ_{\geq 2} \land b \in ℤ) \to B Y_{rm} b \in ℤ$
35	33 25 34	syl2anc	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to B Y_{rm} b \in ℤ$
36	2	adantl	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to B \in ℤ$
37	36	3ad2ant2	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to B \in ℤ$
38	35 37	zmulcld	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to (B Y_{rm} b) B \in ℤ$
39	22 38	zmulcld	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to 2 (B Y_{rm} b) B \in ℤ$
40		peano2zm	$⊢ b \in ℤ \to b - 1 \in ℤ$
41	24 40	syl	$⊢ b \in ℕ \to b - 1 \in ℤ$
42	41	3ad2ant1	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to b - 1 \in ℤ$
43	26	fovcl	$⊢ (A \in ℤ_{\geq 2} \land b - 1 \in ℤ) \to A Y_{rm} (b - 1) \in ℤ$
44	23 42 43	syl2anc	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to A Y_{rm} (b - 1) \in ℤ$
45	26	fovcl	$⊢ (B \in ℤ_{\geq 2} \land b - 1 \in ℤ) \to B Y_{rm} (b - 1) \in ℤ$
46	33 42 45	syl2anc	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to B Y_{rm} (b - 1) \in ℤ$
47		congid	$⊢ (A - B \in ℤ \land 2 \in ℤ) \to (A - B) ∥ (2 - 2)$
48	20 21 47	sylancl	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to (A - B) ∥ (2 - 2)$
49		simp3r	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b))$
50		iddvds	$⊢ A - B \in ℤ \to (A - B) ∥ (A - B)$
51	20 50	syl	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to (A - B) ∥ (A - B)$
52		congmul	$⊢ ((A - B \in ℤ \land A Y_{rm} b \in ℤ \land B Y_{rm} b \in ℤ) \land (A \in ℤ \land B \in ℤ) \land ((A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)) \land (A - B) ∥ (A - B))) \to (A - B) ∥ ((A Y_{rm} b) A - (B Y_{rm} b) B)$
53	20 28 35 30 37 49 51 52	syl322anc	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to (A - B) ∥ ((A Y_{rm} b) A - (B Y_{rm} b) B)$
54		congmul	$⊢ ((A - B \in ℤ \land 2 \in ℤ \land 2 \in ℤ) \land ((A Y_{rm} b) A \in ℤ \land (B Y_{rm} b) B \in ℤ) \land ((A - B) ∥ (2 - 2) \land (A - B) ∥ ((A Y_{rm} b) A - (B Y_{rm} b) B))) \to (A - B) ∥ (2 (A Y_{rm} b) A - 2 (B Y_{rm} b) B)$
55	20 22 22 31 38 48 53 54	syl322anc	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to (A - B) ∥ (2 (A Y_{rm} b) A - 2 (B Y_{rm} b) B)$
56		simp3l	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to (A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1)))$
57		congsub	$⊢ ((A - B \in ℤ \land 2 (A Y_{rm} b) A \in ℤ \land 2 (B Y_{rm} b) B \in ℤ) \land (A Y_{rm} (b - 1) \in ℤ \land B Y_{rm} (b - 1) \in ℤ) \land ((A - B) ∥ (2 (A Y_{rm} b) A - 2 (B Y_{rm} b) B) \land (A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))))) \to (A - B) ∥ (2 (A Y_{rm} b) A - (A Y_{rm} (b - 1)) - (2 (B Y_{rm} b) B - (B Y_{rm} (b - 1))))$
58	20 32 39 44 46 55 56 57	syl322anc	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to (A - B) ∥ (2 (A Y_{rm} b) A - (A Y_{rm} (b - 1)) - (2 (B Y_{rm} b) B - (B Y_{rm} (b - 1))))$
59		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))$
60	23 25 59	syl2anc	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to A Y_{rm} (b + 1) = 2 (A Y_{rm} b) A - (A Y_{rm} (b - 1))$
61		rmyluc	$⊢ (B \in ℤ_{\geq 2} \land b \in ℤ) \to B Y_{rm} (b + 1) = 2 (B Y_{rm} b) B - (B Y_{rm} (b - 1))$
62	33 25 61	syl2anc	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to B Y_{rm} (b + 1) = 2 (B Y_{rm} b) B - (B Y_{rm} (b - 1))$
63	60 62	oveq12d	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to (A Y_{rm} (b + 1)) - (B Y_{rm} (b + 1)) = 2 (A Y_{rm} b) A - (A Y_{rm} (b - 1)) - (2 (B Y_{rm} b) B - (B Y_{rm} (b - 1)))$
64	58 63	breqtrrd	$⊢ (b \in ℕ \land (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to (A - B) ∥ ((A Y_{rm} (b + 1)) - (B Y_{rm} (b + 1)))$
65	64	3exp	$⊢ b \in ℕ \to ((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b))) \to (A - B) ∥ ((A Y_{rm} (b + 1)) - (B Y_{rm} (b + 1)))))$
66	65	a2d	$⊢ b \in ℕ \to (((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to ((A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))) \land (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to ((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} (b + 1)) - (B Y_{rm} (b + 1)))))$
67	19 66	syl5	$⊢ b \in ℕ \to ((((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1)))) \land ((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))) \to ((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} (b + 1)) - (B Y_{rm} (b + 1)))))$
68		oveq2	$⊢ a = 0 \to A Y_{rm} a = A Y_{rm} 0$
69		oveq2	$⊢ a = 0 \to B Y_{rm} a = B Y_{rm} 0$
70	68 69	oveq12d	$⊢ a = 0 \to (A Y_{rm} a) - (B Y_{rm} a) = (A Y_{rm} 0) - (B Y_{rm} 0)$
71	70	breq2d	$⊢ a = 0 \to ((A - B) ∥ ((A Y_{rm} a) - (B Y_{rm} a)) \leftrightarrow (A - B) ∥ ((A Y_{rm} 0) - (B Y_{rm} 0)))$
72	71	imbi2d	$⊢ a = 0 \to (((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} a) - (B Y_{rm} a))) \leftrightarrow ((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} 0) - (B Y_{rm} 0))))$
73		oveq2	$⊢ a = 1 \to A Y_{rm} a = A Y_{rm} 1$
74		oveq2	$⊢ a = 1 \to B Y_{rm} a = B Y_{rm} 1$
75	73 74	oveq12d	$⊢ a = 1 \to (A Y_{rm} a) - (B Y_{rm} a) = (A Y_{rm} 1) - (B Y_{rm} 1)$
76	75	breq2d	$⊢ a = 1 \to ((A - B) ∥ ((A Y_{rm} a) - (B Y_{rm} a)) \leftrightarrow (A - B) ∥ ((A Y_{rm} 1) - (B Y_{rm} 1)))$
77	76	imbi2d	$⊢ a = 1 \to (((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} a) - (B Y_{rm} a))) \leftrightarrow ((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} 1) - (B Y_{rm} 1))))$
78		oveq2	$⊢ a = b - 1 \to A Y_{rm} a = A Y_{rm} (b - 1)$
79		oveq2	$⊢ a = b - 1 \to B Y_{rm} a = B Y_{rm} (b - 1)$
80	78 79	oveq12d	$⊢ a = b - 1 \to (A Y_{rm} a) - (B Y_{rm} a) = (A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))$
81	80	breq2d	$⊢ a = b - 1 \to ((A - B) ∥ ((A Y_{rm} a) - (B Y_{rm} a)) \leftrightarrow (A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1))))$
82	81	imbi2d	$⊢ a = b - 1 \to (((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} a) - (B Y_{rm} a))) \leftrightarrow ((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} (b - 1)) - (B Y_{rm} (b - 1)))))$
83		oveq2	$⊢ a = b \to A Y_{rm} a = A Y_{rm} b$
84		oveq2	$⊢ a = b \to B Y_{rm} a = B Y_{rm} b$
85	83 84	oveq12d	$⊢ a = b \to (A Y_{rm} a) - (B Y_{rm} a) = (A Y_{rm} b) - (B Y_{rm} b)$
86	85	breq2d	$⊢ a = b \to ((A - B) ∥ ((A Y_{rm} a) - (B Y_{rm} a)) \leftrightarrow (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b)))$
87	86	imbi2d	$⊢ a = b \to (((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} a) - (B Y_{rm} a))) \leftrightarrow ((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} b) - (B Y_{rm} b))))$
88		oveq2	$⊢ a = b + 1 \to A Y_{rm} a = A Y_{rm} (b + 1)$
89		oveq2	$⊢ a = b + 1 \to B Y_{rm} a = B Y_{rm} (b + 1)$
90	88 89	oveq12d	$⊢ a = b + 1 \to (A Y_{rm} a) - (B Y_{rm} a) = (A Y_{rm} (b + 1)) - (B Y_{rm} (b + 1))$
91	90	breq2d	$⊢ a = b + 1 \to ((A - B) ∥ ((A Y_{rm} a) - (B Y_{rm} a)) \leftrightarrow (A - B) ∥ ((A Y_{rm} (b + 1)) - (B Y_{rm} (b + 1))))$
92	91	imbi2d	$⊢ a = b + 1 \to (((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} a) - (B Y_{rm} a))) \leftrightarrow ((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} (b + 1)) - (B Y_{rm} (b + 1)))))$
93		oveq2	$⊢ a = N \to A Y_{rm} a = A Y_{rm} N$
94		oveq2	$⊢ a = N \to B Y_{rm} a = B Y_{rm} N$
95	93 94	oveq12d	$⊢ a = N \to (A Y_{rm} a) - (B Y_{rm} a) = (A Y_{rm} N) - (B Y_{rm} N)$
96	95	breq2d	$⊢ a = N \to ((A - B) ∥ ((A Y_{rm} a) - (B Y_{rm} a)) \leftrightarrow (A - B) ∥ ((A Y_{rm} N) - (B Y_{rm} N)))$
97	96	imbi2d	$⊢ a = N \to (((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} a) - (B Y_{rm} a))) \leftrightarrow ((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} N) - (B Y_{rm} N))))$
98	11 18 67 72 77 82 87 92 97	2nn0ind	$⊢ N \in ℕ_{0} \to ((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \to (A - B) ∥ ((A Y_{rm} N) - (B Y_{rm} N)))$
99	98	impcom	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2}) \land N \in ℕ_{0}) \to (A - B) ∥ ((A Y_{rm} N) - (B Y_{rm} N))$
100	99	3impa	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to (A - B) ∥ ((A Y_{rm} N) - (B Y_{rm} N))$

Metamath Proof Explorer

Theorem jm2.15nn0

Proof