Metamath Proof Explorer

Theorem jm2.26a

Description: Lemma for jm2.26 . Reverse direction is required to prove forward direction, so do it separately. Induction on difference between K and M, together with the addition formula fact that adding 2N only inverts sign. (Contributed by Stefan O'Rear, 2-Oct-2014)

Ref Expression
Assertion jm2.26a 
|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( ( 2 x. N ) || ( K - M ) \/ ( 2 x. N ) || ( K - -u M ) ) -> ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) )

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 simplr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> N e. ZZ )
3 zmulcl 
 |-  ( ( 2 e. ZZ /\ N e. ZZ ) -> ( 2 x. N ) e. ZZ )
4 1 2 3 sylancr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( 2 x. N ) e. ZZ )
5 zsubcl 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( K - M ) e. ZZ )
6 5 adantl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( K - M ) e. ZZ )
7 divides 
 |-  ( ( ( 2 x. N ) e. ZZ /\ ( K - M ) e. ZZ ) -> ( ( 2 x. N ) || ( K - M ) <-> E. a e. ZZ ( a x. ( 2 x. N ) ) = ( K - M ) ) )
8 4 6 7 syl2anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( 2 x. N ) || ( K - M ) <-> E. a e. ZZ ( a x. ( 2 x. N ) ) = ( K - M ) ) )
9 simplll 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> A e. ( ZZ>= ` 2 ) )
10 simplrr 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> M e. ZZ )
11 simpllr 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> N e. ZZ )
12 simpr 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> a e. ZZ )
13 jm2.25 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) /\ a e. ZZ ) -> ( ( A rmX N ) || ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) )
14 9 10 11 12 13 syl121anc 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> ( ( A rmX N ) || ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) )
15 14 adantr 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) /\ ( a x. ( 2 x. N ) ) = ( K - M ) ) -> ( ( A rmX N ) || ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) )
16 oveq2 
 |-  ( ( a x. ( 2 x. N ) ) = ( K - M ) -> ( M + ( a x. ( 2 x. N ) ) ) = ( M + ( K - M ) ) )
17 16 oveq2d 
 |-  ( ( a x. ( 2 x. N ) ) = ( K - M ) -> ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) = ( A rmY ( M + ( K - M ) ) ) )
18 zcn 
 |-  ( M e. ZZ -> M e. CC )
19 zcn 
 |-  ( K e. ZZ -> K e. CC )
20 pncan3 
 |-  ( ( M e. CC /\ K e. CC ) -> ( M + ( K - M ) ) = K )
21 18 19 20 syl2anr 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( M + ( K - M ) ) = K )
22 21 ad2antlr 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> ( M + ( K - M ) ) = K )
23 22 oveq2d 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> ( A rmY ( M + ( K - M ) ) ) = ( A rmY K ) )
24 17 23 sylan9eqr 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) /\ ( a x. ( 2 x. N ) ) = ( K - M ) ) -> ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) = ( A rmY K ) )
25 eqidd 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) /\ ( a x. ( 2 x. N ) ) = ( K - M ) ) -> ( A rmY M ) = ( A rmY M ) )
26 24 25 acongeq12d 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) /\ ( a x. ( 2 x. N ) ) = ( K - M ) ) -> ( ( ( A rmX N ) || ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY ( M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY M ) ) ) <-> ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) )
27 15 26 mpbid 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) /\ ( a x. ( 2 x. N ) ) = ( K - M ) ) -> ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) )
28 27 rexlimdva2 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( E. a e. ZZ ( a x. ( 2 x. N ) ) = ( K - M ) -> ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) )
29 8 28 sylbid 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( 2 x. N ) || ( K - M ) -> ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) )
30 simprl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> K e. ZZ )
31 znegcl 
 |-  ( M e. ZZ -> -u M e. ZZ )
32 31 ad2antll 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> -u M e. ZZ )
33 30 32 zsubcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( K - -u M ) e. ZZ )
34 divides 
 |-  ( ( ( 2 x. N ) e. ZZ /\ ( K - -u M ) e. ZZ ) -> ( ( 2 x. N ) || ( K - -u M ) <-> E. a e. ZZ ( a x. ( 2 x. N ) ) = ( K - -u M ) ) )
35 4 33 34 syl2anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( 2 x. N ) || ( K - -u M ) <-> E. a e. ZZ ( a x. ( 2 x. N ) ) = ( K - -u M ) ) )
36 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
37 36 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
38 37 nn0zd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. ZZ )
39 9 11 38 syl2anc 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> ( A rmX N ) e. ZZ )
40 simplrl 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> K e. ZZ )
41 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
42 41 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ZZ ) -> ( A rmY K ) e. ZZ )
43 9 40 42 syl2anc 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> ( A rmY K ) e. ZZ )
44 41 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( A rmY M ) e. ZZ )
45 9 10 44 syl2anc 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> ( A rmY M ) e. ZZ )
46 39 43 45 3jca 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> ( ( A rmX N ) e. ZZ /\ ( A rmY K ) e. ZZ /\ ( A rmY M ) e. ZZ ) )
47 46 adantr 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) /\ ( a x. ( 2 x. N ) ) = ( K - -u M ) ) -> ( ( A rmX N ) e. ZZ /\ ( A rmY K ) e. ZZ /\ ( A rmY M ) e. ZZ ) )
48 32 adantr 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> -u M e. ZZ )
49 jm2.25 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( -u M e. ZZ /\ N e. ZZ ) /\ a e. ZZ ) -> ( ( A rmX N ) || ( ( A rmY ( -u M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY -u M ) ) \/ ( A rmX N ) || ( ( A rmY ( -u M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY -u M ) ) ) )
50 9 48 11 12 49 syl121anc 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> ( ( A rmX N ) || ( ( A rmY ( -u M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY -u M ) ) \/ ( A rmX N ) || ( ( A rmY ( -u M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY -u M ) ) ) )
51 50 adantr 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) /\ ( a x. ( 2 x. N ) ) = ( K - -u M ) ) -> ( ( A rmX N ) || ( ( A rmY ( -u M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY -u M ) ) \/ ( A rmX N ) || ( ( A rmY ( -u M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY -u M ) ) ) )
52 oveq2 
 |-  ( ( a x. ( 2 x. N ) ) = ( K - -u M ) -> ( -u M + ( a x. ( 2 x. N ) ) ) = ( -u M + ( K - -u M ) ) )
53 52 oveq2d 
 |-  ( ( a x. ( 2 x. N ) ) = ( K - -u M ) -> ( A rmY ( -u M + ( a x. ( 2 x. N ) ) ) ) = ( A rmY ( -u M + ( K - -u M ) ) ) )
54 18 negcld 
 |-  ( M e. ZZ -> -u M e. CC )
55 pncan3 
 |-  ( ( -u M e. CC /\ K e. CC ) -> ( -u M + ( K - -u M ) ) = K )
56 54 19 55 syl2anr 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( -u M + ( K - -u M ) ) = K )
57 56 ad2antlr 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> ( -u M + ( K - -u M ) ) = K )
58 57 oveq2d 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> ( A rmY ( -u M + ( K - -u M ) ) ) = ( A rmY K ) )
59 53 58 sylan9eqr 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) /\ ( a x. ( 2 x. N ) ) = ( K - -u M ) ) -> ( A rmY ( -u M + ( a x. ( 2 x. N ) ) ) ) = ( A rmY K ) )
60 rmyneg 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( A rmY -u M ) = -u ( A rmY M ) )
61 9 10 60 syl2anc 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) -> ( A rmY -u M ) = -u ( A rmY M ) )
62 61 adantr 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) /\ ( a x. ( 2 x. N ) ) = ( K - -u M ) ) -> ( A rmY -u M ) = -u ( A rmY M ) )
63 59 62 acongeq12d 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) /\ ( a x. ( 2 x. N ) ) = ( K - -u M ) ) -> ( ( ( A rmX N ) || ( ( A rmY ( -u M + ( a x. ( 2 x. N ) ) ) ) - ( A rmY -u M ) ) \/ ( A rmX N ) || ( ( A rmY ( -u M + ( a x. ( 2 x. N ) ) ) ) - -u ( A rmY -u M ) ) ) <-> ( ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u -u ( A rmY M ) ) ) ) )
64 51 63 mpbid 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) /\ ( a x. ( 2 x. N ) ) = ( K - -u M ) ) -> ( ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u -u ( A rmY M ) ) ) )
65 acongneg2 
 |-  ( ( ( ( A rmX N ) e. ZZ /\ ( A rmY K ) e. ZZ /\ ( A rmY M ) e. ZZ ) /\ ( ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u -u ( A rmY M ) ) ) ) -> ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) )
66 47 64 65 syl2anc 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ a e. ZZ ) /\ ( a x. ( 2 x. N ) ) = ( K - -u M ) ) -> ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) )
67 66 rexlimdva2 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( E. a e. ZZ ( a x. ( 2 x. N ) ) = ( K - -u M ) -> ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) )
68 35 67 sylbid 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( 2 x. N ) || ( K - -u M ) -> ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) )
69 29 68 jaod 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( ( 2 x. N ) || ( K - M ) \/ ( 2 x. N ) || ( K - -u M ) ) -> ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) )