algcvgblem - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > algcvgblem		GIF version

Theorem algcvgblem 11766

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

**Assertion**
Ref	Expression
algcvgblem	⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑀 = 0 → 𝑁 = 0))))

**Proof of Theorem algcvgblem**
Step	Hyp	Ref	Expression
1		nn0z 9098	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
2		0z 9089	. . . . . . . . 9 ⊢ 0 ∈ ℤ
3		zdceq 9150	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 = 0)
4	1, 2, 3	sylancl 410	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → DECID 𝑁 = 0)
5	4	dcned 2315	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → DECID 𝑁 ≠ 0)
6		imordc 883	. . . . . . 7 ⊢ (DECID 𝑁 ≠ 0 → ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ (¬ 𝑁 ≠ 0 ∨ 𝑁 < 𝑀)))
7	5, 6	syl 14	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ (¬ 𝑁 ≠ 0 ∨ 𝑁 < 𝑀)))
8	7	adantl 275	. . . . 5 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ (¬ 𝑁 ≠ 0 ∨ 𝑁 < 𝑀)))
9		nn0z 9098	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ₀ → 𝑀 ∈ ℤ)
10		zltnle 9124	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0 < 𝑀 ↔ ¬ 𝑀 ≤ 0))
11	2, 9, 10	sylancr 411	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ₀ → (0 < 𝑀 ↔ ¬ 𝑀 ≤ 0))
12	11	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (0 < 𝑀 ↔ ¬ 𝑀 ≤ 0))
13		nn0le0eq0 9029	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ₀ → (𝑀 ≤ 0 ↔ 𝑀 = 0))
14	13	notbid 657	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ₀ → (¬ 𝑀 ≤ 0 ↔ ¬ 𝑀 = 0))
15	14	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (¬ 𝑀 ≤ 0 ↔ ¬ 𝑀 = 0))
16	12, 15	bitrd 187	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (0 < 𝑀 ↔ ¬ 𝑀 = 0))
17		df-ne 2310	. . . . . . . . . . 11 ⊢ (𝑀 ≠ 0 ↔ ¬ 𝑀 = 0)
18	16, 17	syl6bbr 197	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (0 < 𝑀 ↔ 𝑀 ≠ 0))
19	18	anbi2d 460	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((¬ 𝑁 ≠ 0 ∧ 0 < 𝑀) ↔ (¬ 𝑁 ≠ 0 ∧ 𝑀 ≠ 0)))
20	1	adantl 275	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 𝑁 ∈ ℤ)
21	20, 2, 3	sylancl 410	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → DECID 𝑁 = 0)
22		nnedc 2314	. . . . . . . . . . . . 13 ⊢ (DECID 𝑁 = 0 → (¬ 𝑁 ≠ 0 ↔ 𝑁 = 0))
23	21, 22	syl 14	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (¬ 𝑁 ≠ 0 ↔ 𝑁 = 0))
24		breq1 3940	. . . . . . . . . . . 12 ⊢ (𝑁 = 0 → (𝑁 < 𝑀 ↔ 0 < 𝑀))
25	23, 24	syl6bi 162	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (¬ 𝑁 ≠ 0 → (𝑁 < 𝑀 ↔ 0 < 𝑀)))
26		bi2 129	. . . . . . . . . . 11 ⊢ ((𝑁 < 𝑀 ↔ 0 < 𝑀) → (0 < 𝑀 → 𝑁 < 𝑀))
27	25, 26	syl6 33	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (¬ 𝑁 ≠ 0 → (0 < 𝑀 → 𝑁 < 𝑀)))
28	27	impd 252	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((¬ 𝑁 ≠ 0 ∧ 0 < 𝑀) → 𝑁 < 𝑀))
29	19, 28	sylbird 169	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((¬ 𝑁 ≠ 0 ∧ 𝑀 ≠ 0) → 𝑁 < 𝑀))
30	29	expd 256	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (¬ 𝑁 ≠ 0 → (𝑀 ≠ 0 → 𝑁 < 𝑀)))
31		ax-1 6	. . . . . . 7 ⊢ (𝑁 < 𝑀 → (𝑀 ≠ 0 → 𝑁 < 𝑀))
32	30, 31	jctir 311	. . . . . 6 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((¬ 𝑁 ≠ 0 → (𝑀 ≠ 0 → 𝑁 < 𝑀)) ∧ (𝑁 < 𝑀 → (𝑀 ≠ 0 → 𝑁 < 𝑀))))
33		jaob 700	. . . . . 6 ⊢ (((¬ 𝑁 ≠ 0 ∨ 𝑁 < 𝑀) → (𝑀 ≠ 0 → 𝑁 < 𝑀)) ↔ ((¬ 𝑁 ≠ 0 → (𝑀 ≠ 0 → 𝑁 < 𝑀)) ∧ (𝑁 < 𝑀 → (𝑀 ≠ 0 → 𝑁 < 𝑀))))
34	32, 33	sylibr 133	. . . . 5 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((¬ 𝑁 ≠ 0 ∨ 𝑁 < 𝑀) → (𝑀 ≠ 0 → 𝑁 < 𝑀)))
35	8, 34	sylbid 149	. . . 4 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) → (𝑀 ≠ 0 → 𝑁 < 𝑀)))
36		nn0ge0 9026	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → 0 ≤ 𝑁)
37	36	adantl 275	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 0 ≤ 𝑁)
38		nn0re 9010	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
39		nn0re 9010	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ₀ → 𝑀 ∈ ℝ)
40		0re 7790	. . . . . . . . 9 ⊢ 0 ∈ ℝ
41		lelttr 7876	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((0 ≤ 𝑁 ∧ 𝑁 < 𝑀) → 0 < 𝑀))
42	40, 41	mp3an1 1303	. . . . . . . 8 ⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((0 ≤ 𝑁 ∧ 𝑁 < 𝑀) → 0 < 𝑀))
43	38, 39, 42	syl2anr 288	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((0 ≤ 𝑁 ∧ 𝑁 < 𝑀) → 0 < 𝑀))
44	37, 43	mpand 426	. . . . . 6 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑁 < 𝑀 → 0 < 𝑀))
45	44, 18	sylibd 148	. . . . 5 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑁 < 𝑀 → 𝑀 ≠ 0))
46	45	imim2d 54	. . . 4 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) → (𝑁 ≠ 0 → 𝑀 ≠ 0)))
47	35, 46	jcad 305	. . 3 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) → ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑁 ≠ 0 → 𝑀 ≠ 0))))
48		pm3.34 344	. . 3 ⊢ (((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑁 ≠ 0 → 𝑀 ≠ 0)) → (𝑁 ≠ 0 → 𝑁 < 𝑀))
49	47, 48	impbid1 141	. 2 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑁 ≠ 0 → 𝑀 ≠ 0))))
50		con34bdc 857	. . . . 5 ⊢ (DECID 𝑁 = 0 → ((𝑀 = 0 → 𝑁 = 0) ↔ (¬ 𝑁 = 0 → ¬ 𝑀 = 0)))
51	21, 50	syl 14	. . . 4 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((𝑀 = 0 → 𝑁 = 0) ↔ (¬ 𝑁 = 0 → ¬ 𝑀 = 0)))
52		df-ne 2310	. . . . 5 ⊢ (𝑁 ≠ 0 ↔ ¬ 𝑁 = 0)
53	52, 17	imbi12i 238	. . . 4 ⊢ ((𝑁 ≠ 0 → 𝑀 ≠ 0) ↔ (¬ 𝑁 = 0 → ¬ 𝑀 = 0))
54	51, 53	syl6bbr 197	. . 3 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((𝑀 = 0 → 𝑁 = 0) ↔ (𝑁 ≠ 0 → 𝑀 ≠ 0)))
55	54	anbi2d 460	. 2 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑀 = 0 → 𝑁 = 0)) ↔ ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑁 ≠ 0 → 𝑀 ≠ 0))))
56	49, 55	bitr4d 190	1 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑀 = 0 → 𝑁 = 0))))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 698 DECID wdc 820 = wceq 1332 ∈ wcel 1481 ≠ wne 2309 class class class wbr 3937 ℝcr 7643 0cc0 7644 < clt 7824 ≤ cle 7825 ℕ₀cn0 9001 ℤcz 9078

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-13 1492 ax-14 1493 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 ax-sep 4054 ax-pow 4106 ax-pr 4139 ax-un 4363 ax-setind 4460 ax-cnex 7735 ax-resscn 7736 ax-1cn 7737 ax-1re 7738 ax-icn 7739 ax-addcl 7740 ax-addrcl 7741 ax-mulcl 7742 ax-addcom 7744 ax-addass 7746 ax-distr 7748 ax-i2m1 7749 ax-0lt1 7750 ax-0id 7752 ax-rnegex 7753 ax-cnre 7755 ax-pre-ltirr 7756 ax-pre-ltwlin 7757 ax-pre-lttrn 7758 ax-pre-apti 7759 ax-pre-ltadd 7760

This theorem depends on definitions: df-bi 116 df-stab 817 df-dc 821 df-3or 964 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1737 df-eu 2003 df-mo 2004 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ne 2310 df-nel 2405 df-ral 2422 df-rex 2423 df-reu 2424 df-rab 2426 df-v 2691 df-sbc 2914 df-dif 3078 df-un 3080 df-in 3082 df-ss 3089 df-pw 3517 df-sn 3538 df-pr 3539 df-op 3541 df-uni 3745 df-int 3780 df-br 3938 df-opab 3998 df-id 4223 df-xp 4553 df-rel 4554 df-cnv 4555 df-co 4556 df-dm 4557 df-iota 5096 df-fun 5133 df-fv 5139 df-riota 5738 df-ov 5785 df-oprab 5786 df-mpo 5787 df-pnf 7826 df-mnf 7827 df-xr 7828 df-ltxr 7829 df-le 7830 df-sub 7959 df-neg 7960 df-inn 8745 df-n0 9002 df-z 9079

This theorem is referenced by: algcvgb 11767

W3C validator