Metamath Proof Explorer

Theorem deg1le1

Description: Dichotomy for a univariate polynomial of degree at most one. (Contributed by Thierry Arnoux, 8-Nov-2026)

Ref Expression
Hypotheses deg1le1.d ⊢ D = deg 1 ⁡ R
deg1le1.p ⊢ P = Poly 1 ⁡ R
deg1le1.b ⊢ B = Base P
deg1le1.f ⊢ φ → F ∈ B
deg1le1.1 ⊢ φ → D ⁡ F ≤ 1
Assertion deg1le1 ⊢ φ → D ⁡ F ≤ 0 ∨ D ⁡ F = 1

Proof

Step Hyp Ref Expression
1 deg1le1.d ⊢ D = deg 1 ⁡ R
2 deg1le1.p ⊢ P = Poly 1 ⁡ R
3 deg1le1.b ⊢ B = Base P
4 deg1le1.f ⊢ φ → F ∈ B
5 deg1le1.1 ⊢ φ → D ⁡ F ≤ 1
6 simpr ⊢ φ ∧ D ⁡ F ∈ ℕ 0 ∧ D ⁡ F = 0 → D ⁡ F = 0
7 0le0 ⊢ 0 ≤ 0
8 6 7 eqbrtrdi ⊢ φ ∧ D ⁡ F ∈ ℕ 0 ∧ D ⁡ F = 0 → D ⁡ F ≤ 0
9 simpr ⊢ φ ∧ D ⁡ F ∈ ℕ 0 ∧ D ⁡ F = 1 → D ⁡ F = 1
10 simpr ⊢ φ ∧ D ⁡ F ∈ ℕ 0 → D ⁡ F ∈ ℕ 0
11 1nn0 ⊢ 1 ∈ ℕ 0
12 11 a1i ⊢ φ ∧ D ⁡ F ∈ ℕ 0 → 1 ∈ ℕ 0
13 5 adantr ⊢ φ ∧ D ⁡ F ∈ ℕ 0 → D ⁡ F ≤ 1
14 nn0leltp1 ⊢ D ⁡ F ∈ ℕ 0 ∧ 1 ∈ ℕ 0 → D ⁡ F ≤ 1 ↔ D ⁡ F < 1 + 1
15 14 biimpa ⊢ D ⁡ F ∈ ℕ 0 ∧ 1 ∈ ℕ 0 ∧ D ⁡ F ≤ 1 → D ⁡ F < 1 + 1
16 10 12 13 15 syl21anc ⊢ φ ∧ D ⁡ F ∈ ℕ 0 → D ⁡ F < 1 + 1
17 1p1e2 ⊢ 1 + 1 = 2
18 16 17 breqtrdi ⊢ φ ∧ D ⁡ F ∈ ℕ 0 → D ⁡ F < 2
19 nn0lt2 ⊢ D ⁡ F ∈ ℕ 0 ∧ D ⁡ F < 2 → D ⁡ F = 0 ∨ D ⁡ F = 1
20 10 18 19 syl2anc ⊢ φ ∧ D ⁡ F ∈ ℕ 0 → D ⁡ F = 0 ∨ D ⁡ F = 1
21 8 9 20 orim12da ⊢ φ ∧ D ⁡ F ∈ ℕ 0 → D ⁡ F ≤ 0 ∨ D ⁡ F = 1
22 simpr ⊢ φ ∧ D ⁡ F = −∞ → D ⁡ F = −∞
23 0xr ⊢ 0 ∈ ℝ *
24 23 a1i ⊢ φ ∧ D ⁡ F = −∞ → 0 ∈ ℝ *
25 24 mnfled ⊢ φ ∧ D ⁡ F = −∞ → −∞ ≤ 0
26 22 25 eqbrtrd ⊢ φ ∧ D ⁡ F = −∞ → D ⁡ F ≤ 0
27 26 orcd ⊢ φ ∧ D ⁡ F = −∞ → D ⁡ F ≤ 0 ∨ D ⁡ F = 1
28 1 2 3 deg1cl ⊢ F ∈ B → D ⁡ F ∈ ℕ 0 ∪ −∞
29 elunsn ⊢ D ⁡ F ∈ ℕ 0 ∪ −∞ → D ⁡ F ∈ ℕ 0 ∪ −∞ ↔ D ⁡ F ∈ ℕ 0 ∨ D ⁡ F = −∞
30 29 ibi ⊢ D ⁡ F ∈ ℕ 0 ∪ −∞ → D ⁡ F ∈ ℕ 0 ∨ D ⁡ F = −∞
31 4 28 30 3syl ⊢ φ → D ⁡ F ∈ ℕ 0 ∨ D ⁡ F = −∞
32 21 27 31 mpjaodan ⊢ φ → D ⁡ F ≤ 0 ∨ D ⁡ F = 1