Theorem 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	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐾 ) ∧ ¬ 𝑀 ∈ ( 1 ..^ 𝐾 ) ) → ( 𝑀 = 0 ∨ 𝑀 = 𝐾 ) )

Proof

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