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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elznn0 | |
|
2 | jm2.19lem3 | |
|
3 | 2 | 3expia | |
4 | 3 | adantr | |
5 | simplll | |
|
6 | simprl | |
|
7 | 6 | ad2antrr | |
8 | simprr | |
|
9 | 8 | ad2antrr | |
10 | nn0z | |
|
11 | 10 | adantl | |
12 | simplr | |
|
13 | 12 | recnd | |
14 | znegclb | |
|
15 | 13 14 | syl | |
16 | 11 15 | mpbird | |
17 | 16 7 | zmulcld | |
18 | 9 17 | zaddcld | |
19 | simpr | |
|
20 | jm2.19lem3 | |
|
21 | 5 7 18 19 20 | syl121anc | |
22 | zcn | |
|
23 | 22 | ad2antrl | |
24 | 23 | ad2antrr | |
25 | 13 24 | mulneg1d | |
26 | 25 | oveq2d | |
27 | zcn | |
|
28 | 27 | ad2antll | |
29 | 28 | ad2antrr | |
30 | 13 24 | mulcld | |
31 | 29 30 | addcld | |
32 | 31 30 | negsubd | |
33 | 29 30 | pncand | |
34 | 26 32 33 | 3eqtrd | |
35 | 34 | oveq2d | |
36 | 35 | breq2d | |
37 | 21 36 | bitr2d | |
38 | 37 | ex | |
39 | 4 38 | jaod | |
40 | 39 | expimpd | |
41 | 1 40 | biimtrid | |
42 | 41 | 3impia | |