Metamath Proof Explorer


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 ∨ 𝑀 = 𝐾 ) )