Step | Hyp | Ref | Expression |
1 |
|
idvd |
(x + y) * n = a + b -> n || a + b |
2 |
|
addmul |
(x + y) * n = x * n + y * n |
3 |
|
addeq |
x * n = a -> y * n = b -> x * n + y * n = a + b |
4 |
3 |
imp |
x * n = a /\ y * n = b -> x * n + y * n = a + b |
5 |
2, 4 |
syl5eq |
x * n = a /\ y * n = b -> (x + y) * n = a + b |
6 |
1, 5 |
syl |
x * n = a /\ y * n = b -> n || a + b |
7 |
6 |
eexda |
x * n = a -> E. y y * n = b -> n || a + b |
8 |
7 |
conv dvd |
x * n = a -> n || b -> n || a + b |
9 |
|
idvd |
(z - x) * n = b -> n || b |
10 |
|
addcan2 |
a + (z - x) * n = a + b <-> (z - x) * n = b |
11 |
|
addeq1 |
x * n = a -> x * n + (z - x) * n = a + (z - x) * n |
12 |
11 |
anwl |
x * n = a /\ z * n = a + b -> x * n + (z - x) * n = a + (z - x) * n |
13 |
|
addmul |
(x + (z - x)) * n = x * n + (z - x) * n |
14 |
|
mul0 |
(x + (z - x)) * 0 = 0 |
15 |
|
muleq2 |
n = 0 -> (x + (z - x)) * n = (x + (z - x)) * 0 |
16 |
14, 15 |
syl6eq |
n = 0 -> (x + (z - x)) * n = 0 |
17 |
|
mul0 |
z * 0 = 0 |
18 |
|
muleq2 |
n = 0 -> z * n = z * 0 |
19 |
17, 18 |
syl6eq |
n = 0 -> z * n = 0 |
20 |
16, 19 |
eqtr4d |
n = 0 -> (x + (z - x)) * n = z * n |
21 |
20 |
anwr |
x * n = a /\ z * n = a + b /\ n = 0 -> (x + (z - x)) * n = z * n |
22 |
|
pncan3 |
x <= z -> x + (z - x) = z |
23 |
|
leaddid1 |
a <= a + b |
24 |
|
lt01 |
0 < n <-> n != 0 |
25 |
24 |
conv ne |
0 < n <-> ~n = 0 |
26 |
|
lemul1 |
0 < n -> (x <= z <-> x * n <= z * n) |
27 |
25, 26 |
sylbir |
~n = 0 -> (x <= z <-> x * n <= z * n) |
28 |
27 |
anwr |
x * n = a /\ z * n = a + b /\ ~n = 0 -> (x <= z <-> x * n <= z * n) |
29 |
|
anll |
x * n = a /\ z * n = a + b /\ ~n = 0 -> x * n = a |
30 |
|
anlr |
x * n = a /\ z * n = a + b /\ ~n = 0 -> z * n = a + b |
31 |
29, 30 |
leeqd |
x * n = a /\ z * n = a + b /\ ~n = 0 -> (x * n <= z * n <-> a <= a + b) |
32 |
28, 31 |
bitrd |
x * n = a /\ z * n = a + b /\ ~n = 0 -> (x <= z <-> a <= a + b) |
33 |
23, 32 |
mpbiri |
x * n = a /\ z * n = a + b /\ ~n = 0 -> x <= z |
34 |
22, 33 |
syl |
x * n = a /\ z * n = a + b /\ ~n = 0 -> x + (z - x) = z |
35 |
34 |
muleq1d |
x * n = a /\ z * n = a + b /\ ~n = 0 -> (x + (z - x)) * n = z * n |
36 |
21, 35 |
casesda |
x * n = a /\ z * n = a + b -> (x + (z - x)) * n = z * n |
37 |
|
anr |
x * n = a /\ z * n = a + b -> z * n = a + b |
38 |
36, 37 |
eqtrd |
x * n = a /\ z * n = a + b -> (x + (z - x)) * n = a + b |
39 |
13, 38 |
syl5eqr |
x * n = a /\ z * n = a + b -> x * n + (z - x) * n = a + b |
40 |
12, 39 |
eqtr3d |
x * n = a /\ z * n = a + b -> a + (z - x) * n = a + b |
41 |
10, 40 |
sylib |
x * n = a /\ z * n = a + b -> (z - x) * n = b |
42 |
9, 41 |
syl |
x * n = a /\ z * n = a + b -> n || b |
43 |
42 |
eexda |
x * n = a -> E. z z * n = a + b -> n || b |
44 |
43 |
conv dvd |
x * n = a -> n || a + b -> n || b |
45 |
8, 44 |
ibid |
x * n = a -> (n || b <-> n || a + b) |
46 |
45 |
eex |
E. x x * n = a -> (n || b <-> n || a + b) |
47 |
46 |
conv dvd |
n || a -> (n || b <-> n || a + b) |