nn0le2is012 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > nn0le2is012		Structured version Unicode version

Theorem nn0le2is012 33156

Description: A nonnegative integer which is less than or equal to 2 is either 0 or 1 or 2. (Contributed by AV, 16-Mar-2019.)

**Assertion**
Ref	Expression
nn0le2is012	$/\$ $\/$ $\/$

**Proof of Theorem nn0le2is012**
Step	Hyp	Ref	Expression
1		nn0re 10721	. . . 4
2		2re 10522	. . . . 5
3	2	a1i 11	. . . 4
4	1, 3	leloed 9639	. . 3 $\/$
5		nn0z 10804	. . . . . . . . 9
6		2z 10813	. . . . . . . . 9
7		zltlem1 10833	. . . . . . . . 9 $/\$
8	5, 6, 7	sylancl 660	. . . . . . . 8
9		2m1e1 10567	. . . . . . . . . 10
10	9	a1i 11	. . . . . . . . 9
11	10	breq2d 4379	. . . . . . . 8
12	8, 11	bitrd 253	. . . . . . 7
13		1red 9522	. . . . . . . . 9
14	1, 13	leloed 9639	. . . . . . . 8 $\/$
15		nn0lt10b 10842	. . . . . . . . . . . 12
16		3mix1 1163	. . . . . . . . . . . 12 $\/$ $\/$
17	15, 16	syl6bi 228	. . . . . . . . . . 11 $\/$ $\/$
18	17	com12 31	. . . . . . . . . 10 $\/$ $\/$
19		3mix2 1164	. . . . . . . . . . 11 $\/$ $\/$
20	19	a1d 25	. . . . . . . . . 10 $\/$ $\/$
21	18, 20	jaoi 377	. . . . . . . . 9 $\/$ $\/$ $\/$
22	21	com12 31	. . . . . . . 8 $\/$ $\/$ $\/$
23	14, 22	sylbid 215	. . . . . . 7 $\/$ $\/$
24	12, 23	sylbid 215	. . . . . 6 $\/$ $\/$
25	24	com12 31	. . . . 5 $\/$ $\/$
26		3mix3 1165	. . . . . 6 $\/$ $\/$
27	26	a1d 25	. . . . 5 $\/$ $\/$
28	25, 27	jaoi 377	. . . 4 $\/$ $\/$ $\/$
29	28	com12 31	. . 3 $\/$ $\/$ $\/$
30	4, 29	sylbid 215	. 2 $\/$ $\/$
31	30	imp 427	1 $/\$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367 $\/$ w3o 970

wceq 1399

wcel 1826 class class class wbr 4367 (class class class)co 6196

cr 9402

cc0 9403

c1 9404

clt 9539

cle 9540

cmin 9718

c2 10502

cn0 10712

cz 10781

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-resscn 9460 ax-1cn 9461 ax-icn 9462 ax-addcl 9463 ax-addrcl 9464 ax-mulcl 9465 ax-mulrcl 9466 ax-mulcom 9467 ax-addass 9468 ax-mulass 9469 ax-distr 9470 ax-i2m1 9471 ax-1ne0 9472 ax-1rid 9473 ax-rnegex 9474 ax-rrecex 9475 ax-cnre 9476 ax-pre-lttri 9477 ax-pre-lttrn 9478 ax-pre-ltadd 9479 ax-pre-mulgt0 9480

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-iun 4245 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-om 6600 df-recs 6960 df-rdg 6994 df-er 7229 df-en 7436 df-dom 7437 df-sdom 7438 df-pnf 9541 df-mnf 9542 df-xr 9543 df-ltxr 9544 df-le 9545 df-sub 9720 df-neg 9721 df-nn 10453 df-2 10511 df-n0 10713 df-z 10782

This theorem is referenced by: exple2lt6 33157