Discrete-Math/Exercise 1.1 at master · A454545/Discrete-Math · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
Theorem (15.17) “Self-inverse of unary minus”:
   - (- a) = a
Proof:
    (- (- a))
  =⟨ “Identity of +” ⟩
    (- (- a)) + 0
  =⟨ “Unary minus” ⟩
    (- (- a)) + (a + (- a))
  =⟨ “Symmetry of +” ⟩
    (- (- a)) + ((- a) + a)
  =⟨ “Associativity of +” ⟩
    ((- (- a)) + (- a)) + a
  =⟨ “Symmetry of +” ⟩
    ((- a) + (- (- a))) + a
  =⟨ “Unary minus” ⟩
    0 + a
  =⟨ “Identity of +” ⟩
    a

Theorem (15.18) “Fixpoint of unary minus”: - 0 = 0
Proof:
    - 0
  =⟨ “Identity of +” ⟩
    0 + - 0
  =⟨ “Unary minus” ⟩
    0

Theorem (15.20): - a = (- 1) · a
Proof:
    - a = (- 1) · a
  =⟨ “Identity of +” ⟩
    0 + - a  = (- 1) · a
  =⟨ “Unary minus” ⟩
    ((1) · a + - (1 · a)) + - a = (- 1) · a
  =⟨ “Identity of ·” ⟩
    (a + - (1 · a)) + - a = (- 1) · a
  =⟨ “Symmetry of +” ⟩
    ( - (1 · a) + a) + - a = (- 1) · a
  =⟨ “Associativity of +” ⟩
    - (1 · a) + (a + - a) = (- 1) · a
  =⟨ “Unary minus” ⟩
    - (1 · a) + 0 = (- 1) · a
  =⟨ “Identity of +” ⟩
    - (1 · a) + 0 = (- 1) · a + 0
  =⟨ “Unary minus” ⟩
    - (1 · a) + ((- (1 · a)) + (- (- (1 · a))) = (- 1) · a + 0

    Theorem (15.20): - a = (- 1) · a
Proof:
    - a
  =⟨ “Identity of +” with `a ≔ - a` ⟩
    0 + (- a)
  =⟨ “Zero of ·” with `a ≔ a` ⟩
    0 · a + (- a)
  =⟨ “Unary minus” with `a ≔ 1` ⟩
    (1 + (- 1)) · a + (- a)
  =⟨ “Symmetry of ·” with `a, b ≔ (1 + (- 1)), a` ⟩
    a · (1 + (- 1)) + (- a)
  =⟨ “Distributivity of · over +” with `a, b, c ≔ a, 1, - 1` ⟩
    1 · a + (- 1) · a + (- a)
  =⟨ “Identity of ·” with `a ≔ a` ⟩
    (- 1) · a + a + (- a)
  =⟨ “Unary minus” with `a ≔ a` ⟩
    (- 1) · a + 0
  =⟨ “Identity of +” with `a ≔ (- 1) · a` ⟩
    (- 1) · a

    Theorem (15.19) “Distributivity of unary minus over +”:
    - (a + b) = (- a) + (- b)
Proof:
    - (a + b)
  =⟨ (15.20) with `a ≔ (a + b)` ⟩
    (- 1) · (a + b)
  =⟨ “Distributivity of · over +” with `a, b, c ≔ (- 1), a, b ` ⟩
    (- 1) · a + (- 1) · b
  =⟨ (15.20) with `a ≔ a` ⟩
    - a + (- 1) · b
  =⟨ (15.20) with `a ≔ b` ⟩
    - a + - b