Metamath Proof Explorer - mmtheorems49

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 4801-4900 - Page 49 of 58

Type	Label	Description
Statement
Theorem	absvalt 4801	The absolute value (modulus) of a complex number. Proposition 10-3.7(a) of [Gleason] p. 133.
⊢ (A ∈ ℂ → (abs ‘A) = (√ ‘(A · (∗ ‘A))))
Theorem	recl 4802	The real part of a complex number is real (closure law).
⊢ A ∈ ℂ    ⇒   ⊢ (ℜ ‘A) ∈ ℝ
Theorem	imcl 4803	The imaginary part of a complex number is real (closure law).
⊢ A ∈ ℂ    ⇒   ⊢ (ℑ ‘A) ∈ ℝ
Theorem	cjcl 4804	Closure law for complex conjugate.
⊢ A ∈ ℂ    ⇒   ⊢ (∗ ‘A) ∈ ℂ
Theorem	replim 4805	Construct a complex number from its real and imaginary parts.
⊢ A ∈ ℂ    ⇒   ⊢ A = ((ℜ ‘A) + ((ℑ ‘A) · i))
Theorem	crre 4806	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (ℜ ‘(A + (B · i))) = A
Theorem	crim 4807	The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (ℑ ‘(A + (B · i))) = B
Theorem	cjcj 4808	The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133.
⊢ A ∈ ℂ    ⇒   ⊢ (∗ ‘(∗ ‘A)) = A
Theorem	reim0 4809	The imaginary part of a real number is 0.
⊢ A ∈ ℂ    ⇒   ⊢ (A ∈ ℝ ↔ (ℑ ‘A) = 0)
Theorem	rere 4810	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133.
⊢ A ∈ ℂ    ⇒   ⊢ (A ∈ ℝ ↔ (ℜ ‘A) = A)
Theorem	cjre 4811	A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133.
⊢ A ∈ ℂ    ⇒   ⊢ (A ∈ ℝ ↔ (∗ ‘A) = A)
Theorem	recj 4812	Real part of a complex conjugate.
⊢ A ∈ ℂ    ⇒   ⊢ (ℜ ‘(∗ ‘A)) = (ℜ ‘A)
Theorem	imcj 4813	Imaginary part of a complex conjugate.
⊢ A ∈ ℂ    ⇒   ⊢ (ℑ ‘(∗ ‘A)) = -(ℑ ‘A)
Theorem	readd 4814	Real part distributes over addition.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℜ ‘(A + B)) = ((ℜ ‘A) + (ℜ ‘B))
Theorem	imadd 4815	Imaginary part distributes over addition.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℑ ‘(A + B)) = ((ℑ ‘A) + (ℑ ‘B))
Theorem	remul 4816	Real part of a product.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℜ ‘(A · B)) = (((ℜ ‘A) · (ℜ ‘B)) − ((ℑ ‘A) · (ℑ ‘B)))
Theorem	immul 4817	Imaginary part of a product.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℑ ‘(A · B)) = (((ℜ ‘A) · (ℑ ‘B)) + ((ℑ ‘A) · (ℜ ‘B)))
Theorem	cjadd 4818	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (∗ ‘(A + B)) = ((∗ ‘A) + (∗ ‘B))
Theorem	cjmul 4819	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (∗ ‘(A · B)) = ((∗ ‘A) · (∗ ‘B))
Theorem	ipcn 4820	Standard inner product on complex numbers.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℜ ‘(A · (∗ ‘B))) = (((ℜ ‘A) · (ℜ ‘B)) + ((ℑ ‘A) · (ℑ ‘B)))
Theorem	cjmulrcl 4821	A complex number times its conjugate is real.
⊢ A ∈ ℂ    ⇒   ⊢ (A · (∗ ‘A)) ∈ ℝ
Theorem	cjmulval 4822	A complex number times its conjugate.
⊢ A ∈ ℂ    ⇒   ⊢ (A · (∗ ‘A)) = (((ℜ ‘A)↑2) + ((ℑ ‘A)↑2))
Theorem	cjmulge0 4823	A complex number times its conjugate is nonnegative.
⊢ A ∈ ℂ    ⇒   ⊢ 0 ≤ (A · (∗ ‘A))
Theorem	reneg 4824	Real part of negative.
⊢ A ∈ ℂ    ⇒   ⊢ (ℜ ‘-A) = -(ℜ ‘A)
Theorem	negre 4825	The negative of a real is real.
⊢ A ∈ ℂ    ⇒   ⊢ (-A ∈ ℝ ↔ A ∈ ℝ)
Theorem	imneg 4826	Imaginary part of negative.
⊢ A ∈ ℂ    ⇒   ⊢ (ℑ ‘-A) = -(ℑ ‘A)
Theorem	cjneg 4827	Complex conjugate of negative.
⊢ A ∈ ℂ    ⇒   ⊢ (∗ ‘-A) = -(∗ ‘A)
Theorem	addcj 4828	A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133.
⊢ A ∈ ℂ    ⇒   ⊢ (A + (∗ ‘A)) = (2 · (ℜ ‘A))
Theorem	cjret 4829	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133.
⊢ (A ∈ ℝ → (∗ ‘A) = A)
Theorem	cjcjt 4830	The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133.
⊢ (A ∈ ℂ → (∗ ‘(∗ ‘A)) = A)
Theorem	cjaddt 4831	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (∗ ‘(A + B)) = ((∗ ‘A) + (∗ ‘B)))
Theorem	cjmult 4832	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (∗ ‘(A · B)) = ((∗ ‘A) · (∗ ‘B)))
Theorem	re0 4833	The real part of zero.
⊢ (ℜ ‘0) = 0
Theorem	im0 4834	The imaginary part of zero.
⊢ (ℑ ‘0) = 0
Theorem	cj0 4835	The conjugate of zero.
⊢ (∗ ‘0) = 0
Theorem	absval2 4836	Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
⊢ A ∈ ℂ    ⇒   ⊢ (abs ‘A) = (√ ‘(((ℜ ‘A)↑2) + ((ℑ ‘A)↑2)))
Theorem	absvalsq 4837	Square of value of absolute value function.
⊢ A ∈ ℂ    ⇒   ⊢ ((abs ‘A)↑2) = (A · (∗ ‘A))
Theorem	absvalsq2 4838	Square of value of absolute value function.
⊢ A ∈ ℂ    ⇒   ⊢ ((abs ‘A)↑2) = (((ℜ ‘A)↑2) + ((ℑ ‘A)↑2))
Theorem	abs00 4839	The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133.
⊢ A ∈ ℂ    ⇒   ⊢ ((abs ‘A) = 0 ↔ A = 0)
Theorem	abscl 4840	Real closure of absolute value.
⊢ A ∈ ℂ    ⇒   ⊢ (abs ‘A) ∈ ℝ
Theorem	absge0 4841	Absolute value is nonnegative.
⊢ A ∈ ℂ    ⇒   ⊢ 0 ≤ (abs ‘A)
Theorem	absgt0 4842	The absolute value of a non-zero number is positive. Remark of [Apostol] p. 363.
⊢ A ∈ ℂ    ⇒   ⊢ (¬ A = 0 ↔ 0 < (abs ‘A))
Theorem	absneg 4843	Absolute value of negative.
⊢ A ∈ ℂ    ⇒   ⊢ (abs ‘-A) = (abs ‘A)
Theorem	abscj 4844	The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133.
⊢ A ∈ ℂ    ⇒   ⊢ (abs ‘A) = (abs ‘(∗ ‘A))
Theorem	abssub 4845	Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (abs ‘(A − B)) = (abs ‘(B − A))
Theorem	absmul 4846	Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (abs ‘(A · B)) = ((abs ‘A) · (abs ‘B))
Theorem	sqabsadd 4847	Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ ((abs ‘(A + B))↑2) = ((((abs ‘A)↑2) + ((abs ‘B)↑2)) + (2 · (ℜ ‘(A · (∗ ‘B)))))
Theorem	absclt 4848	Real closure of absolute value.
⊢ (A ∈ ℂ → (abs ‘A) ∈ ℝ)
Theorem	absmult 4849	Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (abs ‘(A · B)) = ((abs ‘A) · (abs ‘B)))
Theorem	absid 4850	A nonnegative number is its own absolute value.
⊢ A ∈ ℝ    ⇒   ⊢ (0 ≤ A → (abs ‘A) = A)
Theorem	absnid 4851	A negative number is the negative of its own absolute value.
⊢ A ∈ ℝ    ⇒   ⊢ (A ≤ 0 → (abs ‘A) = -A)
Theorem	leabs 4852	A real number is less than or equal to its absolute value.
⊢ A ∈ ℝ    ⇒   ⊢ A ≤ (abs ‘A)
Theorem	absor 4853	The absolute value of a real number is either that number or its negative.
⊢ A ∈ ℝ    ⇒   ⊢ ((abs ‘A) = A ∨ (abs ‘A) = -A)
Theorem	absre 4854	Absolute value of a real number.
⊢ A ∈ ℝ    ⇒   ⊢ (abs ‘A) = (√ ‘(A↑2))
Theorem	abslt 4855	Absolute value and 'less than' relation.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((abs ‘A) < B ↔ (A < B ∧ -A < B))
Theorem	absle 4856	Absolute value and 'less than or equal to' relation.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((abs ‘A) ≤ B ↔ (A ≤ B ∧ -A ≤ B))
Theorem	absltt 4857	Absolute value and 'less than' relation.
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((abs ‘A) < B ↔ (A < B ∧ -A < B)))
Theorem	releabs 4858	The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of [Gleason] p. 133.
⊢ A ∈ ℂ    ⇒   ⊢ (ℜ ‘A) ≤ (abs ‘A)
Theorem	abstri 4859	Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (abs ‘(A + B)) ≤ ((abs ‘A) + (abs ‘B))
Theorem	abs3dif 4860	Absolute value of differences around common element.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    ⇒   ⊢ (abs ‘(A − B)) ≤ ((abs ‘(A − C)) + (abs ‘(C − B)))
Theorem	abs3lem 4861	Lemma involving absolute value of differences.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ C ∈ ℂ    &   ⊢ D ∈ ℝ    ⇒   ⊢ (((abs ‘(A − C)) < (D / 2) ∧ (abs ‘(C − B)) < (D / 2)) → (abs ‘(A − B)) < D)
Theorem	absidt 4862	A nonnegative number is its own absolute value.
⊢ (A ∈ ℝ → (0 ≤ A → (abs ‘A) = A))
Theorem	absgt0t 4863	The absolute value of a non-zero number is positive.
⊢ (A ∈ ℂ → (¬ A = 0 ↔ 0 < (abs ‘A)))
Theorem	abssubt 4864	Swapping order of subtraction doesn't change the absolute value.
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (abs ‘(A − B)) = (abs ‘(B − A)))
Theorem	abs3lemt 4865	Lemma involving absolute value of differences.
⊢ (((A ∈ ℂ ∧ B ∈ ℂ) ∧ (C ∈ ℂ ∧ D ∈ ℝ)) → (((abs ‘(A − C)) < (D / 2) ∧ (abs ‘(C − B)) < (D / 2)) → (abs ‘(A − B)) < D))
Theorem	abslem2i 4866	Lemma involving absolute values.
⊢ A ∈ ℂ    &   ⊢ A ≠ 0    ⇒   ⊢ (((∗ ‘(A / (abs ‘A))) · A) + ((A / (abs ‘A)) · (∗ ‘A))) = (2 · (abs ‘A))
Theorem	abslem2 4867	Lemma involving absolute values.
⊢ A ∈ ℂ    ⇒   ⊢ (A ≠ 0 → (((∗ ‘(A / (abs ‘A))) · A) + ((A / (abs ‘A)) · (∗ ‘A))) = (2 · (abs ‘A)))
Syntax	cfa 4868	Extend class notation to include the factorial of nonnegative integers.
class !
Definition	df-fac 4869	Define the factorial function on nonnegative integers. In the literature, the factorial function is written as a postscript exclamation point.
⊢ ! = (( · seq(I ↾ ℕ)) ∪ {⟨0, 1⟩})
Theorem	facnnt 4870	Value of the factorial function for positive integers.
⊢ (A ∈ ℕ → (! ‘A) = (( · seq(I ↾ ℕ)) ‘A))
Theorem	fac0 4871	The factorial of 0.
⊢ (! ‘0) = 1
Theorem	fac1 4872	The factorial of 1.
⊢ (! ‘1) = 1
Theorem	facp1t 4873	The factorial of a successor.
⊢ (A ∈ ℕ0 → (! ‘(A + 1)) = ((! ‘A) · (A + 1)))
Theorem	facclt 4874	Closure of the factorial function.
⊢ (A ∈ ℕ0 → (! ‘A) ∈ ℕ)
Syntax	cli 4875	Extend class notation with convergence relation for limits.
class ⇝
Definition	df-clim 4876	Define the limit relation for complex number sequences. See clim 4877 for its relational expression. Note that f:ℕ–→ℂ is an infinite sequence of complex numbers, i.e. a mapping from integers to complex numbers.
⊢ ⇝ = {⟨f, w⟩∣((f:ℕ–→ℂ ∧ w ∈ ℂ) ∧ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ (y ≤ z → (abs ‘((f ‘z) − w)) < x)))}
Theorem	clim 4877	Express the predicate: The limit of complex number sequence F is A, or F converges to A. This means that for any real x, no matter how small, there always exists an integer y such that the absolute difference of any later complex number in the sequence and the limit is less than x.
⊢ F ∈ V    &   ⊢ A ∈ V    ⇒   ⊢ (F ⇝ A ↔ ((F:ℕ–→ℂ ∧ A ∈ ℂ) ∧ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ (y ≤ z → (abs ‘((F ‘z) − A)) < x))))
Theorem	climseq 4878	A sequence of complex numbers with a limit is a sequence.
⊢ F ∈ V    &   ⊢ A ∈ V    ⇒   ⊢ (F ⇝ A → F:ℕ–→ℂ)
Theorem	climcn 4879	Closure of the limit of a sequence of complex numbers.
⊢ F ∈ V    &   ⊢ A ∈ V    ⇒   ⊢ (F ⇝ A → A ∈ ℂ)
Theorem	climconv 4880	Convergence of a sequence of complex numbers.
⊢ F ∈ V    &   ⊢ A ∈ V    ⇒   ⊢ (F ⇝ A → ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ (y ≤ z → (abs ‘((F ‘z) − A)) < x)))
Theorem	clim2 4881	The limit of a sequence of complex numbers.
⊢ ((F:ℕ–→ℂ ∧ A ∈ ℂ) → (F ⇝ A ↔ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ (y ≤ z → (abs ‘((F ‘z) − A)) < x))))
Theorem	clim0 4882	The zero sequence converges to zero.
⊢ (ℕ × {0}) ⇝ 0
Theorem	climunii 4883	A sequence of complex numbers converges to at most one limit.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ F ∈ V    &   ⊢ (F ⇝ A ∧ F ⇝ B)    ⇒   ⊢ A = B
Theorem	climuni 4884	A complex number sequence converges to at most one limit.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ F ∈ V    ⇒   ⊢ ((F ⇝ A ∧ F ⇝ B) → A = B)
Theorem	ruclem1 4885	Lemma for ruc 4924 (the reals are uncountable). This is an arithmetic fact that will be used to compute ordering relations.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A < B ↔ A < (((2 · A) + B) / 3))
Theorem	ruclem2 4886	Lemma for ruc 4924. Arithmetic fact that will be used to compute ordering relations.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A < B ↔ (((2 · A) + B) / 3) < ((A + (2 · B)) / 3))
Theorem	ruclem3 4887	Lemma for ruc 4924. Arithmetic fact that will be used to compute ordering relations.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (A < B ↔ ((A + (2 · B)) / 3) < B)
Theorem	ruclem4 4888	Lemma for ruc 4924. Helper lemma showing a tedious equality used several times.
⊢ ((A = C ∧ B = D) → if(((1st ‘A) < B ∧ B < (2nd ‘A)), ⟨(((2 · B) + (2nd ‘A)) / 3), ((B + (2 · (2nd ‘A))) / 3)⟩, ⟨(((2 · (1st ‘A)) + (2nd ‘A)) / 3), (((1st ‘A) + (2 · (2nd ‘A))) / 3)⟩) = if(((1st ‘C) < D ∧ D < (2nd ‘C)), ⟨(((2 · D) + (2nd ‘C)) / 3), ((D + (2 · (2nd ‘C))) / 3)⟩, ⟨(((2 · (1st ‘C)) + (2nd ‘C)) / 3), (((1st ‘C) + (2 · (2nd ‘C))) / 3)⟩))
Theorem	ruclem5 4889	Lemma for ruc 4924. Helper lemma showing the input function used for our sequence builder (defined in ruclem13 4897) is a set.
⊢ F:ℕ–→ℝ    &   ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1})))    ⇒   ⊢ C ∈ V
Theorem	ruclem6 4890	Lemma for ruc 4924. Helper lemma showing the input function used for our sequence builder (defined in ruclem13 4897) matches our input mapping F for successor values.
⊢ F:ℕ–→ℝ    &   ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1})))    ⇒   ⊢ (C ↾ (ℕ ∖ {1})) = (F ↾ (ℕ ∖ {1}))
Theorem	ruclem7 4891	Lemma for ruc 4924. Helper lemma showing the initial value of the input function for our sequence builder (defined in ruclem13 4897).
⊢ F:ℕ–→ℝ    &   ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1})))    ⇒   ⊢ (C ‘1) = ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩
Theorem	ruclem8 4892	Lemma for ruc 4924. Helper lemma showing the successor value of the input function for our sequence builder (defined in ruclem13 4897).
⊢ F:ℕ–→ℝ    &   ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1})))    &   ⊢ A ∈ ℕ    ⇒   ⊢ (C ‘(A + 1)) = (F ‘(A + 1))
Theorem	ruclem9 4893	Lemma for ruc 4924. Helper lemma showing the operation used for our sequence builder (defined in ruclem13 4897) is a set.
⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = A)}    ⇒   ⊢ D ∈ V
Theorem	ruclem10 4894	Lemma for ruc 4924. The values of our sequence builder are pairs of real numbers. The values of our constructed function G are the first of these pairs.
⊢ A ∈ ℕ    &   ⊢ D ∈ V    &   ⊢ C ∈ V    &   ⊢ G = (1st ∘ (DseqC))    ⇒   ⊢ (1st ‘((DseqC) ‘A)) = (G ‘A)
Theorem	ruclem11 4895	Lemma for ruc 4924. The values of our sequence builder are pairs of real numbers. The values of our constructed function H are the second of these pairs.
⊢ A ∈ ℕ    &   ⊢ D ∈ V    &   ⊢ C ∈ V    &   ⊢ H = (2nd ∘ (DseqC))    ⇒   ⊢ (2nd ‘((DseqC) ‘A)) = (H ‘A)
Theorem	ruclem12 4896	Lemma for ruc 4924. A helper lemma that changes bound variables.
⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1st ‘x) < y ∧ y < (2nd ‘x)), ⟨(((2 · y) + (2nd ‘x)) / 3), ((y + (2 · (2nd ‘x))) / 3)⟩, ⟨(((2 · (1st ‘x)) + (2nd ‘x)) / 3), (((1st ‘x) + (2 · (2nd ‘x))) / 3)⟩))}    ⇒   ⊢ D = {⟨⟨w, v⟩, u⟩∣((w ∈ (ℝ × ℝ) ∧ v ∈ ℝ) ∧ u = if(((1st ‘w) < v ∧ v < (2nd ‘w)), ⟨(((2 · v) + (2nd ‘w)) / 3), ((v + (2 · (2nd ‘w))) / 3)⟩, ⟨(((2 · (1st ‘w)) + (2nd ‘w)) / 3), (((1st ‘w) + (2 · (2nd ‘w))) / 3)⟩))}
Theorem	ruclem13 4897	Lemma for ruc 4924. A helper lemma showing the sequence builder used for our construction maps natural numbers to pairs of reals.
⊢ F:ℕ–→ℝ    &   ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1})))    &   ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1st ‘x) < y ∧ y < (2nd ‘x)), ⟨(((2 · y) + (2nd ‘x)) / 3), ((y + (2 · (2nd ‘x))) / 3)⟩, ⟨(((2 · (1st ‘x)) + (2nd ‘x)) / 3), (((1st ‘x) + (2 · (2nd ‘x))) / 3)⟩))}    ⇒   ⊢ (DseqC):ℕ–→(ℝ × ℝ)
Theorem	ruclem14 4898	Lemma for ruc 4924. A helper lemma showing the initial value of the sequence builder used for our construction.
⊢ F:ℕ–→ℝ    &   ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1})))    &   ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1st ‘x) < y ∧ y < (2nd ‘x)), ⟨(((2 · y) + (2nd ‘x)) / 3), ((y + (2 · (2nd ‘x))) / 3)⟩, ⟨(((2 · (1st ‘x)) + (2nd ‘x)) / 3), (((1st ‘x) + (2 · (2nd ‘x))) / 3)⟩))}    &   ⊢ G = (1st ∘ (DseqC))    &   ⊢ H = (2nd ∘ (DseqC))    ⇒   ⊢ ((DseqC) ‘1) = ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩
Theorem	ruclem15 4899	Lemma for ruc 4924. A helper lemma showing the successor value of the sequence builder used for our construction.
⊢ F:ℕ–→ℝ    &   ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1})))    &   ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1st ‘x) < y ∧ y < (2nd ‘x)), ⟨(((2 · y) + (2nd ‘x)) / 3), ((y + (2 · (2nd ‘x))) / 3)⟩, ⟨(((2 · (1st ‘x)) + (2nd ‘x)) / 3), (((1st ‘x) + (2 · (2nd ‘x))) / 3)⟩))}    &   ⊢ G = (1st ∘ (DseqC))    &   ⊢ H = (2nd ∘ (DseqC))    &   ⊢ A ∈ ℕ    ⇒   ⊢ ((DseqC) ‘(A + 1)) = if(((G ‘A) < (F ‘(A + 1)) ∧ (F ‘(A + 1)) < (H ‘A)), ⟨(((2 · (F ‘(A + 1))) + (H ‘A)) / 3), (((F ‘(A + 1)) + (2 · (H ‘A))) / 3)⟩, ⟨(((2 · (G ‘A)) + (H ‘A)) / 3), (((G ‘A) + (2 · (H ‘A))) / 3)⟩)
Theorem	ruclem16 4900	Lemma for ruc 4924. A helper lemma showing the initial value of our constructed G.
⊢ F:ℕ–→ℝ    &   ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1})))    &   ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1st ‘x) < y ∧ y < (2nd ‘x)), ⟨(((2 · y) + (2nd ‘x)) / 3), ((y + (2 · (2nd ‘x))) / 3)⟩, ⟨(((2 · (1st ‘x)) + (2nd ‘x)) / 3), (((1st ‘x) + (2 · (2nd ‘x))) / 3)⟩))}    &   ⊢ G = (1st ∘ (DseqC))    &   ⊢ H = (2nd ∘ (DseqC))    ⇒   ⊢ (G ‘1) = ((F ‘1) + 1)