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 \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to (A - 1) ∥ ((A Y_{rm} N) - N)$

Proof

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

Metamath Proof Explorer

Theorem jm2.16nn0

Proof