P. 116 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 11501-11600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	9p7e16 11501	9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 7) = ;16
Theorem	9p8e17 11502	9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 8) = ;17
Theorem	9p9e18 11503	9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 9) = ;18
Theorem	10p10e20 11504	10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (;10 + ;10) = ;20
Theorem	10p10e20OLD 11505	Obsolete version of 10p10e20 11504 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (10 + 10) = ;20
Theorem	10m1e9 11506	10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
⊢ (;10 − 1) = 9
Theorem	4t3lem 11507	Lemma for 4t3e12 11508 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 = (𝐵 + 1)    &   ⊢ (𝐴 · 𝐵) = 𝐷    &   ⊢ (𝐷 + 𝐴) = 𝐸    ⇒   ⊢ (𝐴 · 𝐶) = 𝐸
Theorem	4t3e12 11508	4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (4 · 3) = ;12
Theorem	4t4e16 11509	4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (4 · 4) = ;16
Theorem	5t2e10 11510	5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 4-Sep-2021.)
⊢ (5 · 2) = ;10
Theorem	5t3e15 11511	5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (5 · 3) = ;15
Theorem	5t3e15OLD 11512	Obsolete proof of 5t3e15 11511 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (5 · 3) = ;15
Theorem	5t4e20 11513	5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (5 · 4) = ;20
Theorem	5t4e20OLD 11514	Obsolete proof of 5t4e20 11513 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (5 · 4) = ;20
Theorem	5t5e25 11515	5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (5 · 5) = ;25
Theorem	5t5e25OLD 11516	Obsolete proof of 5t5e25 11515 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (5 · 5) = ;25
Theorem	6t2e12 11517	6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 2) = ;12
Theorem	6t3e18 11518	6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 3) = ;18
Theorem	6t4e24 11519	6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 4) = ;24
Theorem	6t5e30 11520	6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (6 · 5) = ;30
Theorem	6t5e30OLD 11521	Obsolete proof of 6t5e30 11520 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (6 · 5) = ;30
Theorem	6t6e36 11522	6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (6 · 6) = ;36
Theorem	6t6e36OLD 11523	Obsolete proof of 6t6e36 11522 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (6 · 6) = ;36
Theorem	7t2e14 11524	7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 2) = ;14
Theorem	7t3e21 11525	7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 3) = ;21
Theorem	7t4e28 11526	7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 4) = ;28
Theorem	7t5e35 11527	7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 5) = ;35
Theorem	7t6e42 11528	7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 6) = ;42
Theorem	7t7e49 11529	7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 7) = ;49
Theorem	8t2e16 11530	8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 2) = ;16
Theorem	8t3e24 11531	8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 3) = ;24
Theorem	8t4e32 11532	8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 4) = ;32
Theorem	8t5e40 11533	8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (8 · 5) = ;40
Theorem	8t5e40OLD 11534	Obsolete proof of 8t5e40 11533 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (8 · 5) = ;40
Theorem	8t6e48 11535	8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (8 · 6) = ;48
Theorem	8t6e48OLD 11536	Obsolete proof of 8t6e48 11535 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (8 · 6) = ;48
Theorem	8t7e56 11537	8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 7) = ;56
Theorem	8t8e64 11538	8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 8) = ;64
Theorem	9t2e18 11539	9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 2) = ;18
Theorem	9t3e27 11540	9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 3) = ;27
Theorem	9t4e36 11541	9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 4) = ;36
Theorem	9t5e45 11542	9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 5) = ;45
Theorem	9t6e54 11543	9 times 6 equals 54. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 6) = ;54
Theorem	9t7e63 11544	9 times 7 equals 63. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 7) = ;63
Theorem	9t8e72 11545	9 times 8 equals 72. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 8) = ;72
Theorem	9t9e81 11546	9 times 9 equals 81. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 9) = ;81
Theorem	9t11e99 11547	9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.)
⊢ (9 · ;11) = ;99
Theorem	9t11e99OLD 11548	Obsolete proof of 9t11e99 11547 as of 6-Sep-2021. (Contributed by AV, 14-Jun-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (9 · ;11) = ;99
Theorem	9lt10 11549	9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 9 < ;10
Theorem	8lt10 11550	8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 8 < ;10
Theorem	7lt10 11551	7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 7 < ;10
Theorem	6lt10 11552	6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 6 < ;10
Theorem	5lt10 11553	5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 5 < ;10
Theorem	4lt10 11554	4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 4 < ;10
Theorem	3lt10 11555	3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 3 < ;10
Theorem	2lt10 11556	2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 2 < ;10
Theorem	1lt10 11557	1 is less than 10. (Contributed by NM, 7-Nov-2012.) (Revised by Mario Carneiro, 9-Mar-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 1 < ;10
Theorem	decbin0 11558	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (4 · 𝐴) = (2 · (2 · 𝐴))
Theorem	decbin2 11559	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((4 · 𝐴) + 2) = (2 · ((2 · 𝐴) + 1))
Theorem	decbin3 11560	Decompose base 4 into base 2. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((4 · 𝐴) + 3) = ((2 · ((2 · 𝐴) + 1)) + 1)
Theorem	halfthird 11561	Half minus a third. (Contributed by Scott Fenton, 8-Jul-2015.)
⊢ ((1 / 2) − (1 / 3)) = (1 / 6)
Theorem	5recm6rec 11562	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 11563	Extend class notation with the upper integer function. Read "ℤ≥‘𝑀 " as "the set of integers greater than or equal to 𝑀."
class ℤ≥
Definition	df-uz 11564*	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 11565 for its value, uzssz 11583 for its relationship to ℤ, nnuz 11599 and nn0uz 11598 for its relationships to ℕ and ℕ0, and eluz1 11567 and eluz2 11569 for its membership relations. (Contributed by NM, 5-Sep-2005.)
⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘})
Theorem	uzval 11565*	The value of the upper integers function. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝑁 ∈ ℤ → (ℤ≥‘𝑁) = {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘})
Theorem	uzf 11566	The domain and range of the upper integers function. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ ℤ≥:ℤ⟶𝒫 ℤ
Theorem	eluz1 11567	Membership in the upper set of integers starting at 𝑀. (Contributed by NM, 5-Sep-2005.)
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
Theorem	eluzel2 11568	Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
Theorem	eluz2 11569	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 11570	Membership in an earlier upper set of integers. (Contributed by Thierry Arnoux, 8-Oct-2018.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ (ℤ≥‘(𝑀 − 𝑁)))
Theorem	eluz1i 11571	Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005.)
⊢ 𝑀 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
Theorem	eluzuzle 11572	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 11573	A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
Theorem	eluzelre 11574	A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ)
Theorem	eluzelcn 11575	A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ)
Theorem	eluzle 11576	Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁)
Theorem	eluz 11577	Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁))
Theorem	uzid 11578	Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.)
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
Theorem	uzn0 11579	The upper integers are all nonempty. (Contributed by Mario Carneiro, 16-Jan-2014.)
⊢ (𝑀 ∈ ran ℤ≥ → 𝑀 ≠ ∅)
Theorem	uztrn 11580	Transitive law for sets of upper integers. (Contributed by NM, 20-Sep-2005.)
⊢ ((𝑀 ∈ (ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝑁))
Theorem	uztrn2 11581	Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝐾)    ⇒   ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍)
Theorem	uzneg 11582	Contraposition law for upper integers. (Contributed by NM, 28-Nov-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → -𝑀 ∈ (ℤ≥‘-𝑁))
Theorem	uzssz 11583	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	uzss 11584	Subset relationship for two sets of upper integers. (Contributed by NM, 5-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝑀))
Theorem	uztric 11585	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 11586	The upper integers function is one-to-one. (Contributed by NM, 12-Dec-2005.)
⊢ (𝑀 ∈ ℤ → ((ℤ≥‘𝑀) = (ℤ≥‘𝑁) ↔ 𝑀 = 𝑁))
Theorem	eluzp1m1 11587	Membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈ (ℤ≥‘𝑀))
Theorem	eluzp1l 11588	Strict ordering implied by membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁)
Theorem	eluzp1p1 11589	Membership in the next upper set of integers. (Contributed by NM, 5-Oct-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘(𝑀 + 1)))
Theorem	eluzaddi 11590	Membership in a later upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.)
⊢ 𝑀 ∈ ℤ    &   ⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾)))
Theorem	eluzsubi 11591	Membership in an earlier upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.)
⊢ 𝑀 ∈ ℤ    &   ⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾)) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀))
Theorem	eluzadd 11592	Membership in a later upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ (ℤ≥‘(𝑀 + 𝐾)))
Theorem	eluzsub 11593	Membership in an earlier upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 𝐾))) → (𝑁 − 𝐾) ∈ (ℤ≥‘𝑀))
Theorem	uzm1 11594	Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈ (ℤ≥‘𝑀)))
Theorem	uznn0sub 11595	The nonnegative difference of integers is a nonnegative integer. (Contributed by NM, 4-Sep-2005.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 − 𝑀) ∈ ℕ0)
Theorem	uzin 11596	Intersection of two upper intervals of integers. (Contributed by Mario Carneiro, 24-Dec-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((ℤ≥‘𝑀) ∩ (ℤ≥‘𝑁)) = (ℤ≥‘if(𝑀 ≤ 𝑁, 𝑁, 𝑀)))
Theorem	uzp1 11597	Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))))
Theorem	nn0uz 11598	Nonnegative integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
⊢ ℕ0 = (ℤ≥‘0)
Theorem	nnuz 11599	Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.)
⊢ ℕ = (ℤ≥‘1)
Theorem	elnnuz 11600	A positive integer expressed as a member of an upper set of integers. (Contributed by NM, 6-Jun-2006.)
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ≥‘1))