Metamath Proof Explorer

Theorem algcvgblem

Description: Lemma for algcvgb . (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Assertion algcvgblem ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 ≠ 0 → 𝑁 < 𝑀 ) ↔ ( ( 𝑀 ≠ 0 → 𝑁 < 𝑀 ) ∧ ( 𝑀 = 0 → 𝑁 = 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 imor ⊢ ( ( 𝑁 ≠ 0 → 𝑁 < 𝑀 ) ↔ ( ¬ 𝑁 ≠ 0 ∨ 𝑁 < 𝑀 ) )
2 0re ⊢ 0 ∈ ℝ
3 nn0re ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
4 3 adantr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
5 ltnle ⊢ ( ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 0 < 𝑀 ↔ ¬ 𝑀 ≤ 0 ) )
6 2 4 5 sylancr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 0 < 𝑀 ↔ ¬ 𝑀 ≤ 0 ) )
7 nn0le0eq0 ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 ≤ 0 ↔ 𝑀 = 0 ) )
8 7 notbid ⊢ ( 𝑀 ∈ ℕ0 → ( ¬ 𝑀 ≤ 0 ↔ ¬ 𝑀 = 0 ) )
9 8 adantr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ¬ 𝑀 ≤ 0 ↔ ¬ 𝑀 = 0 ) )
10 6 9 bitrd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 0 < 𝑀 ↔ ¬ 𝑀 = 0 ) )
11 df-ne ⊢ ( 𝑀 ≠ 0 ↔ ¬ 𝑀 = 0 )
12 10 11 bitr4di ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 0 < 𝑀 ↔ 𝑀 ≠ 0 ) )
13 12 anbi2d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ¬ 𝑁 ≠ 0 ∧ 0 < 𝑀 ) ↔ ( ¬ 𝑁 ≠ 0 ∧ 𝑀 ≠ 0 ) ) )
14 nne ⊢ ( ¬ 𝑁 ≠ 0 ↔ 𝑁 = 0 )
15 breq1 ⊢ ( 𝑁 = 0 → ( 𝑁 < 𝑀 ↔ 0 < 𝑀 ) )
16 14 15 sylbi ⊢ ( ¬ 𝑁 ≠ 0 → ( 𝑁 < 𝑀 ↔ 0 < 𝑀 ) )
17 16 biimpar ⊢ ( ( ¬ 𝑁 ≠ 0 ∧ 0 < 𝑀 ) → 𝑁 < 𝑀 )
18 13 17 syl6bir ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ¬ 𝑁 ≠ 0 ∧ 𝑀 ≠ 0 ) → 𝑁 < 𝑀 ) )
19 18 expd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ¬ 𝑁 ≠ 0 → ( 𝑀 ≠ 0 → 𝑁 < 𝑀 ) ) )
20 ax-1 ⊢ ( 𝑁 < 𝑀 → ( 𝑀 ≠ 0 → 𝑁 < 𝑀 ) )
21 jaob ⊢ ( ( ( ¬ 𝑁 ≠ 0 ∨ 𝑁 < 𝑀 ) → ( 𝑀 ≠ 0 → 𝑁 < 𝑀 ) ) ↔ ( ( ¬ 𝑁 ≠ 0 → ( 𝑀 ≠ 0 → 𝑁 < 𝑀 ) ) ∧ ( 𝑁 < 𝑀 → ( 𝑀 ≠ 0 → 𝑁 < 𝑀 ) ) ) )
22 19 20 21 sylanblrc ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ¬ 𝑁 ≠ 0 ∨ 𝑁 < 𝑀 ) → ( 𝑀 ≠ 0 → 𝑁 < 𝑀 ) ) )
23 1 22 syl5bi ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 ≠ 0 → 𝑁 < 𝑀 ) → ( 𝑀 ≠ 0 → 𝑁 < 𝑀 ) ) )
24 nn0ge0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
25 24 adantl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 0 ≤ 𝑁 )
26 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
27 lelttr ⊢ ( ( 0 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( 0 ≤ 𝑁 ∧ 𝑁 < 𝑀 ) → 0 < 𝑀 ) )
28 2 27 mp3an1 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( 0 ≤ 𝑁 ∧ 𝑁 < 𝑀 ) → 0 < 𝑀 ) )
29 26 3 28 syl2anr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 0 ≤ 𝑁 ∧ 𝑁 < 𝑀 ) → 0 < 𝑀 ) )
30 25 29 mpand ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 < 𝑀 → 0 < 𝑀 ) )
31 30 12 sylibd ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 < 𝑀 → 𝑀 ≠ 0 ) )
32 31 imim2d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 ≠ 0 → 𝑁 < 𝑀 ) → ( 𝑁 ≠ 0 → 𝑀 ≠ 0 ) ) )
33 23 32 jcad ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 ≠ 0 → 𝑁 < 𝑀 ) → ( ( 𝑀 ≠ 0 → 𝑁 < 𝑀 ) ∧ ( 𝑁 ≠ 0 → 𝑀 ≠ 0 ) ) ) )
34 pm3.34 ⊢ ( ( ( 𝑀 ≠ 0 → 𝑁 < 𝑀 ) ∧ ( 𝑁 ≠ 0 → 𝑀 ≠ 0 ) ) → ( 𝑁 ≠ 0 → 𝑁 < 𝑀 ) )
35 33 34 impbid1 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 ≠ 0 → 𝑁 < 𝑀 ) ↔ ( ( 𝑀 ≠ 0 → 𝑁 < 𝑀 ) ∧ ( 𝑁 ≠ 0 → 𝑀 ≠ 0 ) ) ) )
36 con34b ⊢ ( ( 𝑀 = 0 → 𝑁 = 0 ) ↔ ( ¬ 𝑁 = 0 → ¬ 𝑀 = 0 ) )
37 df-ne ⊢ ( 𝑁 ≠ 0 ↔ ¬ 𝑁 = 0 )
38 37 11 imbi12i ⊢ ( ( 𝑁 ≠ 0 → 𝑀 ≠ 0 ) ↔ ( ¬ 𝑁 = 0 → ¬ 𝑀 = 0 ) )
39 36 38 bitr4i ⊢ ( ( 𝑀 = 0 → 𝑁 = 0 ) ↔ ( 𝑁 ≠ 0 → 𝑀 ≠ 0 ) )
40 39 anbi2i ⊢ ( ( ( 𝑀 ≠ 0 → 𝑁 < 𝑀 ) ∧ ( 𝑀 = 0 → 𝑁 = 0 ) ) ↔ ( ( 𝑀 ≠ 0 → 𝑁 < 𝑀 ) ∧ ( 𝑁 ≠ 0 → 𝑀 ≠ 0 ) ) )
41 35 40 bitr4di ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 ≠ 0 → 𝑁 < 𝑀 ) ↔ ( ( 𝑀 ≠ 0 → 𝑁 < 𝑀 ) ∧ ( 𝑀 = 0 → 𝑁 = 0 ) ) ) )