Theorem zdvdadd1 ≪ | index | src | ≫

theorem zdvdadd1 (a b n: nat): $ n |Z a -> (n |Z b <-> n |Z a +Z b) $;

Step	Hyp	Ref	Expression
1		zdvddef	n \|Z a <-> E. x x *Z n = a
2		zdvddef	n \|Z b <-> E. y y *Z n = b
3		izdvd	(x +Z y) *Z n = a +Z b -> n \|Z a +Z b
4		zaddmul	(x +Z y) Z n = x Z n +Z y *Z n
5		zaddeq	x Z n = a -> y Z n = b -> x Z n +Z y Z n = a +Z b
6	5	imp	x Z n = a /\ y Z n = b -> x Z n +Z y Z n = a +Z b
7	4, 6	syl5eq	x Z n = a /\ y Z n = b -> (x +Z y) *Z n = a +Z b
8	3, 7	syl	x Z n = a /\ y Z n = b -> n \|Z a +Z b
9	8	eexda	x Z n = a -> E. y y Z n = b -> n \|Z a +Z b
10	2, 9	syl5bi	x *Z n = a -> n \|Z b -> n \|Z a +Z b
11		zdvddef	n \|Z a +Z b <-> E. z z *Z n = a +Z b
12		izdvd	(z -Z x) *Z n = b -> n \|Z b
13		zaddcan2	a +Z (z -Z x) Z n = a +Z b <-> (z -Z x) Z n = b
14		zaddeq1	x Z n = a -> x Z n +Z (z -Z x) Z n = a +Z (z -Z x) Z n
15	14	anwl	x Z n = a /\ z Z n = a +Z b -> x Z n +Z (z -Z x) Z n = a +Z (z -Z x) *Z n
16		zaddmul	(x +Z (z -Z x)) Z n = x Z n +Z (z -Z x) *Z n
17		zmul02	(x +Z (z -Z x)) *Z 0 = 0
18		zmuleq2	n = 0 -> (x +Z (z -Z x)) Z n = (x +Z (z -Z x)) Z 0
19	17, 18	syl6eq	n = 0 -> (x +Z (z -Z x)) *Z n = 0
20		zmul02	z *Z 0 = 0
21		zmuleq2	n = 0 -> z Z n = z Z 0
22	20, 21	syl6eq	n = 0 -> z *Z n = 0
23	19, 22	eqtr4d	n = 0 -> (x +Z (z -Z x)) Z n = z Z n
24	23	anwr	x Z n = a /\ z Z n = a +Z b /\ n = 0 -> (x +Z (z -Z x)) Z n = z Z n
25		zpncan3	x +Z (z -Z x) = z
26	25	a1i	x Z n = a /\ z Z n = a +Z b /\ ~n = 0 -> x +Z (z -Z x) = z
27	26	zmuleq1d	x Z n = a /\ z Z n = a +Z b /\ ~n = 0 -> (x +Z (z -Z x)) Z n = z Z n
28	24, 27	casesda	x Z n = a /\ z Z n = a +Z b -> (x +Z (z -Z x)) Z n = z Z n
29		anr	x Z n = a /\ z Z n = a +Z b -> z *Z n = a +Z b
30	28, 29	eqtrd	x Z n = a /\ z Z n = a +Z b -> (x +Z (z -Z x)) *Z n = a +Z b
31	16, 30	syl5eqr	x Z n = a /\ z Z n = a +Z b -> x Z n +Z (z -Z x) Z n = a +Z b
32	15, 31	eqtr3d	x Z n = a /\ z Z n = a +Z b -> a +Z (z -Z x) *Z n = a +Z b
33	13, 32	sylib	x Z n = a /\ z Z n = a +Z b -> (z -Z x) *Z n = b
34	12, 33	syl	x Z n = a /\ z Z n = a +Z b -> n \|Z b
35	34	eexda	x Z n = a -> E. z z Z n = a +Z b -> n \|Z b
36	11, 35	syl5bi	x *Z n = a -> n \|Z a +Z b -> n \|Z b
37	10, 36	ibid	x *Z n = a -> (n \|Z b <-> n \|Z a +Z b)
38	37	eex	E. x x *Z n = a -> (n \|Z b <-> n \|Z a +Z b)
39	1, 38	sylbi	n \|Z a -> (n \|Z b <-> n \|Z a +Z b)

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)