Theorem submateqlem2

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

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

Proof

Step	Hyp	Ref	Expression
1		submateqlem2.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		submateqlem2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 1 ... 𝑁 ) )
3		submateqlem2.m	⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
4		submateqlem2.1	⊢ ( 𝜑 → 𝑀 < 𝐾 )
5		fz1ssnn	⊢ ( 1 ... ( 𝑁 − 1 ) ) ⊆ ℕ
6	5 3	sselid	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
7	6	nnge1d	⊢ ( 𝜑 → 1 ≤ 𝑀 )
8	7 4	jca	⊢ ( 𝜑 → ( 1 ≤ 𝑀 ∧ 𝑀 < 𝐾 ) )
9	3	elfzelzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
10		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
11	2	elfzelzd	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
12		elfzo	⊢ ( ( 𝑀 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ∈ ( 1 ..^ 𝐾 ) ↔ ( 1 ≤ 𝑀 ∧ 𝑀 < 𝐾 ) ) )
13	9 10 11 12	syl3anc	⊢ ( 𝜑 → ( 𝑀 ∈ ( 1 ..^ 𝐾 ) ↔ ( 1 ≤ 𝑀 ∧ 𝑀 < 𝐾 ) ) )
14	8 13	mpbird	⊢ ( 𝜑 → 𝑀 ∈ ( 1 ..^ 𝐾 ) )
15	3	orcd	⊢ ( 𝜑 → ( 𝑀 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑀 = 𝑁 ) )
16		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
17	1 16	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
18		fzm1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( 𝑀 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑀 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑀 = 𝑁 ) ) )
19	17 18	syl	⊢ ( 𝜑 → ( 𝑀 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑀 ∈ ( 1 ... ( 𝑁 − 1 ) ) ∨ 𝑀 = 𝑁 ) ) )
20	15 19	mpbird	⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... 𝑁 ) )
21	6	nnred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
22	21 4	ltned	⊢ ( 𝜑 → 𝑀 ≠ 𝐾 )
23		nelsn	⊢ ( 𝑀 ≠ 𝐾 → ¬ 𝑀 ∈ { 𝐾 } )
24	22 23	syl	⊢ ( 𝜑 → ¬ 𝑀 ∈ { 𝐾 } )
25	20 24	eldifd	⊢ ( 𝜑 → 𝑀 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐾 } ) )
26	14 25	jca	⊢ ( 𝜑 → ( 𝑀 ∈ ( 1 ..^ 𝐾 ) ∧ 𝑀 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝐾 } ) ) )