Proof of Theorem uzin
Step | Hyp | Ref
| Expression |
1 | | uztric 12291 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘𝑀) ∨ 𝑀 ∈ (ℤ≥‘𝑁))) |
2 | | uzss 12290 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀)) |
3 | | sseqin2 4116 |
. . . . 5
⊢
((ℤ≥‘𝑁) ⊆
(ℤ≥‘𝑀) ↔
((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) =
(ℤ≥‘𝑁)) |
4 | 2, 3 | sylib 221 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) →
((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) =
(ℤ≥‘𝑁)) |
5 | | eluzle 12280 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
6 | | iftrue 4419 |
. . . . . 6
⊢ (𝑀 ≤ 𝑁 → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) = 𝑁) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) = 𝑁) |
8 | 7 | fveq2d 6655 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) →
(ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) = (ℤ≥‘𝑁)) |
9 | 4, 8 | eqtr4d 2797 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) →
((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) =
(ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
10 | | uzss 12290 |
. . . . 5
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → (ℤ≥‘𝑀) ⊆
(ℤ≥‘𝑁)) |
11 | | df-ss 3871 |
. . . . 5
⊢
((ℤ≥‘𝑀) ⊆
(ℤ≥‘𝑁) ↔
((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) =
(ℤ≥‘𝑀)) |
12 | 10, 11 | sylib 221 |
. . . 4
⊢ (𝑀 ∈
(ℤ≥‘𝑁) →
((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) =
(ℤ≥‘𝑀)) |
13 | | eluzle 12280 |
. . . . . . . . . 10
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → 𝑁 ≤ 𝑀) |
14 | | eluzel2 12272 |
. . . . . . . . . . 11
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → 𝑁 ∈ ℤ) |
15 | | eluzelz 12277 |
. . . . . . . . . . 11
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → 𝑀 ∈ ℤ) |
16 | | zre 12009 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
17 | | zre 12009 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
18 | | letri3 10749 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝑁 = 𝑀 ↔ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁))) |
19 | 16, 17, 18 | syl2an 599 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 = 𝑀 ↔ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁))) |
20 | 14, 15, 19 | syl2anc 588 |
. . . . . . . . . 10
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → (𝑁 = 𝑀 ↔ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁))) |
21 | 13, 20 | mpbirand 707 |
. . . . . . . . 9
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → (𝑁 = 𝑀 ↔ 𝑀 ≤ 𝑁)) |
22 | 21 | biimprcd 253 |
. . . . . . . 8
⊢ (𝑀 ≤ 𝑁 → (𝑀 ∈ (ℤ≥‘𝑁) → 𝑁 = 𝑀)) |
23 | 6 | eqeq1d 2761 |
. . . . . . . 8
⊢ (𝑀 ≤ 𝑁 → (if(𝑀 ≤ 𝑁, 𝑁, 𝑀) = 𝑀 ↔ 𝑁 = 𝑀)) |
24 | 22, 23 | sylibrd 262 |
. . . . . . 7
⊢ (𝑀 ≤ 𝑁 → (𝑀 ∈ (ℤ≥‘𝑁) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) = 𝑀)) |
25 | 24 | com12 32 |
. . . . . 6
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → (𝑀 ≤ 𝑁 → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) = 𝑀)) |
26 | | iffalse 4422 |
. . . . . 6
⊢ (¬
𝑀 ≤ 𝑁 → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) = 𝑀) |
27 | 25, 26 | pm2.61d1 183 |
. . . . 5
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → if(𝑀 ≤ 𝑁, 𝑁, 𝑀) = 𝑀) |
28 | 27 | fveq2d 6655 |
. . . 4
⊢ (𝑀 ∈
(ℤ≥‘𝑁) →
(ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀)) = (ℤ≥‘𝑀)) |
29 | 12, 28 | eqtr4d 2797 |
. . 3
⊢ (𝑀 ∈
(ℤ≥‘𝑁) →
((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) =
(ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
30 | 9, 29 | jaoi 855 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∨ 𝑀 ∈ (ℤ≥‘𝑁)) →
((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) =
(ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |
31 | 1, 30 | syl 17 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) =
(ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀))) |