P. 129 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12801-12900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	9p9e18 12801	9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 9) = ;18
Theorem	10p10e20 12802	10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (;10 + ;10) = ;20
Theorem	10m1e9 12803	10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
⊢ (;10 − 1) = 9
Theorem	4t3lem 12804	Lemma for 4t3e12 12805 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 = (𝐵 + 1)    &   ⊢ (𝐴 · 𝐵) = 𝐷    &   ⊢ (𝐷 + 𝐴) = 𝐸    ⇒   ⊢ (𝐴 · 𝐶) = 𝐸
Theorem	4t3e12 12805	4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (4 · 3) = ;12
Theorem	4t4e16 12806	4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (4 · 4) = ;16
Theorem	5t2e10 12807	5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 4-Sep-2021.)
⊢ (5 · 2) = ;10
Theorem	5t3e15 12808	5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (5 · 3) = ;15
Theorem	5t4e20 12809	5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (5 · 4) = ;20
Theorem	5t5e25 12810	5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (5 · 5) = ;25
Theorem	6t2e12 12811	6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 2) = ;12
Theorem	6t3e18 12812	6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 3) = ;18
Theorem	6t4e24 12813	6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 4) = ;24
Theorem	6t5e30 12814	6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (6 · 5) = ;30
Theorem	6t6e36 12815	6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (6 · 6) = ;36
Theorem	7t2e14 12816	7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 2) = ;14
Theorem	7t3e21 12817	7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 3) = ;21
Theorem	7t4e28 12818	7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 4) = ;28
Theorem	7t5e35 12819	7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 5) = ;35
Theorem	7t6e42 12820	7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 6) = ;42
Theorem	7t7e49 12821	7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 7) = ;49
Theorem	8t2e16 12822	8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 2) = ;16
Theorem	8t3e24 12823	8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 3) = ;24
Theorem	8t4e32 12824	8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 4) = ;32
Theorem	8t5e40 12825	8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (8 · 5) = ;40
Theorem	8t6e48 12826	8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (8 · 6) = ;48
Theorem	8t7e56 12827	8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 7) = ;56
Theorem	8t8e64 12828	8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 8) = ;64
Theorem	9t2e18 12829	9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 2) = ;18
Theorem	9t3e27 12830	9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 3) = ;27
Theorem	9t4e36 12831	9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 4) = ;36
Theorem	9t5e45 12832	9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 5) = ;45
Theorem	9t6e54 12833	9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 6) = ;54
Theorem	9t7e63 12834	9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 7) = ;63
Theorem	9t8e72 12835	9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 8) = ;72
Theorem	9t9e81 12836	9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 9) = ;81
Theorem	9t11e99 12837	9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ (9 · ;11) = ;99
Theorem	9t11e99OLD 12838	Obsolete version of 9t11e99 12837 as of 10-Jun-2026. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (9 · ;11) = ;99
Theorem	9lt10 12839	9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 9 < ;10
Theorem	8lt10 12840	8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 8 < ;10
Theorem	7lt10 12841	7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 7 < ;10
Theorem	6lt10 12842	6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 6 < ;10
Theorem	5lt10 12843	5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 5 < ;10
Theorem	4lt10 12844	4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 4 < ;10
Theorem	3lt10 12845	3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 3 < ;10
Theorem	2lt10 12846	2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 2 < ;10
Theorem	1lt10 12847	1 is less than 10. (Contributed by NM, 7-Nov-2012.) (Revised by Mario Carneiro, 9-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 1 < ;10
Theorem	1lt10OLD 12848	Obsolete version of 1lt10 12847 as of 10-Jun-2026. (Contributed by NM, 7-Nov-2012.) (Revised by Mario Carneiro, 9-Mar-2015.) (Revised by AV, 8-Sep-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 1 < ;10
Theorem	decbin0 12849	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (4 · 𝐴) = (2 · (2 · 𝐴))
Theorem	decbin2 12850	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1))
Theorem	decbin3 12851	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1)
Theorem	5recm6rec 12852	One fifth minus one sixth. (Contributed by Scott Fenton, 9-Jan-2017.)
⊢ ((1 / 5) − (1 / 6)) = (1 / ;30)
5.4.11  Upper sets of integers
Syntax	cuz 12853	Extend class notation with the upper integer function. Read "ℤ≥‘𝑀 " as "the set of integers greater than or equal to 𝑀".
class ℤ≥
Definition	df-uz 12854*	Define a function whose value at 𝑗 is the semi-infinite set of contiguous integers starting at 𝑗, which we will also call the upper integers starting at 𝑗. Read "ℤ≥‘𝑀 " as "the set of integers greater than or equal to 𝑀". See uzval 12855 for its value, uzssz 12874 for its relationship to ℤ, nnuz 12892 and nn0uz 12891 for its relationships to ℕ and ℕ0, and eluz1 12857 and eluz2 12859 for its membership relations. (Contributed by NM, 5-Sep-2005.)
⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘})
Theorem	uzval 12855*	The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝑁 ∈ ℤ → (ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘})
Theorem	uzf 12856	The domain and codomain of the upper integers function. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ℤ≥:ℤ⟶𝒫 ℤ
Theorem	eluz1 12857	Membership in the upper set of integers starting at 𝑀. (Contributed by NM, 5-Sep-2005.)
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
Theorem	eluzel2 12858	Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
Theorem	eluz2 12859	Membership in an upper set of integers. We use the fact that a function's value (under our function value definition) is empty outside of its domain to show 𝑀 ∈ ℤ. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
Theorem	eluzmn 12860	Membership in an earlier upper set of integers. (Contributed by Thierry Arnoux, 8-Oct-2018.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ (ℤ≥‘(𝑀 − 𝑁)))
Theorem	eluz1i 12861	Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005.)
⊢ 𝑀 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
Theorem	eluzuzle 12862	An integer in an upper set of integers is an element of an upper set of integers with a smaller bound. (Contributed by Alexander van der Vekens, 17-Jun-2018.)
⊢ ((𝐵 ∈ ℤ ∧ 𝐵 ≤ 𝐴) → (𝐶 ∈ (ℤ≥‘𝐴) → 𝐶 ∈ (ℤ≥‘𝐵)))
Theorem	eluzelz 12863	A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
Theorem	eluzelre 12864	A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ)
Theorem	eluzelcn 12865	A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ)
Theorem	eluzle 12866	Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁)
Theorem	eluz 12867	Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁))
Theorem	uzid 12868	Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.)
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
Theorem	uzidd 12869	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀))
Theorem	uzn0 12870	The upper integers are all nonempty. (Contributed by Mario Carneiro, 16-Jan-2014.)
⊢ (𝑀 ∈ ran ℤ≥ → 𝑀 ≠ ∅)
Theorem	uztrn 12871	Transitive law for sets of upper integers. (Contributed by NM, 20-Sep-2005.)
⊢ ((𝑀 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝑁))
Theorem	uztrn2 12872	Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝐾)    ⇒   ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍)
Theorem	uzneg 12873	Contraposition law for upper integers. (Contributed by NM, 28-Nov-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → -𝑀 ∈ (ℤ≥‘-𝑁))
Theorem	uzssz 12874	An upper set of integers is a subset of all integers. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (ℤ≥‘𝑀) ⊆ ℤ
Theorem	uzssre 12875	An upper set of integers is a subset of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (ℤ≥‘𝑀) ⊆ ℝ
Theorem	uzss 12876	Subset relationship for two sets of upper integers. (Contributed by NM, 5-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝑀))
Theorem	uztric 12877	Totality of the ordering relation on integers, stated in terms of upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 25-Jun-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ∨ 𝑀 ∈ (ℤ≥‘𝑁)))
Theorem	uz11 12878	The upper integers function is one-to-one. (Contributed by NM, 12-Dec-2005.)
⊢ (𝑀 ∈ ℤ → ((ℤ≥‘𝑀) = (ℤ≥‘𝑁) ↔ 𝑀 = 𝑁))
Theorem	eluzp1m1 12879	Membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈ (ℤ≥‘𝑀))
Theorem	eluzp1l 12880	Strict ordering implied by membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁)
Theorem	eluzp1p1 12881	Membership in the next upper set of integers. (Contributed by NM, 5-Oct-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘(𝑀 + 1)))
Theorem	eluzadd 12882	Membership in a later upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by SN, 7-Feb-2025.)
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾)))
Theorem	eluzsub 12883	Membership in an earlier upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by SN, 7-Feb-2025.)
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾))) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀))
Theorem	eluzaddi 12884	Membership in a later upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.) Shorten and remove 𝑀 ∈ ℤ hypothesis. (Revised by SN, 7-Feb-2025.)
⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾)))
Theorem	eluzsubi 12885	Membership in an earlier upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.) (Proof shortened by SN, 7-Feb-2025.)
⊢ 𝑀 ∈ ℤ    &   ⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾)) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀))
Theorem	subeluzsub 12886	Membership of a difference in an earlier upper set of integers. (Contributed by AV, 10-May-2022.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → (𝑀 − 𝐾) ∈ (ℤ≥‘(𝑀 − 𝑁)))
Theorem	uzm1 12887	Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈ (ℤ≥‘𝑀)))
Theorem	uznn0sub 12888	The nonnegative difference of integers is a nonnegative integer. (Contributed by NM, 4-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 − 𝑀) ∈ ℕ0)
Theorem	uzin 12889	Intersection of two upper intervals of integers. (Contributed by Mario Carneiro, 24-Dec-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) = (ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀)))
Theorem	uzp1 12890	Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))))
Theorem	nn0uz 12891	Nonnegative integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
⊢ ℕ0 = (ℤ≥‘0)
Theorem	nnuz 12892	Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
⊢ ℕ = (ℤ≥‘1)
Theorem	elnnuz 12893	A positive integer expressed as a member of an upper set of integers. (Contributed by NM, 6-Jun-2006.)
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ≥‘1))
Theorem	elnn0uz 12894	A nonnegative integer expressed as a member an upper set of integers. (Contributed by NM, 6-Jun-2006.)
⊢ (𝑁 ∈ ℕ0 ↔ 𝑁 ∈ (ℤ≥‘0))
Theorem	1eluzge0 12895	1 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
⊢ 1 ∈ (ℤ≥‘0)
Theorem	2eluzge0 12896	2 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ 2 ∈ (ℤ≥‘0)
Theorem	2eluzge1 12897	2 is an integer greater than or equal to 1. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
⊢ 2 ∈ (ℤ≥‘1)
Theorem	5eluz3 12898	5 is an integer greater than or equal to 3. (Contributed by AV, 7-Sep-2025.)
⊢ 5 ∈ (ℤ≥‘3)
Theorem	uzuzle23 12899	An integer greater than or equal to 3 is an integer greater than or equal to 2. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
⊢ (𝐴 ∈ (ℤ≥‘3) → 𝐴 ∈ (ℤ≥‘2))
Theorem	uzuzle24 12900	An integer greater than or equal to 4 is an integer greater than or equal to 2. (Contributed by AV, 30-May-2023.)
⊢ (𝑋 ∈ (ℤ≥‘4) → 𝑋 ∈ (ℤ≥‘2))