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 A2MNIAYrmMAYrmNAYrmMAYrmN+ I M

Proof

Step Hyp Ref Expression
1 elznn0 III0I0
2 jm2.19lem3 A2MNI0AYrmMAYrmNAYrmMAYrmN+ I M
3 2 3expia A2MNI0AYrmMAYrmNAYrmMAYrmN+ I M
4 3 adantr A2MNII0AYrmMAYrmNAYrmMAYrmN+ I M
5 simplll A2MNII0A2
6 simprl A2MNM
7 6 ad2antrr A2MNII0M
8 simprr A2MNN
9 8 ad2antrr A2MNII0N
10 nn0z I0I
11 10 adantl A2MNII0I
12 simplr A2MNII0I
13 12 recnd A2MNII0I
14 znegclb III
15 13 14 syl A2MNII0II
16 11 15 mpbird A2MNII0I
17 16 7 zmulcld A2MNII0 I M
18 9 17 zaddcld A2MNII0N+ I M
19 simpr A2MNII0I0
20 jm2.19lem3 A2MN+ I MI0AYrmMAYrmN+ I MAYrmMAYrmN+ I M+- I M
21 5 7 18 19 20 syl121anc A2MNII0AYrmMAYrmN+ I MAYrmMAYrmN+ I M+- I M
22 zcn MM
23 22 ad2antrl A2MNM
24 23 ad2antrr A2MNII0M
25 13 24 mulneg1d A2MNII0- I M= I M
26 25 oveq2d A2MNII0N+ I M+- I M=N+ I M+ I M
27 zcn NN
28 27 ad2antll A2MNN
29 28 ad2antrr A2MNII0N
30 13 24 mulcld A2MNII0 I M
31 29 30 addcld A2MNII0N+ I M
32 31 30 negsubd A2MNII0N+ I M+ I M=N+ I M- I M
33 29 30 pncand A2MNII0N+ I M- I M=N
34 26 32 33 3eqtrd A2MNII0N+ I M+- I M=N
35 34 oveq2d A2MNII0AYrmN+ I M+- I M=AYrmN
36 35 breq2d A2MNII0AYrmMAYrmN+ I M+- I MAYrmMAYrmN
37 21 36 bitr2d A2MNII0AYrmMAYrmNAYrmMAYrmN+ I M
38 37 ex A2MNII0AYrmMAYrmNAYrmMAYrmN+ I M
39 4 38 jaod A2MNII0I0AYrmMAYrmNAYrmMAYrmN+ I M
40 39 expimpd A2MNII0I0AYrmMAYrmNAYrmMAYrmN+ I M
41 1 40 biimtrid A2MNIAYrmMAYrmNAYrmMAYrmN+ I M
42 41 3impia A2MNIAYrmMAYrmNAYrmMAYrmN+ I M