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	|- ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A - B ) || ( ( A rmY N ) - ( B rmY N ) ) )

Proof

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