This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem algcvgblem

Description: Lemma for algcvgb . (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Assertion algcvgblem 
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( N =/= 0 -> N < M ) <-> ( ( M =/= 0 -> N < M ) /\ ( M = 0 -> N = 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 imor 
 |-  ( ( N =/= 0 -> N < M ) <-> ( -. N =/= 0 \/ N < M ) )
2 0re 
 |-  0 e. RR
3 nn0re 
 |-  ( M e. NN0 -> M e. RR )
4 3 adantr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> M e. RR )
5 ltnle 
 |-  ( ( 0 e. RR /\ M e. RR ) -> ( 0 < M <-> -. M <_ 0 ) )
6 2 4 5 sylancr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( 0 < M <-> -. M <_ 0 ) )
7 nn0le0eq0 
 |-  ( M e. NN0 -> ( M <_ 0 <-> M = 0 ) )
8 7 notbid 
 |-  ( M e. NN0 -> ( -. M <_ 0 <-> -. M = 0 ) )
9 8 adantr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( -. M <_ 0 <-> -. M = 0 ) )
10 6 9 bitrd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( 0 < M <-> -. M = 0 ) )
11 df-ne 
 |-  ( M =/= 0 <-> -. M = 0 )
12 10 11 bitr4di 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( 0 < M <-> M =/= 0 ) )
13 12 anbi2d 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( -. N =/= 0 /\ 0 < M ) <-> ( -. N =/= 0 /\ M =/= 0 ) ) )
14 nne 
 |-  ( -. N =/= 0 <-> N = 0 )
15 breq1 
 |-  ( N = 0 -> ( N < M <-> 0 < M ) )
16 14 15 sylbi 
 |-  ( -. N =/= 0 -> ( N < M <-> 0 < M ) )
17 16 biimpar 
 |-  ( ( -. N =/= 0 /\ 0 < M ) -> N < M )
18 13 17 biimtrrdi 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( -. N =/= 0 /\ M =/= 0 ) -> N < M ) )
19 18 expd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( -. N =/= 0 -> ( M =/= 0 -> N < M ) ) )
20 ax-1 
 |-  ( N < M -> ( M =/= 0 -> N < M ) )
21 jaob 
 |-  ( ( ( -. N =/= 0 \/ N < M ) -> ( M =/= 0 -> N < M ) ) <-> ( ( -. N =/= 0 -> ( M =/= 0 -> N < M ) ) /\ ( N < M -> ( M =/= 0 -> N < M ) ) ) )
22 19 20 21 sylanblrc 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( -. N =/= 0 \/ N < M ) -> ( M =/= 0 -> N < M ) ) )
23 1 22 biimtrid 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( N =/= 0 -> N < M ) -> ( M =/= 0 -> N < M ) ) )
24 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
25 24 adantl 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> 0 <_ N )
26 nn0re 
 |-  ( N e. NN0 -> N e. RR )
27 lelttr 
 |-  ( ( 0 e. RR /\ N e. RR /\ M e. RR ) -> ( ( 0 <_ N /\ N < M ) -> 0 < M ) )
28 2 27 mp3an1 
 |-  ( ( N e. RR /\ M e. RR ) -> ( ( 0 <_ N /\ N < M ) -> 0 < M ) )
29 26 3 28 syl2anr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( 0 <_ N /\ N < M ) -> 0 < M ) )
30 25 29 mpand 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( N < M -> 0 < M ) )
31 30 12 sylibd 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( N < M -> M =/= 0 ) )
32 31 imim2d 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( N =/= 0 -> N < M ) -> ( N =/= 0 -> M =/= 0 ) ) )
33 23 32 jcad 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( N =/= 0 -> N < M ) -> ( ( M =/= 0 -> N < M ) /\ ( N =/= 0 -> M =/= 0 ) ) ) )
34 pm3.34 
 |-  ( ( ( M =/= 0 -> N < M ) /\ ( N =/= 0 -> M =/= 0 ) ) -> ( N =/= 0 -> N < M ) )
35 33 34 impbid1 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( N =/= 0 -> N < M ) <-> ( ( M =/= 0 -> N < M ) /\ ( N =/= 0 -> M =/= 0 ) ) ) )
36 con34b 
 |-  ( ( M = 0 -> N = 0 ) <-> ( -. N = 0 -> -. M = 0 ) )
37 df-ne 
 |-  ( N =/= 0 <-> -. N = 0 )
38 37 11 imbi12i 
 |-  ( ( N =/= 0 -> M =/= 0 ) <-> ( -. N = 0 -> -. M = 0 ) )
39 36 38 bitr4i 
 |-  ( ( M = 0 -> N = 0 ) <-> ( N =/= 0 -> M =/= 0 ) )
40 39 anbi2i 
 |-  ( ( ( M =/= 0 -> N < M ) /\ ( M = 0 -> N = 0 ) ) <-> ( ( M =/= 0 -> N < M ) /\ ( N =/= 0 -> M =/= 0 ) ) )
41 35 40 bitr4di 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( N =/= 0 -> N < M ) <-> ( ( M =/= 0 -> N < M ) /\ ( M = 0 -> N = 0 ) ) ) )