Theorem submateqlem1

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

	Ref	Expression
Hypotheses	submateqlem1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	submateqlem1.k	⊢ ( 𝜑 → 𝐾 ∈ ( 1 ... 𝑁 ) )
	submateqlem1.m	⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
	submateqlem1.1	⊢ ( 𝜑 → 𝐾 ≤ 𝑀 )
Assertion	submateqlem1	⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝐾 ... 𝑁 ) ∧ ( 𝑀 + 1 ) ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐾 } ) ) )

Proof

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