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	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1le1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1le1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	deg1le1.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	deg1le1.1	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 1 )
Assertion	deg1le1	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) ≤ 0 ∨ ( 𝐷 ‘ 𝐹 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		deg1le1.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1le1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1le1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		deg1le1.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
5		deg1le1.1	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ≤ 1 )
6		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( 𝐷 ‘ 𝐹 ) = 0 ) → ( 𝐷 ‘ 𝐹 ) = 0 )
7		0le0	⊢ 0 ≤ 0
8	6 7	eqbrtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( 𝐷 ‘ 𝐹 ) = 0 ) → ( 𝐷 ‘ 𝐹 ) ≤ 0 )
9		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) ∧ ( 𝐷 ‘ 𝐹 ) = 1 ) → ( 𝐷 ‘ 𝐹 ) = 1 )
10		simpr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
11		1nn0	⊢ 1 ∈ ℕ0
12	11	a1i	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) → 1 ∈ ℕ0 )
13	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) → ( 𝐷 ‘ 𝐹 ) ≤ 1 )
14		nn0leltp1	⊢ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 1 ↔ ( 𝐷 ‘ 𝐹 ) < ( 1 + 1 ) ) )
15	14	biimpa	⊢ ( ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 𝐷 ‘ 𝐹 ) ≤ 1 ) → ( 𝐷 ‘ 𝐹 ) < ( 1 + 1 ) )
16	10 12 13 15	syl21anc	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) → ( 𝐷 ‘ 𝐹 ) < ( 1 + 1 ) )
17		1p1e2	⊢ ( 1 + 1 ) = 2
18	16 17	breqtrdi	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) → ( 𝐷 ‘ 𝐹 ) < 2 )
19		nn0lt2	⊢ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ∧ ( 𝐷 ‘ 𝐹 ) < 2 ) → ( ( 𝐷 ‘ 𝐹 ) = 0 ∨ ( 𝐷 ‘ 𝐹 ) = 1 ) )
20	10 18 19	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) → ( ( 𝐷 ‘ 𝐹 ) = 0 ∨ ( 𝐷 ‘ 𝐹 ) = 1 ) )
21	8 9 20	orim12da	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 0 ∨ ( 𝐷 ‘ 𝐹 ) = 1 ) )
22		simpr	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = -∞ ) → ( 𝐷 ‘ 𝐹 ) = -∞ )
23		0xr	⊢ 0 ∈ ℝ*
24	23	a1i	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = -∞ ) → 0 ∈ ℝ* )
25	24	mnfled	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = -∞ ) → -∞ ≤ 0 )
26	22 25	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = -∞ ) → ( 𝐷 ‘ 𝐹 ) ≤ 0 )
27	26	orcd	⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐹 ) = -∞ ) → ( ( 𝐷 ‘ 𝐹 ) ≤ 0 ∨ ( 𝐷 ‘ 𝐹 ) = 1 ) )
28	1 2 3	deg1cl	⊢ ( 𝐹 ∈ 𝐵 → ( 𝐷 ‘ 𝐹 ) ∈ ( ℕ0 ∪ { -∞ } ) )
29		elunsn	⊢ ( ( 𝐷 ‘ 𝐹 ) ∈ ( ℕ0 ∪ { -∞ } ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ( ℕ0 ∪ { -∞ } ) ↔ ( ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ∨ ( 𝐷 ‘ 𝐹 ) = -∞ ) ) )
30	29	ibi	⊢ ( ( 𝐷 ‘ 𝐹 ) ∈ ( ℕ0 ∪ { -∞ } ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ∨ ( 𝐷 ‘ 𝐹 ) = -∞ ) )
31	4 28 30	3syl	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ∨ ( 𝐷 ‘ 𝐹 ) = -∞ ) )
32	21 27 31	mpjaodan	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐹 ) ≤ 0 ∨ ( 𝐷 ‘ 𝐹 ) = 1 ) )