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 28081

Description: Lemma for crctcshwlkn0 28087. (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 7262	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
2		0p1e1 12025	. . . . . . . . 9 ⊢ (0 + 1) = 1
3	1, 2	eqtrdi 2795	. . . . . . . 8 ⊢ (𝑖 = 0 → (𝑖 + 1) = 1)
4		wkslem2 27878	. . . . . . . 8 ⊢ ((𝑖 = 0 ∧ (𝑖 + 1) = 1) → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))))
5	3, 4	mpdan 683	. . . . . . 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 13365	. . . . . . . . . 10 ⊢ (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁))
9		simp2 1135	. . . . . . . . . 10 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ∈ ℕ)
10	8, 9	sylbi 216	. . . . . . . . 9 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℕ)
11	7, 10	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
12		lbfzo0 13355	. . . . . . . 8 ⊢ (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
13	11, 12	sylibr 233	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝑁))
14	5, 6, 13	rspcdva 3554	. . . . . 6 ⊢ (𝜑 → if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
15		crctcshwlkn0lem.e	. . . . . . 7 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))
16		eqeq1 2742	. . . . . . . 8 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → ((𝑃‘𝑁) = (𝑃‘1) ↔ (𝑃‘0) = (𝑃‘1)))
17		sneq 4568	. . . . . . . . 9 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → {(𝑃‘𝑁)} = {(𝑃‘0)})
18	17	eqeq2d 2749	. . . . . . . 8 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → ((𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)} ↔ (𝐼‘(𝐹‘0)) = {(𝑃‘0)}))
19		preq1 4666	. . . . . . . . 9 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → {(𝑃‘𝑁), (𝑃‘1)} = {(𝑃‘0), (𝑃‘1)})
20	19	sseq1d 3948	. . . . . . . 8 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → ({(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ↔ {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
21	16, 18, 20	ifpbi123d 1076	. . . . . . 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 256	. . . . 5 ⊢ (𝜑 → if-((𝑃‘𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
24		nncn 11911	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
25		nncn 11911	. . . . . . . . . 10 ⊢ (𝑆 ∈ ℕ → 𝑆 ∈ ℂ)
26		npcan 11160	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℂ ∧ 𝑆 ∈ ℂ) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
27	24, 25, 26	syl2anr 596	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
28		simpr 484	. . . . . . . . . 10 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
29		oveq1 7262	. . . . . . . . . . 11 ⊢ (((𝑁 − 𝑆) + 𝑆) = 𝑁 → (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = (𝑁 mod (♯‘𝐹)))
30		crctcshwlkn0lem.n	. . . . . . . . . . . . . . 15 ⊢ 𝑁 = (♯‘𝐹)
31	30	eqcomi 2747	. . . . . . . . . . . . . 14 ⊢ (♯‘𝐹) = 𝑁
32	31	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (♯‘𝐹) = 𝑁)
33	32	oveq2d 7271	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod (♯‘𝐹)) = (𝑁 mod 𝑁))
34		nnrp 12670	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ⁺)
35		modid0 13545	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℝ⁺ → (𝑁 mod 𝑁) = 0)
36	34, 35	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑁 mod 𝑁) = 0)
37	36	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod 𝑁) = 0)
38	33, 37	eqtrd 2778	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod (♯‘𝐹)) = 0)
39	29, 38	sylan9eqr 2801	. . . . . . . . . 10 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0)
40		simpl 482	. . . . . . . . . 10 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ))
41	28, 39, 40	3jca 1126	. . . . . . . . 9 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
42	27, 41	mpdan 683	. . . . . . . 8 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
43	42	3adant3 1130	. . . . . . 7 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
44	8, 43	sylbi 216	. . . . . 6 ⊢ (𝑆 ∈ (1..^𝑁) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
45		simp1 1134	. . . . . . . . 9 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
46	45	fveq2d 6760	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘𝑁))
47	46	eqeq1d 2740	. . . . . . 7 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1) ↔ (𝑃‘𝑁) = (𝑃‘1)))
48		simp2 1135	. . . . . . . . . 10 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0)
49	48	fveq2d 6760	. . . . . . . . 9 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))) = (𝐹‘0))
50	49	fveq2d 6760	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = (𝐼‘(𝐹‘0)))
51	46	sneqd 4570	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → {(𝑃‘((𝑁 − 𝑆) + 𝑆))} = {(𝑃‘𝑁)})
52	50, 51	eqeq12d 2754	. . . . . . 7 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))} ↔ (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}))
53	46	preq1d 4672	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} = {(𝑃‘𝑁), (𝑃‘1)})
54	53, 50	sseq12d 3950	. . . . . . 7 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ({(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) ↔ {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
55	47, 52, 54	ifpbi123d 1076	. . . . . 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 256	. . . 4 ⊢ (𝜑 → if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))))
58		nnsub 11947	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑆 < 𝑁 ↔ (𝑁 − 𝑆) ∈ ℕ))
59	58	biimp3a 1467	. . . . . . . . . 10 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 𝑆) ∈ ℕ)
60	59	nnnn0d 12223	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 𝑆) ∈ ℕ₀)
61	8, 60	sylbi 216	. . . . . . . 8 ⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈ ℕ₀)
62	7, 61	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑁 − 𝑆) ∈ ℕ₀)
63		nn0fz0 13283	. . . . . . 7 ⊢ ((𝑁 − 𝑆) ∈ ℕ₀ ↔ (𝑁 − 𝑆) ∈ (0...(𝑁 − 𝑆)))
64	62, 63	sylib 217	. . . . . 6 ⊢ (𝜑 → (𝑁 − 𝑆) ∈ (0...(𝑁 − 𝑆)))
65		crctcshwlkn0lem.q	. . . . . . 7 ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))
66	7, 65	crctcshwlkn0lem2 28077	. . . . . 6 ⊢ ((𝜑 ∧ (𝑁 − 𝑆) ∈ (0...(𝑁 − 𝑆))) → (𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)))
67	64, 66	mpdan 683	. . . . 5 ⊢ (𝜑 → (𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)))
68		elfzoel2 13315	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℤ)
69		elfzoelz 13316	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ ℤ)
70	68, 69	zsubcld 12360	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈ ℤ)
71	70	peano2zd 12358	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1..^𝑁) → ((𝑁 − 𝑆) + 1) ∈ ℤ)
72		nnre 11910	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
73	72	anim1i 614	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝑆 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ))
74	73	ancoms 458	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ))
75		crctcshwlkn0lem1 28076	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
76	74, 75	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
77	76	3adant3 1130	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
78	8, 77	sylbi 216	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1..^𝑁) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
79	71, 68, 78	3jca 1126	. . . . . . . . . 10 ⊢ (𝑆 ∈ (1..^𝑁) → (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁))
80	7, 79	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁))
81		eluz2 12517	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘((𝑁 − 𝑆) + 1)) ↔ (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁))
82	80, 81	sylibr 233	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘((𝑁 − 𝑆) + 1)))
83		eluzfz1 13192	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘((𝑁 − 𝑆) + 1)) → ((𝑁 − 𝑆) + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁))
84	82, 83	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑁 − 𝑆) + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁))
85	7, 65	crctcshwlkn0lem3 28078	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑁 − 𝑆) + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁)) → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁)))
86	84, 85	mpdan 683	. . . . . 6 ⊢ (𝜑 → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁)))
87		subcl 11150	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑁 − 𝑆) ∈ ℂ)
88	87	ancoms 458	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑁 − 𝑆) ∈ ℂ)
89		ax-1cn 10860	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
90		pncan2 11158	. . . . . . . . . . . . . 14 ⊢ (((𝑁 − 𝑆) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)) = 1)
91	90	eqcomd 2744	. . . . . . . . . . . . 13 ⊢ (((𝑁 − 𝑆) ∈ ℂ ∧ 1 ∈ ℂ) → 1 = (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)))
92	88, 89, 91	sylancl 585	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 1 = (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)))
93		peano2cn 11077	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 𝑆) ∈ ℂ → ((𝑁 − 𝑆) + 1) ∈ ℂ)
94	88, 93	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑁 − 𝑆) + 1) ∈ ℂ)
95		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 𝑁 ∈ ℂ)
96		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 𝑆 ∈ ℂ)
97	94, 95, 96	subsub3d 11292	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)) = ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁))
98	92, 97	eqtr2d 2779	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
99	25, 24, 98	syl2an 595	. . . . . . . . . 10 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
100	99	3adant3 1130	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
101	8, 100	sylbi 216	. . . . . . . 8 ⊢ (𝑆 ∈ (1..^𝑁) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
102	7, 101	syl 17	. . . . . . 7 ⊢ (𝜑 → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
103	102	fveq2d 6760	. . . . . 6 ⊢ (𝜑 → (𝑃‘((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁)) = (𝑃‘1))
104	86, 103	eqtrd 2778	. . . . 5 ⊢ (𝜑 → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1))
105		crctcshwlkn0lem.h	. . . . . . 7 ⊢ 𝐻 = (𝐹 cyclShift 𝑆)
106	105	fveq1i 6757	. . . . . 6 ⊢ (𝐻‘(𝑁 − 𝑆)) = ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆))
107		crctcshwlkn0lem.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ Word 𝐴)
108	107	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → 𝐹 ∈ Word 𝐴)
109	69	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → 𝑆 ∈ ℤ)
110		elfzofz 13331	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ (1...𝑁))
111		ubmelfzo 13380	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1...𝑁) → (𝑁 − 𝑆) ∈ (0..^𝑁))
112	110, 111	syl 17	. . . . . . . . . 10 ⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈ (0..^𝑁))
113	112	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → (𝑁 − 𝑆) ∈ (0..^𝑁))
114	31	oveq2i 7266	. . . . . . . . 9 ⊢ (0..^(♯‘𝐹)) = (0..^𝑁)
115	113, 114	eleqtrrdi 2850	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → (𝑁 − 𝑆) ∈ (0..^(♯‘𝐹)))
116		cshwidxmod 14444	. . . . . . . 8 ⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ (𝑁 − 𝑆) ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
117	108, 109, 115, 116	syl3anc 1369	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
118	7, 117	mpdan 683	. . . . . 6 ⊢ (𝜑 → ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
119	106, 118	syl5eq 2791	. . . . 5 ⊢ (𝜑 → (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
120		simp1 1134	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)))
121		simp2 1135	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1))
122	120, 121	eqeq12d 2754	. . . . . 6 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → ((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)) ↔ (𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1)))
123		simp3 1136	. . . . . . . 8 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
124	123	fveq2d 6760	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝐼‘(𝐻‘(𝑁 − 𝑆))) = (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))))
125	120	sneqd 4570	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → {(𝑄‘(𝑁 − 𝑆))} = {(𝑃‘((𝑁 − 𝑆) + 𝑆))})
126	124, 125	eqeq12d 2754	. . . . . 6 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → ((𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))} ↔ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}))
127	120, 121	preq12d 4674	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} = {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)})
128	127, 124	sseq12d 3950	. . . . . 6 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → ({(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))) ↔ {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))))
129	122, 126, 128	ifpbi123d 1076	. . . . 5 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))) ↔ if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))))))
130	67, 104, 119, 129	syl3anc 1369	. . . 4 ⊢ (𝜑 → (if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))) ↔ if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))))))
131	57, 130	mpbird 256	. . 3 ⊢ (𝜑 → if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))))
132	131	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))))
133		wkslem1 27877	. . 3 ⊢ (𝐽 = (𝑁 − 𝑆) → (if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))) ↔ if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))))))
134	133	adantl 481	. 2 ⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → (if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))) ↔ if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))))))
135	132, 134	mpbird 256	1 ⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 if-wif 1059 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ∀wral 3063 ⊆ wss 3883 ifcif 4456 {csn 4558 {cpr 4560 class class class wbr 5070 ↦ cmpt 5153 ‘cfv 6418 (class class class)co 7255 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 < clt 10940 ≤ cle 10941 − cmin 11135 ℕcn 11903 ℕ₀cn0 12163 ℤcz 12249 ℤ_≥cuz 12511 ℝ⁺crp 12659 ...cfz 13168 ..^cfzo 13311 mod cmo 13517 ♯chash 13972 Word cword 14145 cyclShift ccsh 14429

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-ifp 1060 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-inf 9132 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-n0 12164 df-z 12250 df-uz 12512 df-rp 12660 df-fz 13169 df-fzo 13312 df-fl 13440 df-mod 13518 df-hash 13973 df-word 14146 df-concat 14202 df-substr 14282 df-pfx 14312 df-csh 14430

This theorem is referenced by: crctcshwlkn0lem7 28082

W3C validator