crctcshwlkn0lem6 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > crctcshwlkn0lem6		Structured version Visualization version GIF version

Theorem crctcshwlkn0lem6 27745

Description: Lemma for crctcshwlkn0 27751. (Contributed by AV, 12-Mar-2021.)

**Hypotheses**
Ref	Expression
crctcshwlkn0lem.s	⊢ (𝜑 → 𝑆 ∈ (1..^𝑁))
crctcshwlkn0lem.q	⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))
crctcshwlkn0lem.h	⊢ 𝐻 = (𝐹 cyclShift 𝑆)
crctcshwlkn0lem.n	⊢ 𝑁 = (♯‘𝐹)
crctcshwlkn0lem.f	⊢ (𝜑 → 𝐹 ∈ Word 𝐴)
crctcshwlkn0lem.p	⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))
crctcshwlkn0lem.e	⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))

**Assertion**
Ref	Expression
crctcshwlkn0lem6	⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))))

Distinct variable groups: 𝑥,𝐽 𝑥,𝑁 𝑥,𝑃 𝑥,𝑆 𝜑,𝑥 𝑖,𝐹 𝑖,𝐼 𝑖,𝑁 𝑃,𝑖 𝑆,𝑖 𝜑,𝑖 Allowed substitution hints: 𝐴(𝑥,𝑖) 𝑄(𝑥,𝑖) 𝐹(𝑥) 𝐻(𝑥,𝑖) 𝐼(𝑥) 𝐽(𝑖)

