Metamath Proof Explorer

Theorem jm2.26

Description: Lemma 2.26 of JonesMatijasevic p. 697, the "second step down lemma". (Contributed by Stefan O'Rear, 2-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 acongrep 
 |-  ( ( N e. NN /\ M e. ZZ ) -> E. m e. ( 0 ... N ) ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) )
2 1 ad2ant2l 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> E. m e. ( 0 ... N ) ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) )
3 acongrep 
 |-  ( ( N e. NN /\ K e. ZZ ) -> E. k e. ( 0 ... N ) ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) )
4 3 ad2ant2lr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> E. k e. ( 0 ... N ) ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) )
5 2z 
 |-  2 e. ZZ
6 simpl1l 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) )
7 nnz 
 |-  ( N e. NN -> N e. ZZ )
8 7 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> N e. ZZ )
9 6 8 syl 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> N e. ZZ )
10 zmulcl 
 |-  ( ( 2 e. ZZ /\ N e. ZZ ) -> ( 2 x. N ) e. ZZ )
11 5 9 10 sylancr 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( 2 x. N ) e. ZZ )
12 simplrl 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> K e. ZZ )
13 12 3ad2antl1 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> K e. ZZ )
14 simpl3l 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> m e. ( 0 ... N ) )
15 14 elfzelzd 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> m e. ZZ )
16 simplrr 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> M e. ZZ )
17 16 3ad2antl1 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> M e. ZZ )
18 simpl2r 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) )
19 simpl2l 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> k e. ( 0 ... N ) )
20 simplll 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> A e. ( ZZ>= ` 2 ) )
21 20 3ad2antl1 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> A e. ( ZZ>= ` 2 ) )
22 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
23 22 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
24 23 nn0zd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. ZZ )
25 21 9 24 syl2anc 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( A rmX N ) e. ZZ )
26 19 elfzelzd 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> k e. ZZ )
27 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
28 27 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ k e. ZZ ) -> ( A rmY k ) e. ZZ )
29 21 26 28 syl2anc 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( A rmY k ) e. ZZ )
30 27 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( A rmY M ) e. ZZ )
31 21 17 30 syl2anc 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( A rmY M ) e. ZZ )
32 27 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ m e. ZZ ) -> ( A rmY m ) e. ZZ )
33 21 15 32 syl2anc 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( A rmY m ) e. ZZ )
34 27 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ K e. ZZ ) -> ( A rmY K ) e. ZZ )
35 21 13 34 syl2anc 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( A rmY K ) e. ZZ )
36 jm2.26a 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( k e. ZZ /\ K e. ZZ ) ) -> ( ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) -> ( ( A rmX N ) || ( ( A rmY k ) - ( A rmY K ) ) \/ ( A rmX N ) || ( ( A rmY k ) - -u ( A rmY K ) ) ) ) )
37 21 9 26 13 36 syl22anc 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) -> ( ( A rmX N ) || ( ( A rmY k ) - ( A rmY K ) ) \/ ( A rmX N ) || ( ( A rmY k ) - -u ( A rmY K ) ) ) ) )
38 18 37 mpd 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( ( A rmX N ) || ( ( A rmY k ) - ( A rmY K ) ) \/ ( A rmX N ) || ( ( A rmY k ) - -u ( A rmY K ) ) ) )
39 simpr 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) )
40 acongtr 
 |-  ( ( ( ( A rmX N ) e. ZZ /\ ( A rmY k ) e. ZZ ) /\ ( ( A rmY K ) e. ZZ /\ ( A rmY M ) e. ZZ ) /\ ( ( ( A rmX N ) || ( ( A rmY k ) - ( A rmY K ) ) \/ ( A rmX N ) || ( ( A rmY k ) - -u ( A rmY K ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) ) -> ( ( A rmX N ) || ( ( A rmY k ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY k ) - -u ( A rmY M ) ) ) )
41 25 29 35 31 38 39 40 syl222anc 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( ( A rmX N ) || ( ( A rmY k ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY k ) - -u ( A rmY M ) ) ) )
42 simpl3r 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) )
43 acongsym 
 |-  ( ( ( ( 2 x. N ) e. ZZ /\ m e. ZZ /\ M e. ZZ ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) -> ( ( 2 x. N ) || ( M - m ) \/ ( 2 x. N ) || ( M - -u m ) ) )
44 11 15 17 42 43 syl31anc 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( ( 2 x. N ) || ( M - m ) \/ ( 2 x. N ) || ( M - -u m ) ) )
45 jm2.26a 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( M e. ZZ /\ m e. ZZ ) ) -> ( ( ( 2 x. N ) || ( M - m ) \/ ( 2 x. N ) || ( M - -u m ) ) -> ( ( A rmX N ) || ( ( A rmY M ) - ( A rmY m ) ) \/ ( A rmX N ) || ( ( A rmY M ) - -u ( A rmY m ) ) ) ) )
46 21 9 17 15 45 syl22anc 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( ( ( 2 x. N ) || ( M - m ) \/ ( 2 x. N ) || ( M - -u m ) ) -> ( ( A rmX N ) || ( ( A rmY M ) - ( A rmY m ) ) \/ ( A rmX N ) || ( ( A rmY M ) - -u ( A rmY m ) ) ) ) )
47 44 46 mpd 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( ( A rmX N ) || ( ( A rmY M ) - ( A rmY m ) ) \/ ( A rmX N ) || ( ( A rmY M ) - -u ( A rmY m ) ) ) )
48 acongtr 
 |-  ( ( ( ( A rmX N ) e. ZZ /\ ( A rmY k ) e. ZZ ) /\ ( ( A rmY M ) e. ZZ /\ ( A rmY m ) e. ZZ ) /\ ( ( ( A rmX N ) || ( ( A rmY k ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY k ) - -u ( A rmY M ) ) ) /\ ( ( A rmX N ) || ( ( A rmY M ) - ( A rmY m ) ) \/ ( A rmX N ) || ( ( A rmY M ) - -u ( A rmY m ) ) ) ) ) -> ( ( A rmX N ) || ( ( A rmY k ) - ( A rmY m ) ) \/ ( A rmX N ) || ( ( A rmY k ) - -u ( A rmY m ) ) ) )
