Proof of Theorem algcvgblem
Step | Hyp | Ref
| Expression |
1 | | imor 428 |
. . . . 5
⊢ ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ (¬ 𝑁 ≠ 0 ∨ 𝑁 < 𝑀)) |
2 | | 0re 10040 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
3 | | nn0re 11301 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
4 | 3 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑀 ∈ ℝ) |
5 | | ltnle 10117 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ 𝑀
∈ ℝ) → (0 < 𝑀 ↔ ¬ 𝑀 ≤ 0)) |
6 | 2, 4, 5 | sylancr 695 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (0 < 𝑀 ↔ ¬ 𝑀 ≤ 0)) |
7 | | nn0le0eq0 11321 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ0
→ (𝑀 ≤ 0 ↔
𝑀 = 0)) |
8 | 7 | notbid 308 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ0
→ (¬ 𝑀 ≤ 0
↔ ¬ 𝑀 =
0)) |
9 | 8 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (¬ 𝑀 ≤ 0 ↔ ¬ 𝑀 = 0)) |
10 | 6, 9 | bitrd 268 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (0 < 𝑀 ↔ ¬ 𝑀 = 0)) |
11 | | df-ne 2795 |
. . . . . . . . . . 11
⊢ (𝑀 ≠ 0 ↔ ¬ 𝑀 = 0) |
12 | 10, 11 | syl6bbr 278 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (0 < 𝑀 ↔ 𝑀 ≠ 0)) |
13 | 12 | anbi2d 740 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((¬ 𝑁 ≠ 0 ∧ 0 < 𝑀) ↔ (¬ 𝑁 ≠ 0 ∧ 𝑀 ≠ 0))) |
14 | | nne 2798 |
. . . . . . . . . . 11
⊢ (¬
𝑁 ≠ 0 ↔ 𝑁 = 0) |
15 | | breq1 4656 |
. . . . . . . . . . 11
⊢ (𝑁 = 0 → (𝑁 < 𝑀 ↔ 0 < 𝑀)) |
16 | 14, 15 | sylbi 207 |
. . . . . . . . . 10
⊢ (¬
𝑁 ≠ 0 → (𝑁 < 𝑀 ↔ 0 < 𝑀)) |
17 | 16 | biimpar 502 |
. . . . . . . . 9
⊢ ((¬
𝑁 ≠ 0 ∧ 0 < 𝑀) → 𝑁 < 𝑀) |
18 | 13, 17 | syl6bir 244 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((¬ 𝑁 ≠ 0 ∧ 𝑀 ≠ 0) → 𝑁 < 𝑀)) |
19 | 18 | expd 452 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (¬ 𝑁 ≠ 0 → (𝑀 ≠ 0 → 𝑁 < 𝑀))) |
20 | | ax-1 6 |
. . . . . . 7
⊢ (𝑁 < 𝑀 → (𝑀 ≠ 0 → 𝑁 < 𝑀)) |
21 | 19, 20 | jctir 561 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((¬ 𝑁 ≠ 0 → (𝑀 ≠ 0 → 𝑁 < 𝑀)) ∧ (𝑁 < 𝑀 → (𝑀 ≠ 0 → 𝑁 < 𝑀)))) |
22 | | jaob 822 |
. . . . . 6
⊢ (((¬
𝑁 ≠ 0 ∨ 𝑁 < 𝑀) → (𝑀 ≠ 0 → 𝑁 < 𝑀)) ↔ ((¬ 𝑁 ≠ 0 → (𝑀 ≠ 0 → 𝑁 < 𝑀)) ∧ (𝑁 < 𝑀 → (𝑀 ≠ 0 → 𝑁 < 𝑀)))) |
23 | 21, 22 | sylibr 224 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((¬ 𝑁 ≠ 0 ∨ 𝑁 < 𝑀) → (𝑀 ≠ 0 → 𝑁 < 𝑀))) |
24 | 1, 23 | syl5bi 232 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) → (𝑀 ≠ 0 → 𝑁 < 𝑀))) |
25 | | nn0ge0 11318 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
26 | 25 | adantl 482 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 0 ≤ 𝑁) |
27 | | nn0re 11301 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
28 | | lelttr 10128 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝑁
∈ ℝ ∧ 𝑀
∈ ℝ) → ((0 ≤ 𝑁 ∧ 𝑁 < 𝑀) → 0 < 𝑀)) |
29 | 2, 28 | mp3an1 1411 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((0 ≤
𝑁 ∧ 𝑁 < 𝑀) → 0 < 𝑀)) |
30 | 27, 3, 29 | syl2anr 495 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((0 ≤ 𝑁 ∧ 𝑁 < 𝑀) → 0 < 𝑀)) |
31 | 26, 30 | mpand 711 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 < 𝑀 → 0 < 𝑀)) |
32 | 31, 12 | sylibd 229 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 < 𝑀 → 𝑀 ≠ 0)) |
33 | 32 | imim2d 57 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) → (𝑁 ≠ 0 → 𝑀 ≠ 0))) |
34 | 24, 33 | jcad 555 |
. . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) → ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑁 ≠ 0 → 𝑀 ≠ 0)))) |
35 | | pm3.34 610 |
. . 3
⊢ (((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑁 ≠ 0 → 𝑀 ≠ 0)) → (𝑁 ≠ 0 → 𝑁 < 𝑀)) |
36 | 34, 35 | impbid1 215 |
. 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑁 ≠ 0 → 𝑀 ≠ 0)))) |
37 | | con34b 306 |
. . . 4
⊢ ((𝑀 = 0 → 𝑁 = 0) ↔ (¬ 𝑁 = 0 → ¬ 𝑀 = 0)) |
38 | | df-ne 2795 |
. . . . 5
⊢ (𝑁 ≠ 0 ↔ ¬ 𝑁 = 0) |
39 | 38, 11 | imbi12i 340 |
. . . 4
⊢ ((𝑁 ≠ 0 → 𝑀 ≠ 0) ↔ (¬ 𝑁 = 0 → ¬ 𝑀 = 0)) |
40 | 37, 39 | bitr4i 267 |
. . 3
⊢ ((𝑀 = 0 → 𝑁 = 0) ↔ (𝑁 ≠ 0 → 𝑀 ≠ 0)) |
41 | 40 | anbi2i 730 |
. 2
⊢ (((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑀 = 0 → 𝑁 = 0)) ↔ ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑁 ≠ 0 → 𝑀 ≠ 0))) |
42 | 36, 41 | syl6bbr 278 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑀 = 0 → 𝑁 = 0)))) |