# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {I}\in ℤ\right)\to \left(\left({A}{Y}_{\mathrm{rm}}{M}\right)\parallel \left({A}{Y}_{\mathrm{rm}}{N}\right)↔\left({A}{Y}_{\mathrm{rm}}{M}\right)\parallel \left({A}{Y}_{\mathrm{rm}}\left({N}+{I}\cdot {M}\right)\right)\right)$

### Proof

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