clwwisshclwwslemlem

		Ref	Expression
	Assertion	clwwisshclwwslemlem	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land \forall i \in (0 ..^L - 1) \{W (i), W (i + 1)\} \in R \land \{W (L - 1), W (0)\} \in R) \to \{W ((A + B) \mod L), W ((A + 1 + B) \mod L)\} \in R$

Proof

Step	Hyp	Ref	Expression
1		zcn	$⊢ A \in ℤ \to A \in ℂ$
2	1	3ad2ant2	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to A \in ℂ$
3		1cnd	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to 1 \in ℂ$
4		zcn	$⊢ B \in ℤ \to B \in ℂ$
5	4	3ad2ant3	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to B \in ℂ$
6	2 3 5	add32d	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to A + 1 + B = A + B + 1$
7	6	fvoveq1d	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to W ((A + 1 + B) \mod L) = W ((A + B + 1) \mod L)$
8	7	3ad2ant1	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land \forall i \in (0 ..^L - 1) \{W (i), W (i + 1)\} \in R \land \{W (L - 1), W (0)\} \in R) \to W ((A + 1 + B) \mod L) = W ((A + B + 1) \mod L)$
9	8	preq2d	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land \forall i \in (0 ..^L - 1) \{W (i), W (i + 1)\} \in R \land \{W (L - 1), W (0)\} \in R) \to \{W ((A + B) \mod L), W ((A + 1 + B) \mod L)\} = \{W ((A + B) \mod L), W ((A + B + 1) \mod L)\}$
10		zaddcl	$⊢ (A \in ℤ \land B \in ℤ) \to A + B \in ℤ$
11	10	3adant1	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to A + B \in ℤ$
12		eluz2nn	$⊢ L \in ℤ_{\geq 2} \to L \in ℕ$
13	12	3ad2ant1	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to L \in ℕ$
14	11 13	zmodcld	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to (A + B) \mod L \in ℕ_{0}$
15	14	adantr	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land (A + B) \mod L < L - 1) \to (A + B) \mod L \in ℕ_{0}$
16		uz2m1nn	$⊢ L \in ℤ_{\geq 2} \to L - 1 \in ℕ$
17	16	3ad2ant1	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to L - 1 \in ℕ$
18	17	adantr	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land (A + B) \mod L < L - 1) \to L - 1 \in ℕ$
19		simpr	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land (A + B) \mod L < L - 1) \to (A + B) \mod L < L - 1$
20		elfzo0	$⊢ (A + B) \mod L \in (0 ..^L - 1) \leftrightarrow ((A + B) \mod L \in ℕ_{0} \land L - 1 \in ℕ \land (A + B) \mod L < L - 1)$
21	15 18 19 20	syl3anbrc	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land (A + B) \mod L < L - 1) \to (A + B) \mod L \in (0 ..^L - 1)$
22		fveq2	$⊢ i = (A + B) \mod L \to W (i) = W ((A + B) \mod L)$
23		fvoveq1	$⊢ i = (A + B) \mod L \to W (i + 1) = W (((A + B) \mod L) + 1)$
24	22 23	preq12d	$⊢ i = (A + B) \mod L \to \{W (i), W (i + 1)\} = \{W ((A + B) \mod L), W (((A + B) \mod L) + 1)\}$
25	24	eleq1d	$⊢ i = (A + B) \mod L \to (\{W (i), W (i + 1)\} \in R \leftrightarrow \{W ((A + B) \mod L), W (((A + B) \mod L) + 1)\} \in R)$
26	25	rspcv	$⊢ (A + B) \mod L \in (0 ..^L - 1) \to (\forall i \in (0 ..^L - 1) \{W (i), W (i + 1)\} \in R \to \{W ((A + B) \mod L), W (((A + B) \mod L) + 1)\} \in R)$
27	21 26	syl	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land (A + B) \mod L < L - 1) \to (\forall i \in (0 ..^L - 1) \{W (i), W (i + 1)\} \in R \to \{W ((A + B) \mod L), W (((A + B) \mod L) + 1)\} \in R)$
28	10	zred	$⊢ (A \in ℤ \land B \in ℤ) \to A + B \in ℝ$
29	28	3adant1	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to A + B \in ℝ$
30	29	adantr	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land (A + B) \mod L < L - 1) \to A + B \in ℝ$
31	12	nnrpd	$⊢ L \in ℤ_{\geq 2} \to L \in ℝ^{+}$
32	31	3ad2ant1	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to L \in ℝ^{+}$
33	32	adantr	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land (A + B) \mod L < L - 1) \to L \in ℝ^{+}$
34		modltm1p1mod	$⊢ (A + B \in ℝ \land L \in ℝ^{+} \land (A + B) \mod L < L - 1) \to (A + B + 1) \mod L = ((A + B) \mod L) + 1$
35	30 33 19 34	syl3anc	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land (A + B) \mod L < L - 1) \to (A + B + 1) \mod L = ((A + B) \mod L) + 1$
36	35	fveq2d	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land (A + B) \mod L < L - 1) \to W ((A + B + 1) \mod L) = W (((A + B) \mod L) + 1)$
37	36	preq2d	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land (A + B) \mod L < L - 1) \to \{W ((A + B) \mod L), W ((A + B + 1) \mod L)\} = \{W ((A + B) \mod L), W (((A + B) \mod L) + 1)\}$
38	37	eleq1d	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land (A + B) \mod L < L - 1) \to (\{W ((A + B) \mod L), W ((A + B + 1) \mod L)\} \in R \leftrightarrow \{W ((A + B) \mod L), W (((A + B) \mod L) + 1)\} \in R)$
39	27 38	sylibrd	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land (A + B) \mod L < L - 1) \to (\forall i \in (0 ..^L - 1) \{W (i), W (i + 1)\} \in R \to \{W ((A + B) \mod L), W ((A + B + 1) \mod L)\} \in R)$
40	39	impancom	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land \forall i \in (0 ..^L - 1) \{W (i), W (i + 1)\} \in R) \to ((A + B) \mod L < L - 1 \to \{W ((A + B) \mod L), W ((A + B + 1) \mod L)\} \in R)$
41	40	3adant3	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land \forall i \in (0 ..^L - 1) \{W (i), W (i + 1)\} \in R \land \{W (L - 1), W (0)\} \in R) \to ((A + B) \mod L < L - 1 \to \{W ((A + B) \mod L), W ((A + B + 1) \mod L)\} \in R)$
42		zmodfzo	$⊢ (A + B \in ℤ \land L \in ℕ) \to (A + B) \mod L \in (0 ..^L)$
43	11 13 42	syl2anc	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to (A + B) \mod L \in (0 ..^L)$
44		elfzonlteqm1	$⊢ ((A + B) \mod L \in (0 ..^L) \land \neg (A + B) \mod L < L - 1) \to (A + B) \mod L = L - 1$
45	44	eqcomd	$⊢ ((A + B) \mod L \in (0 ..^L) \land \neg (A + B) \mod L < L - 1) \to L - 1 = (A + B) \mod L$
46	45	ex	$⊢ (A + B) \mod L \in (0 ..^L) \to (\neg (A + B) \mod L < L - 1 \to L - 1 = (A + B) \mod L)$
47	43 46	syl	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to (\neg (A + B) \mod L < L - 1 \to L - 1 = (A + B) \mod L)$
48		fveq2	$⊢ L - 1 = (A + B) \mod L \to W (L - 1) = W ((A + B) \mod L)$
49	48	adantl	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land L - 1 = (A + B) \mod L) \to W (L - 1) = W ((A + B) \mod L)$
50		zre	$⊢ A \in ℤ \to A \in ℝ$
51		zre	$⊢ B \in ℤ \to B \in ℝ$
52		readdcl	$⊢ (A \in ℝ \land B \in ℝ) \to A + B \in ℝ$
53	50 51 52	syl2an	$⊢ (A \in ℤ \land B \in ℤ) \to A + B \in ℝ$
54	53	3adant1	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to A + B \in ℝ$
55	54 32	jca	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to (A + B \in ℝ \land L \in ℝ^{+})$
56	55	adantr	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land L - 1 = (A + B) \mod L) \to (A + B \in ℝ \land L \in ℝ^{+})$
57		simpr	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land L - 1 = (A + B) \mod L) \to L - 1 = (A + B) \mod L$
58	57	eqcomd	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land L - 1 = (A + B) \mod L) \to (A + B) \mod L = L - 1$
59		modm1p1mod0	$⊢ (A + B \in ℝ \land L \in ℝ^{+}) \to ((A + B) \mod L = L - 1 \to (A + B + 1) \mod L = 0)$
60	56 58 59	sylc	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land L - 1 = (A + B) \mod L) \to (A + B + 1) \mod L = 0$
61	60	eqcomd	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land L - 1 = (A + B) \mod L) \to 0 = (A + B + 1) \mod L$
62	61	fveq2d	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land L - 1 = (A + B) \mod L) \to W (0) = W ((A + B + 1) \mod L)$
63	49 62	preq12d	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land L - 1 = (A + B) \mod L) \to \{W (L - 1), W (0)\} = \{W ((A + B) \mod L), W ((A + B + 1) \mod L)\}$
64	63	eleq1d	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land L - 1 = (A + B) \mod L) \to (\{W (L - 1), W (0)\} \in R \leftrightarrow \{W ((A + B) \mod L), W ((A + B + 1) \mod L)\} \in R)$
65	64	biimpd	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land L - 1 = (A + B) \mod L) \to (\{W (L - 1), W (0)\} \in R \to \{W ((A + B) \mod L), W ((A + B + 1) \mod L)\} \in R)$
66	65	ex	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to (L - 1 = (A + B) \mod L \to (\{W (L - 1), W (0)\} \in R \to \{W ((A + B) \mod L), W ((A + B + 1) \mod L)\} \in R))$
67	47 66	syld	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to (\neg (A + B) \mod L < L - 1 \to (\{W (L - 1), W (0)\} \in R \to \{W ((A + B) \mod L), W ((A + B + 1) \mod L)\} \in R))$
68	67	com23	$⊢ (L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \to (\{W (L - 1), W (0)\} \in R \to (\neg (A + B) \mod L < L - 1 \to \{W ((A + B) \mod L), W ((A + B + 1) \mod L)\} \in R))$
69	68	imp	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land \{W (L - 1), W (0)\} \in R) \to (\neg (A + B) \mod L < L - 1 \to \{W ((A + B) \mod L), W ((A + B + 1) \mod L)\} \in R)$
70	69	3adant2	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land \forall i \in (0 ..^L - 1) \{W (i), W (i + 1)\} \in R \land \{W (L - 1), W (0)\} \in R) \to (\neg (A + B) \mod L < L - 1 \to \{W ((A + B) \mod L), W ((A + B + 1) \mod L)\} \in R)$
71	41 70	pm2.61d	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land \forall i \in (0 ..^L - 1) \{W (i), W (i + 1)\} \in R \land \{W (L - 1), W (0)\} \in R) \to \{W ((A + B) \mod L), W ((A + B + 1) \mod L)\} \in R$
72	9 71	eqeltrd	$⊢ ((L \in ℤ_{\geq 2} \land A \in ℤ \land B \in ℤ) \land \forall i \in (0 ..^L - 1) \{W (i), W (i + 1)\} \in R \land \{W (L - 1), W (0)\} \in R) \to \{W ((A + B) \mod L), W ((A + 1 + B) \mod L)\} \in R$

Metamath Proof Explorer

Theorem clwwisshclwwslemlem

Proof