hughmcguire
x = 2 if and only if x³ - 2·x² + x = 2
| (#) | Comments | Suppositions and derivations | Theorem and subgoals |
|---|---|---|---|
| We presuppose the following: | |||
| (1) |
(∀a,b)[a = b ↔ a - b = 0] |
||
| (2) |
(∀a,b,c,d) [(a - b + c) - d = (a - b) + (c - d)] |
||
| (3) |
(∀a)[a³ = a·a²] |
||
| (4) |
(∀a,b,c)[a·c - b·c = (a - b)·c] |
||
| (5) |
(∀a,b)[a·b + a = a(b + 1)] |
||
| (6) |
(∀a,b)[a·b = 0 ↔ a = 0 ∨ b = 0] |
||
| (7) |
(∀a)[¬(a² + 1 = 0)] |
||
|
We start working with the formula being proved as follows: |
|||
| (8) |
x = 2 if and only if x³ - 2·x² + x = 2 |
||
≡ by rewriting the form "φ1 if and only if φ2"to " (φ1 implies φ2) and (φ2 implies φ1)" |
|||
| (9) |
(x = 2 implies x³ - 2·x² + x = 2) and (x³ - 2·x² + x = 2 implies x = 2) |
||
|
We'll handle that formula's subparts in separate cases (below): |
|||
| Formula (7) ≡ by simplifying | |||
| (10) | [unused] |
(∀a)[¬(a² = -1)] |
|
| Case 1: | |||
| (11) |
x = 2 implies x³ - 2·x² + x = 2 |
||
| We'll assume that formula's antecedent: | |||
| (12) |
x = 2 |
||
| and we'll work on proving the consequent: | |||
| (13) |
x³ - 2·x² + x = 2 |
||
| ≡ by (12) | |||
| (14) |
2³ - 2·2² + 2 = 2 |
||
| ≡ by simplifying | |||
| (15) |
true |
||
| That concludes the proof for this case. | |||
| Case 2: | |||
| (16) |
x³ - 2·x² + x = 2 implies x = 2 |
||
| We'll assume that formula's antecedent: | |||
| (17) |
x³ - 2·x² + x = 2 |
||
| and we'll work on proving the consequent: | |||
| (18) |
x = 2 |
||
|
Applying the equivalence in formula (1) to formula (17) with " a := x³-2·x²+x, b := 2"yields: |
|||
| (19) |
(x³ - 2·x² + x) - 2 = 0 |
||
≡ by (2) with "a := x³, b := 2·x², c := x, d := 2" |
|||
| (20) |
[(x³ - (2·x²)) + (x - 2)] = 0 |
||
≡ by (3) with "a := x" |
|||
| (21) |
[([x·x²] - (2·x²)) + (x - 2)] = 0 |
||
≡ by (4) with "a := x, c := x², b := 2" |
|||
| (22) |
[[(x - 2)·x²] + (x - 2)] = 0 |
||
≡ by (5) with "a := x-2, b := x²" |
|||
| (23) |
[(x - 2)(x² + 1)] = 0 |
||
≡ by (6) with "a := x-2, b := x²+1" |
|||
| (24) |
(x - 2) = 0 ∨ (x² + 1) = 0 |
||
↓ by (7) with "a := x" |
|||
| (25) |
(x - 2) = 0 ∨ false |
||
| ≡ by simplifying | |||
| (26) |
x = 2 |
||
|
And formula (26) matches formula (18) so we get: |
|||
| (27) |
true |
||
| That concludes the proof for this case. | |||
| Thus, the theorem that was given is true in all cases. |
identification:
1214420400842
1214419898420
502422