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

Proof

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