**Proof of Theorem crctcshwlkn0lem6**
Step	Hyp	Ref	Expression
1		oveq1 7171	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
2		0p1e1 11831	. . . . . . . . 9 ⊢ (0 + 1) = 1
3	1, 2	eqtrdi 2789	. . . . . . . 8 ⊢ (𝑖 = 0 → (𝑖 + 1) = 1)
4		wkslem2 27542	. . . . . . . 8 ⊢ ((𝑖 = 0 ∧ (𝑖 + 1) = 1) → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))))
5	3, 4	mpdan 687	. . . . . . 7 ⊢ (𝑖 = 0 → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))))
6		crctcshwlkn0lem.p	. . . . . . 7 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))
7		crctcshwlkn0lem.s	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ (1..^𝑁))
8		elfzo1 13171	. . . . . . . . . 10 ⊢ (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁))
9		simp2 1138	. . . . . . . . . 10 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ∈ ℕ)
10	8, 9	sylbi 220	. . . . . . . . 9 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℕ)
11	7, 10	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
12		lbfzo0 13161	. . . . . . . 8 ⊢ (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
13	11, 12	sylibr 237	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝑁))
14	5, 6, 13	rspcdva 3526	. . . . . 6 ⊢ (𝜑 → if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
15		crctcshwlkn0lem.e	. . . . . . 7 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))
16		eqeq1 2742	. . . . . . . 8 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → ((𝑃‘𝑁) = (𝑃‘1) ↔ (𝑃‘0) = (𝑃‘1)))
17		sneq 4523	. . . . . . . . 9 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → {(𝑃‘𝑁)} = {(𝑃‘0)})
18	17	eqeq2d 2749	. . . . . . . 8 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → ((𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)} ↔ (𝐼‘(𝐹‘0)) = {(𝑃‘0)}))
19		preq1 4621	. . . . . . . . 9 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → {(𝑃‘𝑁), (𝑃‘1)} = {(𝑃‘0), (𝑃‘1)})
20	19	sseq1d 3906	. . . . . . . 8 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → ({(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ↔ {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
21	16, 18, 20	ifpbi123d 1079	. . . . . . 7 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → (if-((𝑃‘𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))))
22	15, 21	syl 17	. . . . . 6 ⊢ (𝜑 → (if-((𝑃‘𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))))
23	14, 22	mpbird 260	. . . . 5 ⊢ (𝜑 → if-((𝑃‘𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
24		nncn 11717	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
25		nncn 11717	. . . . . . . . . 10 ⊢ (𝑆 ∈ ℕ → 𝑆 ∈ ℂ)
26		npcan 10966	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℂ ∧ 𝑆 ∈ ℂ) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
27	24, 25, 26	syl2anr 600	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
28		simpr 488	. . . . . . . . . 10 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
29		oveq1 7171	. . . . . . . . . . 11 ⊢ (((𝑁 − 𝑆) + 𝑆) = 𝑁 → (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = (𝑁 mod (♯‘𝐹)))
30		crctcshwlkn0lem.n	. . . . . . . . . . . . . . 15 ⊢ 𝑁 = (♯‘𝐹)
31	30	eqcomi 2747	. . . . . . . . . . . . . 14 ⊢ (♯‘𝐹) = 𝑁
32	31	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (♯‘𝐹) = 𝑁)
33	32	oveq2d 7180	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod (♯‘𝐹)) = (𝑁 mod 𝑁))
34		nnrp 12476	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ⁺)
35		modid0 13349	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℝ⁺ → (𝑁 mod 𝑁) = 0)
36	34, 35	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑁 mod 𝑁) = 0)
37	36	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod 𝑁) = 0)
38	33, 37	eqtrd 2773	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod (♯‘𝐹)) = 0)
39	29, 38	sylan9eqr 2795	. . . . . . . . . 10 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0)
40		simpl 486	. . . . . . . . . 10 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ))
41	28, 39, 40	3jca 1129	. . . . . . . . 9 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
42	27, 41	mpdan 687	. . . . . . . 8 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
43	42	3adant3 1133	. . . . . . 7 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
44	8, 43	sylbi 220	. . . . . 6 ⊢ (𝑆 ∈ (1..^𝑁) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
45		simp1 1137	. . . . . . . . 9 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
46	45	fveq2d 6672	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘𝑁))
47	46	eqeq1d 2740	. . . . . . 7 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1) ↔ (𝑃‘𝑁) = (𝑃‘1)))
48		simp2 1138	. . . . . . . . . 10 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0)
49	48	fveq2d 6672	. . . . . . . . 9 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))) = (𝐹‘0))
50	49	fveq2d 6672	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = (𝐼‘(𝐹‘0)))
51	46	sneqd 4525	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → {(𝑃‘((𝑁 − 𝑆) + 𝑆))} = {(𝑃‘𝑁)})
52	50, 51	eqeq12d 2754	. . . . . . 7 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))} ↔ (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}))
53	46	preq1d 4627	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} = {(𝑃‘𝑁), (𝑃‘1)})
54	53, 50	sseq12d 3908	. . . . . . 7 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ({(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) ↔ {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
55	47, 52, 54	ifpbi123d 1079	. . . . . 6 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))) ↔ if-((𝑃‘𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))))
56	7, 44, 55	3syl 18	. . . . 5 ⊢ (𝜑 → (if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))) ↔ if-((𝑃‘𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))))
57	23, 56	mpbird 260	. . . 4 ⊢ (𝜑 → if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))))
58		nnsub 11753	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑆 < 𝑁 ↔ (𝑁 − 𝑆) ∈ ℕ))
59	58	biimp3a 1470	. . . . . . . . . 10 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 𝑆) ∈ ℕ)
60	59	nnnn0d 12029	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 𝑆) ∈ ℕ₀)
61	8, 60	sylbi 220	. . . . . . . 8 ⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈ ℕ₀)
62	7, 61	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑁 − 𝑆) ∈ ℕ₀)
63		nn0fz0 13089	. . . . . . 7 ⊢ ((𝑁 − 𝑆) ∈ ℕ₀ ↔ (𝑁 − 𝑆) ∈ (0...(𝑁 − 𝑆)))
64	62, 63	sylib 221	. . . . . 6 ⊢ (𝜑 → (𝑁 − 𝑆) ∈ (0...(𝑁 − 𝑆)))
65		crctcshwlkn0lem.q	. . . . . . 7 ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))
66	7, 65	crctcshwlkn0lem2 27741	. . . . . 6 ⊢ ((𝜑 ∧ (𝑁 − 𝑆) ∈ (0...(𝑁 − 𝑆))) → (𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)))
67	64, 66	mpdan 687	. . . . 5 ⊢ (𝜑 → (𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)))
68		elfzoel2 13121	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℤ)
69		elfzoelz 13122	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ ℤ)
70	68, 69	zsubcld 12166	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈ ℤ)
71	70	peano2zd 12164	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1..^𝑁) → ((𝑁 − 𝑆) + 1) ∈ ℤ)
72		nnre 11716	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
73	72	anim1i 618	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝑆 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ))
74	73	ancoms 462	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ))
75		crctcshwlkn0lem1 27740	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
76	74, 75	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
77	76	3adant3 1133	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
78	8, 77	sylbi 220	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1..^𝑁) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
79	71, 68, 78	3jca 1129	. . . . . . . . . 10 ⊢ (𝑆 ∈ (1..^𝑁) → (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁))
80	7, 79	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁))
81		eluz2 12323	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘((𝑁 − 𝑆) + 1)) ↔ (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁))
82	80, 81	sylibr 237	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘((𝑁 − 𝑆) + 1)))
83		eluzfz1 12998	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘((𝑁 − 𝑆) + 1)) → ((𝑁 − 𝑆) + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁))
84	82, 83	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑁 − 𝑆) + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁))
85	7, 65	crctcshwlkn0lem3 27742	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑁 − 𝑆) + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁)) → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁)))
86	84, 85	mpdan 687	. . . . . 6 ⊢ (𝜑 → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁)))
87		subcl 10956	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑁 − 𝑆) ∈ ℂ)
88	87	ancoms 462	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑁 − 𝑆) ∈ ℂ)
89		ax-1cn 10666	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
90		pncan2 10964	. . . . . . . . . . . . . 14 ⊢ (((𝑁 − 𝑆) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)) = 1)
91	90	eqcomd 2744	. . . . . . . . . . . . 13 ⊢ (((𝑁 − 𝑆) ∈ ℂ ∧ 1 ∈ ℂ) → 1 = (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)))
92	88, 89, 91	sylancl 589	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 1 = (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)))
93		peano2cn 10883	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 𝑆) ∈ ℂ → ((𝑁 − 𝑆) + 1) ∈ ℂ)
94	88, 93	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑁 − 𝑆) + 1) ∈ ℂ)
95		simpr 488	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 𝑁 ∈ ℂ)
96		simpl 486	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 𝑆 ∈ ℂ)
97	94, 95, 96	subsub3d 11098	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)) = ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁))
98	92, 97	eqtr2d 2774	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
99	25, 24, 98	syl2an 599	. . . . . . . . . 10 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
100	99	3adant3 1133	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
101	8, 100	sylbi 220	. . . . . . . 8 ⊢ (𝑆 ∈ (1..^𝑁) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
102	7, 101	syl 17	. . . . . . 7 ⊢ (𝜑 → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
103	102	fveq2d 6672	. . . . . 6 ⊢ (𝜑 → (𝑃‘((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁)) = (𝑃‘1))
104	86, 103	eqtrd 2773	. . . . 5 ⊢ (𝜑 → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1))
105		crctcshwlkn0lem.h	. . . . . . 7 ⊢ 𝐻 = (𝐹 cyclShift 𝑆)
106	105	fveq1i 6669	. . . . . 6 ⊢ (𝐻‘(𝑁 − 𝑆)) = ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆))
107		crctcshwlkn0lem.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ Word 𝐴)
108	107	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → 𝐹 ∈ Word 𝐴)
109	69	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → 𝑆 ∈ ℤ)
110		elfzofz 13137	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ (1...𝑁))
111		ubmelfzo 13186	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1...𝑁) → (𝑁 − 𝑆) ∈ (0..^𝑁))
112	110, 111	syl 17	. . . . . . . . . 10 ⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈ (0..^𝑁))
113	112	adantl 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → (𝑁 − 𝑆) ∈ (0..^𝑁))
114	31	oveq2i 7175	. . . . . . . . 9 ⊢ (0..^(♯‘𝐹)) = (0..^𝑁)
115	113, 114	eleqtrrdi 2844	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → (𝑁 − 𝑆) ∈ (0..^(♯‘𝐹)))
116		cshwidxmod 14247	. . . . . . . 8 ⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ (𝑁 − 𝑆) ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
117	108, 109, 115, 116	syl3anc 1372	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
118	7, 117	mpdan 687	. . . . . 6 ⊢ (𝜑 → ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
119	106, 118	syl5eq 2785	. . . . 5 ⊢ (𝜑 → (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
120		simp1 1137	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)))
121		simp2 1138	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1))
122	120, 121	eqeq12d 2754	. . . . . 6 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → ((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)) ↔ (𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1)))
123		simp3 1139	. . . . . . . 8 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
124	123	fveq2d 6672	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝐼‘(𝐻‘(𝑁 − 𝑆))) = (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))))
125	120	sneqd 4525	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → {(𝑄‘(𝑁 − 𝑆))} = {(𝑃‘((𝑁 − 𝑆) + 𝑆))})
126	124, 125	eqeq12d 2754	. . . . . 6 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → ((𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))} ↔ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}))
127	120, 121	preq12d 4629	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} = {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)})
128	127, 124	sseq12d 3908	. . . . . 6 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → ({(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))) ↔ {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))))
129	122, 126, 128	ifpbi123d 1079	. . . . 5 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))) ↔ if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))))))
130	67, 104, 119, 129	syl3anc 1372	. . . 4 ⊢ (𝜑 → (if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))) ↔ if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))))))
131	57, 130	mpbird 260	. . 3 ⊢ (𝜑 → if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))))
132	131	adantr 484	. 2 ⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))))
133		wkslem1 27541	. . 3 ⊢ (𝐽 = (𝑁 − 𝑆) → (if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))) ↔ if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))))))
134	133	adantl 485	. 2 ⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → (if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))) ↔ if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))))))
135	132, 134	mpbird 260	1 ⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 if-wif 1062 ∧ w3a 1088 = wceq 1542 ∈ wcel 2113 ∀wral 3053 ⊆ wss 3841 ifcif 4411 {csn 4513 {cpr 4515 class class class wbr 5027 ↦ cmpt 5107 ‘cfv 6333 (class class class)co 7164 ℂcc 10606 ℝcr 10607 0cc0 10608 1c1 10609 + caddc 10611 < clt 10746 ≤ cle 10747 − cmin 10941 ℕcn 11709 ℕ₀cn0 11969 ℤcz 12055 ℤ_≥cuz 12317 ℝ⁺crp 12465 ...cfz 12974 ..^cfzo 13117 mod cmo 13321 ♯chash 13775 Word cword 13948 cyclShift ccsh 14232

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-rep 5151 ax-sep 5164 ax-nul 5171 ax-pow 5229 ax-pr 5293 ax-un 7473 ax-cnex 10664 ax-resscn 10665 ax-1cn 10666 ax-icn 10667 ax-addcl 10668 ax-addrcl 10669 ax-mulcl 10670 ax-mulrcl 10671 ax-mulcom 10672 ax-addass 10673 ax-mulass 10674 ax-distr 10675 ax-i2m1 10676 ax-1ne0 10677 ax-1rid 10678 ax-rnegex 10679 ax-rrecex 10680 ax-cnre 10681 ax-pre-lttri 10682 ax-pre-lttrn 10683 ax-pre-ltadd 10684 ax-pre-mulgt0 10685 ax-pre-sup 10686

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-ifp 1063 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-pss 3860 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-tp 4518 df-op 4520 df-uni 4794 df-int 4834 df-iun 4880 df-br 5028 df-opab 5090 df-mpt 5108 df-tr 5134 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6123 df-ord 6169 df-on 6170 df-lim 6171 df-suc 6172 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-riota 7121 df-ov 7167 df-oprab 7168 df-mpo 7169 df-om 7594 df-1st 7707 df-2nd 7708 df-wrecs 7969 df-recs 8030 df-rdg 8068 df-1o 8124 df-er 8313 df-en 8549 df-dom 8550 df-sdom 8551 df-fin 8552 df-sup 8972 df-inf 8973 df-card 9434 df-pnf 10748 df-mnf 10749 df-xr 10750 df-ltxr 10751 df-le 10752 df-sub 10943 df-neg 10944 df-div 11369 df-nn 11710 df-2 11772 df-n0 11970 df-z 12056 df-uz 12318 df-rp 12466 df-fz 12975 df-fzo 13118 df-fl 13246 df-mod 13322 df-hash 13776 df-word 13949 df-concat 14005 df-substr 14085 df-pfx 14115 df-csh 14233

This theorem is referenced by: crctcshwlkn0lem7 27746

W3C validator