crctcshwlkn0lem3

	Ref	Expression
Hypotheses	crctcshwlkn0lem.s	$⊢ φ \to S \in (1 ..^N)$
	crctcshwlkn0lem.q	$⊢ Q = (x \in (0 \dots N) ⟼ if (x \leq N - S, P (x + S), P (x + S - N)))$
Assertion	crctcshwlkn0lem3	$⊢ (φ \land J \in (N - S + 1 \dots N)) \to Q (J) = P (J + S - N)$

Proof

Step	Hyp	Ref	Expression
1		crctcshwlkn0lem.s	$⊢ φ \to S \in (1 ..^N)$
2		crctcshwlkn0lem.q	$⊢ Q = (x \in (0 \dots N) ⟼ if (x \leq N - S, P (x + S), P (x + S - N)))$
3		breq1	$⊢ x = J \to (x \leq N - S \leftrightarrow J \leq N - S)$
4		fvoveq1	$⊢ x = J \to P (x + S) = P (J + S)$
5		oveq1	$⊢ x = J \to x + S = J + S$
6	5	fvoveq1d	$⊢ x = J \to P (x + S - N) = P (J + S - N)$
7	3 4 6	ifbieq12d	$⊢ x = J \to if (x \leq N - S, P (x + S), P (x + S - N)) = if (J \leq N - S, P (J + S), P (J + S - N))$
8		0zd	$⊢ S \in (1 ..^N) \to 0 \in ℤ$
9		elfzoel2	$⊢ S \in (1 ..^N) \to N \in ℤ$
10		elfzoelz	$⊢ S \in (1 ..^N) \to S \in ℤ$
11	9 10	zsubcld	$⊢ S \in (1 ..^N) \to N - S \in ℤ$
12	11	peano2zd	$⊢ S \in (1 ..^N) \to N - S + 1 \in ℤ$
13		elfzo1	$⊢ S \in (1 ..^N) \leftrightarrow (S \in ℕ \land N \in ℕ \land S < N)$
14		nnre	$⊢ S \in ℕ \to S \in ℝ$
15		nnre	$⊢ N \in ℕ \to N \in ℝ$
16		posdif	$⊢ (S \in ℝ \land N \in ℝ) \to (S < N \leftrightarrow 0 < N - S)$
17		0red	$⊢ (S \in ℝ \land N \in ℝ) \to 0 \in ℝ$
18		resubcl	$⊢ (N \in ℝ \land S \in ℝ) \to N - S \in ℝ$
19	18	ancoms	$⊢ (S \in ℝ \land N \in ℝ) \to N - S \in ℝ$
20		ltle	$⊢ (0 \in ℝ \land N - S \in ℝ) \to (0 < N - S \to 0 \leq N - S)$
21	17 19 20	syl2anc	$⊢ (S \in ℝ \land N \in ℝ) \to (0 < N - S \to 0 \leq N - S)$
22	19	lep1d	$⊢ (S \in ℝ \land N \in ℝ) \to N - S \leq N - S + 1$
23		1red	$⊢ (S \in ℝ \land N \in ℝ) \to 1 \in ℝ$
24	19 23	readdcld	$⊢ (S \in ℝ \land N \in ℝ) \to N - S + 1 \in ℝ$
25		letr	$⊢ (0 \in ℝ \land N - S \in ℝ \land N - S + 1 \in ℝ) \to ((0 \leq N - S \land N - S \leq N - S + 1) \to 0 \leq N - S + 1)$
26	17 19 24 25	syl3anc	$⊢ (S \in ℝ \land N \in ℝ) \to ((0 \leq N - S \land N - S \leq N - S + 1) \to 0 \leq N - S + 1)$
27	22 26	mpan2d	$⊢ (S \in ℝ \land N \in ℝ) \to (0 \leq N - S \to 0 \leq N - S + 1)$
28	21 27	syld	$⊢ (S \in ℝ \land N \in ℝ) \to (0 < N - S \to 0 \leq N - S + 1)$
29	16 28	sylbid	$⊢ (S \in ℝ \land N \in ℝ) \to (S < N \to 0 \leq N - S + 1)$
30	14 15 29	syl2an	$⊢ (S \in ℕ \land N \in ℕ) \to (S < N \to 0 \leq N - S + 1)$
31	30	3impia	$⊢ (S \in ℕ \land N \in ℕ \land S < N) \to 0 \leq N - S + 1$
32	13 31	sylbi	$⊢ S \in (1 ..^N) \to 0 \leq N - S + 1$
33		eluz2	$⊢ N - S + 1 \in ℤ_{\geq 0} \leftrightarrow (0 \in ℤ \land N - S + 1 \in ℤ \land 0 \leq N - S + 1)$
34	8 12 32 33	syl3anbrc	$⊢ S \in (1 ..^N) \to N - S + 1 \in ℤ_{\geq 0}$
35	1 34	syl	$⊢ φ \to N - S + 1 \in ℤ_{\geq 0}$
36		fzss1	$⊢ N - S + 1 \in ℤ_{\geq 0} \to (N - S + 1 \dots N) \subseteq (0 \dots N)$
37	35 36	syl	$⊢ φ \to (N - S + 1 \dots N) \subseteq (0 \dots N)$
38	37	sselda	$⊢ (φ \land J \in (N - S + 1 \dots N)) \to J \in (0 \dots N)$
39		fvex	$⊢ P (J + S) \in V$
40		fvex	$⊢ P (J + S - N) \in V$
41	39 40	ifex	$⊢ if (J \leq N - S, P (J + S), P (J + S - N)) \in V$
42	41	a1i	$⊢ (φ \land J \in (N - S + 1 \dots N)) \to if (J \leq N - S, P (J + S), P (J + S - N)) \in V$
43	2 7 38 42	fvmptd3	$⊢ (φ \land J \in (N - S + 1 \dots N)) \to Q (J) = if (J \leq N - S, P (J + S), P (J + S - N))$
44		elfz2	$⊢ J \in (N - S + 1 \dots N) \leftrightarrow ((N - S + 1 \in ℤ \land N \in ℤ \land J \in ℤ) \land (N - S + 1 \leq J \land J \leq N))$
45		zre	$⊢ S \in ℤ \to S \in ℝ$
46		zre	$⊢ J \in ℤ \to J \in ℝ$
47		zre	$⊢ N \in ℤ \to N \in ℝ$
48	46 47	anim12i	$⊢ (J \in ℤ \land N \in ℤ) \to (J \in ℝ \land N \in ℝ)$
49		simprr	$⊢ (S \in ℝ \land (J \in ℝ \land N \in ℝ)) \to N \in ℝ$
50		simpl	$⊢ (S \in ℝ \land (J \in ℝ \land N \in ℝ)) \to S \in ℝ$
51	49 50	resubcld	$⊢ (S \in ℝ \land (J \in ℝ \land N \in ℝ)) \to N - S \in ℝ$
52	51	ltp1d	$⊢ (S \in ℝ \land (J \in ℝ \land N \in ℝ)) \to N - S < N - S + 1$
53		1red	$⊢ (S \in ℝ \land (J \in ℝ \land N \in ℝ)) \to 1 \in ℝ$
54	51 53	readdcld	$⊢ (S \in ℝ \land (J \in ℝ \land N \in ℝ)) \to N - S + 1 \in ℝ$
55		simprl	$⊢ (S \in ℝ \land (J \in ℝ \land N \in ℝ)) \to J \in ℝ$
56		ltletr	$⊢ (N - S \in ℝ \land N - S + 1 \in ℝ \land J \in ℝ) \to ((N - S < N - S + 1 \land N - S + 1 \leq J) \to N - S < J)$
57	51 54 55 56	syl3anc	$⊢ (S \in ℝ \land (J \in ℝ \land N \in ℝ)) \to ((N - S < N - S + 1 \land N - S + 1 \leq J) \to N - S < J)$
58	52 57	mpand	$⊢ (S \in ℝ \land (J \in ℝ \land N \in ℝ)) \to (N - S + 1 \leq J \to N - S < J)$
59	51 55	ltnled	$⊢ (S \in ℝ \land (J \in ℝ \land N \in ℝ)) \to (N - S < J \leftrightarrow \neg J \leq N - S)$
60	58 59	sylibd	$⊢ (S \in ℝ \land (J \in ℝ \land N \in ℝ)) \to (N - S + 1 \leq J \to \neg J \leq N - S)$
61	45 48 60	syl2an	$⊢ (S \in ℤ \land (J \in ℤ \land N \in ℤ)) \to (N - S + 1 \leq J \to \neg J \leq N - S)$
62	61	expcom	$⊢ (J \in ℤ \land N \in ℤ) \to (S \in ℤ \to (N - S + 1 \leq J \to \neg J \leq N - S))$
63	62	ancoms	$⊢ (N \in ℤ \land J \in ℤ) \to (S \in ℤ \to (N - S + 1 \leq J \to \neg J \leq N - S))$
64	63	3adant1	$⊢ (N - S + 1 \in ℤ \land N \in ℤ \land J \in ℤ) \to (S \in ℤ \to (N - S + 1 \leq J \to \neg J \leq N - S))$
65	10 64	syl5com	$⊢ S \in (1 ..^N) \to ((N - S + 1 \in ℤ \land N \in ℤ \land J \in ℤ) \to (N - S + 1 \leq J \to \neg J \leq N - S))$
66	65	com13	$⊢ N - S + 1 \leq J \to ((N - S + 1 \in ℤ \land N \in ℤ \land J \in ℤ) \to (S \in (1 ..^N) \to \neg J \leq N - S))$
67	66	adantr	$⊢ (N - S + 1 \leq J \land J \leq N) \to ((N - S + 1 \in ℤ \land N \in ℤ \land J \in ℤ) \to (S \in (1 ..^N) \to \neg J \leq N - S))$
68	67	impcom	$⊢ ((N - S + 1 \in ℤ \land N \in ℤ \land J \in ℤ) \land (N - S + 1 \leq J \land J \leq N)) \to (S \in (1 ..^N) \to \neg J \leq N - S)$
69	68	com12	$⊢ S \in (1 ..^N) \to (((N - S + 1 \in ℤ \land N \in ℤ \land J \in ℤ) \land (N - S + 1 \leq J \land J \leq N)) \to \neg J \leq N - S)$
70	44 69	syl5bi	$⊢ S \in (1 ..^N) \to (J \in (N - S + 1 \dots N) \to \neg J \leq N - S)$
71	1 70	syl	$⊢ φ \to (J \in (N - S + 1 \dots N) \to \neg J \leq N - S)$
72	71	imp	$⊢ (φ \land J \in (N - S + 1 \dots N)) \to \neg J \leq N - S$
73	72	iffalsed	$⊢ (φ \land J \in (N - S + 1 \dots N)) \to if (J \leq N - S, P (J + S), P (J + S - N)) = P (J + S - N)$
74	43 73	eqtrd	$⊢ (φ \land J \in (N - S + 1 \dots N)) \to Q (J) = P (J + S - N)$

Metamath Proof Explorer

Theorem crctcshwlkn0lem3

Proof