P. 104 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10301-10400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cjdivapd 10301	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵)))
Theorem	rered 10302	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.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℜ‘𝐴) = 𝐴)
Theorem	reim0d 10303	The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℑ‘𝐴) = 0)
Theorem	cjred 10304	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (∗‘𝐴) = 𝐴)
Theorem	remul2d 10305	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵)))
Theorem	immul2d 10306	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵)))
Theorem	redivapd 10307	Real part of a division. Related to remul2 10206. (Contributed by Jim Kingdon, 15-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐵 / 𝐴)) = ((ℜ‘𝐵) / 𝐴))
Theorem	imdivapd 10308	Imaginary part of a division. Related to remul2 10206. (Contributed by Jim Kingdon, 15-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐵 / 𝐴)) = ((ℑ‘𝐵) / 𝐴))
Theorem	crred 10309	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
Theorem	crimd 10310	The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
3.7.3  Sequence convergence
Theorem	caucvgrelemrec 10311*	Two ways to express a reciprocal. (Contributed by Jim Kingdon, 20-Jul-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 # 0) → (℩𝑟 ∈ ℝ (𝐴 · 𝑟) = 1) = (1 / 𝐴))
Theorem	caucvgrelemcau 10312*	Lemma for caucvgre 10313. Converting the Cauchy condition. (Contributed by Jim Kingdon, 20-Jul-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛))))    ⇒   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ ℕ (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))
Theorem	caucvgre 10313*	Convergence of real sequences. A Cauchy sequence (as defined here, which has a rate of convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within 1 / 𝑛 of the nth term. (Contributed by Jim Kingdon, 19-Jul-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛))))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))
Theorem	cvg1nlemcxze 10314	Lemma for cvg1n 10318. Rearranging an expression related to the rate of convergence. (Contributed by Jim Kingdon, 6-Aug-2021.)
⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑍 ∈ ℕ)    &   ⊢ (𝜑 → 𝐸 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → ((((𝐶 · 2) / 𝑋) / 𝑍) + 𝐴) < 𝐸)    ⇒   ⊢ (𝜑 → (𝐶 / (𝐸 · 𝑍)) < (𝑋 / 2))
Theorem	cvg1nlemf 10315*	Lemma for cvg1n 10318. The modified sequence 𝐺 is a sequence. (Contributed by Jim Kingdon, 1-Aug-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))))    &   ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍)))    &   ⊢ (𝜑 → 𝑍 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 < 𝑍)    ⇒   ⊢ (𝜑 → 𝐺:ℕ⟶ℝ)
Theorem	cvg1nlemcau 10316*	Lemma for cvg1n 10318. By selecting spaced out terms for the modified sequence 𝐺, the terms are within 1 / 𝑛 (without the constant 𝐶). (Contributed by Jim Kingdon, 1-Aug-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))))    &   ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍)))    &   ⊢ (𝜑 → 𝑍 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 < 𝑍)    ⇒   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐺‘𝑛) < ((𝐺‘𝑘) + (1 / 𝑛)) ∧ (𝐺‘𝑘) < ((𝐺‘𝑛) + (1 / 𝑛))))
Theorem	cvg1nlemres 10317*	Lemma for cvg1n 10318. The original sequence 𝐹 has a limit (turns out it is the same as the limit of the modified sequence 𝐺). (Contributed by Jim Kingdon, 1-Aug-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))))    &   ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍)))    &   ⊢ (𝜑 → 𝑍 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 < 𝑍)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))
Theorem	cvg1n 10318*	Convergence of real sequences. This is a version of caucvgre 10313 with a constant multiplier 𝐶 on the rate of convergence. That is, all terms after the nth term must be within 𝐶 / 𝑛 of the nth term. (Contributed by Jim Kingdon, 1-Aug-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛))))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥)))
Theorem	uzin2 10319	The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.)
⊢ ((𝐴 ∈ ran ℤ≥ ∧ 𝐵 ∈ ran ℤ≥) → (𝐴 ∩ 𝐵) ∈ ran ℤ≥)
Theorem	rexanuz 10320*	Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.)
⊢ (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓))
Theorem	rexfiuz 10321*	Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.)
⊢ (𝐴 ∈ Fin → (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑛 ∈ 𝐴 𝜑 ↔ ∀𝑛 ∈ 𝐴 ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑))
Theorem	rexuz3 10322*	Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑))
Theorem	rexanuz2 10323*	Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓))
Theorem	r19.29uz 10324*	A version of 19.29 1554 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((∀𝑘 ∈ 𝑍 𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓))
Theorem	r19.2uz 10325*	A version of r19.2m 3356 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 → ∃𝑘 ∈ 𝑍 𝜑)
Theorem	recvguniqlem 10326	Lemma for recvguniq 10327. Some of the rearrangements of the expressions. (Contributed by Jim Kingdon, 8-Aug-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 < ((𝐹‘𝐾) + ((𝐴 − 𝐵) / 2)))    &   ⊢ (𝜑 → (𝐹‘𝐾) < (𝐵 + ((𝐴 − 𝐵) / 2)))    ⇒   ⊢ (𝜑 → ⊥)
Theorem	recvguniq 10327*	Limits are unique. (Contributed by Jim Kingdon, 7-Aug-2021.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) < (𝐿 + 𝑥) ∧ 𝐿 < ((𝐹‘𝑘) + 𝑥)))    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) < (𝑀 + 𝑥) ∧ 𝑀 < ((𝐹‘𝑘) + 𝑥)))    ⇒   ⊢ (𝜑 → 𝐿 = 𝑀)
3.7.4  Square root; absolute value
Syntax	csqrt 10328	Extend class notation to include square root of a complex number.
class √
Syntax	cabs 10329	Extend class notation to include a function for the absolute value (modulus) of a complex number.
class abs
Definition	df-rsqrt 10330*	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.)
⊢ √ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦)))
Definition	df-abs 10331	Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.)
⊢ abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥))))
Theorem	sqrtrval 10332*	Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.)
⊢ (𝐴 ∈ ℝ → (√‘𝐴) = (℩𝑥 ∈ ℝ ((𝑥↑2) = 𝐴 ∧ 0 ≤ 𝑥)))
Theorem	absval 10333	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.)
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) = (√‘(𝐴 · (∗‘𝐴))))
Theorem	rennim 10334	A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.)
⊢ (𝐴 ∈ ℝ → (i · 𝐴) ∉ ℝ+)
Theorem	sqrt0rlem 10335	Lemma for sqrt0 10336. (Contributed by Jim Kingdon, 26-Aug-2020.)
⊢ ((𝐴 ∈ ℝ ∧ ((𝐴↑2) = 0 ∧ 0 ≤ 𝐴)) ↔ 𝐴 = 0)
Theorem	sqrt0 10336	Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ (√‘0) = 0
Theorem	resqrexlem1arp 10337*	Lemma for resqrex 10358. 1 + 𝐴 is a positive real (expressed in a way that will help apply iseqfcl 9796 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → ((ℕ × {(1 + 𝐴)})‘𝑁) ∈ ℝ+)
Theorem	resqrexlemp1rp 10338*	Lemma for resqrex 10358. Applying the recursion rule yields a positive real (expressed in a way that will help apply iseqfcl 9796 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ ((𝜑 ∧ (𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+)) → (𝐵(𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2))𝐶) ∈ ℝ+)
Theorem	resqrexlemf 10339*	Lemma for resqrex 10358. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 𝐹:ℕ⟶ℝ+)
Theorem	resqrexlemf1 10340*	Lemma for resqrex 10358. Initial value. Although this sequence converges to the square root with any positive initial value, this choice makes various steps in the proof of convergence easier. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹‘1) = (1 + 𝐴))
Theorem	resqrexlemfp1 10341*	Lemma for resqrex 10358. Recursion rule. This sequence is the ancient method for computing square roots, often known as the babylonian method, although known to many ancient cultures. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝐹‘(𝑁 + 1)) = (((𝐹‘𝑁) + (𝐴 / (𝐹‘𝑁))) / 2))
Theorem	resqrexlemover 10342*	Lemma for resqrex 10358. Each element of the sequence is an overestimate. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝐴 < ((𝐹‘𝑁)↑2))
Theorem	resqrexlemdec 10343*	Lemma for resqrex 10358. The sequence is decreasing. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝐹‘(𝑁 + 1)) < (𝐹‘𝑁))
Theorem	resqrexlemdecn 10344*	Lemma for resqrex 10358. The sequence is decreasing. (Contributed by Jim Kingdon, 31-Jul-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 < 𝑀)    ⇒   ⊢ (𝜑 → (𝐹‘𝑀) < (𝐹‘𝑁))
Theorem	resqrexlemlo 10345*	Lemma for resqrex 10358. A (variable) lower bound for each term of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (1 / (2↑𝑁)) < (𝐹‘𝑁))
Theorem	resqrexlemcalc1 10346*	Lemma for resqrex 10358. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (((𝐹‘(𝑁 + 1))↑2) − 𝐴) = (((((𝐹‘𝑁)↑2) − 𝐴)↑2) / (4 · ((𝐹‘𝑁)↑2))))
Theorem	resqrexlemcalc2 10347*	Lemma for resqrex 10358. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (((𝐹‘(𝑁 + 1))↑2) − 𝐴) ≤ ((((𝐹‘𝑁)↑2) − 𝐴) / 4))
Theorem	resqrexlemcalc3 10348*	Lemma for resqrex 10358. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (((𝐹‘𝑁)↑2) − 𝐴) ≤ (((𝐹‘1)↑2) / (4↑(𝑁 − 1))))
Theorem	resqrexlemnmsq 10349*	Lemma for resqrex 10358. The difference between the squares of two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 30-Jul-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ≤ 𝑀)    ⇒   ⊢ (𝜑 → (((𝐹‘𝑁)↑2) − ((𝐹‘𝑀)↑2)) < (((𝐹‘1)↑2) / (4↑(𝑁 − 1))))
Theorem	resqrexlemnm 10350*	Lemma for resqrex 10358. The difference between two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 31-Jul-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ≤ 𝑀)    ⇒   ⊢ (𝜑 → ((𝐹‘𝑁) − (𝐹‘𝑀)) < ((((𝐹‘1)↑2) · 2) / (2↑(𝑁 − 1))))
Theorem	resqrexlemcvg 10351*	Lemma for resqrex 10358. The sequence has a limit. (Contributed by Jim Kingdon, 6-Aug-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑟 + 𝑥) ∧ 𝑟 < ((𝐹‘𝑖) + 𝑥)))
Theorem	resqrexlemgt0 10352*	Lemma for resqrex 10358. A limit is nonnegative. (Contributed by Jim Kingdon, 7-Aug-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)))    ⇒   ⊢ (𝜑 → 0 ≤ 𝐿)
Theorem	resqrexlemoverl 10353*	Lemma for resqrex 10358. Every term in the sequence is an overestimate compared with the limit 𝐿. Although this theorem is stated in terms of a particular sequence the proof could be adapted for any decreasing convergent sequence. (Contributed by Jim Kingdon, 9-Aug-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)))    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐿 ≤ (𝐹‘𝐾))
Theorem	resqrexlemglsq 10354*	Lemma for resqrex 10358. The sequence formed by squaring each term of 𝐹 converges to (𝐿↑2). (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)))    &   ⊢ 𝐺 = (𝑥 ∈ ℕ ↦ ((𝐹‘𝑥)↑2))    ⇒   ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘) < ((𝐿↑2) + 𝑒) ∧ (𝐿↑2) < ((𝐺‘𝑘) + 𝑒)))
Theorem	resqrexlemga 10355*	Lemma for resqrex 10358. The sequence formed by squaring each term of 𝐹 converges to 𝐴. (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)))    &   ⊢ 𝐺 = (𝑥 ∈ ℕ ↦ ((𝐹‘𝑥)↑2))    ⇒   ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘) < (𝐴 + 𝑒) ∧ 𝐴 < ((𝐺‘𝑘) + 𝑒)))
Theorem	resqrexlemsqa 10356*	Lemma for resqrex 10358. The square of a limit is 𝐴. (Contributed by Jim Kingdon, 7-Aug-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐿 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒)))    ⇒   ⊢ (𝜑 → (𝐿↑2) = 𝐴)
Theorem	resqrexlemex 10357*	Lemma for resqrex 10358. Existence of square root given a sequence which converges to the square root. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (0 ≤ 𝑥 ∧ (𝑥↑2) = 𝐴))
Theorem	resqrex 10358*	Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃𝑥 ∈ ℝ (0 ≤ 𝑥 ∧ (𝑥↑2) = 𝐴))
Theorem	rsqrmo 10359*	Uniqueness for the square root function. (Contributed by Jim Kingdon, 10-Aug-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃*𝑥 ∈ ℝ ((𝑥↑2) = 𝐴 ∧ 0 ≤ 𝑥))
Theorem	rersqreu 10360*	Existence and uniqueness for the real square root function. (Contributed by Jim Kingdon, 10-Aug-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃!𝑥 ∈ ℝ ((𝑥↑2) = 𝐴 ∧ 0 ≤ 𝑥))
Theorem	resqrtcl 10361	Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘𝐴) ∈ ℝ)
Theorem	rersqrtthlem 10362	Lemma for resqrtth 10363. (Contributed by Jim Kingdon, 10-Aug-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (√‘𝐴)))
Theorem	resqrtth 10363	Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴)↑2) = 𝐴)
Theorem	remsqsqrt 10364	Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴) · (√‘𝐴)) = 𝐴)
Theorem	sqrtge0 10365	The square root function is nonnegative for nonnegative input. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 9-Jul-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 0 ≤ (√‘𝐴))
Theorem	sqrtgt0 10366	The square root function is positive for positive input. (Contributed by Mario Carneiro, 10-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2013.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 0 < (√‘𝐴))
Theorem	sqrtmul 10367	Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵)))
Theorem	sqrtle 10368	Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵)))
Theorem	sqrtlt 10369	Square root is strictly monotonic. Closed form of sqrtlti 10469. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵)))
Theorem	sqrt11ap 10370	Analogue to sqrt11 10371 but for apartness. (Contributed by Jim Kingdon, 11-Aug-2021.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) # (√‘𝐵) ↔ 𝐴 # 𝐵))
Theorem	sqrt11 10371	The square root function is one-to-one. Also see sqrt11ap 10370 which would follow easily from this given excluded middle, but which is proved another way without it. (Contributed by Scott Fenton, 11-Jun-2013.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) = (√‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	sqrt00 10372	A square root is zero iff its argument is 0. (Contributed by NM, 27-Jul-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴) = 0 ↔ 𝐴 = 0))
Theorem	rpsqrtcl 10373	The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.)
⊢ (𝐴 ∈ ℝ+ → (√‘𝐴) ∈ ℝ+)
Theorem	sqrtdiv 10374	Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ+) → (√‘(𝐴 / 𝐵)) = ((√‘𝐴) / (√‘𝐵)))
Theorem	sqrtsq2 10375	Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) = 𝐵 ↔ 𝐴 = (𝐵↑2)))
Theorem	sqrtsq 10376	Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴↑2)) = 𝐴)
Theorem	sqrtmsq 10377	Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴 · 𝐴)) = 𝐴)
Theorem	sqrt1 10378	The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
⊢ (√‘1) = 1
Theorem	sqrt4 10379	The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
⊢ (√‘4) = 2
Theorem	sqrt9 10380	The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
⊢ (√‘9) = 3
Theorem	sqrt2gt1lt2 10381	The square root of 2 is bounded by 1 and 2. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 6-Sep-2013.)
⊢ (1 < (√‘2) ∧ (√‘2) < 2)
Theorem	absneg 10382	Absolute value of negative. (Contributed by NM, 27-Feb-2005.)
⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) = (abs‘𝐴))
Theorem	abscl 10383	Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
Theorem	abscj 10384	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.)
⊢ (𝐴 ∈ ℂ → (abs‘(∗‘𝐴)) = (abs‘𝐴))
Theorem	absvalsq 10385	Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.)
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
Theorem	absvalsq2 10386	Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.)
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
Theorem	sqabsadd 10387	Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133. (Contributed by NM, 21-Jan-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘(𝐴 + 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) + (2 · (ℜ‘(𝐴 · (∗‘𝐵))))))
Theorem	sqabssub 10388	Square of absolute value of difference. (Contributed by NM, 21-Jan-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘(𝐴 − 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) − (2 · (ℜ‘(𝐴 · (∗‘𝐵))))))
Theorem	absval2 10389	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.)
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))))
Theorem	abs0 10390	The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (abs‘0) = 0
Theorem	absi 10391	The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
⊢ (abs‘i) = 1
Theorem	absge0 10392	Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
Theorem	absrpclap 10393	The absolute value of a number apart from zero is a positive real. (Contributed by Jim Kingdon, 11-Aug-2021.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (abs‘𝐴) ∈ ℝ+)
Theorem	abs00ap 10394	The absolute value of a number is apart from zero iff the number is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.)
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) # 0 ↔ 𝐴 # 0))
Theorem	absext 10395	Strong extensionality for absolute value. (Contributed by Jim Kingdon, 12-Aug-2021.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) # (abs‘𝐵) → 𝐴 # 𝐵))
Theorem	abs00 10396	The absolute value of a number is zero iff the number is zero. Also see abs00ap 10394 which is similar but for apartness. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by NM, 26-Sep-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) = 0 ↔ 𝐴 = 0))
Theorem	abs00ad 10397	A complex number is zero iff its absolute value is zero. Deduction form of abs00 10396. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((abs‘𝐴) = 0 ↔ 𝐴 = 0))
Theorem	abs00bd 10398	If a complex number is zero, its absolute value is zero. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 = 0)    ⇒   ⊢ (𝜑 → (abs‘𝐴) = 0)
Theorem	absreimsq 10399	Square of the absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 1-Feb-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((abs‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴↑2) + (𝐵↑2)))
Theorem	absreim 10400	Absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 14-Jan-2006.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (abs‘(𝐴 + (i · 𝐵))) = (√‘((𝐴↑2) + (𝐵↑2))))