Proof of Theorem uz11
Step | Hyp | Ref
| Expression |
1 | | uzid 12597 |
. . . . 5
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
2 | | eleq2 2827 |
. . . . . 6
⊢
((ℤ≥‘𝑀) = (ℤ≥‘𝑁) → (𝑀 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ∈ (ℤ≥‘𝑁))) |
3 | | eluzel2 12587 |
. . . . . 6
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → 𝑁 ∈ ℤ) |
4 | 2, 3 | syl6bi 252 |
. . . . 5
⊢
((ℤ≥‘𝑀) = (ℤ≥‘𝑁) → (𝑀 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)) |
5 | 1, 4 | mpan9 507 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧
(ℤ≥‘𝑀) = (ℤ≥‘𝑁)) → 𝑁 ∈ ℤ) |
6 | | uzid 12597 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
7 | | eleq2 2827 |
. . . . . . . . . . 11
⊢
((ℤ≥‘𝑀) = (ℤ≥‘𝑁) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑁 ∈ (ℤ≥‘𝑁))) |
8 | 6, 7 | syl5ibr 245 |
. . . . . . . . . 10
⊢
((ℤ≥‘𝑀) = (ℤ≥‘𝑁) → (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ≥‘𝑀))) |
9 | | eluzle 12595 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
10 | 8, 9 | syl6 35 |
. . . . . . . . 9
⊢
((ℤ≥‘𝑀) = (ℤ≥‘𝑁) → (𝑁 ∈ ℤ → 𝑀 ≤ 𝑁)) |
11 | 1, 2 | syl5ib 243 |
. . . . . . . . . 10
⊢
((ℤ≥‘𝑀) = (ℤ≥‘𝑁) → (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑁))) |
12 | | eluzle 12595 |
. . . . . . . . . 10
⊢ (𝑀 ∈
(ℤ≥‘𝑁) → 𝑁 ≤ 𝑀) |
13 | 11, 12 | syl6 35 |
. . . . . . . . 9
⊢
((ℤ≥‘𝑀) = (ℤ≥‘𝑁) → (𝑀 ∈ ℤ → 𝑁 ≤ 𝑀)) |
14 | 10, 13 | anim12d 609 |
. . . . . . . 8
⊢
((ℤ≥‘𝑀) = (ℤ≥‘𝑁) → ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀))) |
15 | 14 | impl 456 |
. . . . . . 7
⊢
((((ℤ≥‘𝑀) = (ℤ≥‘𝑁) ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ∈ ℤ) → (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)) |
16 | 15 | ancoms 459 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧
((ℤ≥‘𝑀) = (ℤ≥‘𝑁) ∧ 𝑁 ∈ ℤ)) → (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)) |
17 | 16 | anassrs 468 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧
(ℤ≥‘𝑀) = (ℤ≥‘𝑁)) ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)) |
18 | | zre 12323 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
19 | | zre 12323 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
20 | | letri3 11060 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀))) |
21 | 18, 19, 20 | syl2an 596 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀))) |
22 | 21 | adantlr 712 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧
(ℤ≥‘𝑀) = (ℤ≥‘𝑁)) ∧ 𝑁 ∈ ℤ) → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀))) |
23 | 17, 22 | mpbird 256 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧
(ℤ≥‘𝑀) = (ℤ≥‘𝑁)) ∧ 𝑁 ∈ ℤ) → 𝑀 = 𝑁) |
24 | 5, 23 | mpdan 684 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧
(ℤ≥‘𝑀) = (ℤ≥‘𝑁)) → 𝑀 = 𝑁) |
25 | 24 | ex 413 |
. 2
⊢ (𝑀 ∈ ℤ →
((ℤ≥‘𝑀) = (ℤ≥‘𝑁) → 𝑀 = 𝑁)) |
26 | | fveq2 6774 |
. 2
⊢ (𝑀 = 𝑁 → (ℤ≥‘𝑀) =
(ℤ≥‘𝑁)) |
27 | 25, 26 | impbid1 224 |
1
⊢ (𝑀 ∈ ℤ →
((ℤ≥‘𝑀) = (ℤ≥‘𝑁) ↔ 𝑀 = 𝑁)) |