Theorem divlem3 ≪ | index | src | ≫ 

theorem divlem3 (a b: nat) {q r: nat}:
  $ b != 0 -> E. q E. r (r < b /\ b * q + r = a) $;
StepHypRefExpression
1 id 
_1 = a -> _1 = a
2 1 eqeq2d 
_1 = a -> (b * q + r = _1 <-> b * q + r = a)
3 2 aneq2d 
_1 = a -> (r < b /\ b * q + r = _1 <-> r < b /\ b * q + r = a)
4 3 exeqd 
_1 = a -> (E. r (r < b /\ b * q + r = _1) <-> E. r (r < b /\ b * q + r = a))
5 4 exeqd 
_1 = a -> (E. q E. r (r < b /\ b * q + r = _1) <-> E. q E. r (r < b /\ b * q + r = a))
6 id 
_1 = 0 -> _1 = 0
7 6 eqeq2d 
_1 = 0 -> (b * q + r = _1 <-> b * q + r = 0)
8 7 aneq2d 
_1 = 0 -> (r < b /\ b * q + r = _1 <-> r < b /\ b * q + r = 0)
9 8 exeqd 
_1 = 0 -> (E. r (r < b /\ b * q + r = _1) <-> E. r (r < b /\ b * q + r = 0))
10 9 exeqd 
_1 = 0 -> (E. q E. r (r < b /\ b * q + r = _1) <-> E. q E. r (r < b /\ b * q + r = 0))
11 id 
_1 = a1 -> _1 = a1
12 11 eqeq2d 
_1 = a1 -> (b * q + r = _1 <-> b * q + r = a1)
13 12 aneq2d 
_1 = a1 -> (r < b /\ b * q + r = _1 <-> r < b /\ b * q + r = a1)
14 13 exeqd 
_1 = a1 -> (E. r (r < b /\ b * q + r = _1) <-> E. r (r < b /\ b * q + r = a1))
15 14 exeqd 
_1 = a1 -> (E. q E. r (r < b /\ b * q + r = _1) <-> E. q E. r (r < b /\ b * q + r = a1))
16 id 
_1 = suc a1 -> _1 = suc a1
17 16 eqeq2d 
_1 = suc a1 -> (b * q + r = _1 <-> b * q + r = suc a1)
18 17 aneq2d 
_1 = suc a1 -> (r < b /\ b * q + r = _1 <-> r < b /\ b * q + r = suc a1)
19 18 exeqd 
_1 = suc a1 -> (E. r (r < b /\ b * q + r = _1) <-> E. r (r < b /\ b * q + r = suc a1))
20 19 exeqd 
_1 = suc a1 -> (E. q E. r (r < b /\ b * q + r = _1) <-> E. q E. r (r < b /\ b * q + r = suc a1))
21 lteq1 
r = 0 -> (r < b <-> 0 < b)
22 21 anwr 
b != 0 /\ q = 0 /\ r = 0 -> (r < b <-> 0 < b)
23 lt01 
0 < b <-> b != 0
24 anll 
b != 0 /\ q = 0 /\ r = 0 -> b != 0
25 23, 24 sylibr 
b != 0 /\ q = 0 /\ r = 0 -> 0 < b
26 22, 25 mpbird 
b != 0 /\ q = 0 /\ r = 0 -> r < b
27 add0 
0 + 0 = 0
28 mul02 
b * 0 = 0
29 muleq2 
q = 0 -> b * q = b * 0
30 29 anwr 
b != 0 /\ q = 0 -> b * q = b * 0
31 30 anwl 
b != 0 /\ q = 0 /\ r = 0 -> b * q = b * 0
32 28, 31 syl6eq 
b != 0 /\ q = 0 /\ r = 0 -> b * q = 0
33 anr 
b != 0 /\ q = 0 /\ r = 0 -> r = 0
34 32, 33 addeqd 
b != 0 /\ q = 0 /\ r = 0 -> b * q + r = 0 + 0
35 27, 34 syl6eq 
b != 0 /\ q = 0 /\ r = 0 -> b * q + r = 0
36 26, 35 iand 
b != 0 /\ q = 0 /\ r = 0 -> r < b /\ b * q + r = 0
37 36 iexde 
b != 0 /\ q = 0 -> E. r (r < b /\ b * q + r = 0)
38 37 iexde 
b != 0 -> E. q E. r (r < b /\ b * q + r = 0)
39 lteq1 
r = v -> (r < b <-> v < b)
40 39 anwr 
q = u /\ r = v -> (r < b <-> v < b)
41 muleq2 
q = u -> b * q = b * u
42 41 anwl 
q = u /\ r = v -> b * q = b * u
43 anr 
q = u /\ r = v -> r = v
44 42, 43 addeqd 
q = u /\ r = v -> b * q + r = b * u + v
45 44 eqeq1d 
q = u /\ r = v -> (b * q + r = a1 <-> b * u + v = a1)
46 40, 45 aneqd 
q = u /\ r = v -> (r < b /\ b * q + r = a1 <-> v < b /\ b * u + v = a1)
47 46 cbvexd 
q = u -> (E. r (r < b /\ b * q + r = a1) <-> E. v (v < b /\ b * u + v = a1))
48 47 cbvex 
E. q E. r (r < b /\ b * q + r = a1) <-> E. u E. v (v < b /\ b * u + v = a1)
49 leloe 
suc v <= b <-> suc v < b \/ suc v = b
50 anrl 
b != 0 /\ (v < b /\ b * u + v = a1) -> v < b
51 50 conv lt 
b != 0 /\ (v < b /\ b * u + v = a1) -> suc v <= b
52 49, 51 sylib 
b != 0 /\ (v < b /\ b * u + v = a1) -> suc v < b \/ suc v = b
53 lteq1 
r = suc v -> (r < b <-> suc v < b)
54 53 anwr 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b /\ q = u /\ r = suc v -> (r < b <-> suc v < b)
55 anr 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b -> suc v < b
56 55 anwll 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b /\ q = u /\ r = suc v -> suc v < b
57 54, 56 mpbird 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b /\ q = u /\ r = suc v -> r < b
58 addeq2 
r = suc v -> b * q + r = b * q + suc v
59 58 anwr 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b /\ q = u /\ r = suc v -> b * q + r = b * q + suc v
60 addS 
b * q + suc v = suc (b * q + v)
61 anlr 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b /\ q = u /\ r = suc v -> q = u
62 61 muleq2d 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b /\ q = u /\ r = suc v -> b * q = b * u
63 62 addeq1d 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b /\ q = u /\ r = suc v -> b * q + v = b * u + v
64 anrr 
b != 0 /\ (v < b /\ b * u + v = a1) -> b * u + v = a1
65 64 anw3l 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b /\ q = u /\ r = suc v -> b * u + v = a1
66 63, 65 eqtrd 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b /\ q = u /\ r = suc v -> b * q + v = a1
67 66 suceqd 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b /\ q = u /\ r = suc v -> suc (b * q + v) = suc a1
68 60, 67 syl5eq 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b /\ q = u /\ r = suc v -> b * q + suc v = suc a1
69 59, 68 eqtrd 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b /\ q = u /\ r = suc v -> b * q + r = suc a1
70 57, 69 iand 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b /\ q = u /\ r = suc v -> r < b /\ b * q + r = suc a1
71 70 iexde 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b /\ q = u -> E. r (r < b /\ b * q + r = suc a1)
72 71 iexde 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v < b -> E. q E. r (r < b /\ b * q + r = suc a1)
73 21 anwr 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> (r < b <-> 0 < b)
74 anl 
b != 0 /\ (v < b /\ b * u + v = a1) -> b != 0
75 74 anw3l 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> b != 0
76 23, 75 sylibr 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> 0 < b
77 73, 76 mpbird 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> r < b
78 anlr 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> q = suc u
79 78 muleq2d 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> b * q = b * suc u
80 anr 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> r = 0
81 79, 80 addeqd 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> b * q + r = b * suc u + 0
82 add0 
b * suc u + 0 = b * suc u
83 mulS 
b * suc u = b * u + b
84 anr 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b -> suc v = b
85 84 anwll 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> suc v = b
86 85 addeq2d 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> b * u + suc v = b * u + b
87 addS 
b * u + suc v = suc (b * u + v)
88 64 anw3l 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> b * u + v = a1
89 88 suceqd 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> suc (b * u + v) = suc a1
90 87, 89 syl5eq 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> b * u + suc v = suc a1
91 86, 90 eqtr3d 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> b * u + b = suc a1
92 83, 91 syl5eq 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> b * suc u = suc a1
93 82, 92 syl5eq 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> b * suc u + 0 = suc a1
94 81, 93 eqtrd 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> b * q + r = suc a1
95 77, 94 iand 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u /\ r = 0 -> r < b /\ b * q + r = suc a1
96 95 iexde 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b /\ q = suc u -> E. r (r < b /\ b * q + r = suc a1)
97 96 iexde 
b != 0 /\ (v < b /\ b * u + v = a1) /\ suc v = b -> E. q E. r (r < b /\ b * q + r = suc a1)
98 72, 97 eorda 
b != 0 /\ (v < b /\ b * u + v = a1) -> suc v < b \/ suc v = b -> E. q E. r (r < b /\ b * q + r = suc a1)
99 52, 98 mpd 
b != 0 /\ (v < b /\ b * u + v = a1) -> E. q E. r (r < b /\ b * q + r = suc a1)
100 99 eexda 
b != 0 -> E. v (v < b /\ b * u + v = a1) -> E. q E. r (r < b /\ b * q + r = suc a1)
101 100 eexd 
b != 0 -> E. u E. v (v < b /\ b * u + v = a1) -> E. q E. r (r < b /\ b * q + r = suc a1)
102 48, 101 syl5bi 
b != 0 -> E. q E. r (r < b /\ b * q + r = a1) -> E. q E. r (r < b /\ b * q + r = suc a1)
103 102 imp 
b != 0 /\ E. q E. r (r < b /\ b * q + r = a1) -> E. q E. r (r < b /\ b * q + r = suc a1)
104 5, 10, 15, 20, 38, 103 indd 
b != 0 -> E. q E. r (r < b /\ b * q + r = 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_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)