Theorem zmodb1 ≪ | index | src | ≫ 

theorem zmodb1 (a n: nat): $ a < n -> b1 a %Z n = n - suc a $;
StepHypRefExpression
1 zmodn02 
n != 0 -> b1 a %Z n = (zfst (b1 a) + n - zsnd (b1 a) % n) % n
2 lt01 
0 < n <-> n != 0
3 lelttr 
0 <= a -> a < n -> 0 < n
4 le01 
0 <= a
5 3, 4 ax_mp 
a < n -> 0 < n
6 2, 5 sylib 
a < n -> n != 0
7 1, 6 syl 
a < n -> b1 a %Z n = (zfst (b1 a) + n - zsnd (b1 a) % n) % n
8 modeq1 
zfst (b1 a) + n - zsnd (b1 a) % n = n - suc a % n -> (zfst (b1 a) + n - zsnd (b1 a) % n) % n = (n - suc a % n) % n
9 subeq 
zfst (b1 a) + n = n -> zsnd (b1 a) % n = suc a % n -> zfst (b1 a) + n - zsnd (b1 a) % n = n - suc a % n
10 eqtr 
zfst (b1 a) + n = 0 + n -> 0 + n = n -> zfst (b1 a) + n = n
11 addeq1 
zfst (b1 a) = 0 -> zfst (b1 a) + n = 0 + n
12 zfstb1 
zfst (b1 a) = 0
13 11, 12 ax_mp 
zfst (b1 a) + n = 0 + n
14 10, 13 ax_mp 
0 + n = n -> zfst (b1 a) + n = n
15 add01 
0 + n = n
16 14, 15 ax_mp 
zfst (b1 a) + n = n
17 9, 16 ax_mp 
zsnd (b1 a) % n = suc a % n -> zfst (b1 a) + n - zsnd (b1 a) % n = n - suc a % n
18 modeq1 
zsnd (b1 a) = suc a -> zsnd (b1 a) % n = suc a % n
19 zsndb1 
zsnd (b1 a) = suc a
20 18, 19 ax_mp 
zsnd (b1 a) % n = suc a % n
21 17, 20 ax_mp 
zfst (b1 a) + n - zsnd (b1 a) % n = n - suc a % n
22 8, 21 ax_mp 
(zfst (b1 a) + n - zsnd (b1 a) % n) % n = (n - suc a % n) % n
23 leloe 
suc a <= n <-> suc a < n \/ suc a = n
24 23 conv lt 
a < n <-> suc a < n \/ suc a = n
25 eor 
(suc a < n -> (n - suc a % n) % n = n - suc a) -> (suc a = n -> (n - suc a % n) % n = n - suc a) -> suc a < n \/ suc a = n -> (n - suc a % n) % n = n - suc a
26 modlteq 
suc a < n -> suc a % n = suc a
27 26 subeq2d 
suc a < n -> n - suc a % n = n - suc a
28 27 modeq1d 
suc a < n -> (n - suc a % n) % n = (n - suc a) % n
29 modlteq 
n - suc a < n -> (n - suc a) % n = n - suc a
30 subltid 
0 < n /\ 0 < suc a -> n - suc a < n
31 lttr 
0 < suc a -> suc a < n -> 0 < n
32 lt01S 
0 < suc a
33 31, 32 ax_mp 
suc a < n -> 0 < n
34 32 a1i 
suc a < n -> 0 < suc a
35 30, 33, 34 sylan 
suc a < n -> n - suc a < n
36 29, 35 syl 
suc a < n -> (n - suc a) % n = n - suc a
37 28, 36 eqtrd 
suc a < n -> (n - suc a % n) % n = n - suc a
38 25, 37 ax_mp 
(suc a = n -> (n - suc a % n) % n = n - suc a) -> suc a < n \/ suc a = n -> (n - suc a % n) % n = n - suc a
39 sub02 
n - 0 = n
40 modid 
n % n = 0
41 modeq1 
suc a = n -> suc a % n = n % n
42 40, 41 syl6eq 
suc a = n -> suc a % n = 0
43 42 subeq2d 
suc a = n -> n - suc a % n = n - 0
44 39, 43 syl6eq 
suc a = n -> n - suc a % n = n
45 44 modeq1d 
suc a = n -> (n - suc a % n) % n = n % n
46 subid 
n - n = 0
47 subeq2 
suc a = n -> n - suc a = n - n
48 46, 47 syl6eq 
suc a = n -> n - suc a = 0
49 40, 48 syl6eqr 
suc a = n -> n - suc a = n % n
50 45, 49 eqtr4d 
suc a = n -> (n - suc a % n) % n = n - suc a
51 38, 50 ax_mp 
suc a < n \/ suc a = n -> (n - suc a % n) % n = n - suc a
52 24, 51 sylbi 
a < n -> (n - suc a % n) % n = n - suc a
53 22, 52 syl5eq 
a < n -> (zfst (b1 a) + n - zsnd (b1 a) % n) % n = n - suc a
54 7, 53 eqtrd 
a < n -> b1 a %Z n = n - suc 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)