This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrid ⊢ ( ( 𝐾 ∈ ℕ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 ∨ 𝑀 = 𝐾 ) )