Proof of Theorem submateqlem1
Step | Hyp | Ref
| Expression |
1 | | submateqlem1.1 |
. . . 4
⊢ (𝜑 → 𝐾 ≤ 𝑀) |
2 | | fz1ssnn 12753 |
. . . . . . 7
⊢
(1...(𝑁 − 1))
⊆ ℕ |
3 | | submateqlem1.m |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1))) |
4 | 2, 3 | sseldi 3851 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
5 | 4 | nnred 11455 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℝ) |
6 | | submateqlem1.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
7 | 6 | nnred 11455 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℝ) |
8 | | 1red 10439 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
9 | 7, 8 | resubcld 10868 |
. . . . 5
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
10 | | elfzle2 12726 |
. . . . . 6
⊢ (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ≤ (𝑁 − 1)) |
11 | 3, 10 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑀 ≤ (𝑁 − 1)) |
12 | 7 | lem1d 11373 |
. . . . 5
⊢ (𝜑 → (𝑁 − 1) ≤ 𝑁) |
13 | 5, 9, 7, 11, 12 | letrd 10596 |
. . . 4
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
14 | 1, 13 | jca 504 |
. . 3
⊢ (𝜑 → (𝐾 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁)) |
15 | 4 | nnzd 11898 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
16 | | fz1ssnn 12753 |
. . . . . 6
⊢
(1...𝑁) ⊆
ℕ |
17 | | submateqlem1.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (1...𝑁)) |
18 | 16, 17 | sseldi 3851 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ℕ) |
19 | 18 | nnzd 11898 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ ℤ) |
20 | 6 | nnzd 11898 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
21 | | elfz 12713 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (𝐾...𝑁) ↔ (𝐾 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁))) |
22 | 15, 19, 20, 21 | syl3anc 1352 |
. . 3
⊢ (𝜑 → (𝑀 ∈ (𝐾...𝑁) ↔ (𝐾 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁))) |
23 | 14, 22 | mpbird 249 |
. 2
⊢ (𝜑 → 𝑀 ∈ (𝐾...𝑁)) |
24 | 4 | nnnn0d 11766 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
25 | 24 | nn0ge0d 11769 |
. . . . . 6
⊢ (𝜑 → 0 ≤ 𝑀) |
26 | | 1re 10438 |
. . . . . . 7
⊢ 1 ∈
ℝ |
27 | | addge02 10951 |
. . . . . . 7
⊢ ((1
∈ ℝ ∧ 𝑀
∈ ℝ) → (0 ≤ 𝑀 ↔ 1 ≤ (𝑀 + 1))) |
28 | 26, 5, 27 | sylancr 579 |
. . . . . 6
⊢ (𝜑 → (0 ≤ 𝑀 ↔ 1 ≤ (𝑀 + 1))) |
29 | 25, 28 | mpbid 224 |
. . . . 5
⊢ (𝜑 → 1 ≤ (𝑀 + 1)) |
30 | 6 | nnnn0d 11766 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
31 | | nn0ltlem1 11854 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) |
32 | 24, 30, 31 | syl2anc 576 |
. . . . . . 7
⊢ (𝜑 → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1))) |
33 | 11, 32 | mpbird 249 |
. . . . . 6
⊢ (𝜑 → 𝑀 < 𝑁) |
34 | | nnltp1le 11850 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) |
35 | 4, 6, 34 | syl2anc 576 |
. . . . . 6
⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁)) |
36 | 33, 35 | mpbid 224 |
. . . . 5
⊢ (𝜑 → (𝑀 + 1) ≤ 𝑁) |
37 | 29, 36 | jca 504 |
. . . 4
⊢ (𝜑 → (1 ≤ (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁)) |
38 | 15 | peano2zd 11902 |
. . . . 5
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) |
39 | | 1zzd 11825 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
40 | | elfz 12713 |
. . . . 5
⊢ (((𝑀 + 1) ∈ ℤ ∧ 1
∈ ℤ ∧ 𝑁
∈ ℤ) → ((𝑀
+ 1) ∈ (1...𝑁) ↔
(1 ≤ (𝑀 + 1) ∧
(𝑀 + 1) ≤ 𝑁))) |
41 | 38, 39, 20, 40 | syl3anc 1352 |
. . . 4
⊢ (𝜑 → ((𝑀 + 1) ∈ (1...𝑁) ↔ (1 ≤ (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁))) |
42 | 37, 41 | mpbird 249 |
. . 3
⊢ (𝜑 → (𝑀 + 1) ∈ (1...𝑁)) |
43 | 18 | nnred 11455 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ℝ) |
44 | | nnleltp1 11849 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝐾 ≤ 𝑀 ↔ 𝐾 < (𝑀 + 1))) |
45 | 18, 4, 44 | syl2anc 576 |
. . . . . . 7
⊢ (𝜑 → (𝐾 ≤ 𝑀 ↔ 𝐾 < (𝑀 + 1))) |
46 | 1, 45 | mpbid 224 |
. . . . . 6
⊢ (𝜑 → 𝐾 < (𝑀 + 1)) |
47 | 43, 46 | ltned 10575 |
. . . . 5
⊢ (𝜑 → 𝐾 ≠ (𝑀 + 1)) |
48 | 47 | necomd 3017 |
. . . 4
⊢ (𝜑 → (𝑀 + 1) ≠ 𝐾) |
49 | | nelsn 4474 |
. . . 4
⊢ ((𝑀 + 1) ≠ 𝐾 → ¬ (𝑀 + 1) ∈ {𝐾}) |
50 | 48, 49 | syl 17 |
. . 3
⊢ (𝜑 → ¬ (𝑀 + 1) ∈ {𝐾}) |
51 | 42, 50 | eldifd 3835 |
. 2
⊢ (𝜑 → (𝑀 + 1) ∈ ((1...𝑁) ∖ {𝐾})) |
52 | 23, 51 | jca 504 |
1
⊢ (𝜑 → (𝑀 ∈ (𝐾...𝑁) ∧ (𝑀 + 1) ∈ ((1...𝑁) ∖ {𝐾}))) |