Proof of Theorem zextle
Step | Hyp | Ref
| Expression |
1 | | zre 9216 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
2 | 1 | leidd 8433 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀) |
3 | 2 | adantr 274 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧
∀𝑘 ∈ ℤ
(𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁)) → 𝑀 ≤ 𝑀) |
4 | | breq1 3992 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → (𝑘 ≤ 𝑀 ↔ 𝑀 ≤ 𝑀)) |
5 | | breq1 3992 |
. . . . . . . . 9
⊢ (𝑘 = 𝑀 → (𝑘 ≤ 𝑁 ↔ 𝑀 ≤ 𝑁)) |
6 | 4, 5 | bibi12d 234 |
. . . . . . . 8
⊢ (𝑘 = 𝑀 → ((𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁) ↔ (𝑀 ≤ 𝑀 ↔ 𝑀 ≤ 𝑁))) |
7 | 6 | rspcva 2832 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧
∀𝑘 ∈ ℤ
(𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁)) → (𝑀 ≤ 𝑀 ↔ 𝑀 ≤ 𝑁)) |
8 | 3, 7 | mpbid 146 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧
∀𝑘 ∈ ℤ
(𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁)) → 𝑀 ≤ 𝑁) |
9 | 8 | adantlr 474 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧
∀𝑘 ∈ ℤ
(𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁)) → 𝑀 ≤ 𝑁) |
10 | | zre 9216 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
11 | 10 | leidd 8433 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → 𝑁 ≤ 𝑁) |
12 | 11 | adantr 274 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧
∀𝑘 ∈ ℤ
(𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁)) → 𝑁 ≤ 𝑁) |
13 | | breq1 3992 |
. . . . . . . . 9
⊢ (𝑘 = 𝑁 → (𝑘 ≤ 𝑀 ↔ 𝑁 ≤ 𝑀)) |
14 | | breq1 3992 |
. . . . . . . . 9
⊢ (𝑘 = 𝑁 → (𝑘 ≤ 𝑁 ↔ 𝑁 ≤ 𝑁)) |
15 | 13, 14 | bibi12d 234 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → ((𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁) ↔ (𝑁 ≤ 𝑀 ↔ 𝑁 ≤ 𝑁))) |
16 | 15 | rspcva 2832 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧
∀𝑘 ∈ ℤ
(𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁)) → (𝑁 ≤ 𝑀 ↔ 𝑁 ≤ 𝑁)) |
17 | 12, 16 | mpbird 166 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧
∀𝑘 ∈ ℤ
(𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁)) → 𝑁 ≤ 𝑀) |
18 | 17 | adantll 473 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧
∀𝑘 ∈ ℤ
(𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁)) → 𝑁 ≤ 𝑀) |
19 | 9, 18 | jca 304 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧
∀𝑘 ∈ ℤ
(𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁)) → (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)) |
20 | 19 | ex 114 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(∀𝑘 ∈ ℤ
(𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁) → (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀))) |
21 | | letri3 8000 |
. . . 4
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀))) |
22 | 1, 10, 21 | syl2an 287 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀))) |
23 | 20, 22 | sylibrd 168 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(∀𝑘 ∈ ℤ
(𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁) → 𝑀 = 𝑁)) |
24 | 23 | 3impia 1195 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧
∀𝑘 ∈ ℤ
(𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁)) → 𝑀 = 𝑁) |