Theorem eqmdvdsub ≪ | index | src | ≫ 

theorem eqmdvdsub (a b n: nat): $ a <= b -> (mod(n): a = b <-> n || b - a) $;
StepHypRefExpression
1 dvdadd2 
n || a - a % n -> (n || b - a <-> n || b - a + (a - a % n))
2 dvdsubmod 
n || a - a % n
3 1, 2 ax_mp 
n || b - a <-> n || b - a + (a - a % n)
4 dvdsubmod 
n || b - b % n
5 eqidd 
a <= b /\ mod(n): a = b -> n = n
6 eqsub1 
b - a + (a - a % n) + a % n = b -> b - a % n = b - a + (a - a % n)
7 addass 
b - a + (a - a % n) + a % n = b - a + (a - a % n + a % n)
8 addeq2 
a - a % n + a % n = a -> b - a + (a - a % n + a % n) = b - a + a
9 npcan 
a % n <= a -> a - a % n + a % n = a
10 modle1 
a % n <= a
11 9, 10 ax_mp 
a - a % n + a % n = a
12 8, 11 ax_mp 
b - a + (a - a % n + a % n) = b - a + a
13 npcan 
a <= b -> b - a + a = b
14 12, 13 syl5eq 
a <= b -> b - a + (a - a % n + a % n) = b
15 7, 14 syl5eq 
a <= b -> b - a + (a - a % n) + a % n = b
16 6, 15 syl 
a <= b -> b - a % n = b - a + (a - a % n)
17 16 anwl 
a <= b /\ mod(n): a = b -> b - a % n = b - a + (a - a % n)
18 subeq2 
a % n = b % n -> b - a % n = b - b % n
19 18 conv eqm 
mod(n): a = b -> b - a % n = b - b % n
20 19 anwr 
a <= b /\ mod(n): a = b -> b - a % n = b - b % n
21 17, 20 eqtr3d 
a <= b /\ mod(n): a = b -> b - a + (a - a % n) = b - b % n
22 5, 21 dvdeqd 
a <= b /\ mod(n): a = b -> (n || b - a + (a - a % n) <-> n || b - b % n)
23 4, 22 mpbiri 
a <= b /\ mod(n): a = b -> n || b - a + (a - a % n)
24 3, 23 sylibr 
a <= b /\ mod(n): a = b -> n || b - a
25 add01 
0 + a = a
26 dvd01 
0 || b - a <-> b - a = 0
27 dvdeq1 
n = 0 -> (n || b - a <-> 0 || b - a)
28 27 anwr 
a <= b /\ n || b - a /\ n = 0 -> (n || b - a <-> 0 || b - a)
29 anlr 
a <= b /\ n || b - a /\ n = 0 -> n || b - a
30 28, 29 mpbid 
a <= b /\ n || b - a /\ n = 0 -> 0 || b - a
31 26, 30 sylib 
a <= b /\ n || b - a /\ n = 0 -> b - a = 0
32 31 addeq1d 
a <= b /\ n || b - a /\ n = 0 -> b - a + a = 0 + a
33 25, 32 syl6eq 
a <= b /\ n || b - a /\ n = 0 -> b - a + a = a
34 13 anwll 
a <= b /\ n || b - a /\ n = 0 -> b - a + a = b
35 33, 34 eqtr3d 
a <= b /\ n || b - a /\ n = 0 -> a = b
36 35 modeq1d 
a <= b /\ n || b - a /\ n = 0 -> a % n = b % n
37 36 conv eqm 
a <= b /\ n || b - a /\ n = 0 -> mod(n): a = b
38 modlt 
n != 0 -> a % n < n
39 38 conv ne 
~n = 0 -> a % n < n
40 39 anwr 
a <= b /\ n || b - a /\ ~n = 0 -> a % n < n
41 muladd 
n * ((b - a) // n + a // n) = n * ((b - a) // n) + n * (a // n)
42 muldiv3 
n || b - a -> n * ((b - a) // n) = b - a
43 anlr 
a <= b /\ n || b - a /\ ~n = 0 -> n || b - a
44 42, 43 syl 
a <= b /\ n || b - a /\ ~n = 0 -> n * ((b - a) // n) = b - a
45 eqcom 
a - a % n = n * (a // n) -> n * (a // n) = a - a % n
46 eqsub1 
n * (a // n) + a % n = a -> a - a % n = n * (a // n)
47 divmod 
n * (a // n) + a % n = a
48 46, 47 ax_mp 
a - a % n = n * (a // n)
49 45, 48 ax_mp 
n * (a // n) = a - a % n
50 49 a1i 
a <= b /\ n || b - a /\ ~n = 0 -> n * (a // n) = a - a % n
51 44, 50 addeqd 
a <= b /\ n || b - a /\ ~n = 0 -> n * ((b - a) // n) + n * (a // n) = b - a + (a - a % n)
52 16 anwll 
a <= b /\ n || b - a /\ ~n = 0 -> b - a % n = b - a + (a - a % n)
53 51, 52 eqtr4d 
a <= b /\ n || b - a /\ ~n = 0 -> n * ((b - a) // n) + n * (a // n) = b - a % n
54 41, 53 syl5eq 
a <= b /\ n || b - a /\ ~n = 0 -> n * ((b - a) // n + a // n) = b - a % n
55 54 addeq1d 
a <= b /\ n || b - a /\ ~n = 0 -> n * ((b - a) // n + a // n) + a % n = b - a % n + a % n
56 npcan 
a % n <= b -> b - a % n + a % n = b
57 10 a1i 
a <= b /\ n || b - a /\ ~n = 0 -> a % n <= a
58 anll 
a <= b /\ n || b - a /\ ~n = 0 -> a <= b
59 57, 58 letrd 
a <= b /\ n || b - a /\ ~n = 0 -> a % n <= b
60 56, 59 syl 
a <= b /\ n || b - a /\ ~n = 0 -> b - a % n + a % n = b
61 55, 60 eqtrd 
a <= b /\ n || b - a /\ ~n = 0 -> n * ((b - a) // n + a // n) + a % n = b
62 40, 61 eqdivmod 
a <= b /\ n || b - a /\ ~n = 0 -> b // n = (b - a) // n + a // n /\ b % n = a % n
63 62 anrd 
a <= b /\ n || b - a /\ ~n = 0 -> b % n = a % n
64 63 eqcomd 
a <= b /\ n || b - a /\ ~n = 0 -> a % n = b % n
65 64 conv eqm 
a <= b /\ n || b - a /\ ~n = 0 -> mod(n): a = b
66 37, 65 casesda 
a <= b /\ n || b - a -> mod(n): a = b
67 24, 66 ibida 
a <= b -> (mod(n): a = b <-> n || b - a)

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)