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