jm2.19lem4

Description: Lemma for jm2.19 . Extend to ZZ by symmetry. TODO: use zindbi . (Contributed by Stefan O'Rear, 26-Sep-2014)

		Ref	Expression
	Assertion	jm2.19lem4	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ) \land I \in ℤ) \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		elznn0	$⊢ I \in ℤ \leftrightarrow (I \in ℝ \land (I \in ℕ_{0} \lor - I \in ℕ_{0}))$
2		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)))$
3	2	3expia	$⊢ (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))))$
4	3	adantr	$⊢ ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \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))))$
5		simplll	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to A \in ℤ_{\geq 2}$
6		simprl	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to M \in ℤ$
7	6	ad2antrr	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to M \in ℤ$
8		simprr	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to N \in ℤ$
9	8	ad2antrr	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to N \in ℤ$
10		nn0z	$⊢ - I \in ℕ_{0} \to - I \in ℤ$
11	10	adantl	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to - I \in ℤ$
12		simplr	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to I \in ℝ$
13	12	recnd	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to I \in ℂ$
14		znegclb	$⊢ I \in ℂ \to (I \in ℤ \leftrightarrow - I \in ℤ)$
15	13 14	syl	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to (I \in ℤ \leftrightarrow - I \in ℤ)$
16	11 15	mpbird	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to I \in ℤ$
17	16 7	zmulcld	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to I \cdot M \in ℤ$
18	9 17	zaddcld	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to N + I \cdot M \in ℤ$
19		simpr	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to - I \in ℕ_{0}$
20		jm2.19lem3	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N + I \cdot M \in ℤ) \land - I \in ℕ_{0}) \to ((A Y_{rm} M) ∥ (A Y_{rm} (N + I \cdot M)) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + I \cdot M + -I \cdot M)))$
21	5 7 18 19 20	syl121anc	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to ((A Y_{rm} M) ∥ (A Y_{rm} (N + I \cdot M)) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + I \cdot M + -I \cdot M)))$
22		zcn	$⊢ M \in ℤ \to M \in ℂ$
23	22	ad2antrl	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to M \in ℂ$
24	23	ad2antrr	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to M \in ℂ$
25	13 24	mulneg1d	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to -I \cdot M = - I \cdot M$
26	25	oveq2d	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to N + I \cdot M + -I \cdot M = N + I \cdot M + (- I \cdot M)$
27		zcn	$⊢ N \in ℤ \to N \in ℂ$
28	27	ad2antll	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to N \in ℂ$
29	28	ad2antrr	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to N \in ℂ$
30	13 24	mulcld	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to I \cdot M \in ℂ$
31	29 30	addcld	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to N + I \cdot M \in ℂ$
32	31 30	negsubd	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to N + I \cdot M + (- I \cdot M) = N + I \cdot M - I \cdot M$
33	29 30	pncand	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to N + I \cdot M - I \cdot M = N$
34	26 32 33	3eqtrd	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to N + I \cdot M + -I \cdot M = N$
35	34	oveq2d	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to A Y_{rm} (N + I \cdot M + -I \cdot M) = A Y_{rm} N$
36	35	breq2d	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \land - I \in ℕ_{0}) \to ((A Y_{rm} M) ∥ (A Y_{rm} (N + I \cdot M + -I \cdot M)) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} N))$
37	21 36	bitr2d	$⊢ (((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \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)))$
38	37	ex	$⊢ ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \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))))$
39	4 38	jaod	$⊢ ((A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \land I \in ℝ) \to ((I \in ℕ_{0} \lor - I \in ℕ_{0}) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + I \cdot M))))$
40	39	expimpd	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to ((I \in ℝ \land (I \in ℕ_{0} \lor - I \in ℕ_{0})) \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + I \cdot M))))$
41	1 40	syl5bi	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ)) \to (I \in ℤ \to ((A Y_{rm} M) ∥ (A Y_{rm} N) \leftrightarrow (A Y_{rm} M) ∥ (A Y_{rm} (N + I \cdot M))))$
42	41	3impia	$⊢ (A \in ℤ_{\geq 2} \land (M \in ℤ \land N \in ℤ) \land I \in ℤ) \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.19lem4

Proof