Theorem 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	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑁 ) − ( 𝐵 Yrm 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eluzelz	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℤ )
2		eluzelz	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℤ )
3		zsubcl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
5		0z	⊢ 0 ∈ ℤ
6		congid	⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℤ ∧ 0 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∥ ( 0 − 0 ) )
7	4 5 6	sylancl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( 0 − 0 ) )
8		rmy0	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 0 ) = 0 )
9		rmy0	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐵 Yrm 0 ) = 0 )
10	8 9	oveqan12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 Yrm 0 ) − ( 𝐵 Yrm 0 ) ) = ( 0 − 0 ) )
11	7 10	breqtrrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 0 ) − ( 𝐵 Yrm 0 ) ) )
12		1z	⊢ 1 ∈ ℤ
13		congid	⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∥ ( 1 − 1 ) )
14	4 12 13	sylancl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( 1 − 1 ) )
15		rmy1	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 1 ) = 1 )
16		rmy1	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐵 Yrm 1 ) = 1 )
17	15 16	oveqan12d	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 Yrm 1 ) − ( 𝐵 Yrm 1 ) ) = ( 1 − 1 ) )
18	14 17	breqtrrd	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 1 ) − ( 𝐵 Yrm 1 ) ) )
19		pm3.43	⊢ ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ) ∧ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) )
20	4	3ad2ant2	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
21		2z	⊢ 2 ∈ ℤ
22	21	a1i	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → 2 ∈ ℤ )
23		simp2l	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
24		nnz	⊢ ( 𝑏 ∈ ℕ → 𝑏 ∈ ℤ )
25	24	3ad2ant1	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → 𝑏 ∈ ℤ )
26		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
27	26	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm 𝑏 ) ∈ ℤ )
28	23 25 27	syl2anc	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝐴 Yrm 𝑏 ) ∈ ℤ )
29	1	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ∈ ℤ )
30	29	3ad2ant2	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → 𝐴 ∈ ℤ )
31	28 30	zmulcld	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) ∈ ℤ )
32	22 31	zmulcld	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 2 · ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) ) ∈ ℤ )
33		simp2r	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → 𝐵 ∈ ( ℤ≥ ‘ 2 ) )
34	26	fovcl	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐵 Yrm 𝑏 ) ∈ ℤ )
35	33 25 34	syl2anc	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝐵 Yrm 𝑏 ) ∈ ℤ )
36	2	adantl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐵 ∈ ℤ )
37	36	3ad2ant2	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → 𝐵 ∈ ℤ )
38	35 37	zmulcld	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( ( 𝐵 Yrm 𝑏 ) · 𝐵 ) ∈ ℤ )
39	22 38	zmulcld	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 2 · ( ( 𝐵 Yrm 𝑏 ) · 𝐵 ) ) ∈ ℤ )
40		peano2zm	⊢ ( 𝑏 ∈ ℤ → ( 𝑏 − 1 ) ∈ ℤ )
41	24 40	syl	⊢ ( 𝑏 ∈ ℕ → ( 𝑏 − 1 ) ∈ ℤ )
42	41	3ad2ant1	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝑏 − 1 ) ∈ ℤ )
43	26	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑏 − 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( 𝑏 − 1 ) ) ∈ ℤ )
44	23 42 43	syl2anc	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝐴 Yrm ( 𝑏 − 1 ) ) ∈ ℤ )
45	26	fovcl	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑏 − 1 ) ∈ ℤ ) → ( 𝐵 Yrm ( 𝑏 − 1 ) ) ∈ ℤ )
46	33 42 45	syl2anc	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝐵 Yrm ( 𝑏 − 1 ) ) ∈ ℤ )
47		congid	⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℤ ∧ 2 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∥ ( 2 − 2 ) )
48	20 21 47	sylancl	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝐴 − 𝐵 ) ∥ ( 2 − 2 ) )
49		simp3r	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) )
50		iddvds	⊢ ( ( 𝐴 − 𝐵 ) ∈ ℤ → ( 𝐴 − 𝐵 ) ∥ ( 𝐴 − 𝐵 ) )
51	20 50	syl	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝐴 − 𝐵 ) ∥ ( 𝐴 − 𝐵 ) )
52		congmul	⊢ ( ( ( ( 𝐴 − 𝐵 ) ∈ ℤ ∧ ( 𝐴 Yrm 𝑏 ) ∈ ℤ ∧ ( 𝐵 Yrm 𝑏 ) ∈ ℤ ) ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( 𝐴 − 𝐵 ) ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) − ( ( 𝐵 Yrm 𝑏 ) · 𝐵 ) ) )
53	20 28 35 30 37 49 51 52	syl322anc	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) − ( ( 𝐵 Yrm 𝑏 ) · 𝐵 ) ) )
54		congmul	⊢ ( ( ( ( 𝐴 − 𝐵 ) ∈ ℤ ∧ 2 ∈ ℤ ∧ 2 ∈ ℤ ) ∧ ( ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) ∈ ℤ ∧ ( ( 𝐵 Yrm 𝑏 ) · 𝐵 ) ∈ ℤ ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( 2 − 2 ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) − ( ( 𝐵 Yrm 𝑏 ) · 𝐵 ) ) ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 2 · ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) ) − ( 2 · ( ( 𝐵 Yrm 𝑏 ) · 𝐵 ) ) ) )
55	20 22 22 31 38 48 53 54	syl322anc	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 2 · ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) ) − ( 2 · ( ( 𝐵 Yrm 𝑏 ) · 𝐵 ) ) ) )
56		simp3l	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) )
57		congsub	⊢ ( ( ( ( 𝐴 − 𝐵 ) ∈ ℤ ∧ ( 2 · ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) ) ∈ ℤ ∧ ( 2 · ( ( 𝐵 Yrm 𝑏 ) · 𝐵 ) ) ∈ ℤ ) ∧ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) ∈ ℤ ∧ ( 𝐵 Yrm ( 𝑏 − 1 ) ) ∈ ℤ ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 2 · ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) ) − ( 2 · ( ( 𝐵 Yrm 𝑏 ) · 𝐵 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( ( 2 · ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) ) − ( 𝐴 Yrm ( 𝑏 − 1 ) ) ) − ( ( 2 · ( ( 𝐵 Yrm 𝑏 ) · 𝐵 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ) )
58	20 32 39 44 46 55 56 57	syl322anc	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( ( 2 · ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) ) − ( 𝐴 Yrm ( 𝑏 − 1 ) ) ) − ( ( 2 · ( ( 𝐵 Yrm 𝑏 ) · 𝐵 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ) )
59		rmyluc	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) = ( ( 2 · ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) ) − ( 𝐴 Yrm ( 𝑏 − 1 ) ) ) )
60	23 25 59	syl2anc	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝐴 Yrm ( 𝑏 + 1 ) ) = ( ( 2 · ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) ) − ( 𝐴 Yrm ( 𝑏 − 1 ) ) ) )
61		rmyluc	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 𝐵 Yrm ( 𝑏 + 1 ) ) = ( ( 2 · ( ( 𝐵 Yrm 𝑏 ) · 𝐵 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) )
62	33 25 61	syl2anc	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝐵 Yrm ( 𝑏 + 1 ) ) = ( ( 2 · ( ( 𝐵 Yrm 𝑏 ) · 𝐵 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) )
63	60 62	oveq12d	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) − ( 𝐵 Yrm ( 𝑏 + 1 ) ) ) = ( ( ( 2 · ( ( 𝐴 Yrm 𝑏 ) · 𝐴 ) ) − ( 𝐴 Yrm ( 𝑏 − 1 ) ) ) − ( ( 2 · ( ( 𝐵 Yrm 𝑏 ) · 𝐵 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ) )
64	58 63	breqtrrd	⊢ ( ( 𝑏 ∈ ℕ ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) − ( 𝐵 Yrm ( 𝑏 + 1 ) ) ) )
65	64	3exp	⊢ ( 𝑏 ∈ ℕ → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) − ( 𝐵 Yrm ( 𝑏 + 1 ) ) ) ) ) )
66	65	a2d	⊢ ( 𝑏 ∈ ℕ → ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ∧ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) − ( 𝐵 Yrm ( 𝑏 + 1 ) ) ) ) ) )
67	19 66	syl5	⊢ ( 𝑏 ∈ ℕ → ( ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ) ∧ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) − ( 𝐵 Yrm ( 𝑏 + 1 ) ) ) ) ) )
68		oveq2	⊢ ( 𝑎 = 0 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 0 ) )
69		oveq2	⊢ ( 𝑎 = 0 → ( 𝐵 Yrm 𝑎 ) = ( 𝐵 Yrm 0 ) )
70	68 69	oveq12d	⊢ ( 𝑎 = 0 → ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) = ( ( 𝐴 Yrm 0 ) − ( 𝐵 Yrm 0 ) ) )
71	70	breq2d	⊢ ( 𝑎 = 0 → ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) ↔ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 0 ) − ( 𝐵 Yrm 0 ) ) ) )
72	71	imbi2d	⊢ ( 𝑎 = 0 → ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 0 ) − ( 𝐵 Yrm 0 ) ) ) ) )
73		oveq2	⊢ ( 𝑎 = 1 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 1 ) )
74		oveq2	⊢ ( 𝑎 = 1 → ( 𝐵 Yrm 𝑎 ) = ( 𝐵 Yrm 1 ) )
75	73 74	oveq12d	⊢ ( 𝑎 = 1 → ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) = ( ( 𝐴 Yrm 1 ) − ( 𝐵 Yrm 1 ) ) )
76	75	breq2d	⊢ ( 𝑎 = 1 → ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) ↔ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 1 ) − ( 𝐵 Yrm 1 ) ) ) )
77	76	imbi2d	⊢ ( 𝑎 = 1 → ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 1 ) − ( 𝐵 Yrm 1 ) ) ) ) )
78		oveq2	⊢ ( 𝑎 = ( 𝑏 − 1 ) → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm ( 𝑏 − 1 ) ) )
79		oveq2	⊢ ( 𝑎 = ( 𝑏 − 1 ) → ( 𝐵 Yrm 𝑎 ) = ( 𝐵 Yrm ( 𝑏 − 1 ) ) )
80	78 79	oveq12d	⊢ ( 𝑎 = ( 𝑏 − 1 ) → ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) = ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) )
81	80	breq2d	⊢ ( 𝑎 = ( 𝑏 − 1 ) → ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) ↔ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ) )
82	81	imbi2d	⊢ ( 𝑎 = ( 𝑏 − 1 ) → ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 − 1 ) ) − ( 𝐵 Yrm ( 𝑏 − 1 ) ) ) ) ) )
83		oveq2	⊢ ( 𝑎 = 𝑏 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑏 ) )
84		oveq2	⊢ ( 𝑎 = 𝑏 → ( 𝐵 Yrm 𝑎 ) = ( 𝐵 Yrm 𝑏 ) )
85	83 84	oveq12d	⊢ ( 𝑎 = 𝑏 → ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) = ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) )
86	85	breq2d	⊢ ( 𝑎 = 𝑏 → ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) ↔ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) )
87	86	imbi2d	⊢ ( 𝑎 = 𝑏 → ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑏 ) − ( 𝐵 Yrm 𝑏 ) ) ) ) )
88		oveq2	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm ( 𝑏 + 1 ) ) )
89		oveq2	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐵 Yrm 𝑎 ) = ( 𝐵 Yrm ( 𝑏 + 1 ) ) )
90	88 89	oveq12d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) = ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) − ( 𝐵 Yrm ( 𝑏 + 1 ) ) ) )
91	90	breq2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) ↔ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) − ( 𝐵 Yrm ( 𝑏 + 1 ) ) ) ) )
92	91	imbi2d	⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm ( 𝑏 + 1 ) ) − ( 𝐵 Yrm ( 𝑏 + 1 ) ) ) ) ) )
93		oveq2	⊢ ( 𝑎 = 𝑁 → ( 𝐴 Yrm 𝑎 ) = ( 𝐴 Yrm 𝑁 ) )
94		oveq2	⊢ ( 𝑎 = 𝑁 → ( 𝐵 Yrm 𝑎 ) = ( 𝐵 Yrm 𝑁 ) )
95	93 94	oveq12d	⊢ ( 𝑎 = 𝑁 → ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) = ( ( 𝐴 Yrm 𝑁 ) − ( 𝐵 Yrm 𝑁 ) ) )
96	95	breq2d	⊢ ( 𝑎 = 𝑁 → ( ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) ↔ ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑁 ) − ( 𝐵 Yrm 𝑁 ) ) ) )
97	96	imbi2d	⊢ ( 𝑎 = 𝑁 → ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑎 ) − ( 𝐵 Yrm 𝑎 ) ) ) ↔ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑁 ) − ( 𝐵 Yrm 𝑁 ) ) ) ) )
98	11 18 67 72 77 82 87 92 97	2nn0ind	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑁 ) − ( 𝐵 Yrm 𝑁 ) ) ) )
99	98	impcom	⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑁 ) − ( 𝐵 Yrm 𝑁 ) ) )
100	99	3impa	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 − 𝐵 ) ∥ ( ( 𝐴 Yrm 𝑁 ) − ( 𝐵 Yrm 𝑁 ) ) )