Metamath Proof Explorer


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 ... 𝑁 ) ∖ { 𝐾 } ) ) )