Statement List for Metamath Proof Explorer - 4701-4800 - Page 48 of 58
| Type | Label | Description |
|---|
| Statement |
|---|
| |
| Theorem | le2sqe 4701 |
Two nonnegative reals compare the same as their squares.
|
| ⊢
A ∈ ℝ
& ⊢ B ∈ ℝ
⇒ ⊢ ((0 ≤
A ∧ 0 ≤ B) → (A
≤ B ↔ (A↑2) ≤ (B↑2))) |
| |
| Theorem | sqe11 4702 |
The square function is one-to-one for nonnegative reals.
|
| ⊢
A ∈ ℝ
& ⊢ B ∈ ℝ
⇒ ⊢ ((0 ≤
A ∧ 0 ≤ B) → ((A↑2) = (B↑2) ↔ A = B)) |
| |
| Theorem | sqegt0 4703 |
The square of a non-zero real is positive.
|
| ⊢
A ∈ ℝ
⇒ ⊢ (A ≠ 0 → 0 < (A↑2)) |
| |
| Theorem | sqege0 4704 |
A square of a real is nonnegative.
|
| ⊢
A ∈ ℝ
⇒ ⊢ 0 ≤ (A↑2) |
| |
| Theorem | sqe11t 4705 |
The square function is one-to-one for nonnegative reals.
|
| ⊢
((A ∈ ℝ ∧ B ∈ ℝ) → ((0 ≤ A ∧ 0 ≤ B) → ((A↑2) = (B↑2) ↔ A = B))) |
| |
| Theorem | lt2sqet 4706 |
Two nonnegative numbers compare the same as their squares.
|
| ⊢
((A ∈ ℝ ∧ B ∈ ℝ) → ((0 ≤ A ∧ 0 ≤ B) → (A
< B ↔ (A↑2) < (B↑2)))) |
| |
| Theorem | le2sqet 4707 |
Two nonnegative numbers compare the same as their squares.
|
| ⊢
((A ∈ ℝ ∧ B ∈ ℝ) → ((0 ≤ A ∧ 0 ≤ B) → (A
≤ B ↔ (A↑2) ≤ (B↑2)))) |
| |
| Theorem | sqege0t 4708 |
A square of a real is nonnegative.
|
| ⊢
(A ∈ ℝ → 0 ≤
(A↑2)) |
| |
| Theorem | sq1 4709 |
The square of 1 is 1.
|
| ⊢
(1↑2) = 1 |
| |
| Theorem | sq2 4710 |
The square of 2 is 4.
|
| ⊢
(2↑2) = 4 |
| |
| Theorem | cu2 4711 |
The cube of 2 is 8.
|
| ⊢
(2↑3) = 8 |
| |
| Theorem | binom 4712 |
Binomial expansion.
|
| ⊢
A ∈ ℂ
& ⊢ B ∈ ℂ
⇒ ⊢ ((A + B)↑2)
= (((A↑2) + (2 · (A · B)))
+ (B↑2)) |
| |
| Theorem | discrlem1 4713 |
Lemma for discriminant theorem.
|
| ⊢
A ∈ ℝ
& ⊢ B ∈ ℝ
& ⊢ C ∈ ℝ
& ⊢ D = -(B / (2
· A))
& ⊢ 0 < A ⇒ ⊢ (0 ≤ (((A · (D↑2)) + (B
· D)) + C) ↔ ((B↑2) − (4 · (A · C)))
≤ 0) |
| |
| Theorem | discrlem2 4714 |
Lemma for discriminant theorem.
|
| ⊢
A ∈ ℝ
& ⊢ B ∈ ℝ
& ⊢ C ∈ ℝ
& ⊢ D = -(B / (2
· A))
& ⊢ (D ∈ ℝ → 0 ≤ (((A · (D↑2)) + (B
· D)) + C))
⇒ ⊢ (0 < A → ((B↑2) − (4 · (A · C)))
≤ 0) |
| |
| Theorem | discrlem3 4715 |
Lemma for discriminant theorem.
|
| ⊢
A ∈ ℝ
& ⊢ B ∈ ℝ
& ⊢ C ∈ ℝ
& ⊢ D = ((C + 1) /
-B)
& ⊢ (D ∈ ℝ → 0 ≤ (((A · (D↑2)) + (B
· D)) + C))
⇒ ⊢ (0 = A → ((B↑2) − (4 · (A · C)))
≤ 0) |
| |
| Theorem | discrlem 4716 |
If a quadratic polynomial (with a nonnegative high-order coefficient)
is nonnegative for all values, then its discriminant is
non-positive.
|
| ⊢
A ∈ ℝ
& ⊢ B ∈ ℝ
& ⊢ C ∈ ℝ
& ⊢ ∀x ∈ ℝ 0 ≤ (((A · (x↑2)) + (B
· x)) + C) ⇒ ⊢ (0 ≤ A
→ ((B↑2) − (4 ·
(A · C))) ≤ 0) |
| |
| Theorem | nnsqcl 4717 |
The square of a natural number is a natural number.
|
| ⊢
A ∈ ℕ
⇒ ⊢ (A↑2) ∈ ℕ |
| |
| Theorem | nnlesq 4718 |
A natural number is less than or equal to its square.
|
| ⊢
A ∈ ℕ
⇒ ⊢ A ≤ (A↑2) |
| |
| Theorem | nneo 4719 |
A natural number is even or odd but not both.
|
| ⊢
A ∈ ℕ
⇒ ⊢ ((A / 2) ∈ ℕ ↔ ¬ ((A + 1) / 2) ∈ ℕ) |
| |
| Theorem | nnesq 4720 |
A natural number is even iff its square is even.
|
| ⊢
A ∈ ℕ
⇒ ⊢ ((A / 2) ∈ ℕ ↔ ((A↑2) / 2) ∈ ℕ) |
| |
| Theorem | nn0le2sqet 4721 |
Two nonnegative integers compare the same as their squares.
(Contributed by Raph Levien, 10-Dec-02.)
|
| ⊢
A ∈
ℕ0 & ⊢ B ∈
ℕ0 ⇒ ⊢ (A ≤
B ↔ (A · A)
≤ (B · B)) |
| |
| Theorem | nn0opthlem1 4722 |
A rather pretty lemma for nn0opth 4724. (Contributed by Raph Levien,
10-Dec-02.)
|
| ⊢
A ∈
ℕ0 & ⊢ C ∈
ℕ0 ⇒ ⊢ (A <
C ↔ ((A · A) +
(2 · A)) < (C · C)) |
| |
| Theorem | nn0opthlem2 4723 |
Lemma for nn0opth 4724. (Contributed by Raph Levien, 10-Dec-02.)
|
| ⊢
A ∈
ℕ0 & ⊢ B ∈
ℕ0 & ⊢ C ∈
ℕ0 & ⊢ D ∈
ℕ0 ⇒ ⊢ ((B ≤
A ∧ D ≤ C)
→ (A < C → ¬ ((A · A) +
B) = ((C · C) +
D))) |
| |
| Theorem | nn0opth 4724 |
An ordered pair theorem for nonnegative integers. Theorem 17.3 of
[Quine] p. 124. We can represent an
ordered pair of nonnegative
integers A and B by (((A +
B) · (A + B)) +
B). If
two such ordered pairs are equal, their first elements are equal and
their second elements are equal. Contrast this ordered pair
representation with the standard one df-op 1815 that works for any set.
(Contributed by Raph Levien, 10-Dec-02.)
|
| ⊢
A ∈
ℕ0 & ⊢ B ∈
ℕ0 & ⊢ C ∈
ℕ0 & ⊢ D ∈
ℕ0 ⇒ ⊢ ((((A +
B) · (A + B)) +
B) = (((C + D) ·
(C + D)) + D) ↔
(A = C
∧ B = D)) |
| |
| Theorem | nn0opth2 4725 |
An ordered pair theorem for nonnegative integers. Theorem 17.3 of
[Quine] p. 124. See nn0opth 4724.
|
| ⊢
A ∈
ℕ0 & ⊢ B ∈
ℕ0 & ⊢ C ∈
ℕ0 & ⊢ D ∈
ℕ0 ⇒ ⊢ ((((A +
B)↑2) + B) = (((C +
D)↑2) + D) ↔ (A =
C ∧ B = D)) |
| |
| Theorem | nn0opth2t 4726 |
An ordered pair theorem for nonnegative integers. Theorem 17.3 of
[Quine] p. 124. See nn0opth 4724.
|
| ⊢
(((A ∈ ℕ0
∧ B ∈ ℕ0) ∧
(C ∈ ℕ0 ∧
D ∈ ℕ0)) →
((((A + B)↑2) + B)
= (((C + D)↑2) + D)
↔ (A = C ∧ B =
D))) |
| |
| Syntax | csqr 4727 |
Extend class notation to include positive square root of a positive real
number.
|
| class
√ |
| |
| Definition | df-sqr 4728 |
Define a function whose value is the square root of a nonnegative
real number. The square root of x
is the supremum of all reals
whose square is less than x. See sqrcl 4758 for its closure,
sqrval 4729 for its value, sqrsqe 4774 and sqsqr 4775 for its relationship to
squares, and sqr11 4761 for uniqueness.
|
| ⊢
√ = {⟨x, y⟩∣((x ∈ ℝ ∧ 0 ≤ x) ∧ y =
sup({z ∈ ℝ∣(0 ≤
z ∧ (z · z)
≤ x)}, ℝ, < ))} |
| |
| Theorem | sqrval 4729 |
Value of square root function.
|
| ⊢
((A ∈ ℝ ∧ 0 ≤
A) → (√ ‘A) = sup({x
∈ ℝ∣(0 ≤ x ∧
(x · x) ≤ A)},
ℝ, < )) |
| |
| Theorem | sqr0 4730 |
Square root of zero.
|
| ⊢
(√ ‘0) = 0 |
| |
| Theorem | sqrlem1 4731 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A ⇒ ⊢ A < ((1
+ A) · (1 + A)) |
| |
| Theorem | sqrlem2 4732 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A ⇒ ⊢ ((A / (1 +
A)) · (A / (1 + A)))
< A |
| |
| Theorem | sqrlem3 4733 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A ⇒ ⊢ 0 < (A /
(1 + A)) |
| |
| Theorem | sqrlem4 4734 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ S =
{x ∈ ℝ∣(0 ≤ x ∧ (x
· x) ≤ A)}
⇒ ⊢ (D ∈ S
↔ (D ∈ ℝ ∧ (0 ≤
D ∧ (D · D)
≤ A))) |
| |
| Theorem | sqrlem5 4735 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ S =
{x ∈ ℝ∣(0 ≤ x ∧ (x
· x) ≤ A)}
⇒ ⊢ ((D ∈ ℝ ∧ (0 < D ∧ (D
· D) < A)) → D
∈ S) |
| |
| Theorem | sqrlem6 4736 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ S =
{x ∈ ℝ∣(0 ≤ x ∧ (x
· x) ≤ A)}
⇒ ⊢ (S ⊆ ℝ ∧ S ≠ ∅ ∧ ∃x ∈ ℝ ∀y ∈ S
y < x) |
| |
| Theorem | sqrlem7 4737 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ S =
{x ∈ ℝ∣(0 ≤ x ∧ (x
· x) ≤ A)} & ⊢ B =
sup(S, ℝ, < )
⇒ ⊢ B ∈ ℝ |
| |
| Theorem | sqrlem8 4738 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ S =
{x ∈ ℝ∣(0 ≤ x ∧ (x
· x) ≤ A)} & ⊢ B =
sup(S, ℝ, < )
⇒ ⊢ 0 < B |
| |
| Theorem | sqrlem9 4739 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ B ∈
ℝ & ⊢
C ∈ ℝ
& ⊢ 0 < B & ⊢ A <
(B · B) & ⊢ C =
((B + (A / B)) / (1 +
1)) ⇒ ⊢
0 < C |
| |
| Theorem | sqrlem10 4740 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ B ∈
ℝ & ⊢
C ∈ ℝ
& ⊢ 0 < B & ⊢ A <
(B · B) & ⊢ C =
((B + (A / B)) / (1 +
1)) ⇒ ⊢
C < B |
| |
| Theorem | sqrlem11 4741 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ B ∈
ℝ & ⊢
C ∈ ℝ
& ⊢ 0 < B & ⊢ A <
(B · B) & ⊢ C =
((B + (A / B)) / (1 +
1)) ⇒ ⊢
A < (C · C) |
| |
| Theorem | sqrlem12 4742 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ B ∈
ℝ & ⊢
C ∈ ℝ
& ⊢ 0 < B & ⊢ A <
(B · B) & ⊢ C =
((B + (A / B)) / (1 +
1)) & ⊢
S = {x ∈ ℝ∣(0 ≤ x ∧ (x
· x) ≤ A)}
⇒ ⊢ (D ∈ S
→ D < C) |
| |
| Theorem | sqrlem13 4743 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ B ∈
ℝ & ⊢
C ∈ ℝ
& ⊢ 0 < B & ⊢ A <
(B · B) & ⊢ C =
((B + (A / B)) / (1 +
1)) & ⊢
S = {x ∈ ℝ∣(0 ≤ x ∧ (x
· x) ≤ A)}
⇒ ⊢ (B = sup(S,
ℝ, < ) → ¬ C <
B) |
| |
| Theorem | sqrlem14 4744 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ B ∈
ℝ & ⊢
C ∈ ℝ
& ⊢ 0 < B & ⊢ A <
(B · B) & ⊢ C =
((B + (A / B)) / (1 +
1)) & ⊢
S = {x ∈ ℝ∣(0 ≤ x ∧ (x
· x) ≤ A)}
⇒ ⊢ ¬ B = sup(S,
ℝ, < ) |
| |
| Theorem | sqrlem15 4745 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ B ∈
ℝ & ⊢
0 < B
& ⊢ C ∈ ℝ
& ⊢ 0 < C ⇒ ⊢ B <
(B + C) |
| |
| Theorem | sqrlem16 4746 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ B ∈
ℝ & ⊢
0 < B
& ⊢ C ∈ ℝ
& ⊢ 0 < C & ⊢ C <
B
⇒ ⊢ (C < ((A
− (B · B)) / (((1 + 1) + 1) · B)) → ((B
+ C) · (B + C)) <
A) |
| |
| Theorem | sqrlem17 4747 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ B ∈
ℝ & ⊢
0 < B
& ⊢ C ∈ ℝ
& ⊢ 0 < C & ⊢ C <
B
& ⊢ S = {x ∈
ℝ∣(0 ≤ x ∧ (x · x)
≤ A)}
⇒ ⊢ (C < ((A
− (B · B)) / (((1 + 1) + 1) · B)) → (B +
C) ∈ S) |
| |
| Theorem | sqrlem18 4748 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ B ∈
ℝ & ⊢
0 < B
& ⊢ C ∈ ℝ
& ⊢ 0 < C & ⊢ C <
B
& ⊢ S = {x ∈
ℝ∣(0 ≤ x ∧ (x · x)
≤ A)}
⇒ ⊢ (C < ((A
− (B · B)) / (((1 + 1) + 1) · B)) → ¬ B = sup(S,
ℝ, < )) |
| |
| Theorem | sqrlem19 4749 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ B ∈
ℝ & ⊢
0 < B
& ⊢ (B · B)
< A
⇒ ⊢ 0 <
((A − (B · B))
/ (((1 + 1) + 1) · B)) |
| |
| Theorem | sqrlem20 4750 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ B ∈
ℝ & ⊢
0 < B
& ⊢ (B · B)
< A
& ⊢ S = {x ∈
ℝ∣(0 ≤ x ∧ (x · x)
≤ A)}
⇒ ⊢ ¬ B = sup(S,
ℝ, < ) |
| |
| Theorem | sqrlem21 4751 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ S =
{x ∈ ℝ∣(0 ≤ x ∧ (x
· x) ≤ A)} & ⊢ B =
sup(S, ℝ, < )
⇒ ⊢ ¬ A < (B
· B) |
| |
| Theorem | sqrlem22 4752 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ S =
{x ∈ ℝ∣(0 ≤ x ∧ (x
· x) ≤ A)} & ⊢ B =
sup(S, ℝ, < )
⇒ ⊢ ¬ (B · B)
< A |
| |
| Theorem | sqrlem23 4753 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A & ⊢ S =
{x ∈ ℝ∣(0 ≤ x ∧ (x
· x) ≤ A)} & ⊢ B =
sup(S, ℝ, < )
⇒ ⊢ (B · B) =
A |
| |
| Theorem | sqrlem24 4754 |
Lemma for square root closure.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A ⇒ ⊢ (√ ‘A) ∈ ℝ |
| |
| Theorem | sqrgt0i 4755 |
The square root of a positive real is positive.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A ⇒ ⊢ 0 < (√ ‘A) |
| |
| Theorem | sqrlem26 4756 |
Lemma for square root theorem.
|
| ⊢
A ∈ ℝ
& ⊢ 0 < A ⇒ ⊢ ((√ ‘A) · (√ ‘A)) = A |
| |
| Theorem | sqrth 4757 |
Square root theorem. Theorem I.35 of [Apostol] p. 29.
|
| ⊢
A ∈ ℝ
⇒ ⊢ (0 ≤ A → ((√ ‘A) · (√ ‘A)) = A) |
| |
| Theorem | sqrcl 4758 |
The square root of a nonnegative real is a real.
|
| ⊢
A ∈ ℝ
⇒ ⊢ (0 ≤ A → (√ ‘A) ∈ ℝ) |
| |
| Theorem | sqrgt0 4759 |
The square root of a positive real is positive.
|
| ⊢
A ∈ ℝ
⇒ ⊢ (0 < A → 0 < (√ ‘A)) |
| |
| Theorem | sqrge0 4760 |
The square root of a nonnegative real is nonnegative.
|
| ⊢
A ∈ ℝ
⇒ ⊢ (0 ≤ A → 0 ≤ (√ ‘A)) |
| |
| Theorem | sqr11 4761 |
The square root function is one-to-one.
|
| ⊢
A ∈ ℝ
& ⊢ B ∈ ℝ
⇒ ⊢ ((0 ≤
A ∧ 0 ≤ B) → ((√ ‘A) = (√ ‘B) ↔ A =
B)) |
| |
| Theorem | sqrmuli 4762 |
Square root distributes over multiplication.
|
| ⊢
A ∈ ℝ
& ⊢ B ∈ ℝ
& ⊢ 0 ≤ A & ⊢ 0 ≤ B ⇒ ⊢ (√ ‘(A · B))
= ((√ ‘A) · (√
‘B)) |
| |
| Theorem | sqrmul 4763 |
Square root distributes over multiplication.
|
| ⊢
A ∈ ℝ
& ⊢ B ∈ ℝ
⇒ ⊢ ((0 ≤
A ∧ 0 ≤ B) → (√ ‘(A · B))
= ((√ ‘A) · (√
‘B))) |
| |
| Theorem | sqrsq 4764 |
Relationship between square root and squares.
|
| ⊢
A ∈ ℝ
& ⊢ B ∈ ℝ
⇒ ⊢ ((0 ≤
A ∧ 0 ≤ B) → ((√ ‘A) = B ↔
A = (B
· B))) |
| |
| Theorem | sqrle 4765 |
Square root is monotonic.
|
| ⊢
A ∈ ℝ
& ⊢ B ∈ ℝ
⇒ ⊢ ((0 ≤
A ∧ 0 ≤ B) → (A
≤ B ↔ (√ ‘A) ≤ (√ ‘B))) |
| |
| Theorem | sqrsqid 4766 |
Square root of square.
|
| ⊢
A ∈ ℝ
⇒ ⊢ (0 ≤ A → (√ ‘(A · A))
= A) |
| |
| Theorem | sqrclt 4767 |
The square root of a nonnegative real is a real.
|
| ⊢
((A ∈ ℝ ∧ 0 ≤
A) → (√ ‘A) ∈ ℝ) |
| |
| Theorem | sqrgt0t 4768 |
The square root of a positive real is positive.
|
| ⊢
((A ∈ ℝ ∧ 0 <
A) → 0 < (√ ‘A)) |
| |
| Theorem | sqrge0t 4769 |
The square root of a nonnegative real is nonnegative.
|
| ⊢
((A ∈ ℝ ∧ 0 ≤
A) → 0 ≤ (√ ‘A)) |
| |
| Theorem | sqr00t 4770 |
A square root is zero iff its argument is 0.
|
| ⊢
((A ∈ ℝ ∧ 0 ≤
A) → ((√ ‘A) = 0 ↔ A
= 0)) |
| |
| Theorem | sqr1 4771 |
The square root of 1 is 1.
|
| ⊢
(√ ‘1) = 1 |
| |
| Theorem | sqr4 4772 |
The square root of 4 is 2.
|
| ⊢
(√ ‘4) = 2 |
| |
| Theorem | sqr9 4773 |
The square root of 9 is 3.
|
| ⊢
(√ ‘9) = 3 |
| |
| Theorem | sqrsqe 4774 |
Square root of square.
|
| ⊢
A ∈ ℝ
⇒ ⊢ (0 ≤ A → (√ ‘(A↑2)) = A) |
| |
| Theorem | sqsqr 4775 |
Square of square root.
|
| ⊢
A ∈ ℝ
⇒ ⊢ (0 ≤ A → ((√ ‘A)↑2) = A) |
| |
| Theorem | sqsqrt 4776 |
Square of square root.
|
| ⊢
((A ∈ ℝ ∧ 0 ≤
A) → ((√ ‘A)↑2) = A) |
| |
| Theorem | sqr2irrlem1 4777 |
Lemma for irrationality of square root of 2. Technical lemma used
to simplify the main induction step.
|
| ⊢
A ∈ ℕ
& ⊢ B ∈ ℕ
⇒ ⊢ ((A↑2) = (2 · (B↑2)) → ((B < A ∧
(A / 2) ∈ ℕ) ∧ (B↑2) = (2 · ((A / 2)↑2)))) |
| |
| Theorem | sqr2irrlem2 4778 |
Lemma for irrationality of square root of 2. Eliminates hypotheses with
weak deduction theorem.
|
| ⊢
((A ∈ ℕ ∧ B ∈ ℕ) → ((A↑2) = (2 · (B↑2)) → ((B < A ∧
(A / 2) ∈ ℕ) ∧ (B↑2) = (2 · ((A / 2)↑2))))) |
| |
| Theorem | sqr2irrlem3 4779 |
Main theorem for irrationality of square root of 2. There are no
natural numbers such that the square of one is twice the square of the
other. Uses strong induction.
|
| ⊢
¬ ∃x ∈ ℕ
∃y ∈ ℕ (x↑2) = (2 · (y↑2)) |
| |
| Theorem | sqr2irrlem4 4780 |
Lemma for irrationality of square root of 2.
|
| ⊢
A ∈ ℕ
& ⊢ B ∈ ℕ
⇒ ⊢ ((√
‘2) = (A / B) ↔ (A↑2) = (2 · (B↑2))) |
| |
| Theorem | sqr2irrlem5 4781 |
Lemma for irrationality of square root of 2. Eliminates hypotheses with
weak deduction theorem.
|
| ⊢
((A ∈ ℕ ∧ B ∈ ℕ) → ((√ ‘2) =
(A / B) ↔ (A↑2) = (2 · (B↑2)))) |
| |
| Theorem | sqr2irr 4782 |
The square root of 2 is irrational.
|
| ⊢
(√ ‘2) ∉ ℚ |
| |
| Theorem | sqr2re 4783 |
The square root of 2 exists and is a real number.
|
| ⊢
(√ ‘2) ∈ ℝ |
| |
| Theorem | nthruc 4784 |
The sequence ℕ, ℤ, ℚ, ℝ, and ℂ forms
a chain of proper subsets. In each case the proper subset
relationship is shown by demonstrating a number that belongs to
one set but not the other. We show that zero belongs to ℤ
but not ℕ, one-half belongs to ℚ but not ℤ,
the square root of 2 belongs to ℝ but not ℚ, and finally
that the imaginary number i belongs to ℂ but not ℝ.
See nthruz 4785 for a further refinement.
|
| ⊢
((ℕ ⊂ ℤ ∧ ℤ ⊂ ℚ) ∧ (ℚ
⊂ ℝ ∧ ℝ ⊂ ℂ)) |
| |
| Theorem | nthruz 4785 |
The sequence ℕ, ℕ0, and ℤ forms a chain of proper
subsets. In each case the proper subset relationship is shown by
demonstrating a number that belongs to one set but not the other. We
show that zero belongs to ℕ0 but not ℕ and minus
one belongs
to ℤ but not ℕ0. This theorem refines the chain
of proper
subsets nthruc 4784.
|
| ⊢
(ℕ ⊂ ℕ0 ∧ ℕ0 ⊂
ℤ) |
| |
| Syntax | cre 4786 |
Extend class notation to include real part of a complex number.
|
| class
ℜ |
| |
| Syntax | cim 4787 |
Extend class notation to include imaginary part of a complex number.
|
| class
ℑ |
| |
| Syntax | ccj 4788 |
Extend class notation to include complex conjugate function.
|
| class
∗ |
| |
| Syntax | cabs 4789 |
Extend class notation to include a function for the absolute value
(modulus) of a complex number.
|
| class
abs |
| |
| Definition | df-re 4790 |
Define a function whose value is the real part of a complex number.
See revalt 4794 for its value, recl 4802
for its closure, and replimt 4798
for its use in decomposing a complex number.
|
| ⊢
ℜ = {⟨x, y⟩∣(x ∈ ℂ ∧ y = ∪{z ∈ ℝ∣∃w ∈ ℝ x = (z +
(w · i))})} |
| |
| Definition | df-im 4791 |
Define a function whose value is the imaginary part of a complex
number. See imvalt 4795 for its value, imcl 4803
for its closure, and
replimt 4798 for its use in decomposing a complex number.
|
| ⊢
ℑ = {⟨x, y⟩∣(x ∈ ℂ ∧ y = ∪{w ∈ ℝ∣∃z ∈ ℝ x = (z +
(w · i))})} |
| |
| Definition | df-cj 4792 |
Define the complex conjugate function. See cjcl 4804
for its closure and
cjvalt 4799 for its value.
|
| ⊢
∗ = {⟨x, y⟩∣(x ∈ ℂ ∧ y = ((ℜ ‘x) − ((ℑ ‘x) · i)))} |
| |
| Definition | df-abs 4793 |
Define the function for the absolute value (modulus) of a complex
number. See abscl 4840 for its closure and absvalt 4801 or absval2 4836
for its value.
|
| ⊢
abs = {⟨x, y⟩∣(x ∈ ℂ ∧ y = (√ ‘(x · (∗ ‘x))))} |
| |
| Theorem | revalt 4794 |
The value of the real part of a complex number.
|
| ⊢
(A ∈ ℂ → (ℜ
‘A) = ∪{x ∈
ℝ∣∃y ∈ ℝ
A = (x
+ (y · i))}) |
| |
| Theorem | imvalt 4795 |
The value of the imaginary part of a complex number.
|
| ⊢
(A ∈ ℂ → (ℑ
‘A) = ∪{y ∈
ℝ∣∃x ∈ ℝ
A = (x
+ (y · i))}) |
| |
| Theorem | reclt 4796 |
The real part of a complex number is real.
|
| ⊢
(A ∈ ℂ → (ℜ
‘A) ∈ ℝ) |
| |
| Theorem | imclt 4797 |
The imaginary part of a complex number is real.
|
| ⊢
(A ∈ ℂ → (ℑ
‘A) ∈ ℝ) |
| |
| Theorem | replimt 4798 |
Construct a complex number from its real and imaginary parts.
|
| ⊢
(A ∈ ℂ → A = ((ℜ ‘A) + ((ℑ ‘A) · i))) |
| |
| Theorem | cjvalt 4799 |
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.
|
| ⊢
(A ∈ ℂ → (∗
‘A) = ((ℜ ‘A) − ((ℑ ‘A) · i))) |
| |
| Theorem | cjclt 4800 |
The conjugate of a complex number is a complex number (closure law).
|
| ⊢
(A ∈ ℂ → (∗
‘A) ∈ ℂ) |
Home
Hilbert Space Explorer
(4958-5787)