elfznelfzo

Description: A value in a finite set of sequential integers is a border value if it is not contained in the half-open integer range contained in the finite set of sequential integers. (Contributed by Alexander van der Vekens, 31-Oct-2017) (Revised by Thierry Arnoux, 22-Dec-2021)

		Ref	Expression
	Assertion	elfznelfzo	$⊢ (M \in (0 \dots K) \land \neg M \in (1 ..^K)) \to (M = 0 \lor M = K)$

Proof

Step	Hyp	Ref	Expression
1		elfz2nn0	$⊢ M \in (0 \dots K) \leftrightarrow (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K)$
2		nn0z	$⊢ M \in ℕ_{0} \to M \in ℤ$
3		nn0z	$⊢ K \in ℕ_{0} \to K \in ℤ$
4	2 3	anim12i	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0}) \to (M \in ℤ \land K \in ℤ)$
5	4	3adant3	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (M \in ℤ \land K \in ℤ)$
6		elfzom1b	$⊢ (M \in ℤ \land K \in ℤ) \to (M \in (1 ..^K) \leftrightarrow M - 1 \in (0 ..^K - 1))$
7	5 6	syl	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (M \in (1 ..^K) \leftrightarrow M - 1 \in (0 ..^K - 1))$
8	7	notbid	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (\neg M \in (1 ..^K) \leftrightarrow \neg M - 1 \in (0 ..^K - 1))$
9		elfzo0	$⊢ M - 1 \in (0 ..^K - 1) \leftrightarrow (M - 1 \in ℕ_{0} \land K - 1 \in ℕ \land M - 1 < K - 1)$
10	9	a1i	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (M - 1 \in (0 ..^K - 1) \leftrightarrow (M - 1 \in ℕ_{0} \land K - 1 \in ℕ \land M - 1 < K - 1))$
11	10	notbid	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (\neg M - 1 \in (0 ..^K - 1) \leftrightarrow \neg (M - 1 \in ℕ_{0} \land K - 1 \in ℕ \land M - 1 < K - 1))$
12		3ianor	$⊢ \neg (M - 1 \in ℕ_{0} \land K - 1 \in ℕ \land M - 1 < K - 1) \leftrightarrow (\neg M - 1 \in ℕ_{0} \lor \neg K - 1 \in ℕ \lor \neg M - 1 < K - 1)$
13		elnnne0	$⊢ M \in ℕ \leftrightarrow (M \in ℕ_{0} \land M \neq 0)$
14		df-ne	$⊢ M \neq 0 \leftrightarrow \neg M = 0$
15	14	anbi2i	$⊢ (M \in ℕ_{0} \land M \neq 0) \leftrightarrow (M \in ℕ_{0} \land \neg M = 0)$
16	13 15	bitr2i	$⊢ (M \in ℕ_{0} \land \neg M = 0) \leftrightarrow M \in ℕ$
17		nnm1nn0	$⊢ M \in ℕ \to M - 1 \in ℕ_{0}$
18	16 17	sylbi	$⊢ (M \in ℕ_{0} \land \neg M = 0) \to M - 1 \in ℕ_{0}$
19	18	ex	$⊢ M \in ℕ_{0} \to (\neg M = 0 \to M - 1 \in ℕ_{0})$
20	19	con1d	$⊢ M \in ℕ_{0} \to (\neg M - 1 \in ℕ_{0} \to M = 0)$
21	20	imp	$⊢ (M \in ℕ_{0} \land \neg M - 1 \in ℕ_{0}) \to M = 0$
22	21	orcd	$⊢ (M \in ℕ_{0} \land \neg M - 1 \in ℕ_{0}) \to (M = 0 \lor M = K)$
23	22	ex	$⊢ M \in ℕ_{0} \to (\neg M - 1 \in ℕ_{0} \to (M = 0 \lor M = K))$
24	23	3ad2ant1	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (\neg M - 1 \in ℕ_{0} \to (M = 0 \lor M = K))$
25	24	com12	$⊢ \neg M - 1 \in ℕ_{0} \to ((M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (M = 0 \lor M = K))$
26		ioran	$⊢ \neg (M = 0 \lor M = K) \leftrightarrow (\neg M = 0 \land \neg M = K)$
27		nn1m1nn	$⊢ M \in ℕ \to (M = 1 \lor M - 1 \in ℕ)$
28		df-ne	$⊢ M \neq K \leftrightarrow \neg M = K$
29		necom	$⊢ M \neq K \leftrightarrow K \neq M$
30		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
31	30	ad2antlr	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land M \leq K) \to M \in ℝ$
32		nn0re	$⊢ K \in ℕ_{0} \to K \in ℝ$
33	32	adantr	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to K \in ℝ$
34	33	adantr	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land M \leq K) \to K \in ℝ$
35		simpr	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land M \leq K) \to M \leq K$
36	31 34 35	leltned	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land M \leq K) \to (M < K \leftrightarrow K \neq M)$
37	29 36	bitr4id	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land M \leq K) \to (M \neq K \leftrightarrow M < K)$
38	37	adantr	$⊢ (((K \in ℕ_{0} \land M \in ℕ_{0}) \land M \leq K) \land M = 1) \to (M \neq K \leftrightarrow M < K)$
39		breq1	$⊢ M = 1 \to (M < K \leftrightarrow 1 < K)$
40	39	biimpa	$⊢ (M = 1 \land M < K) \to 1 < K$
41		1red	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to 1 \in ℝ$
42	41 33 41	ltsub1d	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to (1 < K \leftrightarrow 1 - 1 < K - 1)$
43		1m1e0	$⊢ 1 - 1 = 0$
44	43	breq1i	$⊢ 1 - 1 < K - 1 \leftrightarrow 0 < K - 1$
45		1zzd	$⊢ K \in ℕ_{0} \to 1 \in ℤ$
46	3 45	zsubcld	$⊢ K \in ℕ_{0} \to K - 1 \in ℤ$
47	46	adantr	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to K - 1 \in ℤ$
48	47	adantr	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land 0 < K - 1) \to K - 1 \in ℤ$
49		simpr	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land 0 < K - 1) \to 0 < K - 1$
50		elnnz	$⊢ K - 1 \in ℕ \leftrightarrow (K - 1 \in ℤ \land 0 < K - 1)$
51	48 49 50	sylanbrc	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land 0 < K - 1) \to K - 1 \in ℕ$
52	51	ex	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to (0 < K - 1 \to K - 1 \in ℕ)$
53	44 52	biimtrid	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to (1 - 1 < K - 1 \to K - 1 \in ℕ)$
54	42 53	sylbid	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to (1 < K \to K - 1 \in ℕ)$
55	40 54	syl5	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to ((M = 1 \land M < K) \to K - 1 \in ℕ)$
56	55	expd	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to (M = 1 \to (M < K \to K - 1 \in ℕ))$
57	56	adantr	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land M \leq K) \to (M = 1 \to (M < K \to K - 1 \in ℕ))$
58	57	imp	$⊢ (((K \in ℕ_{0} \land M \in ℕ_{0}) \land M \leq K) \land M = 1) \to (M < K \to K - 1 \in ℕ)$
59	38 58	sylbid	$⊢ (((K \in ℕ_{0} \land M \in ℕ_{0}) \land M \leq K) \land M = 1) \to (M \neq K \to K - 1 \in ℕ)$
60	59	exp31	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to (M \leq K \to (M = 1 \to (M \neq K \to K - 1 \in ℕ)))$
61	60	com14	$⊢ M \neq K \to (M \leq K \to (M = 1 \to ((K \in ℕ_{0} \land M \in ℕ_{0}) \to K - 1 \in ℕ)))$
62	28 61	sylbir	$⊢ \neg M = K \to (M \leq K \to (M = 1 \to ((K \in ℕ_{0} \land M \in ℕ_{0}) \to K - 1 \in ℕ)))$
63	62	com23	$⊢ \neg M = K \to (M = 1 \to (M \leq K \to ((K \in ℕ_{0} \land M \in ℕ_{0}) \to K - 1 \in ℕ)))$
64	63	com14	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to (M = 1 \to (M \leq K \to (\neg M = K \to K - 1 \in ℕ)))$
65	64	ex	$⊢ K \in ℕ_{0} \to (M \in ℕ_{0} \to (M = 1 \to (M \leq K \to (\neg M = K \to K - 1 \in ℕ))))$
66	65	com14	$⊢ M \leq K \to (M \in ℕ_{0} \to (M = 1 \to (K \in ℕ_{0} \to (\neg M = K \to K - 1 \in ℕ))))$
67	66	com13	$⊢ M = 1 \to (M \in ℕ_{0} \to (M \leq K \to (K \in ℕ_{0} \to (\neg M = K \to K - 1 \in ℕ))))$
68	30	ad2antlr	$⊢ ((M - 1 \in ℕ \land M \in ℕ_{0}) \land K \in ℕ_{0}) \to M \in ℝ$
69	32	adantl	$⊢ ((M - 1 \in ℕ \land M \in ℕ_{0}) \land K \in ℕ_{0}) \to K \in ℝ$
70		1red	$⊢ ((M - 1 \in ℕ \land M \in ℕ_{0}) \land K \in ℕ_{0}) \to 1 \in ℝ$
71	68 69 70	lesub1d	$⊢ ((M - 1 \in ℕ \land M \in ℕ_{0}) \land K \in ℕ_{0}) \to (M \leq K \leftrightarrow M - 1 \leq K - 1)$
72	3	ad2antlr	$⊢ (((M - 1 \in ℕ \land M \in ℕ_{0}) \land K \in ℕ_{0}) \land M - 1 \leq K - 1) \to K \in ℤ$
73		1zzd	$⊢ (((M - 1 \in ℕ \land M \in ℕ_{0}) \land K \in ℕ_{0}) \land M - 1 \leq K - 1) \to 1 \in ℤ$
74	72 73	zsubcld	$⊢ (((M - 1 \in ℕ \land M \in ℕ_{0}) \land K \in ℕ_{0}) \land M - 1 \leq K - 1) \to K - 1 \in ℤ$
75		nngt0	$⊢ M - 1 \in ℕ \to 0 < M - 1$
76		0red	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0}) \to 0 \in ℝ$
77		peano2rem	$⊢ M \in ℝ \to M - 1 \in ℝ$
78	30 77	syl	$⊢ M \in ℕ_{0} \to M - 1 \in ℝ$
79	78	adantr	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0}) \to M - 1 \in ℝ$
80		peano2rem	$⊢ K \in ℝ \to K - 1 \in ℝ$
81	32 80	syl	$⊢ K \in ℕ_{0} \to K - 1 \in ℝ$
82	81	adantl	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0}) \to K - 1 \in ℝ$
83		ltletr	$⊢ (0 \in ℝ \land M - 1 \in ℝ \land K - 1 \in ℝ) \to ((0 < M - 1 \land M - 1 \leq K - 1) \to 0 < K - 1)$
84	76 79 82 83	syl3anc	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0}) \to ((0 < M - 1 \land M - 1 \leq K - 1) \to 0 < K - 1)$
85	84	ex	$⊢ M \in ℕ_{0} \to (K \in ℕ_{0} \to ((0 < M - 1 \land M - 1 \leq K - 1) \to 0 < K - 1))$
86	85	com13	$⊢ (0 < M - 1 \land M - 1 \leq K - 1) \to (K \in ℕ_{0} \to (M \in ℕ_{0} \to 0 < K - 1))$
87	86	ex	$⊢ 0 < M - 1 \to (M - 1 \leq K - 1 \to (K \in ℕ_{0} \to (M \in ℕ_{0} \to 0 < K - 1)))$
88	87	com24	$⊢ 0 < M - 1 \to (M \in ℕ_{0} \to (K \in ℕ_{0} \to (M - 1 \leq K - 1 \to 0 < K - 1)))$
89	75 88	syl	$⊢ M - 1 \in ℕ \to (M \in ℕ_{0} \to (K \in ℕ_{0} \to (M - 1 \leq K - 1 \to 0 < K - 1)))$
90	89	imp41	$⊢ (((M - 1 \in ℕ \land M \in ℕ_{0}) \land K \in ℕ_{0}) \land M - 1 \leq K - 1) \to 0 < K - 1$
91	74 90 50	sylanbrc	$⊢ (((M - 1 \in ℕ \land M \in ℕ_{0}) \land K \in ℕ_{0}) \land M - 1 \leq K - 1) \to K - 1 \in ℕ$
92	91	a1d	$⊢ (((M - 1 \in ℕ \land M \in ℕ_{0}) \land K \in ℕ_{0}) \land M - 1 \leq K - 1) \to (\neg M = K \to K - 1 \in ℕ)$
93	92	ex	$⊢ ((M - 1 \in ℕ \land M \in ℕ_{0}) \land K \in ℕ_{0}) \to (M - 1 \leq K - 1 \to (\neg M = K \to K - 1 \in ℕ))$
94	71 93	sylbid	$⊢ ((M - 1 \in ℕ \land M \in ℕ_{0}) \land K \in ℕ_{0}) \to (M \leq K \to (\neg M = K \to K - 1 \in ℕ))$
95	94	ex	$⊢ (M - 1 \in ℕ \land M \in ℕ_{0}) \to (K \in ℕ_{0} \to (M \leq K \to (\neg M = K \to K - 1 \in ℕ)))$
96	95	com23	$⊢ (M - 1 \in ℕ \land M \in ℕ_{0}) \to (M \leq K \to (K \in ℕ_{0} \to (\neg M = K \to K - 1 \in ℕ)))$
97	96	ex	$⊢ M - 1 \in ℕ \to (M \in ℕ_{0} \to (M \leq K \to (K \in ℕ_{0} \to (\neg M = K \to K - 1 \in ℕ))))$
98	67 97	jaoi	$⊢ (M = 1 \lor M - 1 \in ℕ) \to (M \in ℕ_{0} \to (M \leq K \to (K \in ℕ_{0} \to (\neg M = K \to K - 1 \in ℕ))))$
99	27 98	syl	$⊢ M \in ℕ \to (M \in ℕ_{0} \to (M \leq K \to (K \in ℕ_{0} \to (\neg M = K \to K - 1 \in ℕ))))$
100	13 99	sylbir	$⊢ (M \in ℕ_{0} \land M \neq 0) \to (M \in ℕ_{0} \to (M \leq K \to (K \in ℕ_{0} \to (\neg M = K \to K - 1 \in ℕ))))$
101	100	ex	$⊢ M \in ℕ_{0} \to (M \neq 0 \to (M \in ℕ_{0} \to (M \leq K \to (K \in ℕ_{0} \to (\neg M = K \to K - 1 \in ℕ)))))$
102	101	pm2.43a	$⊢ M \in ℕ_{0} \to (M \neq 0 \to (M \leq K \to (K \in ℕ_{0} \to (\neg M = K \to K - 1 \in ℕ))))$
103	102	com24	$⊢ M \in ℕ_{0} \to (K \in ℕ_{0} \to (M \leq K \to (M \neq 0 \to (\neg M = K \to K - 1 \in ℕ))))$
104	103	3imp	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (M \neq 0 \to (\neg M = K \to K - 1 \in ℕ))$
105	104	com3l	$⊢ M \neq 0 \to (\neg M = K \to ((M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to K - 1 \in ℕ))$
106	14 105	sylbir	$⊢ \neg M = 0 \to (\neg M = K \to ((M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to K - 1 \in ℕ))$
107	106	imp	$⊢ (\neg M = 0 \land \neg M = K) \to ((M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to K - 1 \in ℕ)$
108	26 107	sylbi	$⊢ \neg (M = 0 \lor M = K) \to ((M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to K - 1 \in ℕ)$
109	108	com12	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (\neg (M = 0 \lor M = K) \to K - 1 \in ℕ)$
110	109	con1d	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (\neg K - 1 \in ℕ \to (M = 0 \lor M = K))$
111	110	com12	$⊢ \neg K - 1 \in ℕ \to ((M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (M = 0 \lor M = K))$
112	30	adantr	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0}) \to M \in ℝ$
113	32	adantl	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0}) \to K \in ℝ$
114		1red	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0}) \to 1 \in ℝ$
115	112 113 114	3jca	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0}) \to (M \in ℝ \land K \in ℝ \land 1 \in ℝ)$
116	115	3adant3	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (M \in ℝ \land K \in ℝ \land 1 \in ℝ)$
117		ltsub1	$⊢ (M \in ℝ \land K \in ℝ \land 1 \in ℝ) \to (M < K \leftrightarrow M - 1 < K - 1)$
118	116 117	syl	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (M < K \leftrightarrow M - 1 < K - 1)$
119	118	bicomd	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (M - 1 < K - 1 \leftrightarrow M < K)$
120	119	notbid	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (\neg M - 1 < K - 1 \leftrightarrow \neg M < K)$
121		eqlelt	$⊢ (M \in ℝ \land K \in ℝ) \to (M = K \leftrightarrow (M \leq K \land \neg M < K))$
122	30 32 121	syl2an	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0}) \to (M = K \leftrightarrow (M \leq K \land \neg M < K))$
123	122	biimpar	$⊢ ((M \in ℕ_{0} \land K \in ℕ_{0}) \land (M \leq K \land \neg M < K)) \to M = K$
124	123	olcd	$⊢ ((M \in ℕ_{0} \land K \in ℕ_{0}) \land (M \leq K \land \neg M < K)) \to (M = 0 \lor M = K)$
125	124	exp43	$⊢ M \in ℕ_{0} \to (K \in ℕ_{0} \to (M \leq K \to (\neg M < K \to (M = 0 \lor M = K))))$
126	125	3imp	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (\neg M < K \to (M = 0 \lor M = K))$
127	120 126	sylbid	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (\neg M - 1 < K - 1 \to (M = 0 \lor M = K))$
128	127	com12	$⊢ \neg M - 1 < K - 1 \to ((M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (M = 0 \lor M = K))$
129	25 111 128	3jaoi	$⊢ (\neg M - 1 \in ℕ_{0} \lor \neg K - 1 \in ℕ \lor \neg M - 1 < K - 1) \to ((M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (M = 0 \lor M = K))$
130	12 129	sylbi	$⊢ \neg (M - 1 \in ℕ_{0} \land K - 1 \in ℕ \land M - 1 < K - 1) \to ((M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (M = 0 \lor M = K))$
131	130	com12	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (\neg (M - 1 \in ℕ_{0} \land K - 1 \in ℕ \land M - 1 < K - 1) \to (M = 0 \lor M = K))$
132	11 131	sylbid	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (\neg M - 1 \in (0 ..^K - 1) \to (M = 0 \lor M = K))$
133	8 132	sylbid	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0} \land M \leq K) \to (\neg M \in (1 ..^K) \to (M = 0 \lor M = K))$
134	1 133	sylbi	$⊢ M \in (0 \dots K) \to (\neg M \in (1 ..^K) \to (M = 0 \lor M = K))$
135	134	imp	$⊢ (M \in (0 \dots K) \land \neg M \in (1 ..^K)) \to (M = 0 \lor M = K)$

Metamath Proof Explorer

Theorem elfznelfzo

Proof