Theorem jm2.16nn0

Description: Lemma 2.16 of JonesMatijasevic p. 695. This may be regarded as a special case of jm2.15nn0 if rmY is redefined as described in rmyluc . (Contributed by Stefan O'Rear, 1-Oct-2014)

	Ref	Expression
Assertion	jm2.16nn0	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 − 1 ) ∥ ( ( 𝐴 Yrm 𝑁 ) − 𝑁 ) )

Proof

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