submateqlem2

Step	Hyp	Ref	Expression
1		submateqlem2.n	$⊢ φ \to N \in ℕ$
2		submateqlem2.k	$⊢ φ \to K \in (1 \dots N)$
3		submateqlem2.m	$⊢ φ \to M \in (1 \dots N - 1)$
4		submateqlem2.1	$⊢ φ \to M < K$
5		fz1ssnn	$⊢ (1 \dots N - 1) \subseteq ℕ$
6	5 3	sselid	$⊢ φ \to M \in ℕ$
7	6	nnge1d	$⊢ φ \to 1 \leq M$
8	7 4	jca	$⊢ φ \to (1 \leq M \land M < K)$
9	3	elfzelzd	$⊢ φ \to M \in ℤ$
10		1zzd	$⊢ φ \to 1 \in ℤ$
11	2	elfzelzd	$⊢ φ \to K \in ℤ$
12		elfzo	$⊢ (M \in ℤ \land 1 \in ℤ \land K \in ℤ) \to (M \in (1 ..^K) \leftrightarrow (1 \leq M \land M < K))$
13	9 10 11 12	syl3anc	$⊢ φ \to (M \in (1 ..^K) \leftrightarrow (1 \leq M \land M < K))$
14	8 13	mpbird	$⊢ φ \to M \in (1 ..^K)$
15	3	orcd	$⊢ φ \to (M \in (1 \dots N - 1) \lor M = N)$
16		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
17	1 16	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
18		fzm1	$⊢ N \in ℤ_{\geq 1} \to (M \in (1 \dots N) \leftrightarrow (M \in (1 \dots N - 1) \lor M = N))$
19	17 18	syl	$⊢ φ \to (M \in (1 \dots N) \leftrightarrow (M \in (1 \dots N - 1) \lor M = N))$
20	15 19	mpbird	$⊢ φ \to M \in (1 \dots N)$
21	6	nnred	$⊢ φ \to M \in ℝ$
22	21 4	ltned	$⊢ φ \to M \neq K$
23		nelsn	$⊢ M \neq K \to \neg M \in \{K\}$
24	22 23	syl	$⊢ φ \to \neg M \in \{K\}$
25	20 24	eldifd	$⊢ φ \to M \in ((1 \dots N) ∖ \{K\})$
26	14 25	jca	$⊢ φ \to (M \in (1 ..^K) \land M \in ((1 \dots N) ∖ \{K\}))$

Metamath Proof Explorer