Proof of Theorem algcvgblem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | imor 853 | . . . . 5
⊢ ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ (¬ 𝑁 ≠ 0 ∨ 𝑁 < 𝑀)) | 
| 2 |  | 0re 11264 | . . . . . . . . . . . 12
⊢ 0 ∈
ℝ | 
| 3 |  | nn0re 12537 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) | 
| 4 | 3 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑀 ∈ ℝ) | 
| 5 |  | ltnle 11341 | . . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 𝑀
∈ ℝ) → (0 < 𝑀 ↔ ¬ 𝑀 ≤ 0)) | 
| 6 | 2, 4, 5 | sylancr 587 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (0 < 𝑀 ↔ ¬ 𝑀 ≤ 0)) | 
| 7 |  | nn0le0eq0 12556 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ0
→ (𝑀 ≤ 0 ↔
𝑀 = 0)) | 
| 8 | 7 | notbid 318 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ0
→ (¬ 𝑀 ≤ 0
↔ ¬ 𝑀 =
0)) | 
| 9 | 8 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (¬ 𝑀 ≤ 0 ↔ ¬ 𝑀 = 0)) | 
| 10 | 6, 9 | bitrd 279 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (0 < 𝑀 ↔ ¬ 𝑀 = 0)) | 
| 11 |  | df-ne 2940 | . . . . . . . . . 10
⊢ (𝑀 ≠ 0 ↔ ¬ 𝑀 = 0) | 
| 12 | 10, 11 | bitr4di 289 | . . . . . . . . 9
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (0 < 𝑀 ↔ 𝑀 ≠ 0)) | 
| 13 | 12 | anbi2d 630 | . . . . . . . 8
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((¬ 𝑁 ≠ 0 ∧ 0 < 𝑀) ↔ (¬ 𝑁 ≠ 0 ∧ 𝑀 ≠ 0))) | 
| 14 |  | nne 2943 | . . . . . . . . . 10
⊢ (¬
𝑁 ≠ 0 ↔ 𝑁 = 0) | 
| 15 |  | breq1 5145 | . . . . . . . . . 10
⊢ (𝑁 = 0 → (𝑁 < 𝑀 ↔ 0 < 𝑀)) | 
| 16 | 14, 15 | sylbi 217 | . . . . . . . . 9
⊢ (¬
𝑁 ≠ 0 → (𝑁 < 𝑀 ↔ 0 < 𝑀)) | 
| 17 | 16 | biimpar 477 | . . . . . . . 8
⊢ ((¬
𝑁 ≠ 0 ∧ 0 < 𝑀) → 𝑁 < 𝑀) | 
| 18 | 13, 17 | biimtrrdi 254 | . . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((¬ 𝑁 ≠ 0 ∧ 𝑀 ≠ 0) → 𝑁 < 𝑀)) | 
| 19 | 18 | expd 415 | . . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (¬ 𝑁 ≠ 0 → (𝑀 ≠ 0 → 𝑁 < 𝑀))) | 
| 20 |  | ax-1 6 | . . . . . 6
⊢ (𝑁 < 𝑀 → (𝑀 ≠ 0 → 𝑁 < 𝑀)) | 
| 21 |  | jaob 963 | . . . . . 6
⊢ (((¬
𝑁 ≠ 0 ∨ 𝑁 < 𝑀) → (𝑀 ≠ 0 → 𝑁 < 𝑀)) ↔ ((¬ 𝑁 ≠ 0 → (𝑀 ≠ 0 → 𝑁 < 𝑀)) ∧ (𝑁 < 𝑀 → (𝑀 ≠ 0 → 𝑁 < 𝑀)))) | 
| 22 | 19, 20, 21 | sylanblrc 590 | . . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((¬ 𝑁 ≠ 0 ∨ 𝑁 < 𝑀) → (𝑀 ≠ 0 → 𝑁 < 𝑀))) | 
| 23 | 1, 22 | biimtrid 242 | . . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) → (𝑀 ≠ 0 → 𝑁 < 𝑀))) | 
| 24 |  | nn0ge0 12553 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) | 
| 25 | 24 | adantl 481 | . . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 0 ≤ 𝑁) | 
| 26 |  | nn0re 12537 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) | 
| 27 |  | lelttr 11352 | . . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝑁
∈ ℝ ∧ 𝑀
∈ ℝ) → ((0 ≤ 𝑁 ∧ 𝑁 < 𝑀) → 0 < 𝑀)) | 
| 28 | 2, 27 | mp3an1 1449 | . . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((0 ≤
𝑁 ∧ 𝑁 < 𝑀) → 0 < 𝑀)) | 
| 29 | 26, 3, 28 | syl2anr 597 | . . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((0 ≤ 𝑁 ∧ 𝑁 < 𝑀) → 0 < 𝑀)) | 
| 30 | 25, 29 | mpand 695 | . . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 < 𝑀 → 0 < 𝑀)) | 
| 31 | 30, 12 | sylibd 239 | . . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 < 𝑀 → 𝑀 ≠ 0)) | 
| 32 | 31 | imim2d 57 | . . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) → (𝑁 ≠ 0 → 𝑀 ≠ 0))) | 
| 33 | 23, 32 | jcad 512 | . . 3
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) → ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑁 ≠ 0 → 𝑀 ≠ 0)))) | 
| 34 |  | pm3.34 765 | . . 3
⊢ (((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑁 ≠ 0 → 𝑀 ≠ 0)) → (𝑁 ≠ 0 → 𝑁 < 𝑀)) | 
| 35 | 33, 34 | impbid1 225 | . 2
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑁 ≠ 0 → 𝑀 ≠ 0)))) | 
| 36 |  | con34b 316 | . . . 4
⊢ ((𝑀 = 0 → 𝑁 = 0) ↔ (¬ 𝑁 = 0 → ¬ 𝑀 = 0)) | 
| 37 |  | df-ne 2940 | . . . . 5
⊢ (𝑁 ≠ 0 ↔ ¬ 𝑁 = 0) | 
| 38 | 37, 11 | imbi12i 350 | . . . 4
⊢ ((𝑁 ≠ 0 → 𝑀 ≠ 0) ↔ (¬ 𝑁 = 0 → ¬ 𝑀 = 0)) | 
| 39 | 36, 38 | bitr4i 278 | . . 3
⊢ ((𝑀 = 0 → 𝑁 = 0) ↔ (𝑁 ≠ 0 → 𝑀 ≠ 0)) | 
| 40 | 39 | anbi2i 623 | . 2
⊢ (((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑀 = 0 → 𝑁 = 0)) ↔ ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑁 ≠ 0 → 𝑀 ≠ 0))) | 
| 41 | 35, 40 | bitr4di 289 | 1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑀 = 0 → 𝑁 = 0)))) |