jm2.19lem3

		Ref	Expression
	Assertion	jm2.19lem3	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ) \land I \in ℕ_{0}) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + I \cdot M)))$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ a = 0 \to a \cdot M = 0 \cdot M$
2	1	oveq2d	$⊢ a = 0 \to N + a \cdot M = N + 0 \cdot M$
3	2	oveq2d	$⊢ a = 0 \to A Y_{rm} (N + a \cdot M) = A Y_{rm} (N + 0 \cdot M)$
4	3	breq2d	$⊢ a = 0 \to ((A Y_{rm} M) ∥ (A Y_{rm} (N + a \cdot M)) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + 0 \cdot M)))$
5	4	bibi2d	$⊢ a = 0 \to (((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + a \cdot M))) \leftrightarrow ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + 0 \cdot M))))$
6	5	imbi2d	$⊢ a = 0 \to (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + a \cdot M)))) \leftrightarrow ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + 0 \cdot M)))))$
7		oveq1	$⊢ a = b \to a \cdot M = b \cdot M$
8	7	oveq2d	$⊢ a = b \to N + a \cdot M = N + b \cdot M$
9	8	oveq2d	$⊢ a = b \to A Y_{rm} (N + a \cdot M) = A Y_{rm} (N + b \cdot M)$
10	9	breq2d	$⊢ a = b \to ((A Y_{rm} M) ∥ (A Y_{rm} (N + a \cdot M)) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M)))$
11	10	bibi2d	$⊢ a = b \to (((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + a \cdot M))) \leftrightarrow ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M))))$
12	11	imbi2d	$⊢ a = b \to (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + a \cdot M)))) \leftrightarrow ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M)))))$
13		oveq1	$⊢ a = b + 1 \to a \cdot M = (b + 1) \cdot M$
14	13	oveq2d	$⊢ a = b + 1 \to N + a \cdot M = N + (b + 1) \cdot M$
15	14	oveq2d	$⊢ a = b + 1 \to A Y_{rm} (N + a \cdot M) = A Y_{rm} (N + (b + 1) \cdot M)$
16	15	breq2d	$⊢ a = b + 1 \to ((A Y_{rm} M) ∥ (A Y_{rm} (N + a \cdot M)) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + (b + 1) \cdot M)))$
17	16	bibi2d	$⊢ a = b + 1 \to (((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + a \cdot M))) \leftrightarrow ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + (b + 1) \cdot M))))$
18	17	imbi2d	$⊢ a = b + 1 \to (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + a \cdot M)))) \leftrightarrow ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + (b + 1) \cdot M)))))$
19		oveq1	$⊢ a = I \to a \cdot M = I \cdot M$
20	19	oveq2d	$⊢ a = I \to N + a \cdot M = N + I \cdot M$
21	20	oveq2d	$⊢ a = I \to A Y_{rm} (N + a \cdot M) = A Y_{rm} (N + I \cdot M)$
22	21	breq2d	$⊢ a = I \to ((A Y_{rm} M) ∥ (A Y_{rm} (N + a \cdot M)) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + I \cdot M)))$
23	22	bibi2d	$⊢ a = I \to (((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + a \cdot M))) \leftrightarrow ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + I \cdot M))))$
24	23	imbi2d	$⊢ a = I \to (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + a \cdot M)))) \leftrightarrow ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + I \cdot M)))))$
25		zcn	$⊢ M \in ℤ \to M \in ℂ$
26	25	ad2antrl	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to M \in ℂ$
27	26	mul02d	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to 0 \cdot M = 0$
28	27	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to N + 0 \cdot M = N + 0$
29		zcn	$⊢ N \in ℤ \to N \in ℂ$
30	29	ad2antll	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to N \in ℂ$
31	30	addridd	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to N + 0 = N$
32	28 31	eqtr2d	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to N = N + 0 \cdot M$
33	32	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to A Y_{rm} N = A Y_{rm} (N + 0 \cdot M)$
34	33	breq2d	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + 0 \cdot M)))$
35		simp3	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M)))) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M)))$
36		simprl	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A \in ℤ_{\geq 2}$
37		simprrl	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to M \in ℤ$
38		simprrr	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to N \in ℤ$
39		nn0z	$⊢ b \in ℕ_{0} \to b \in ℤ$
40	39	adantr	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to b \in ℤ$
41	40 37	zmulcld	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to b \cdot M \in ℤ$
42	38 41	zaddcld	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to N + b \cdot M \in ℤ$
43		jm2.19lem2	$⊢ (A \in ℤ_{\geq 2} \land M \in ℤ \land N + b \cdot M \in ℤ) \to ((A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M)) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M + M)))$
44	36 37 42 43	syl3anc	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to ((A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M)) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M + M)))$
45	38	zcnd	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to N \in ℂ$
46	41	zcnd	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to b \cdot M \in ℂ$
47	37	zcnd	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to M \in ℂ$
48	45 46 47	addassd	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to N + b \cdot M + M = N + b \cdot M + M$
49		nn0cn	$⊢ b \in ℕ_{0} \to b \in ℂ$
50	49	adantr	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to b \in ℂ$
51		1cnd	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 1 \in ℂ$
52	50 51 47	adddird	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to (b + 1) \cdot M = b \cdot M + 1 \cdot M$
53	47	mullidd	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to 1 \cdot M = M$
54	53	oveq2d	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to b \cdot M + 1 \cdot M = b \cdot M + M$
55	52 54	eqtr2d	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to b \cdot M + M = (b + 1) \cdot M$
56	55	oveq2d	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to N + b \cdot M + M = N + (b + 1) \cdot M$
57	48 56	eqtrd	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to N + b \cdot M + M = N + (b + 1) \cdot M$
58	57	oveq2d	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to A Y_{rm} (N + b \cdot M + M) = A Y_{rm} (N + (b + 1) \cdot M)$
59	58	breq2d	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to ((A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M + M)) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + (b + 1) \cdot M)))$
60	44 59	bitrd	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ))) \to ((A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M)) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + (b + 1) \cdot M)))$
61	60	3adant3	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M)))) \to ((A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M)) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + (b + 1) \cdot M)))$
62	35 61	bitrd	$⊢ (b \in ℕ_{0} \land (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M)))) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + (b + 1) \cdot M)))$
63	62	3exp	$⊢ b \in ℕ_{0} \to ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to (((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M))) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + (b + 1) \cdot M)))))$
64	63	a2d	$⊢ b \in ℕ_{0} \to (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + b \cdot M)))) \to ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + (b + 1) \cdot M)))))$
65	6 12 18 24 34 64	nn0ind	$⊢ I \in ℕ_{0} \to ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + I \cdot M))))$
66	65	com12	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to (I \in ℕ_{0} \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + I \cdot M))))$
67	66	3impia	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ) \land I \in ℕ_{0}) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + I \cdot M)))$

Metamath Proof Explorer

Theorem jm2.19lem3

Proof