Theorem zneqb ≪ | index | src | ≫ 

theorem zneqb (a b c d: nat): $ a -ZN c = b -ZN d <-> a + d = b + c $;
StepHypRefExpression
1 ifpos 
a < c -> if (a < c) (b1 (c - suc a)) (b0 (a - c)) = b1 (c - suc a)
2 1 conv znsub 
a < c -> a -ZN c = b1 (c - suc a)
3 2 anwl 
a < c /\ b < d -> a -ZN c = b1 (c - suc a)
4 ifpos 
b < d -> if (b < d) (b1 (d - suc b)) (b0 (b - d)) = b1 (d - suc b)
5 4 conv znsub 
b < d -> b -ZN d = b1 (d - suc b)
6 5 anwr 
a < c /\ b < d -> b -ZN d = b1 (d - suc b)
7 3, 6 eqeqd 
a < c /\ b < d -> (a -ZN c = b -ZN d <-> b1 (c - suc a) = b1 (d - suc b))
8 bitr4 
(b1 (c - suc a) = b1 (d - suc b) <-> c - suc a = d - suc b) ->
  (suc (a + b) + (d - suc b) = suc (a + b) + (c - suc a) <-> c - suc a = d - suc b) ->
  (b1 (c - suc a) = b1 (d - suc b) <-> suc (a + b) + (d - suc b) = suc (a + b) + (c - suc a))
9 b1can 
b1 (c - suc a) = b1 (d - suc b) <-> c - suc a = d - suc b
10 8, 9 ax_mp 
(suc (a + b) + (d - suc b) = suc (a + b) + (c - suc a) <-> c - suc a = d - suc b) ->
  (b1 (c - suc a) = b1 (d - suc b) <-> suc (a + b) + (d - suc b) = suc (a + b) + (c - suc a))
11 bitr 
(suc (a + b) + (d - suc b) = suc (a + b) + (c - suc a) <-> d - suc b = c - suc a) ->
  (d - suc b = c - suc a <-> c - suc a = d - suc b) ->
  (suc (a + b) + (d - suc b) = suc (a + b) + (c - suc a) <-> c - suc a = d - suc b)
12 addcan2 
suc (a + b) + (d - suc b) = suc (a + b) + (c - suc a) <-> d - suc b = c - suc a
13 11, 12 ax_mp 
(d - suc b = c - suc a <-> c - suc a = d - suc b) -> (suc (a + b) + (d - suc b) = suc (a + b) + (c - suc a) <-> c - suc a = d - suc b)
14 eqcomb 
d - suc b = c - suc a <-> c - suc a = d - suc b
15 13, 14 ax_mp 
suc (a + b) + (d - suc b) = suc (a + b) + (c - suc a) <-> c - suc a = d - suc b
16 10, 15 ax_mp 
b1 (c - suc a) = b1 (d - suc b) <-> suc (a + b) + (d - suc b) = suc (a + b) + (c - suc a)
17 eqtr3 
a + suc b + (d - suc b) = suc (a + b) + (d - suc b) ->
  a + suc b + (d - suc b) = a + (suc b + (d - suc b)) ->
  suc (a + b) + (d - suc b) = a + (suc b + (d - suc b))
18 addeq1 
a + suc b = suc (a + b) -> a + suc b + (d - suc b) = suc (a + b) + (d - suc b)
19 addS2 
a + suc b = suc (a + b)
20 18, 19 ax_mp 
a + suc b + (d - suc b) = suc (a + b) + (d - suc b)
21 17, 20 ax_mp 
a + suc b + (d - suc b) = a + (suc b + (d - suc b)) -> suc (a + b) + (d - suc b) = a + (suc b + (d - suc b))
22 addass 
a + suc b + (d - suc b) = a + (suc b + (d - suc b))
23 21, 22 ax_mp 
suc (a + b) + (d - suc b) = a + (suc b + (d - suc b))
24 pncan3 
suc b <= d -> suc b + (d - suc b) = d
25 24 conv lt 
b < d -> suc b + (d - suc b) = d
26 25 anwr 
a < c /\ b < d -> suc b + (d - suc b) = d
27 26 addeq2d 
a < c /\ b < d -> a + (suc b + (d - suc b)) = a + d
28 23, 27 syl5eq 
a < c /\ b < d -> suc (a + b) + (d - suc b) = a + d
29 eqtr3 
b + suc a + (c - suc a) = suc (a + b) + (c - suc a) ->
  b + suc a + (c - suc a) = b + (suc a + (c - suc a)) ->
  suc (a + b) + (c - suc a) = b + (suc a + (c - suc a))
