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 
|- ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) /\ I e. ZZ ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elznn0 
 |-  ( I e. ZZ <-> ( I e. RR /\ ( I e. NN0 \/ -u I e. NN0 ) ) )
2 jm2.19lem3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) /\ I e. NN0 ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) )
3 2 3expia 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( I e. NN0 -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) ) )
4 3 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) -> ( I e. NN0 -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) ) )
5 simplll 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> A e. ( ZZ>= ` 2 ) )
6 simprl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> M e. ZZ )
7 6 ad2antrr 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> M e. ZZ )
8 simprr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> N e. ZZ )
9 8 ad2antrr 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> N e. ZZ )
10 nn0z 
 |-  ( -u I e. NN0 -> -u I e. ZZ )
11 10 adantl 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> -u I e. ZZ )
12 simplr 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> I e. RR )
13 12 recnd 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> I e. CC )
14 znegclb 
 |-  ( I e. CC -> ( I e. ZZ <-> -u I e. ZZ ) )
15 13 14 syl 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> ( I e. ZZ <-> -u I e. ZZ ) )
16 11 15 mpbird 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> I e. ZZ )
17 16 7 zmulcld 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> ( I x. M ) e. ZZ )
18 9 17 zaddcld 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> ( N + ( I x. M ) ) e. ZZ )
19 simpr 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> -u I e. NN0 )
20 jm2.19lem3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ ( N + ( I x. M ) ) e. ZZ ) /\ -u I e. NN0 ) -> ( ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) <-> ( A rmY M ) || ( A rmY ( ( N + ( I x. M ) ) + ( -u I x. M ) ) ) ) )
21 5 7 18 19 20 syl121anc 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> ( ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) <-> ( A rmY M ) || ( A rmY ( ( N + ( I x. M ) ) + ( -u I x. M ) ) ) ) )
22 zcn 
 |-  ( M e. ZZ -> M e. CC )
23 22 ad2antrl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> M e. CC )
24 23 ad2antrr 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> M e. CC )
25 13 24 mulneg1d 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> ( -u I x. M ) = -u ( I x. M ) )
26 25 oveq2d 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> ( ( N + ( I x. M ) ) + ( -u I x. M ) ) = ( ( N + ( I x. M ) ) + -u ( I x. M ) ) )
27 zcn 
 |-  ( N e. ZZ -> N e. CC )
28 27 ad2antll 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> N e. CC )
29 28 ad2antrr 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> N e. CC )
30 13 24 mulcld 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> ( I x. M ) e. CC )
31 29 30 addcld 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> ( N + ( I x. M ) ) e. CC )
32 31 30 negsubd 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> ( ( N + ( I x. M ) ) + -u ( I x. M ) ) = ( ( N + ( I x. M ) ) - ( I x. M ) ) )
33 29 30 pncand 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> ( ( N + ( I x. M ) ) - ( I x. M ) ) = N )
34 26 32 33 3eqtrd 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> ( ( N + ( I x. M ) ) + ( -u I x. M ) ) = N )
35 34 oveq2d 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> ( A rmY ( ( N + ( I x. M ) ) + ( -u I x. M ) ) ) = ( A rmY N ) )
36 35 breq2d 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> ( ( A rmY M ) || ( A rmY ( ( N + ( I x. M ) ) + ( -u I x. M ) ) ) <-> ( A rmY M ) || ( A rmY N ) ) )
37 21 36 bitr2d 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) /\ -u I e. NN0 ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) )
38 37 ex 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) -> ( -u I e. NN0 -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) ) )
39 4 38 jaod 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) /\ I e. RR ) -> ( ( I e. NN0 \/ -u I e. NN0 ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) ) )
40 39 expimpd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( I e. RR /\ ( I e. NN0 \/ -u I e. NN0 ) ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) ) )
41 1 40 syl5bi 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( I e. ZZ -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) ) )
42 41 3impia 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) /\ I e. ZZ ) -> ( ( A rmY M ) || ( A rmY N ) <-> ( A rmY M ) || ( A rmY ( N + ( I x. M ) ) ) ) )