49 25 29 31 33 41 47 48 syl222anc 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( ( A rmX N ) || ( ( A rmY k ) - ( A rmY m ) ) \/ ( A rmX N ) || ( ( A rmY k ) - -u ( A rmY m ) ) ) )
50 jm2.26lem3 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( k e. ( 0 ... N ) /\ m e. ( 0 ... N ) ) /\ ( ( A rmX N ) || ( ( A rmY k ) - ( A rmY m ) ) \/ ( A rmX N ) || ( ( A rmY k ) - -u ( A rmY m ) ) ) ) -> k = m )
51 6 19 14 49 50 syl121anc 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> k = m )
52 id 
 |-  ( k = m -> k = m )
53 eqidd 
 |-  ( k = m -> K = K )
54 52 53 acongeq12d 
 |-  ( k = m -> ( ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) <-> ( ( 2 x. N ) || ( m - K ) \/ ( 2 x. N ) || ( m - -u K ) ) ) )
55 51 54 syl 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) <-> ( ( 2 x. N ) || ( m - K ) \/ ( 2 x. N ) || ( m - -u K ) ) ) )
56 18 55 mpbid 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( ( 2 x. N ) || ( m - K ) \/ ( 2 x. N ) || ( m - -u K ) ) )
57 acongsym 
 |-  ( ( ( ( 2 x. N ) e. ZZ /\ m e. ZZ /\ K e. ZZ ) /\ ( ( 2 x. N ) || ( m - K ) \/ ( 2 x. N ) || ( m - -u K ) ) ) -> ( ( 2 x. N ) || ( K - m ) \/ ( 2 x. N ) || ( K - -u m ) ) )
58 11 15 13 56 57 syl31anc 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( ( 2 x. N ) || ( K - m ) \/ ( 2 x. N ) || ( K - -u m ) ) )
59 acongtr 
 |-  ( ( ( ( 2 x. N ) e. ZZ /\ K e. ZZ ) /\ ( m e. ZZ /\ M e. ZZ ) /\ ( ( ( 2 x. N ) || ( K - m ) \/ ( 2 x. N ) || ( K - -u m ) ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) -> ( ( 2 x. N ) || ( K - M ) \/ ( 2 x. N ) || ( K - -u M ) ) )
60 11 13 15 17 58 42 59 syl222anc 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) /\ ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) /\ ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) ) /\ ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) ) -> ( ( 2 x. N ) || ( K - M ) \/ ( 2 x. N ) || ( K - -u M ) ) )
61 60 3exp1 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( k e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) ) -> ( ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) -> ( ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) -> ( ( 2 x. N ) || ( K - M ) \/ ( 2 x. N ) || ( K - -u M ) ) ) ) ) )
62 61 expd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( k e. ( 0 ... N ) -> ( ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) -> ( ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) -> ( ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) -> ( ( 2 x. N ) || ( K - M ) \/ ( 2 x. N ) || ( K - -u M ) ) ) ) ) ) )
63 62 rexlimdv 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( E. k e. ( 0 ... N ) ( ( 2 x. N ) || ( k - K ) \/ ( 2 x. N ) || ( k - -u K ) ) -> ( ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) -> ( ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) -> ( ( 2 x. N ) || ( K - M ) \/ ( 2 x. N ) || ( K - -u M ) ) ) ) ) )
64 4 63 mpd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( m e. ( 0 ... N ) /\ ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) ) -> ( ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) -> ( ( 2 x. N ) || ( K - M ) \/ ( 2 x. N ) || ( K - -u M ) ) ) ) )
65 64 expd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( m e. ( 0 ... N ) -> ( ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) -> ( ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) -> ( ( 2 x. N ) || ( K - M ) \/ ( 2 x. N ) || ( K - -u M ) ) ) ) ) )
66 65 rexlimdv 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( E. m e. ( 0 ... N ) ( ( 2 x. N ) || ( m - M ) \/ ( 2 x. N ) || ( m - -u M ) ) -> ( ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) -> ( ( 2 x. N ) || ( K - M ) \/ ( 2 x. N ) || ( K - -u M ) ) ) ) )
67 2 66 mpd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) -> ( ( 2 x. N ) || ( K - M ) \/ ( 2 x. N ) || ( K - -u M ) ) ) )
68 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 ) ) ) ) )
69 7 68 sylanl2 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( 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 ) ) ) ) )
70 67 69 impbid 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( ( A rmX N ) || ( ( A rmY K ) - ( A rmY M ) ) \/ ( A rmX N ) || ( ( A rmY K ) - -u ( A rmY M ) ) ) <-> ( ( 2 x. N ) || ( K - M ) \/ ( 2 x. N ) || ( K - -u M ) ) ) )