submateqlem1

	Ref	Expression
Hypotheses	submateqlem1.n	$⊢ φ \to N \in ℕ$
	submateqlem1.k	$⊢ φ \to K \in (1 \dots N)$
	submateqlem1.m	$⊢ φ \to M \in (1 \dots N - 1)$
	submateqlem1.1	$⊢ φ \to K \leq M$
Assertion	submateqlem1	$⊢ φ \to (M \in (K \dots N) \land M + 1 \in ((1 \dots N) ∖ \{K\}))$

Proof

Step	Hyp	Ref	Expression
1		submateqlem1.n	$⊢ φ \to N \in ℕ$
2		submateqlem1.k	$⊢ φ \to K \in (1 \dots N)$
3		submateqlem1.m	$⊢ φ \to M \in (1 \dots N - 1)$
4		submateqlem1.1	$⊢ φ \to K \leq M$
5		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
6	5 2	sselid	$⊢ φ \to K \in ℕ$
7	6	nnzd	$⊢ φ \to K \in ℤ$
8	1	nnzd	$⊢ φ \to N \in ℤ$
9		fz1ssnn	$⊢ (1 \dots N - 1) \subseteq ℕ$
10	9 3	sselid	$⊢ φ \to M \in ℕ$
11	10	nnzd	$⊢ φ \to M \in ℤ$
12	10	nnred	$⊢ φ \to M \in ℝ$
13	1	nnred	$⊢ φ \to N \in ℝ$
14		1red	$⊢ φ \to 1 \in ℝ$
15	13 14	resubcld	$⊢ φ \to N - 1 \in ℝ$
16		elfzle2	$⊢ M \in (1 \dots N - 1) \to M \leq N - 1$
17	3 16	syl	$⊢ φ \to M \leq N - 1$
18	13	lem1d	$⊢ φ \to N - 1 \leq N$
19	12 15 13 17 18	letrd	$⊢ φ \to M \leq N$
20	7 8 11 4 19	elfzd	$⊢ φ \to M \in (K \dots N)$
21		1zzd	$⊢ φ \to 1 \in ℤ$
22	11	peano2zd	$⊢ φ \to M + 1 \in ℤ$
23	10	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
24	23	nn0ge0d	$⊢ φ \to 0 \leq M$
25		1re	$⊢ 1 \in ℝ$
26		addge02	$⊢ (1 \in ℝ \land M \in ℝ) \to (0 \leq M \leftrightarrow 1 \leq M + 1)$
27	25 12 26	sylancr	$⊢ φ \to (0 \leq M \leftrightarrow 1 \leq M + 1)$
28	24 27	mpbid	$⊢ φ \to 1 \leq M + 1$
29	1	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
30		nn0ltlem1	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M < N \leftrightarrow M \leq N - 1)$
31	23 29 30	syl2anc	$⊢ φ \to (M < N \leftrightarrow M \leq N - 1)$
32	17 31	mpbird	$⊢ φ \to M < N$
33		nnltp1le	$⊢ (M \in ℕ \land N \in ℕ) \to (M < N \leftrightarrow M + 1 \leq N)$
34	10 1 33	syl2anc	$⊢ φ \to (M < N \leftrightarrow M + 1 \leq N)$
35	32 34	mpbid	$⊢ φ \to M + 1 \leq N$
36	21 8 22 28 35	elfzd	$⊢ φ \to M + 1 \in (1 \dots N)$
37	6	nnred	$⊢ φ \to K \in ℝ$
38		nnleltp1	$⊢ (K \in ℕ \land M \in ℕ) \to (K \leq M \leftrightarrow K < M + 1)$
39	6 10 38	syl2anc	$⊢ φ \to (K \leq M \leftrightarrow K < M + 1)$
40	4 39	mpbid	$⊢ φ \to K < M + 1$
41	37 40	ltned	$⊢ φ \to K \neq M + 1$
42	41	necomd	$⊢ φ \to M + 1 \neq K$
43		nelsn	$⊢ M + 1 \neq K \to \neg M + 1 \in \{K\}$
44	42 43	syl	$⊢ φ \to \neg M + 1 \in \{K\}$
45	36 44	eldifd	$⊢ φ \to M + 1 \in ((1 \dots N) ∖ \{K\})$
46	20 45	jca	$⊢ φ \to (M \in (K \dots N) \land M + 1 \in ((1 \dots N) ∖ \{K\}))$

Metamath Proof Explorer

Theorem submateqlem1

Proof