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

Metamath Proof Explorer

Theorem submateqlem1

Proof