P. 92 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9101-9200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cjexp 9101	Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.)
⊢ ((A ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (∗‘(A↑𝑁)) = ((∗‘A)↑𝑁))
Theorem	imval2 9102	The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.)
⊢ (A ∈ ℂ → (ℑ‘A) = ((A − (∗‘A)) / (2 · i)))
Theorem	re0 9103	The real part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℜ‘0) = 0
Theorem	im0 9104	The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (ℑ‘0) = 0
Theorem	re1 9105	The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘1) = 1
Theorem	im1 9106	The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘1) = 0
Theorem	rei 9107	The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℜ‘i) = 0
Theorem	imi 9108	The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.)
⊢ (ℑ‘i) = 1
Theorem	cj0 9109	The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
⊢ (∗‘0) = 0
Theorem	cji 9110	The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
⊢ (∗‘i) = -i
Theorem	cjreim 9111	The conjugate of a representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (∗‘(A + (i · B))) = (A − (i · B)))
Theorem	cjreim2 9112	The conjugate of the representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (∗‘(A − (i · B))) = (A + (i · B)))
Theorem	cj11 9113	Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((∗‘A) = (∗‘B) ↔ A = B))
Theorem	cjap 9114	Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((∗‘A) # (∗‘B) ↔ A # B))
Theorem	cjap0 9115	A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ (A ∈ ℂ → (A # 0 ↔ (∗‘A) # 0))
Theorem	cjne0 9116	A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005.)
⊢ (A ∈ ℂ → (A ≠ 0 ↔ (∗‘A) ≠ 0))
Theorem	cjdivap 9117	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ B # 0) → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))
Theorem	cnrecnv 9118*	The inverse to the canonical bijection from (ℝ × ℝ) to ℂ from cnref1o 8337. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐹 = (x ∈ ℝ, y ∈ ℝ ↦ (x + (i · y)))    ⇒   ⊢ ◡𝐹 = (z ∈ ℂ ↦ ⟨(ℜ‘z), (ℑ‘z)⟩)
Theorem	recli 9119	The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (ℜ‘A) ∈ ℝ
Theorem	imcli 9120	The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (ℑ‘A) ∈ ℝ
Theorem	cjcli 9121	Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (∗‘A) ∈ ℂ
Theorem	replimi 9122	Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ A = ((ℜ‘A) + (i · (ℑ‘A)))
Theorem	cjcji 9123	The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by NM, 11-May-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (∗‘(∗‘A)) = A
Theorem	reim0bi 9124	A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (A ∈ ℝ ↔ (ℑ‘A) = 0)
Theorem	rerebi 9125	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (A ∈ ℝ ↔ (ℜ‘A) = A)
Theorem	cjrebi 9126	A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 11-Oct-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (A ∈ ℝ ↔ (∗‘A) = A)
Theorem	recji 9127	Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (ℜ‘(∗‘A)) = (ℜ‘A)
Theorem	imcji 9128	Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (ℑ‘(∗‘A)) = -(ℑ‘A)
Theorem	cjmulrcli 9129	A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (A · (∗‘A)) ∈ ℝ
Theorem	cjmulvali 9130	A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (A · (∗‘A)) = (((ℜ‘A)↑2) + ((ℑ‘A)↑2))
Theorem	cjmulge0i 9131	A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ 0 ≤ (A · (∗‘A))
Theorem	renegi 9132	Real part of negative. (Contributed by NM, 2-Aug-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (ℜ‘-A) = -(ℜ‘A)
Theorem	imnegi 9133	Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (ℑ‘-A) = -(ℑ‘A)
Theorem	cjnegi 9134	Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (∗‘-A) = -(∗‘A)
Theorem	addcji 9135	A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (A + (∗‘A)) = (2 · (ℜ‘A))
Theorem	readdi 9136	Real part distributes over addition. (Contributed by NM, 28-Jul-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℜ‘(A + B)) = ((ℜ‘A) + (ℜ‘B))
Theorem	imaddi 9137	Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℑ‘(A + B)) = ((ℑ‘A) + (ℑ‘B))
Theorem	remuli 9138	Real part of a product. (Contributed by NM, 28-Jul-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℜ‘(A · B)) = (((ℜ‘A) · (ℜ‘B)) − ((ℑ‘A) · (ℑ‘B)))
Theorem	immuli 9139	Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℑ‘(A · B)) = (((ℜ‘A) · (ℑ‘B)) + ((ℑ‘A) · (ℜ‘B)))
Theorem	cjaddi 9140	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (∗‘(A + B)) = ((∗‘A) + (∗‘B))
Theorem	cjmuli 9141	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (∗‘(A · B)) = ((∗‘A) · (∗‘B))
Theorem	ipcni 9142	Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℜ‘(A · (∗‘B))) = (((ℜ‘A) · (ℜ‘B)) + ((ℑ‘A) · (ℑ‘B)))
Theorem	cjdivapi 9143	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (B # 0 → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))
Theorem	crrei 9144	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (ℜ‘(A + (i · B))) = A
Theorem	crimi 9145	The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (ℑ‘(A + (i · B))) = B
Theorem	recld 9146	The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘A) ∈ ℝ)
Theorem	imcld 9147	The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘A) ∈ ℝ)
Theorem	cjcld 9148	Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (∗‘A) ∈ ℂ)
Theorem	replimd 9149	Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → A = ((ℜ‘A) + (i · (ℑ‘A))))
Theorem	remimd 9150	Value of the conjugate of a complex number. The value is the real part minus i times the imaginary part. Definition 10-3.2 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (∗‘A) = ((ℜ‘A) − (i · (ℑ‘A))))
Theorem	cjcjd 9151	The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (∗‘(∗‘A)) = A)
Theorem	reim0bd 9152	A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → (ℑ‘A) = 0)    ⇒   ⊢ (φ → A ∈ ℝ)
Theorem	rerebd 9153	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → (ℜ‘A) = A)    ⇒   ⊢ (φ → A ∈ ℝ)
Theorem	cjrebd 9154	A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → (∗‘A) = A)    ⇒   ⊢ (φ → A ∈ ℝ)
Theorem	cjne0d 9155	A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A ≠ 0)    ⇒   ⊢ (φ → (∗‘A) ≠ 0)
Theorem	recjd 9156	Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(∗‘A)) = (ℜ‘A))
Theorem	imcjd 9157	Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘(∗‘A)) = -(ℑ‘A))
Theorem	cjmulrcld 9158	A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A · (∗‘A)) ∈ ℝ)
Theorem	cjmulvald 9159	A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A · (∗‘A)) = (((ℜ‘A)↑2) + ((ℑ‘A)↑2)))
Theorem	cjmulge0d 9160	A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → 0 ≤ (A · (∗‘A)))
Theorem	renegd 9161	Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘-A) = -(ℜ‘A))
Theorem	imnegd 9162	Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘-A) = -(ℑ‘A))
Theorem	cjnegd 9163	Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (∗‘-A) = -(∗‘A))
Theorem	addcjd 9164	A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A + (∗‘A)) = (2 · (ℜ‘A)))
Theorem	cjexpd 9165	Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (∗‘(A↑𝑁)) = ((∗‘A)↑𝑁))
Theorem	readdd 9166	Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(A + B)) = ((ℜ‘A) + (ℜ‘B)))
Theorem	imaddd 9167	Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘(A + B)) = ((ℑ‘A) + (ℑ‘B)))
Theorem	resubd 9168	Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(A − B)) = ((ℜ‘A) − (ℜ‘B)))
Theorem	imsubd 9169	Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘(A − B)) = ((ℑ‘A) − (ℑ‘B)))
Theorem	remuld 9170	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(A · B)) = (((ℜ‘A) · (ℜ‘B)) − ((ℑ‘A) · (ℑ‘B))))
Theorem	immuld 9171	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘(A · B)) = (((ℜ‘A) · (ℑ‘B)) + ((ℑ‘A) · (ℜ‘B))))
Theorem	cjaddd 9172	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (∗‘(A + B)) = ((∗‘A) + (∗‘B)))
Theorem	cjmuld 9173	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (∗‘(A · B)) = ((∗‘A) · (∗‘B)))
Theorem	ipcnd 9174	Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(A · (∗‘B))) = (((ℜ‘A) · (ℜ‘B)) + ((ℑ‘A) · (ℑ‘B))))
Theorem	cjdivapd 9175	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    &   ⊢ (φ → B # 0)    ⇒   ⊢ (φ → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))
Theorem	rered 9176	A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → (ℜ‘A) = A)
Theorem	reim0d 9177	The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → (ℑ‘A) = 0)
Theorem	cjred 9178	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → (∗‘A) = A)
Theorem	remul2d 9179	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(A · B)) = (A · (ℜ‘B)))
Theorem	immul2d 9180	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘(A · B)) = (A · (ℑ‘B)))
Theorem	redivapd 9181	Real part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 15-Jun-2020.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℂ)    &   ⊢ (φ → A # 0)    ⇒   ⊢ (φ → (ℜ‘(B / A)) = ((ℜ‘B) / A))
Theorem	imdivapd 9182	Imaginary part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 15-Jun-2020.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℂ)    &   ⊢ (φ → A # 0)    ⇒   ⊢ (φ → (ℑ‘(B / A)) = ((ℑ‘B) / A))
Theorem	crred 9183	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    ⇒   ⊢ (φ → (ℜ‘(A + (i · B))) = A)
Theorem	crimd 9184	The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    ⇒   ⊢ (φ → (ℑ‘(A + (i · B))) = B)
3.6.2  Square root; absolute value
Syntax	csqrt 9185	Extend class notation to include square root of a complex number.
class √
Syntax	cabs 9186	Extend class notation to include a function for the absolute value (modulus) of a complex number.
class abs
Definition	df-rsqrt 9187*	Define a function whose value is the square root of a nonnegative real number. Defining the square root for complex numbers has one difficult part: choosing between the two roots. The usual way to define a principal square root for all complex numbers relies on excluded middle or something similar. But in the case of a nonnegative real number, we don't have the complications presented for general complex numbers, and we can choose the nonnegative root. (Contributed by Jim Kingdon, 23-Aug-2020.)
⊢ √ = (x ∈ ℝ ↦ (℩y ∈ ℝ ((y↑2) = x ∧ 0 ≤ y)))
Definition	df-abs 9188	Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.)
⊢ abs = (x ∈ ℂ ↦ (√‘(x · (∗‘x))))
Theorem	sqrtrval 9189*	Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.)
⊢ (A ∈ ℝ → (√‘A) = (℩x ∈ ℝ ((x↑2) = A ∧ 0 ≤ x)))
Theorem	absval 9190	The absolute value (modulus) of a complex number. Proposition 10-3.7(a) of [Gleason] p. 133. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
⊢ (A ∈ ℂ → (abs‘A) = (√‘(A · (∗‘A))))
Theorem	rennim 9191	A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.)
⊢ (A ∈ ℝ → (i · A) ∉ ℝ+)
Theorem	sqrt0rlem 9192	Lemma for sqrt0 9193. (Contributed by Jim Kingdon, 26-Aug-2020.)
⊢ ((A ∈ ℝ ∧ ((A↑2) = 0 ∧ 0 ≤ A)) ↔ A = 0)
Theorem	sqrt0 9193	Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ (√‘0) = 0
Theorem	sqrtsq 9194	Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((A ∈ ℝ ∧ 0 ≤ A) → (√‘(A↑2)) = A)
Theorem	sqrtmsq 9195	Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((A ∈ ℝ ∧ 0 ≤ A) → (√‘(A · A)) = A)
Theorem	sqrt1 9196	The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
⊢ (√‘1) = 1
Theorem	sqrt4 9197	The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
⊢ (√‘4) = 2
Theorem	sqrt9 9198	The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
⊢ (√‘9) = 3
Theorem	absneg 9199	Absolute value of negative. (Contributed by NM, 27-Feb-2005.)
⊢ (A ∈ ℂ → (abs‘-A) = (abs‘A))
Theorem	abscj 9200	The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by NM, 28-Apr-2005.)
⊢ (A ∈ ℂ → (abs‘(∗‘A)) = (abs‘A))