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	sseldi	$⊢ φ \to M \in ℕ$
7	6	nnge1d	$⊢ φ \to 1 \leq M$
8	7 4	jca	$⊢ φ \to (1 \leq M \land M < K)$
9	6	nnzd	$⊢ φ \to M \in ℤ$
10		1zzd	$⊢ φ \to 1 \in ℤ$
11		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
12	11 2	sseldi	$⊢ φ \to K \in ℕ$
13	12	nnzd	$⊢ φ \to K \in ℤ$
14		elfzo	$⊢ (M \in ℤ \land 1 \in ℤ \land K \in ℤ) \to (M \in (1 ..^K) \leftrightarrow (1 \leq M \land M < K))$
15	9 10 13 14	syl3anc	$⊢ φ \to (M \in (1 ..^K) \leftrightarrow (1 \leq M \land M < K))$
16	8 15	mpbird	$⊢ φ \to M \in (1 ..^K)$
17	3	orcd	$⊢ φ \to (M \in (1 \dots N - 1) \lor M = N)$
18		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
19	1 18	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
20		fzm1	$⊢ N \in ℤ_{\geq 1} \to (M \in (1 \dots N) \leftrightarrow (M \in (1 \dots N - 1) \lor M = N))$
21	19 20	syl	$⊢ φ \to (M \in (1 \dots N) \leftrightarrow (M \in (1 \dots N - 1) \lor M = N))$
22	17 21	mpbird	$⊢ φ \to M \in (1 \dots N)$
23	6	nnred	$⊢ φ \to M \in ℝ$
24	23 4	ltned	$⊢ φ \to M \neq K$
25		nelsn	$⊢ M \neq K \to \neg M \in \{K\}$
26	24 25	syl	$⊢ φ \to \neg M \in \{K\}$
27	22 26	eldifd	$⊢ φ \to M \in ((1 \dots N) ∖ \{K\})$
28	16 27	jca	$⊢ φ \to (M \in (1 ..^K) \land M \in ((1 \dots N) ∖ \{K\}))$

Metamath Proof Explorer