Metamath Proof Explorer

Theorem submateqlem1

Description: Lemma for submateq . (Contributed by Thierry Arnoux, 25-Aug-2020)

Ref Expression
Hypotheses submateqlem1.n ⊢ φ → N ∈ ℕ
submateqlem1.k ⊢ φ → K ∈ 1 … N
submateqlem1.m ⊢ φ → M ∈ 1 … N − 1
submateqlem1.1 ⊢ φ → K ≤ M
Assertion submateqlem1 ⊢ φ → M ∈ K … N ∧ M + 1 ∈ 1 … N ∖ K

Proof

Step Hyp Ref Expression
1 submateqlem1.n ⊢ φ → N ∈ ℕ
2 submateqlem1.k ⊢ φ → K ∈ 1 … N
3 submateqlem1.m ⊢ φ → M ∈ 1 … N − 1
4 submateqlem1.1 ⊢ φ → K ≤ M
5 fz1ssnn ⊢ 1 … N ⊆ ℕ
6 5 2 sseldi ⊢ φ → K ∈ ℕ
7 6 nnzd ⊢ φ → K ∈ ℤ
8 1 nnzd ⊢ φ → N ∈ ℤ
9 fz1ssnn ⊢ 1 … N − 1 ⊆ ℕ
10 9 3 sseldi ⊢ φ → M ∈ ℕ
11 10 nnzd ⊢ φ → M ∈ ℤ
12 10 nnred ⊢ φ → M ∈ ℝ
13 1 nnred ⊢ φ → N ∈ ℝ
14 1red ⊢ φ → 1 ∈ ℝ
15 13 14 resubcld ⊢ φ → N − 1 ∈ ℝ
16 elfzle2 ⊢ M ∈ 1 … N − 1 → M ≤ N − 1
17 3 16 syl ⊢ φ → M ≤ N − 1
18 13 lem1d ⊢ φ → N − 1 ≤ N
19 12 15 13 17 18 letrd ⊢ φ → M ≤ N
20 7 8 11 4 19 elfzd ⊢ φ → M ∈ K … N
21 1zzd ⊢ φ → 1 ∈ ℤ
22 11 peano2zd ⊢ φ → M + 1 ∈ ℤ
23 10 nnnn0d ⊢ φ → M ∈ ℕ 0
24 23 nn0ge0d ⊢ φ → 0 ≤ M
25 1re ⊢ 1 ∈ ℝ
26 addge02 ⊢ 1 ∈ ℝ ∧ M ∈ ℝ → 0 ≤ M ↔ 1 ≤ M + 1
27 25 12 26 sylancr ⊢ φ → 0 ≤ M ↔ 1 ≤ M + 1
28 24 27 mpbid ⊢ φ → 1 ≤ M + 1
29 1 nnnn0d ⊢ φ → N ∈ ℕ 0
30 nn0ltlem1 ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ 0 → M < N ↔ M ≤ N − 1
31 23 29 30 syl2anc ⊢ φ → M < N ↔ M ≤ N − 1
32 17 31 mpbird ⊢ φ → M < N
33 nnltp1le ⊢ M ∈ ℕ ∧ N ∈ ℕ → M < N ↔ M + 1 ≤ N
34 10 1 33 syl2anc ⊢ φ → M < N ↔ M + 1 ≤ N
35 32 34 mpbid ⊢ φ → M + 1 ≤ N
36 21 8 22 28 35 elfzd ⊢ φ → M + 1 ∈ 1 … N
37 6 nnred ⊢ φ → K ∈ ℝ
38 nnleltp1 ⊢ K ∈ ℕ ∧ M ∈ ℕ → K ≤ M ↔ K < M + 1
39 6 10 38 syl2anc ⊢ φ → K ≤ M ↔ K < M + 1
40 4 39 mpbid ⊢ φ → K < M + 1
41 37 40 ltned ⊢ φ → K ≠ M + 1
42 41 necomd ⊢ φ → M + 1 ≠ K
43 nelsn ⊢ M + 1 ≠ K → ¬ M + 1 ∈ K
44 42 43 syl ⊢ φ → ¬ M + 1 ∈ K
45 36 44 eldifd ⊢ φ → M + 1 ∈ 1 … N ∖ K
46 20 45 jca ⊢ φ → M ∈ K … N ∧ M + 1 ∈ 1 … N ∖ K