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