P. 122 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12101-12200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lbinfle 12101*	If a set of reals contains a lower bound, its infimum is less than or equal to all members of the set. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 4-Sep-2020.)
⊢ ((𝑆 ⊆ ℝ ∧ ∃𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝑆) → inf(𝑆, ℝ, < ) ≤ 𝐴)
Theorem	sup2 12102*	A nonempty, bounded-above set of reals has a supremum. Stronger version of completeness axiom (it has a slightly weaker antecedent). (Contributed by NM, 19-Jan-1997.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	sup3 12103*	A version of the completeness axiom for reals. (Contributed by NM, 12-Oct-2004.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	infm3lem 12104*	Lemma for infm3 12105. (Contributed by NM, 14-Jun-2005.)
⊢ (𝑥 ∈ ℝ → ∃𝑦 ∈ ℝ 𝑥 = -𝑦)
Theorem	infm3 12105*	The completeness axiom for reals in terms of infimum: a nonempty, bounded-below set of reals has an infimum. (This theorem is the dual of sup3 12103.) (Contributed by NM, 14-Jun-2005.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
Theorem	suprcl 12106*	Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Oct-2004.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈ ℝ)
Theorem	suprub 12107*	A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Oct-2004.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐵 ∈ 𝐴) → 𝐵 ≤ sup(𝐴, ℝ, < ))
Theorem	suprubd 12108*	Natural deduction form of suprubd 12108. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < ))
Theorem	suprcld 12109*	Natural deduction form of suprcl 12106. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ ℝ)
Theorem	suprlub 12110*	The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (𝐵 < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 𝐵 < 𝑧))
Theorem	suprnub 12111*	An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Nov-2004.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (¬ 𝐵 < sup(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 ¬ 𝐵 < 𝑧))
Theorem	suprleub 12112*	The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (sup(𝐴, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝐵))
Theorem	supaddc 12113*	The supremum function distributes over addition in a sense similar to that in supmul1 12115. (Contributed by Brendan Leahy, 25-Sep-2017.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 𝑧 = (𝑣 + 𝐵)}    ⇒   ⊢ (𝜑 → (sup(𝐴, ℝ, < ) + 𝐵) = sup(𝐶, ℝ, < ))
Theorem	supadd 12114*	The supremum function distributes over addition in a sense similar to that in supmul 12118. (Contributed by Brendan Leahy, 26-Sep-2017.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥)    &   ⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑣 + 𝑏)}    ⇒   ⊢ (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ))
Theorem	supmul1 12115*	The supremum function distributes over multiplication, in the sense that 𝐴 · (sup𝐵) = sup(𝐴 · 𝐵), where 𝐴 · 𝐵 is shorthand for {𝐴 · 𝑏 ∣ 𝑏 ∈ 𝐵} and is defined as 𝐶 below. This is the simple version, with only one set argument; see supmul 12118 for the more general case with two set arguments. (Contributed by Mario Carneiro, 5-Jul-2013.)
⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐵 𝑧 = (𝐴 · 𝑣)}    &   ⊢ (𝜑 ↔ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀𝑥 ∈ 𝐵 0 ≤ 𝑥) ∧ (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥)))    ⇒   ⊢ (𝜑 → (𝐴 · sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ))
Theorem	supmullem1 12116*	Lemma for supmul 12118. (Contributed by Mario Carneiro, 5-Jul-2013.)
⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑣 · 𝑏)}    &   ⊢ (𝜑 ↔ ((∀𝑥 ∈ 𝐴 0 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐵 0 ≤ 𝑥) ∧ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥)))    ⇒   ⊢ (𝜑 → ∀𝑤 ∈ 𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) · sup(𝐵, ℝ, < )))
Theorem	supmullem2 12117*	Lemma for supmul 12118. (Contributed by Mario Carneiro, 5-Jul-2013.)
⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑣 · 𝑏)}    &   ⊢ (𝜑 ↔ ((∀𝑥 ∈ 𝐴 0 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐵 0 ≤ 𝑥) ∧ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥)))    ⇒   ⊢ (𝜑 → (𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝐶 𝑤 ≤ 𝑥))
Theorem	supmul 12118*	The supremum function distributes over multiplication, in the sense that (sup𝐴) · (sup𝐵) = sup(𝐴 · 𝐵), where 𝐴 · 𝐵 is shorthand for {𝑎 · 𝑏 ∣ 𝑎 ∈ 𝐴, 𝑏 ∈ 𝐵} and is defined as 𝐶 below. We made use of this in our definition of multiplication in the Dedekind cut construction of the reals (see df-mp 10899). (Contributed by Mario Carneiro, 5-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑣 · 𝑏)}    &   ⊢ (𝜑 ↔ ((∀𝑥 ∈ 𝐴 0 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐵 0 ≤ 𝑥) ∧ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥)))    ⇒   ⊢ (𝜑 → (sup(𝐴, ℝ, < ) · sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ))
Theorem	sup3ii 12119*	A version of the completeness axiom for reals. (Contributed by NM, 23-Aug-1999.)
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))
Theorem	suprclii 12120*	Closure of supremum of a nonempty bounded set of reals. (Contributed by NM, 12-Sep-1999.)
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ sup(𝐴, ℝ, < ) ∈ ℝ
Theorem	suprubii 12121*	A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Sep-1999.)
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝐵 ≤ sup(𝐴, ℝ, < ))
Theorem	suprlubii 12122*	The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by NM, 15-Oct-2004.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝐵 ∈ ℝ → (𝐵 < sup(𝐴, ℝ, < ) ↔ ∃𝑧 ∈ 𝐴 𝐵 < 𝑧))
Theorem	suprnubii 12123*	An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Oct-2004.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝐵 ∈ ℝ → (¬ 𝐵 < sup(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 ¬ 𝐵 < 𝑧))
Theorem	suprleubii 12124*	The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 6-Sep-2014.)
⊢ (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝐵 ∈ ℝ → (sup(𝐴, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝐴 𝑧 ≤ 𝐵))
Theorem	riotaneg 12125*	The negative of the unique real such that 𝜑. (Contributed by NM, 13-Jun-2005.)
⊢ (𝑥 = -𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ ℝ 𝜑 → (℩𝑥 ∈ ℝ 𝜑) = -(℩𝑦 ∈ ℝ 𝜓))
Theorem	negiso 12126	Negation is an order anti-isomorphism of the real numbers, which is its own inverse. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ -𝑥)    ⇒   ⊢ (𝐹 Isom < , ◡ < (ℝ, ℝ) ∧ ◡𝐹 = 𝐹)
Theorem	dfinfre 12127*	The infimum of a set of reals 𝐴. (Contributed by NM, 9-Oct-2005.) (Revised by AV, 4-Sep-2020.)
⊢ (𝐴 ⊆ ℝ → inf(𝐴, ℝ, < ) = ∪ {𝑥 ∈ ℝ ∣ (∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))})
Theorem	infrecl 12128*	Closure of infimum of a nonempty bounded set of reals. (Contributed by NM, 8-Oct-2005.) (Revised by AV, 4-Sep-2020.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ∈ ℝ)
Theorem	infrenegsup 12129*	The infimum of a set of reals 𝐴 is the negative of the supremum of the negatives of its elements. The antecedent ensures that 𝐴 is nonempty and has a lower bound. (Contributed by NM, 14-Jun-2005.) (Revised by AV, 4-Sep-2020.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) = -sup({𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴}, ℝ, < ))
Theorem	infregelb 12130*	Any lower bound of a nonempty set of real numbers is less than or equal to its infimum. (Contributed by Jeff Hankins, 1-Sep-2013.) (Revised by AV, 4-Sep-2020.) (Proof modification is discouraged.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 𝐵 ≤ 𝑧))
Theorem	infrelb 12131*	If a nonempty set of real numbers has a lower bound, its infimum is less than or equal to any of its elements. (Contributed by Jeff Hankins, 15-Sep-2013.) (Revised by AV, 4-Sep-2020.)
⊢ ((𝐵 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝐵) → inf(𝐵, ℝ, < ) ≤ 𝐴)
Theorem	infrefilb 12132	The infimum of a finite set of reals is less than or equal to any of its elements. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ ((𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ∧ 𝐴 ∈ 𝐵) → inf(𝐵, ℝ, < ) ≤ 𝐴)
Theorem	supfirege 12133	The supremum of a finite set of real numbers is greater than or equal to all the real numbers of the set. (Contributed by AV, 1-Oct-2019.)
⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 = sup(𝐵, ℝ, < ))    ⇒   ⊢ (𝜑 → 𝐶 ≤ 𝑆)
5.3.9  Imaginary and complex number properties
Theorem	neg1cn 12134	-1 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ -1 ∈ ℂ
Theorem	neg1rr 12135	-1 is a real number. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ -1 ∈ ℝ
Theorem	neg1ne0 12136	-1 is nonzero. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 ≠ 0
Theorem	neg1lt0 12137	-1 is less than 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 < 0
Theorem	negneg1e1 12138	--1 is 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ --1 = 1
Theorem	inelr 12139	The imaginary unit i is not a real number. (Contributed by NM, 6-May-1999.)
⊢ ¬ i ∈ ℝ
Theorem	rimul 12140	A real number times the imaginary unit is real only if the number is 0. (Contributed by NM, 28-May-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ (i · 𝐴) ∈ ℝ) → 𝐴 = 0)
Theorem	cru 12141	The representation of complex numbers in terms of real and imaginary parts is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 + (i · 𝐵)) = (𝐶 + (i · 𝐷)) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	crne0 12142	The real representation of complex numbers is nonzero iff one of its terms is nonzero. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ (𝐴 + (i · 𝐵)) ≠ 0))
Theorem	creur 12143*	The real part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	creui 12144*	The imaginary part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → ∃!𝑦 ∈ ℝ ∃𝑥 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	cju 12145*	The complex conjugate of a complex number is unique. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ))
5.3.10  Function operation analogue theorems
Theorem	ofsubeq0 12146	Function analogue of subeq0 11411. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ) → ((𝐹 ∘f − 𝐺) = (𝐴 × {0}) ↔ 𝐹 = 𝐺))
Theorem	ofnegsub 12147	Function analogue of negsub 11433. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ) → (𝐹 ∘f + ((𝐴 × {-1}) ∘f · 𝐺)) = (𝐹 ∘f − 𝐺))
Theorem	ofsubge0 12148	Function analogue of subge0 11654. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ) → ((𝐴 × {0}) ∘r ≤ (𝐹 ∘f − 𝐺) ↔ 𝐺 ∘r ≤ 𝐹))
5.4  Integer sets
5.4.1  Positive integers (as a subset of complex numbers)
Syntax	cn 12149	Extend class notation to include the class of positive integers.
class ℕ
Definition	df-nn 12150	Define the set of positive integers. Some authors, especially in analysis books, call these the natural numbers, whereas other authors choose to include 0 in their definition of natural numbers. Note that ℕ is a subset of complex numbers (nnsscn 12154), in contrast to the more elementary ordinal natural numbers ω, df-om 7811). See nnind 12167 for the principle of mathematical induction. See df-n0 12406 for the set of nonnegative integers ℕ0. See dfn2 12418 for ℕ defined in terms of ℕ0. This is a technical definition that helps us avoid the Axiom of Infinity ax-inf2 9554 in certain proofs. For a more conventional and intuitive definition ("the smallest set of reals containing 1 as well as the successor of every member") see dfnn3 12163 (or its slight variant dfnn2 12162). (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 3-May-2014.)
⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
Theorem	nnexALT 12151	Alternate proof of nnex 12155, more direct, that makes use of ax-rep 5225. (Contributed by Mario Carneiro, 3-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℕ ∈ V
Theorem	peano5nni 12152*	Peano's inductive postulate. Theorem I.36 (principle of mathematical induction) of [Apostol] p. 34. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ((1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ℕ ⊆ 𝐴)
Theorem	nnssre 12153	The positive integers are a subset of the reals. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)
⊢ ℕ ⊆ ℝ
Theorem	nnsscn 12154	The positive integers are a subset of the complex numbers. Remark: this could also be proven from nnssre 12153 and ax-resscn 11087 at the cost of using more axioms. (Contributed by NM, 2-Aug-2004.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
⊢ ℕ ⊆ ℂ
Theorem	nnex 12155	The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ℕ ∈ V
Theorem	nnre 12156	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
Theorem	nncn 12157	A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
Theorem	nnrei 12158	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ∈ ℝ
Theorem	nncni 12159	A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ∈ ℂ
Theorem	1nn 12160	Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 1 ∈ ℕ
Theorem	peano2nn 12161	Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)
Theorem	dfnn2 12162*	Alternate definition of the set of positive integers. This was our original definition, before the current df-nn 12150 replaced it. This definition requires the axiom of infinity to ensure it has the properties we expect. (Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro, 3-May-2014.)
⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
Theorem	dfnn3 12163*	Alternate definition of the set of positive integers. Definition of positive integers in [Apostol] p. 22. (Contributed by NM, 3-Jul-2005.)
⊢ ℕ = ∩ {𝑥 ∣ (𝑥 ⊆ ℝ ∧ 1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
Theorem	nnred 12164	A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	nncnd 12165	A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℂ)
Theorem	peano2nnd 12166	Peano postulate: a successor of a positive integer is a positive integer. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 + 1) ∈ ℕ)
5.4.2  Principle of mathematical induction
Theorem	nnind 12167*	Principle of Mathematical Induction (inference schema). The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. See nnaddcl 12172 for an example of its use. See nn0ind 12591 for induction on nonnegative integers and uzind 12588, uzind4 12823 for induction on an arbitrary upper set of integers. See indstr 12833 for strong induction. See also nnindALT 12168. This is an alternative for Metamath 100 proof #74. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ ℕ → 𝜏)
Theorem	nnindALT 12168*	Principle of Mathematical Induction (inference schema). The last four hypotheses give us the substitution instances we need; the first two are the induction step and the basis. This ALT version of nnind 12167 has a different hypothesis order. It may be easier to use with the Metamath program Proof Assistant, because "MM-PA> ASSIGN LAST" will be applied to the substitution instances first. We may eventually use this one as the official version. You may use either version. After the proof is complete, the ALT version can be changed to the non-ALT version with "MM-PA> MINIMIZE_WITH nnind / MAYGROW";. (Contributed by NM, 7-Dec-2005.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃))    &   ⊢ 𝜓    &   ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    ⇒   ⊢ (𝐴 ∈ ℕ → 𝜏)
Theorem	nnindd 12169*	Principle of Mathematical Induction (inference schema) on integers, a deduction version. (Contributed by Thierry Arnoux, 19-Jul-2020.)
⊢ (𝑥 = 1 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → 𝜂)
Theorem	nn1m1nn 12170	Every positive integer is one or a successor. (Contributed by Mario Carneiro, 16-May-2014.)
⊢ (𝐴 ∈ ℕ → (𝐴 = 1 ∨ (𝐴 − 1) ∈ ℕ))
Theorem	nn1suc 12171*	If a statement holds for 1 and also holds for a successor, it holds for all positive integers. The first three hypotheses give us the substitution instances we need; the last two show that it holds for 1 and for a successor. (Contributed by NM, 11-Oct-2004.) (Revised by Mario Carneiro, 16-May-2014.)
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜃))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕ → 𝜒)    ⇒   ⊢ (𝐴 ∈ ℕ → 𝜃)
Theorem	nnaddcl 12172	Closure of addition of positive integers, proved by induction on the second addend. (Contributed by NM, 12-Jan-1997.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) ∈ ℕ)
Theorem	nnmulcl 12173	Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997.) Remove dependency on ax-mulcom 11094 and ax-mulass 11096. (Revised by Steven Nguyen, 24-Sep-2022.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ)
Theorem	nnmulcli 12174	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 · 𝐵) ∈ ℕ
Theorem	nnmtmip 12175	"Minus times minus is plus, The reason for this we need not discuss." (W. H. Auden, as quoted in M. Guillen "Bridges to Infinity", p. 64, see also Metamath Book, section 1.1.1, p. 5) This statement, formalized to "The product of two negative integers is a positive integer", is proved by the following theorem, therefore it actually need not be discussed anymore. "The reason for this" is that (-𝐴 · -𝐵) = (𝐴 · 𝐵) for all complex numbers 𝐴 and 𝐵 because of mul2neg 11580, 𝐴 and 𝐵 are complex numbers because of nncn 12157, and (𝐴 · 𝐵) ∈ ℕ because of nnmulcl 12173. This also holds for positive reals, see rpmtmip 12935. Note that the opposites -𝐴 and -𝐵 of the positive integers 𝐴 and 𝐵 are negative integers. (Contributed by AV, 23-Dec-2022.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (-𝐴 · -𝐵) ∈ ℕ)
Theorem	nn2ge 12176*	There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ (𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥))
Theorem	nnge1 12177	A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
Theorem	nngt1ne1 12178	A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.)
⊢ (𝐴 ∈ ℕ → (1 < 𝐴 ↔ 𝐴 ≠ 1))
Theorem	nnle1eq1 12179	A positive integer is less than or equal to one iff it is equal to one. (Contributed by NM, 3-Apr-2005.)
⊢ (𝐴 ∈ ℕ → (𝐴 ≤ 1 ↔ 𝐴 = 1))
Theorem	nngt0 12180	A positive integer is positive. (Contributed by NM, 26-Sep-1999.)
⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
Theorem	nnnlt1 12181	A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℕ → ¬ 𝐴 < 1)
Theorem	nnnle0 12182	A positive integer is not less than or equal to zero. (Contributed by AV, 13-May-2020.)
⊢ (𝐴 ∈ ℕ → ¬ 𝐴 ≤ 0)
Theorem	nnne0 12183	A positive integer is nonzero. See nnne0ALT 12187 for a shorter proof using ax-pre-mulgt0 11107. This proof avoids 0lt1 11663, and thus ax-pre-mulgt0 11107, by splitting ax-1ne0 11099 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11107. (Revised by Steven Nguyen, 30-Jan-2023.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	nnneneg 12184	No positive integer is equal to its negation. (Contributed by AV, 20-Jun-2023.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ -𝐴)
Theorem	0nnn 12185	Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.) Remove dependency on ax-pre-mulgt0 11107. (Revised by Steven Nguyen, 30-Jan-2023.)
⊢ ¬ 0 ∈ ℕ
Theorem	0nnnALT 12186	Alternate proof of 0nnn 12185, which requires ax-pre-mulgt0 11107 but is not based on nnne0 12183 (and which can therefore be used in nnne0ALT 12187). (Contributed by NM, 25-Aug-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ¬ 0 ∈ ℕ
Theorem	nnne0ALT 12187	Alternate version of nnne0 12183. A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	nngt0i 12188	A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 0 < 𝐴
Theorem	nnne0i 12189	A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ≠ 0
Theorem	nndivre 12190	The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) ∈ ℝ)
Theorem	nnrecre 12191	The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.)
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ)
Theorem	nnrecgt0 12192	The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 0 < (1 / 𝐴))
Theorem	nnsub 12193	Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ))
Theorem	nnsubi 12194	Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)
Theorem	nndiv 12195*	Two ways to express "𝐴 divides 𝐵 " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑥 ∈ ℕ (𝐴 · 𝑥) = 𝐵 ↔ (𝐵 / 𝐴) ∈ ℕ))
Theorem	nndivtr 12196	Transitive property of divisibility: if 𝐴 divides 𝐵 and 𝐵 divides 𝐶, then 𝐴 divides 𝐶. Typically, 𝐶 would be an integer, although the theorem holds for complex 𝐶. (Contributed by NM, 3-May-2005.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℂ) ∧ ((𝐵 / 𝐴) ∈ ℕ ∧ (𝐶 / 𝐵) ∈ ℕ)) → (𝐶 / 𝐴) ∈ ℕ)
Theorem	nnge1d 12197	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 1 ≤ 𝐴)
Theorem	nngt0d 12198	A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 0 < 𝐴)
Theorem	nnne0d 12199	A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	nnrecred 12200	The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ)