cncongr1

Description: One direction of the bicondition in cncongr . Theorem 5.4 in ApostolNT p. 109. (Contributed by AV, 13-Jul-2021)

		Ref	Expression
	Assertion	cncongr1	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (A C \mod N = B C \mod N \to A \mod M = B \mod M)$

Proof

Step	Hyp	Ref	Expression
1		zmulcl	$⊢ (A \in ℤ \land C \in ℤ) \to A C \in ℤ$
2	1	3adant2	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A C \in ℤ$
3		zmulcl	$⊢ (B \in ℤ \land C \in ℤ) \to B C \in ℤ$
4	3	3adant1	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to B C \in ℤ$
5		simpl	$⊢ (N \in ℕ \land M = \frac{N}{C \gcd N}) \to N \in ℕ$
6		congr	$⊢ (A C \in ℤ \land B C \in ℤ \land N \in ℕ) \to (A C \mod N = B C \mod N \leftrightarrow \exists k \in ℤ k \cdot N = A C - B C)$
7	2 4 5 6	syl2an3an	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (A C \mod N = B C \mod N \leftrightarrow \exists k \in ℤ k \cdot N = A C - B C)$
8		simpl	$⊢ (C \in ℤ \land N \in ℕ) \to C \in ℤ$
9		nnz	$⊢ N \in ℕ \to N \in ℤ$
10		nnne0	$⊢ N \in ℕ \to N \neq 0$
11	9 10	jca	$⊢ N \in ℕ \to (N \in ℤ \land N \neq 0)$
12	11	adantl	$⊢ (C \in ℤ \land N \in ℕ) \to (N \in ℤ \land N \neq 0)$
13		eqidd	$⊢ (C \in ℤ \land N \in ℕ) \to C \gcd N = C \gcd N$
14	8 12 13	3jca	$⊢ (C \in ℤ \land N \in ℕ) \to (C \in ℤ \land (N \in ℤ \land N \neq 0) \land C \gcd N = C \gcd N)$
15	14	ex	$⊢ C \in ℤ \to (N \in ℕ \to (C \in ℤ \land (N \in ℤ \land N \neq 0) \land C \gcd N = C \gcd N))$
16	15	3ad2ant3	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to (N \in ℕ \to (C \in ℤ \land (N \in ℤ \land N \neq 0) \land C \gcd N = C \gcd N))$
17	16	com12	$⊢ N \in ℕ \to ((A \in ℤ \land B \in ℤ \land C \in ℤ) \to (C \in ℤ \land (N \in ℤ \land N \neq 0) \land C \gcd N = C \gcd N))$
18	17	adantr	$⊢ (N \in ℕ \land M = \frac{N}{C \gcd N}) \to ((A \in ℤ \land B \in ℤ \land C \in ℤ) \to (C \in ℤ \land (N \in ℤ \land N \neq 0) \land C \gcd N = C \gcd N))$
19	18	impcom	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (C \in ℤ \land (N \in ℤ \land N \neq 0) \land C \gcd N = C \gcd N)$
20		divgcdcoprmex	$⊢ (C \in ℤ \land (N \in ℤ \land N \neq 0) \land C \gcd N = C \gcd N) \to \exists r \in ℤ \exists s \in ℤ (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1)$
21	19 20	syl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to \exists r \in ℤ \exists s \in ℤ (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1)$
22	21	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \to \exists r \in ℤ \exists s \in ℤ (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1)$
23		oveq2	$⊢ N = (C \gcd N) s \to k \cdot N = k (C \gcd N) s$
24	23	3ad2ant2	$⊢ (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1) \to k \cdot N = k (C \gcd N) s$
25	24	adantl	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1)) \to k \cdot N = k (C \gcd N) s$
26		oveq2	$⊢ C = (C \gcd N) r \to A C = A (C \gcd N) r$
27		oveq2	$⊢ C = (C \gcd N) r \to B C = B (C \gcd N) r$
28	26 27	oveq12d	$⊢ C = (C \gcd N) r \to A C - B C = A (C \gcd N) r - B (C \gcd N) r$
29	28	3ad2ant1	$⊢ (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1) \to A C - B C = A (C \gcd N) r - B (C \gcd N) r$
30	29	adantl	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1)) \to A C - B C = A (C \gcd N) r - B (C \gcd N) r$
31	25 30	eqeq12d	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1)) \to (k \cdot N = A C - B C \leftrightarrow k (C \gcd N) s = A (C \gcd N) r - B (C \gcd N) r)$
32		simpr	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \to k \in ℤ$
33	32	zcnd	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \to k \in ℂ$
34	33	adantr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to k \in ℂ$
35		simp3	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to C \in ℤ$
36	35	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to C \in ℤ$
37	9	adantr	$⊢ (N \in ℕ \land M = \frac{N}{C \gcd N}) \to N \in ℤ$
38	37	adantl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to N \in ℤ$
39	36 38	gcdcld	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to C \gcd N \in ℕ_{0}$
40	39	nn0cnd	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to C \gcd N \in ℂ$
41	40	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to C \gcd N \in ℂ$
42		simpr	$⊢ (r \in ℤ \land s \in ℤ) \to s \in ℤ$
43	42	zcnd	$⊢ (r \in ℤ \land s \in ℤ) \to s \in ℂ$
44	43	adantl	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to s \in ℂ$
45	34 41 44	mul12d	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to k (C \gcd N) s = (C \gcd N) k s$
46		simp1	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A \in ℤ$
47	46	zcnd	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A \in ℂ$
48	47	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to A \in ℂ$
49	48	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to A \in ℂ$
50	35	ad2antrr	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \to C \in ℤ$
51	5	nnzd	$⊢ (N \in ℕ \land M = \frac{N}{C \gcd N}) \to N \in ℤ$
52	51	adantl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to N \in ℤ$
53	52	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \to N \in ℤ$
54	50 53	gcdcld	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \to C \gcd N \in ℕ_{0}$
55	54	nn0cnd	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \to C \gcd N \in ℂ$
56	55	adantr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to C \gcd N \in ℂ$
57		simpl	$⊢ (r \in ℤ \land s \in ℤ) \to r \in ℤ$
58	57	zcnd	$⊢ (r \in ℤ \land s \in ℤ) \to r \in ℂ$
59	58	adantl	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to r \in ℂ$
60	49 56 59	mul12d	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to A (C \gcd N) r = (C \gcd N) A r$
61		simp2	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to B \in ℤ$
62	61	zcnd	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to B \in ℂ$
63	62	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to B \in ℂ$
64	63	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to B \in ℂ$
65	36 52	gcdcld	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to C \gcd N \in ℕ_{0}$
66	65	nn0cnd	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to C \gcd N \in ℂ$
67	66	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to C \gcd N \in ℂ$
68	64 67 59	mul12d	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to B (C \gcd N) r = (C \gcd N) B r$
69	60 68	oveq12d	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to A (C \gcd N) r - B (C \gcd N) r = (C \gcd N) A r - (C \gcd N) B r$
70	45 69	eqeq12d	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to (k (C \gcd N) s = A (C \gcd N) r - B (C \gcd N) r \leftrightarrow (C \gcd N) k s = (C \gcd N) A r - (C \gcd N) B r)$
71	46	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to A \in ℤ$
72	71	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to A \in ℤ$
73	57	adantl	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to r \in ℤ$
74	72 73	zmulcld	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to A r \in ℤ$
75	74	zcnd	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to A r \in ℂ$
76	61	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to B \in ℤ$
77	76	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to B \in ℤ$
78	77 73	zmulcld	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to B r \in ℤ$
79	78	zcnd	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to B r \in ℂ$
80	67 75 79	subdid	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to (C \gcd N) (A r - B r) = (C \gcd N) A r - (C \gcd N) B r$
81	80	eqcomd	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to (C \gcd N) A r - (C \gcd N) B r = (C \gcd N) (A r - B r)$
82	81	eqeq2d	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to ((C \gcd N) k s = (C \gcd N) A r - (C \gcd N) B r \leftrightarrow (C \gcd N) k s = (C \gcd N) (A r - B r))$
83	32	adantr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to k \in ℤ$
84	42	adantl	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to s \in ℤ$
85	83 84	zmulcld	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to k s \in ℤ$
86	85	zcnd	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to k s \in ℂ$
87		simpl	$⊢ (A \in ℤ \land B \in ℤ) \to A \in ℤ$
88	87 57	anim12i	$⊢ ((A \in ℤ \land B \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to (A \in ℤ \land r \in ℤ)$
89		zmulcl	$⊢ (A \in ℤ \land r \in ℤ) \to A r \in ℤ$
90	88 89	syl	$⊢ ((A \in ℤ \land B \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to A r \in ℤ$
91		simpr	$⊢ (A \in ℤ \land B \in ℤ) \to B \in ℤ$
92	91 57	anim12i	$⊢ ((A \in ℤ \land B \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to (B \in ℤ \land r \in ℤ)$
93		zmulcl	$⊢ (B \in ℤ \land r \in ℤ) \to B r \in ℤ$
94	92 93	syl	$⊢ ((A \in ℤ \land B \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to B r \in ℤ$
95	90 94	zsubcld	$⊢ ((A \in ℤ \land B \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to A r - B r \in ℤ$
96	95	zcnd	$⊢ ((A \in ℤ \land B \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to A r - B r \in ℂ$
97	96	ex	$⊢ (A \in ℤ \land B \in ℤ) \to ((r \in ℤ \land s \in ℤ) \to A r - B r \in ℂ)$
98	97	3adant3	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to ((r \in ℤ \land s \in ℤ) \to A r - B r \in ℂ)$
99	98	ad2antrr	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \to ((r \in ℤ \land s \in ℤ) \to A r - B r \in ℂ)$
100	99	imp	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to A r - B r \in ℂ$
101	10	adantr	$⊢ (N \in ℕ \land M = \frac{N}{C \gcd N}) \to N \neq 0$
102	101	adantl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to N \neq 0$
103		gcd2n0cl	$⊢ (C \in ℤ \land N \in ℤ \land N \neq 0) \to C \gcd N \in ℕ$
104	36 52 102 103	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to C \gcd N \in ℕ$
105		nnne0	$⊢ C \gcd N \in ℕ \to C \gcd N \neq 0$
106	104 105	syl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to C \gcd N \neq 0$
107	106	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to C \gcd N \neq 0$
108	86 100 67 107	mulcand	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to ((C \gcd N) k s = (C \gcd N) (A r - B r) \leftrightarrow k s = A r - B r)$
109	70 82 108	3bitrd	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to (k (C \gcd N) s = A (C \gcd N) r - B (C \gcd N) r \leftrightarrow k s = A r - B r)$
110	109	adantr	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1)) \to (k (C \gcd N) s = A (C \gcd N) r - B (C \gcd N) r \leftrightarrow k s = A r - B r)$
111		zcn	$⊢ A \in ℤ \to A \in ℂ$
112		zcn	$⊢ B \in ℤ \to B \in ℂ$
113	111 112	anim12i	$⊢ (A \in ℤ \land B \in ℤ) \to (A \in ℂ \land B \in ℂ)$
114	113	3adant3	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to (A \in ℂ \land B \in ℂ)$
115	114	ad2antrr	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \to (A \in ℂ \land B \in ℂ)$
116	115 58	anim12i	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to ((A \in ℂ \land B \in ℂ) \land r \in ℂ)$
117		df-3an	$⊢ (A \in ℂ \land B \in ℂ \land r \in ℂ) \leftrightarrow ((A \in ℂ \land B \in ℂ) \land r \in ℂ)$
118	116 117	sylibr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to (A \in ℂ \land B \in ℂ \land r \in ℂ)$
119		subdir	$⊢ (A \in ℂ \land B \in ℂ \land r \in ℂ) \to (A - B) r = A r - B r$
120	118 119	syl	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to (A - B) r = A r - B r$
121	120	eqcomd	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to A r - B r = (A - B) r$
122	121	adantr	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1)) \to A r - B r = (A - B) r$
123	122	eqeq2d	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1)) \to (k s = A r - B r \leftrightarrow k s = (A - B) r)$
124	5	nncnd	$⊢ (N \in ℕ \land M = \frac{N}{C \gcd N}) \to N \in ℂ$
125	124	adantl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to N \in ℂ$
126	125	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to N \in ℂ$
127	84	zcnd	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to s \in ℂ$
128	66 106	jca	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (C \gcd N \in ℂ \land C \gcd N \neq 0)$
129	128	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to (C \gcd N \in ℂ \land C \gcd N \neq 0)$
130		divmul2	$⊢ (N \in ℂ \land s \in ℂ \land (C \gcd N \in ℂ \land C \gcd N \neq 0)) \to (\frac{N}{C \gcd N} = s \leftrightarrow N = (C \gcd N) s)$
131	126 127 129 130	syl3anc	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to (\frac{N}{C \gcd N} = s \leftrightarrow N = (C \gcd N) s)$
132		simpll	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land \frac{N}{C \gcd N} = s) \to (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ)$
133	73	adantr	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land \frac{N}{C \gcd N} = s) \to r \in ℤ$
134	5	adantl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to N \in ℕ$
135	134 36	jca	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (N \in ℕ \land C \in ℤ)$
136		divgcdnnr	$⊢ (N \in ℕ \land C \in ℤ) \to \frac{N}{C \gcd N} \in ℕ$
137	135 136	syl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to \frac{N}{C \gcd N} \in ℕ$
138	137	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \to \frac{N}{C \gcd N} \in ℕ$
139	138	ad2antrr	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land \frac{N}{C \gcd N} = s) \to \frac{N}{C \gcd N} \in ℕ$
140		eleq1	$⊢ s = \frac{N}{C \gcd N} \to (s \in ℕ \leftrightarrow \frac{N}{C \gcd N} \in ℕ)$
141	140	eqcoms	$⊢ \frac{N}{C \gcd N} = s \to (s \in ℕ \leftrightarrow \frac{N}{C \gcd N} \in ℕ)$
142	141	adantl	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land \frac{N}{C \gcd N} = s) \to (s \in ℕ \leftrightarrow \frac{N}{C \gcd N} \in ℕ)$
143	139 142	mpbird	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land \frac{N}{C \gcd N} = s) \to s \in ℕ$
144	133 143	jca	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land \frac{N}{C \gcd N} = s) \to (r \in ℤ \land s \in ℕ)$
145	132 144	jca	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land \frac{N}{C \gcd N} = s) \to ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℕ))$
146		simpr	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land \frac{N}{C \gcd N} = s) \to \frac{N}{C \gcd N} = s$
147	145 146	jca	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land \frac{N}{C \gcd N} = s) \to (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℕ)) \land \frac{N}{C \gcd N} = s)$
148		nnz	$⊢ s \in ℕ \to s \in ℤ$
149	148	adantl	$⊢ (r \in ℤ \land s \in ℕ) \to s \in ℤ$
150	149	anim2i	$⊢ (k \in ℤ \land (r \in ℤ \land s \in ℕ)) \to (k \in ℤ \land s \in ℤ)$
151	150	adantl	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to (k \in ℤ \land s \in ℤ)$
152		dvdsmul2	$⊢ (k \in ℤ \land s \in ℤ) \to s ∥ k s$
153	151 152	syl	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to s ∥ k s$
154		breq2	$⊢ k s = (A - B) r \to (s ∥ k s \leftrightarrow s ∥ (A - B) r)$
155		zsubcl	$⊢ (A \in ℤ \land B \in ℤ) \to A - B \in ℤ$
156	155	zcnd	$⊢ (A \in ℤ \land B \in ℤ) \to A - B \in ℂ$
157	156	adantr	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to A - B \in ℂ$
158		zcn	$⊢ r \in ℤ \to r \in ℂ$
159	158	adantr	$⊢ (r \in ℤ \land s \in ℕ) \to r \in ℂ$
160	159	adantl	$⊢ (k \in ℤ \land (r \in ℤ \land s \in ℕ)) \to r \in ℂ$
161	160	adantl	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to r \in ℂ$
162	157 161	mulcomd	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to (A - B) r = r (A - B)$
163	162	breq2d	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to (s ∥ (A - B) r \leftrightarrow s ∥ r (A - B))$
164	148	anim2i	$⊢ (r \in ℤ \land s \in ℕ) \to (r \in ℤ \land s \in ℤ)$
165		gcdcom	$⊢ (r \in ℤ \land s \in ℤ) \to r \gcd s = s \gcd r$
166	164 165	syl	$⊢ (r \in ℤ \land s \in ℕ) \to r \gcd s = s \gcd r$
167	166	eqeq1d	$⊢ (r \in ℤ \land s \in ℕ) \to (r \gcd s = 1 \leftrightarrow s \gcd r = 1)$
168	167	adantl	$⊢ (k \in ℤ \land (r \in ℤ \land s \in ℕ)) \to (r \gcd s = 1 \leftrightarrow s \gcd r = 1)$
169	168	adantl	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to (r \gcd s = 1 \leftrightarrow s \gcd r = 1)$
170	164	adantl	$⊢ (k \in ℤ \land (r \in ℤ \land s \in ℕ)) \to (r \in ℤ \land s \in ℤ)$
171	170	ancomd	$⊢ (k \in ℤ \land (r \in ℤ \land s \in ℕ)) \to (s \in ℤ \land r \in ℤ)$
172	155 171	anim12i	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to (A - B \in ℤ \land (s \in ℤ \land r \in ℤ))$
173	172	ancomd	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to ((s \in ℤ \land r \in ℤ) \land A - B \in ℤ)$
174		df-3an	$⊢ (s \in ℤ \land r \in ℤ \land A - B \in ℤ) \leftrightarrow ((s \in ℤ \land r \in ℤ) \land A - B \in ℤ)$
175	173 174	sylibr	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to (s \in ℤ \land r \in ℤ \land A - B \in ℤ)$
176		coprmdvds	$⊢ (s \in ℤ \land r \in ℤ \land A - B \in ℤ) \to ((s ∥ r (A - B) \land s \gcd r = 1) \to s ∥ (A - B))$
177	175 176	syl	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to ((s ∥ r (A - B) \land s \gcd r = 1) \to s ∥ (A - B))$
178		simpr	$⊢ (r \in ℤ \land s \in ℕ) \to s \in ℕ$
179	178	adantl	$⊢ (k \in ℤ \land (r \in ℤ \land s \in ℕ)) \to s \in ℕ$
180	179	anim2i	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to ((A \in ℤ \land B \in ℤ) \land s \in ℕ)$
181	180	ancomd	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to (s \in ℕ \land (A \in ℤ \land B \in ℤ))$
182		3anass	$⊢ (s \in ℕ \land A \in ℤ \land B \in ℤ) \leftrightarrow (s \in ℕ \land (A \in ℤ \land B \in ℤ))$
183	181 182	sylibr	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to (s \in ℕ \land A \in ℤ \land B \in ℤ)$
184		moddvds	$⊢ (s \in ℕ \land A \in ℤ \land B \in ℤ) \to (A \mod s = B \mod s \leftrightarrow s ∥ (A - B))$
185	183 184	syl	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to (A \mod s = B \mod s \leftrightarrow s ∥ (A - B))$
186	177 185	sylibrd	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to ((s ∥ r (A - B) \land s \gcd r = 1) \to A \mod s = B \mod s)$
187	186	expcomd	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to (s \gcd r = 1 \to (s ∥ r (A - B) \to A \mod s = B \mod s))$
188	169 187	sylbid	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to (r \gcd s = 1 \to (s ∥ r (A - B) \to A \mod s = B \mod s))$
189	188	com23	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to (s ∥ r (A - B) \to (r \gcd s = 1 \to A \mod s = B \mod s))$
190	163 189	sylbid	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to (s ∥ (A - B) r \to (r \gcd s = 1 \to A \mod s = B \mod s))$
191	190	com3l	$⊢ s ∥ (A - B) r \to (r \gcd s = 1 \to (((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to A \mod s = B \mod s))$
192	154 191	syl6bi	$⊢ k s = (A - B) r \to (s ∥ k s \to (r \gcd s = 1 \to (((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to A \mod s = B \mod s)))$
193	192	com14	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to (s ∥ k s \to (r \gcd s = 1 \to (k s = (A - B) r \to A \mod s = B \mod s)))$
194	153 193	mpd	$⊢ ((A \in ℤ \land B \in ℤ) \land (k \in ℤ \land (r \in ℤ \land s \in ℕ))) \to (r \gcd s = 1 \to (k s = (A - B) r \to A \mod s = B \mod s))$
195	194	ex	$⊢ (A \in ℤ \land B \in ℤ) \to ((k \in ℤ \land (r \in ℤ \land s \in ℕ)) \to (r \gcd s = 1 \to (k s = (A - B) r \to A \mod s = B \mod s)))$
196	195	3adant3	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to ((k \in ℤ \land (r \in ℤ \land s \in ℕ)) \to (r \gcd s = 1 \to (k s = (A - B) r \to A \mod s = B \mod s)))$
197	196	adantr	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to ((k \in ℤ \land (r \in ℤ \land s \in ℕ)) \to (r \gcd s = 1 \to (k s = (A - B) r \to A \mod s = B \mod s)))$
198	197	impl	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℕ)) \to (r \gcd s = 1 \to (k s = (A - B) r \to A \mod s = B \mod s))$
199	198	adantr	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℕ)) \land \frac{N}{C \gcd N} = s) \to (r \gcd s = 1 \to (k s = (A - B) r \to A \mod s = B \mod s))$
200	199	imp	$⊢ ((((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℕ)) \land \frac{N}{C \gcd N} = s) \land r \gcd s = 1) \to (k s = (A - B) r \to A \mod s = B \mod s)$
201		eqtr2	$⊢ (\frac{N}{C \gcd N} = M \land \frac{N}{C \gcd N} = s) \to M = s$
202		oveq2	$⊢ M = s \to A \mod M = A \mod s$
203		oveq2	$⊢ M = s \to B \mod M = B \mod s$
204	202 203	eqeq12d	$⊢ M = s \to (A \mod M = B \mod M \leftrightarrow A \mod s = B \mod s)$
205	201 204	syl	$⊢ (\frac{N}{C \gcd N} = M \land \frac{N}{C \gcd N} = s) \to (A \mod M = B \mod M \leftrightarrow A \mod s = B \mod s)$
206	205	ex	$⊢ \frac{N}{C \gcd N} = M \to (\frac{N}{C \gcd N} = s \to (A \mod M = B \mod M \leftrightarrow A \mod s = B \mod s))$
207	206	eqcoms	$⊢ M = \frac{N}{C \gcd N} \to (\frac{N}{C \gcd N} = s \to (A \mod M = B \mod M \leftrightarrow A \mod s = B \mod s))$
208	207	adantl	$⊢ (N \in ℕ \land M = \frac{N}{C \gcd N}) \to (\frac{N}{C \gcd N} = s \to (A \mod M = B \mod M \leftrightarrow A \mod s = B \mod s))$
209	208	adantl	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (\frac{N}{C \gcd N} = s \to (A \mod M = B \mod M \leftrightarrow A \mod s = B \mod s))$
210	209	ad2antrr	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℕ)) \to (\frac{N}{C \gcd N} = s \to (A \mod M = B \mod M \leftrightarrow A \mod s = B \mod s))$
211	210	imp	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℕ)) \land \frac{N}{C \gcd N} = s) \to (A \mod M = B \mod M \leftrightarrow A \mod s = B \mod s)$
212	211	adantr	$⊢ ((((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℕ)) \land \frac{N}{C \gcd N} = s) \land r \gcd s = 1) \to (A \mod M = B \mod M \leftrightarrow A \mod s = B \mod s)$
213	200 212	sylibrd	$⊢ ((((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℕ)) \land \frac{N}{C \gcd N} = s) \land r \gcd s = 1) \to (k s = (A - B) r \to A \mod M = B \mod M)$
214	213	ex	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℕ)) \land \frac{N}{C \gcd N} = s) \to (r \gcd s = 1 \to (k s = (A - B) r \to A \mod M = B \mod M))$
215	147 214	syl	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land \frac{N}{C \gcd N} = s) \to (r \gcd s = 1 \to (k s = (A - B) r \to A \mod M = B \mod M))$
216	215	ex	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to (\frac{N}{C \gcd N} = s \to (r \gcd s = 1 \to (k s = (A - B) r \to A \mod M = B \mod M)))$
217	131 216	sylbird	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to (N = (C \gcd N) s \to (r \gcd s = 1 \to (k s = (A - B) r \to A \mod M = B \mod M)))$
218	217	com3l	$⊢ N = (C \gcd N) s \to (r \gcd s = 1 \to (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to (k s = (A - B) r \to A \mod M = B \mod M)))$
219	218	a1i	$⊢ C = (C \gcd N) r \to (N = (C \gcd N) s \to (r \gcd s = 1 \to (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to (k s = (A - B) r \to A \mod M = B \mod M))))$
220	219	3imp	$⊢ (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1) \to (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to (k s = (A - B) r \to A \mod M = B \mod M))$
221	220	impcom	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1)) \to (k s = (A - B) r \to A \mod M = B \mod M)$
222	123 221	sylbid	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1)) \to (k s = A r - B r \to A \mod M = B \mod M)$
223	110 222	sylbid	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1)) \to (k (C \gcd N) s = A (C \gcd N) r - B (C \gcd N) r \to A \mod M = B \mod M)$
224	31 223	sylbid	$⊢ (((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \land (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1)) \to (k \cdot N = A C - B C \to A \mod M = B \mod M)$
225	224	ex	$⊢ ((((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \land (r \in ℤ \land s \in ℤ)) \to ((C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1) \to (k \cdot N = A C - B C \to A \mod M = B \mod M))$
226	225	rexlimdvva	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \to (\exists r \in ℤ \exists s \in ℤ (C = (C \gcd N) r \land N = (C \gcd N) s \land r \gcd s = 1) \to (k \cdot N = A C - B C \to A \mod M = B \mod M))$
227	22 226	mpd	$⊢ (((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \land k \in ℤ) \to (k \cdot N = A C - B C \to A \mod M = B \mod M)$
228	227	rexlimdva	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (\exists k \in ℤ k \cdot N = A C - B C \to A \mod M = B \mod M)$
229	7 228	sylbid	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land (N \in ℕ \land M = \frac{N}{C \gcd N})) \to (A C \mod N = B C \mod N \to A \mod M = B \mod M)$

Metamath Proof Explorer

Theorem cncongr1

Proof