30 addeq1 
b + suc a = suc (a + b) -> b + suc a + (c - suc a) = suc (a + b) + (c - suc a)
31 eqtr 
b + suc a = suc a + b -> suc a + b = suc (a + b) -> b + suc a = suc (a + b)
32 addcom 
b + suc a = suc a + b
33 31, 32 ax_mp 
suc a + b = suc (a + b) -> b + suc a = suc (a + b)
34 addS1 
suc a + b = suc (a + b)
35 33, 34 ax_mp 
b + suc a = suc (a + b)
36 30, 35 ax_mp 
b + suc a + (c - suc a) = suc (a + b) + (c - suc a)
37 29, 36 ax_mp 
b + suc a + (c - suc a) = b + (suc a + (c - suc a)) -> suc (a + b) + (c - suc a) = b + (suc a + (c - suc a))
38 addass 
b + suc a + (c - suc a) = b + (suc a + (c - suc a))
39 37, 38 ax_mp 
suc (a + b) + (c - suc a) = b + (suc a + (c - suc a))
40 pncan3 
suc a <= c -> suc a + (c - suc a) = c
41 40 conv lt 
a < c -> suc a + (c - suc a) = c
42 41 anwl 
a < c /\ b < d -> suc a + (c - suc a) = c
43 42 addeq2d 
a < c /\ b < d -> b + (suc a + (c - suc a)) = b + c
44 39, 43 syl5eq 
a < c /\ b < d -> suc (a + b) + (c - suc a) = b + c
45 28, 44 eqeqd 
a < c /\ b < d -> (suc (a + b) + (d - suc b) = suc (a + b) + (c - suc a) <-> a + d = b + c)
46 16, 45 syl5bb 
a < c /\ b < d -> (b1 (c - suc a) = b1 (d - suc b) <-> a + d = b + c)
47 7, 46 bitrd 
a < c /\ b < d -> (a -ZN c = b -ZN d <-> a + d = b + c)
48 2 anwl 
a < c /\ ~b < d -> a -ZN c = b1 (c - suc a)
49 ifneg 
~b < d -> if (b < d) (b1 (d - suc b)) (b0 (b - d)) = b0 (b - d)
50 49 conv znsub 
~b < d -> b -ZN d = b0 (b - d)
51 50 anwr 
a < c /\ ~b < d -> b -ZN d = b0 (b - d)
52 48, 51 eqeqd 
a < c /\ ~b < d -> (a -ZN c = b -ZN d <-> b1 (c - suc a) = b0 (b - d))
53 b1neb0 
b1 (c - suc a) != b0 (b - d)
54 53 conv ne 
~b1 (c - suc a) = b0 (b - d)
55 54 a1i 
a < c /\ ~b < d -> ~b1 (c - suc a) = b0 (b - d)
56 ltne 
a + d < b + c -> a + d != b + c
57 56 conv ne 
a + d < b + c -> ~a + d = b + c
58 ltadd1 
a < c <-> a + d < c + d
59 anl 
a < c /\ ~b < d -> a < c
60 58, 59 sylib 
a < c /\ ~b < d -> a + d < c + d
61 leeq2 
c + b = b + c -> (c + d <= c + b <-> c + d <= b + c)
62 addcom 
c + b = b + c
63 61, 62 ax_mp 
c + d <= c + b <-> c + d <= b + c
64 leadd2 
d <= b <-> c + d <= c + b
65 lenlt 
d <= b <-> ~b < d
66 anr 
a < c /\ ~b < d -> ~b < d
67 65, 66 sylibr 
a < c /\ ~b < d -> d <= b
68 64, 67 sylib 
a < c /\ ~b < d -> c + d <= c + b
69 63, 68 sylib 
a < c /\ ~b < d -> c + d <= b + c
70 60, 69 ltletrd 
a < c /\ ~b < d -> a + d < b + c
71 57, 70 syl 
a < c /\ ~b < d -> ~a + d = b + c
72 55, 71 binthd 
a < c /\ ~b < d -> (b1 (c - suc a) = b0 (b - d) <-> a + d = b + c)
73 52, 72 bitrd 
a < c /\ ~b < d -> (a -ZN c = b -ZN d <-> a + d = b + c)
74 47, 73 casesda 
a < c -> (a -ZN c = b -ZN d <-> a + d = b + c)
75 ifneg 
~a < c -> if (a < c) (b1 (c - suc a)) (b0 (a - c)) = b0 (a - c)
76 75 conv znsub 
~a < c -> a -ZN c = b0 (a - c)
77 76 anwl 
~a < c /\ b < d -> a -ZN c = b0 (a - c)
78 5 anwr 
~a < c /\ b < d -> b -ZN d = b1 (d - suc b)
79 77, 78 eqeqd 
~a < c /\ b < d -> (a -ZN c = b -ZN d <-> b0 (a - c) = b1 (d - suc b))
80 b0neb1 
b0 (a - c) != b1 (d - suc b)
81 80 conv ne 
~b0 (a - c) = b1 (d - suc b)
82 81 a1i 
~a < c /\ b < d -> ~b0 (a - c) = b1 (d - suc b)
83 ltner 
b + c < a + d -> a + d != b + c
84 83 conv ne 
b + c < a + d -> ~a + d = b + c
85 leadd2 
c <= a <-> b + c <= b + a
86 lenlt 
c <= a <-> ~a < c
87 anl 
~a < c /\ b < d -> ~a < c
88 86, 87 sylibr 
~a < c /\ b < d -> c <= a
89 85, 88 sylib 
~a < c /\ b < d -> b + c <= b + a
90 bitr 
(b < d <-> a + b < a + d) -> (a + b < a + d <-> b + a < a + d) -> (b < d <-> b + a < a + d)
91 ltadd2 
b < d <-> a + b < a + d
92 90, 91 ax_mp 
(a + b < a + d <-> b + a < a + d) -> (b < d <-> b + a < a + d)
93 lteq1 
a + b = b + a -> (a + b < a + d <-> b + a < a + d)
94 addcom 
a + b = b + a
95 93, 94 ax_mp 
a + b < a + d <-> b + a < a + d
96 92, 95 ax_mp 
b < d <-> b + a < a + d
97 anr 
~a < c /\ b < d -> b < d
98 96, 97 sylib 
~a < c /\ b < d -> b + a < a + d
99 89, 98 lelttrd 
~a < c /\ b < d -> b + c < a + d
100 84, 99 syl 
~a < c /\ b < d -> ~a + d = b + c
101 82, 100 binthd 
~a < c /\ b < d -> (b0 (a - c) = b1 (d - suc b) <-> a + d = b + c)
102 79, 101 bitrd 
~a < c /\ b < d -> (a -ZN c = b -ZN d <-> a + d = b + c)
103 76 anwl 
~a < c /\ ~b < d -> a -ZN c = b0 (a - c)
104 50 anwr 
~a < c /\ ~b < d -> b -ZN d = b0 (b - d)
105 103, 104 eqeqd 
~a < c /\ ~b < d -> (a -ZN c = b -ZN d <-> b0 (a - c) = b0 (b - d))
106 b0can 
b0 (a - c) = b0 (b - d) <-> a - c = b - d
107 addcan1 
a - c + (c + d) = b - d + (c + d) <-> a - c = b - d
108 addass 
a - c + c + d = a - c + (c + d)
109 npcan 
c <= a -> a - c + c = a
110 anl 
~a < c /\ ~b < d -> ~a < c
111 86, 110 sylibr 
~a < c /\ ~b < d -> c <= a
112 109, 111 syl 
~a < c /\ ~b < d -> a - c + c = a
113 112 addeq1d 
~a < c /\ ~b < d -> a - c + c + d = a + d
114 108, 113 syl5eqr 
~a < c /\ ~b < d -> a - c + (c + d) = a + d
115 addass 
b - d + c + d = b - d + (c + d)
116 addrass 
b - d + c + d = b - d + d + c
117 npcan 
d <= b -> b - d + d = b
118 anr 
~a < c /\ ~b < d -> ~b < d
119 65, 118 sylibr 
~a < c /\ ~b < d -> d <= b
120 117, 119 syl 
~a < c /\ ~b < d -> b - d + d = b
121 120 addeq1d 
~a < c /\ ~b < d -> b - d + d + c = b + c
122 116, 121 syl5eq 
~a < c /\ ~b < d -> b - d + c + d = b + c
123 115, 122 syl5eqr 
~a < c /\ ~b < d -> b - d + (c + d) = b + c
124 114, 123 eqeqd 
~a < c /\ ~b < d -> (a - c + (c + d) = b - d + (c + d) <-> a + d = b + c)
125 107, 124 syl5bbr 
~a < c /\ ~b < d -> (a - c = b - d <-> a + d = b + c)
126 106, 125 syl5bb 
~a < c /\ ~b < d -> (b0 (a - c) = b0 (b - d) <-> a + d = b + c)
127 105, 126 bitrd 
~a < c /\ ~b < d -> (a -ZN c = b -ZN d <-> a + d = b + c)
128 102, 127 casesda 
~a < c -> (a -ZN c = b -ZN d <-> a + d = b + c)
129 74, 128 cases 
a -ZN c = b -ZN d <-> a + d = b + c

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)