algcvgblem

		Ref	Expression
	Assertion	algcvgblem	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((N \neq 0 \to N < M) \leftrightarrow ((M \neq 0 \to N < M) \land (M = 0 \to N = 0)))$

Proof

Step	Hyp	Ref	Expression
1		imor	$⊢ (N \neq 0 \to N < M) \leftrightarrow (\neg N \neq 0 \lor N < M)$
2		0re	$⊢ 0 \in ℝ$
3		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
4	3	adantr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to M \in ℝ$
5		ltnle	$⊢ (0 \in ℝ \land M \in ℝ) \to (0 < M \leftrightarrow \neg M \leq 0)$
6	2 4 5	sylancr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (0 < M \leftrightarrow \neg M \leq 0)$
7		nn0le0eq0	$⊢ M \in ℕ_{0} \to (M \leq 0 \leftrightarrow M = 0)$
8	7	notbid	$⊢ M \in ℕ_{0} \to (\neg M \leq 0 \leftrightarrow \neg M = 0)$
9	8	adantr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (\neg M \leq 0 \leftrightarrow \neg M = 0)$
10	6 9	bitrd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (0 < M \leftrightarrow \neg M = 0)$
11		df-ne	$⊢ M \neq 0 \leftrightarrow \neg M = 0$
12	10 11	bitr4di	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (0 < M \leftrightarrow M \neq 0)$
13	12	anbi2d	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((\neg N \neq 0 \land 0 < M) \leftrightarrow (\neg N \neq 0 \land M \neq 0))$
14		nne	$⊢ \neg N \neq 0 \leftrightarrow N = 0$
15		breq1	$⊢ N = 0 \to (N < M \leftrightarrow 0 < M)$
16	14 15	sylbi	$⊢ \neg N \neq 0 \to (N < M \leftrightarrow 0 < M)$
17	16	biimpar	$⊢ (\neg N \neq 0 \land 0 < M) \to N < M$
18	13 17	syl6bir	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((\neg N \neq 0 \land M \neq 0) \to N < M)$
19	18	expd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (\neg N \neq 0 \to (M \neq 0 \to N < M))$
20		ax-1	$⊢ N < M \to (M \neq 0 \to N < M)$
21		jaob	$⊢ ((\neg N \neq 0 \lor N < M) \to (M \neq 0 \to N < M)) \leftrightarrow ((\neg N \neq 0 \to (M \neq 0 \to N < M)) \land (N < M \to (M \neq 0 \to N < M)))$
22	19 20 21	sylanblrc	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((\neg N \neq 0 \lor N < M) \to (M \neq 0 \to N < M))$
23	1 22	syl5bi	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((N \neq 0 \to N < M) \to (M \neq 0 \to N < M))$
24		nn0ge0	$⊢ N \in ℕ_{0} \to 0 \leq N$
25	24	adantl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to 0 \leq N$
26		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
27		lelttr	$⊢ (0 \in ℝ \land N \in ℝ \land M \in ℝ) \to ((0 \leq N \land N < M) \to 0 < M)$
28	2 27	mp3an1	$⊢ (N \in ℝ \land M \in ℝ) \to ((0 \leq N \land N < M) \to 0 < M)$
29	26 3 28	syl2anr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((0 \leq N \land N < M) \to 0 < M)$
30	25 29	mpand	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (N < M \to 0 < M)$
31	30 12	sylibd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (N < M \to M \neq 0)$
32	31	imim2d	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((N \neq 0 \to N < M) \to (N \neq 0 \to M \neq 0))$
33	23 32	jcad	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((N \neq 0 \to N < M) \to ((M \neq 0 \to N < M) \land (N \neq 0 \to M \neq 0)))$
34		pm3.34	$⊢ ((M \neq 0 \to N < M) \land (N \neq 0 \to M \neq 0)) \to (N \neq 0 \to N < M)$
35	33 34	impbid1	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((N \neq 0 \to N < M) \leftrightarrow ((M \neq 0 \to N < M) \land (N \neq 0 \to M \neq 0)))$
36		con34b	$⊢ (M = 0 \to N = 0) \leftrightarrow (\neg N = 0 \to \neg M = 0)$
37		df-ne	$⊢ N \neq 0 \leftrightarrow \neg N = 0$
38	37 11	imbi12i	$⊢ (N \neq 0 \to M \neq 0) \leftrightarrow (\neg N = 0 \to \neg M = 0)$
39	36 38	bitr4i	$⊢ (M = 0 \to N = 0) \leftrightarrow (N \neq 0 \to M \neq 0)$
40	39	anbi2i	$⊢ ((M \neq 0 \to N < M) \land (M = 0 \to N = 0)) \leftrightarrow ((M \neq 0 \to N < M) \land (N \neq 0 \to M \neq 0))$
41	35 40	bitr4di	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((N \neq 0 \to N < M) \leftrightarrow ((M \neq 0 \to N < M) \land (M = 0 \to N = 0)))$

Metamath Proof Explorer

Theorem algcvgblem

Proof