Theorem divlem2 ≪ | index | src | ≫

theorem divlem2 (G: wff) (Q R a b q: nat) {r: nat}:
  $ G -> R < b $ >
  $ G -> b * Q + R = a $ >
  $ G -> (E. r (r < b /\ b * q + r = a) <-> q = Q) $;

Step	Hyp	Ref	Expression
1		anrl	G /\ (r < b /\ b * q + r = a) -> r < b
2		hyp h1	G -> R < b
3	2	anwl	G /\ (r < b /\ b * q + r = a) -> R < b
4		eqle	b * q + r = b * Q + R -> b * q + r <= b * Q + R
5		anrr	G /\ (r < b /\ b * q + r = a) -> b * q + r = a
6		hyp h2	G -> b * Q + R = a
7	6	anwl	G /\ (r < b /\ b * q + r = a) -> b * Q + R = a
8	5, 7	eqtr4d	G /\ (r < b /\ b * q + r = a) -> b * q + r = b * Q + R
9	4, 8	syl	G /\ (r < b /\ b * q + r = a) -> b * q + r <= b * Q + R
10	1, 3, 9	divlem1	G /\ (r < b /\ b * q + r = a) -> q <= Q
11		eqle	b * Q + R = b * q + r -> b * Q + R <= b * q + r
12	7, 5	eqtr4d	G /\ (r < b /\ b * q + r = a) -> b * Q + R = b * q + r
13	11, 12	syl	G /\ (r < b /\ b * q + r = a) -> b * Q + R <= b * q + r
14	3, 1, 13	divlem1	G /\ (r < b /\ b * q + r = a) -> Q <= q
15	10, 14	leasymd	G /\ (r < b /\ b * q + r = a) -> q = Q
16	15	eexda	G -> E. r (r < b /\ b * q + r = a) -> q = Q
17		lteq1	r = R -> (r < b <-> R < b)
18		addeq2	r = R -> b * q + r = b * q + R
19	18	eqeq1d	r = R -> (b * q + r = a <-> b * q + R = a)
20	17, 19	aneqd	r = R -> (r < b /\ b * q + r = a <-> R < b /\ b * q + R = a)
21	20	iexe	R < b /\ b * q + R = a -> E. r (r < b /\ b * q + r = a)
22	2	anwl	G /\ q = Q -> R < b
23		muleq2	q = Q -> b * q = b * Q
24	23	addeq1d	q = Q -> b * q + R = b * Q + R
25	24	anwr	G /\ q = Q -> b * q + R = b * Q + R
26	6	anwl	G /\ q = Q -> b * Q + R = a
27	25, 26	eqtrd	G /\ q = Q -> b * q + R = a
28	22, 27	iand	G /\ q = Q -> R < b /\ b * q + R = a
29	21, 28	syl	G /\ q = Q -> E. r (r < b /\ b * q + r = a)
30	29	exp	G -> q = Q -> E. r (r < b /\ b * q + r = a)
31	16, 30	ibid	G -> (E. r (r < b /\ b * q + r = a) <-> q = Q)

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)