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 29845

Description: Lemma for crctcshwlkn0 29851. (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 7438	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
2		0p1e1 12386	. . . . . . . . 9 ⊢ (0 + 1) = 1
3	1, 2	eqtrdi 2791	. . . . . . . 8 ⊢ (𝑖 = 0 → (𝑖 + 1) = 1)
4		wkslem2 29641	. . . . . . . 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 13749	. . . . . . . . . 10 ⊢ (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁))
9		simp2 1136	. . . . . . . . . 10 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ∈ ℕ)
10	8, 9	sylbi 217	. . . . . . . . 9 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℕ)
11	7, 10	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
12		lbfzo0 13736	. . . . . . . 8 ⊢ (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
13	11, 12	sylibr 234	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝑁))
14	5, 6, 13	rspcdva 3623	. . . . . 6 ⊢ (𝜑 → if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
15		crctcshwlkn0lem.e	. . . . . . 7 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))
16		eqeq1 2739	. . . . . . . 8 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → ((𝑃‘𝑁) = (𝑃‘1) ↔ (𝑃‘0) = (𝑃‘1)))
17		sneq 4641	. . . . . . . . 9 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → {(𝑃‘𝑁)} = {(𝑃‘0)})
18	17	eqeq2d 2746	. . . . . . . 8 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → ((𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)} ↔ (𝐼‘(𝐹‘0)) = {(𝑃‘0)}))
19		preq1 4738	. . . . . . . . 9 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → {(𝑃‘𝑁), (𝑃‘1)} = {(𝑃‘0), (𝑃‘1)})
20	19	sseq1d 4027	. . . . . . . 8 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → ({(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ↔ {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
21	16, 18, 20	ifpbi123d 1078	. . . . . . 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 257	. . . . 5 ⊢ (𝜑 → if-((𝑃‘𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
24		nncn 12272	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
25		nncn 12272	. . . . . . . . . 10 ⊢ (𝑆 ∈ ℕ → 𝑆 ∈ ℂ)
26		npcan 11515	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℂ ∧ 𝑆 ∈ ℂ) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
27	24, 25, 26	syl2anr 597	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
28		simpr 484	. . . . . . . . . 10 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
29		oveq1 7438	. . . . . . . . . . 11 ⊢ (((𝑁 − 𝑆) + 𝑆) = 𝑁 → (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = (𝑁 mod (♯‘𝐹)))
30		crctcshwlkn0lem.n	. . . . . . . . . . . . . . 15 ⊢ 𝑁 = (♯‘𝐹)
31	30	eqcomi 2744	. . . . . . . . . . . . . 14 ⊢ (♯‘𝐹) = 𝑁
32	31	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (♯‘𝐹) = 𝑁)
33	32	oveq2d 7447	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod (♯‘𝐹)) = (𝑁 mod 𝑁))
34		nnrp 13044	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ⁺)
35		modid0 13934	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℝ⁺ → (𝑁 mod 𝑁) = 0)
36	34, 35	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑁 mod 𝑁) = 0)
37	36	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod 𝑁) = 0)
38	33, 37	eqtrd 2775	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod (♯‘𝐹)) = 0)
39	29, 38	sylan9eqr 2797	. . . . . . . . . 10 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0)
40		simpl 482	. . . . . . . . . 10 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ))
41	28, 39, 40	3jca 1127	. . . . . . . . 9 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
42	27, 41	mpdan 687	. . . . . . . 8 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
43	42	3adant3 1131	. . . . . . 7 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
44	8, 43	sylbi 217	. . . . . 6 ⊢ (𝑆 ∈ (1..^𝑁) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
45		simp1 1135	. . . . . . . . 9 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
46	45	fveq2d 6911	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘𝑁))
47	46	eqeq1d 2737	. . . . . . 7 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1) ↔ (𝑃‘𝑁) = (𝑃‘1)))
48		simp2 1136	. . . . . . . . . 10 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0)
49	48	fveq2d 6911	. . . . . . . . 9 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))) = (𝐹‘0))
50	49	fveq2d 6911	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = (𝐼‘(𝐹‘0)))
51	46	sneqd 4643	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → {(𝑃‘((𝑁 − 𝑆) + 𝑆))} = {(𝑃‘𝑁)})
52	50, 51	eqeq12d 2751	. . . . . . 7 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))} ↔ (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}))
53	46	preq1d 4744	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} = {(𝑃‘𝑁), (𝑃‘1)})
54	53, 50	sseq12d 4029	. . . . . . 7 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ({(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) ↔ {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
55	47, 52, 54	ifpbi123d 1078	. . . . . 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 257	. . . 4 ⊢ (𝜑 → if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))))
58		nnsub 12308	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑆 < 𝑁 ↔ (𝑁 − 𝑆) ∈ ℕ))
59	58	biimp3a 1468	. . . . . . . . . 10 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 𝑆) ∈ ℕ)
60	59	nnnn0d 12585	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 𝑆) ∈ ℕ₀)
61	8, 60	sylbi 217	. . . . . . . 8 ⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈ ℕ₀)
62	7, 61	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑁 − 𝑆) ∈ ℕ₀)
63		nn0fz0 13662	. . . . . . 7 ⊢ ((𝑁 − 𝑆) ∈ ℕ₀ ↔ (𝑁 − 𝑆) ∈ (0...(𝑁 − 𝑆)))
64	62, 63	sylib 218	. . . . . 6 ⊢ (𝜑 → (𝑁 − 𝑆) ∈ (0...(𝑁 − 𝑆)))
65		crctcshwlkn0lem.q	. . . . . . 7 ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))
66	7, 65	crctcshwlkn0lem2 29841	. . . . . 6 ⊢ ((𝜑 ∧ (𝑁 − 𝑆) ∈ (0...(𝑁 − 𝑆))) → (𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)))
67	64, 66	mpdan 687	. . . . 5 ⊢ (𝜑 → (𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)))
68		elfzoel2 13695	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℤ)
69		elfzoelz 13696	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ ℤ)
70	68, 69	zsubcld 12725	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈ ℤ)
71	70	peano2zd 12723	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1..^𝑁) → ((𝑁 − 𝑆) + 1) ∈ ℤ)
72		nnre 12271	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
73	72	anim1i 615	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝑆 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ))
74	73	ancoms 458	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ))
75		crctcshwlkn0lem1 29840	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
76	74, 75	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
77	76	3adant3 1131	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
78	8, 77	sylbi 217	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1..^𝑁) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
79	71, 68, 78	3jca 1127	. . . . . . . . . 10 ⊢ (𝑆 ∈ (1..^𝑁) → (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁))
80	7, 79	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁))
81		eluz2 12882	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘((𝑁 − 𝑆) + 1)) ↔ (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁))
82	80, 81	sylibr 234	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘((𝑁 − 𝑆) + 1)))
83		eluzfz1 13568	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘((𝑁 − 𝑆) + 1)) → ((𝑁 − 𝑆) + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁))
84	82, 83	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑁 − 𝑆) + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁))
85	7, 65	crctcshwlkn0lem3 29842	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑁 − 𝑆) + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁)) → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁)))
86	84, 85	mpdan 687	. . . . . 6 ⊢ (𝜑 → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁)))
87		subcl 11505	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑁 − 𝑆) ∈ ℂ)
88	87	ancoms 458	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑁 − 𝑆) ∈ ℂ)
89		ax-1cn 11211	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
90		pncan2 11513	. . . . . . . . . . . . . 14 ⊢ (((𝑁 − 𝑆) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)) = 1)
91	90	eqcomd 2741	. . . . . . . . . . . . 13 ⊢ (((𝑁 − 𝑆) ∈ ℂ ∧ 1 ∈ ℂ) → 1 = (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)))
92	88, 89, 91	sylancl 586	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 1 = (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)))
93		peano2cn 11431	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 𝑆) ∈ ℂ → ((𝑁 − 𝑆) + 1) ∈ ℂ)
94	88, 93	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑁 − 𝑆) + 1) ∈ ℂ)
95		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 𝑁 ∈ ℂ)
96		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 𝑆 ∈ ℂ)
97	94, 95, 96	subsub3d 11648	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)) = ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁))
98	92, 97	eqtr2d 2776	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
99	25, 24, 98	syl2an 596	. . . . . . . . . 10 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
100	99	3adant3 1131	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
101	8, 100	sylbi 217	. . . . . . . 8 ⊢ (𝑆 ∈ (1..^𝑁) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
102	7, 101	syl 17	. . . . . . 7 ⊢ (𝜑 → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
103	102	fveq2d 6911	. . . . . 6 ⊢ (𝜑 → (𝑃‘((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁)) = (𝑃‘1))
104	86, 103	eqtrd 2775	. . . . 5 ⊢ (𝜑 → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1))
105		crctcshwlkn0lem.h	. . . . . . 7 ⊢ 𝐻 = (𝐹 cyclShift 𝑆)
106	105	fveq1i 6908	. . . . . 6 ⊢ (𝐻‘(𝑁 − 𝑆)) = ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆))
107		crctcshwlkn0lem.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ Word 𝐴)
108	107	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → 𝐹 ∈ Word 𝐴)
109	69	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → 𝑆 ∈ ℤ)
110		elfzofz 13712	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ (1...𝑁))
111		ubmelfzo 13766	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1...𝑁) → (𝑁 − 𝑆) ∈ (0..^𝑁))
112	110, 111	syl 17	. . . . . . . . . 10 ⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈ (0..^𝑁))
113	112	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → (𝑁 − 𝑆) ∈ (0..^𝑁))
114	31	oveq2i 7442	. . . . . . . . 9 ⊢ (0..^(♯‘𝐹)) = (0..^𝑁)
115	113, 114	eleqtrrdi 2850	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → (𝑁 − 𝑆) ∈ (0..^(♯‘𝐹)))
116		cshwidxmod 14838	. . . . . . . 8 ⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ (𝑁 − 𝑆) ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
117	108, 109, 115, 116	syl3anc 1370	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
118	7, 117	mpdan 687	. . . . . 6 ⊢ (𝜑 → ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
119	106, 118	eqtrid 2787	. . . . 5 ⊢ (𝜑 → (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
120		simp1 1135	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)))
121		simp2 1136	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1))
122	120, 121	eqeq12d 2751	. . . . . 6 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → ((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)) ↔ (𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1)))
123		simp3 1137	. . . . . . . 8 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
124	123	fveq2d 6911	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝐼‘(𝐻‘(𝑁 − 𝑆))) = (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))))
125	120	sneqd 4643	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → {(𝑄‘(𝑁 − 𝑆))} = {(𝑃‘((𝑁 − 𝑆) + 𝑆))})
126	124, 125	eqeq12d 2751	. . . . . 6 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → ((𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))} ↔ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}))
127	120, 121	preq12d 4746	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} = {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)})
128	127, 124	sseq12d 4029	. . . . . 6 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → ({(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))) ↔ {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))))
129	122, 126, 128	ifpbi123d 1078	. . . . 5 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))) ↔ if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))))))
130	67, 104, 119, 129	syl3anc 1370	. . . 4 ⊢ (𝜑 → (if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))) ↔ if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))))))
131	57, 130	mpbird 257	. . 3 ⊢ (𝜑 → if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))))
132	131	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))))
133		wkslem1 29640	. . 3 ⊢ (𝐽 = (𝑁 − 𝑆) → (if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))) ↔ if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))))))
134	133	adantl 481	. 2 ⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → (if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))) ↔ if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))))))
135	132, 134	mpbird 257	1 ⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 if-wif 1062 ∧ w3a 1086 = wceq 1537 ∈ wcel 2106 ∀wral 3059 ⊆ wss 3963 ifcif 4531 {csn 4631 {cpr 4633 class class class wbr 5148 ↦ cmpt 5231 ‘cfv 6563 (class class class)co 7431 ℂcc 11151 ℝcr 11152 0cc0 11153 1c1 11154 + caddc 11156 < clt 11293 ≤ cle 11294 − cmin 11490 ℕcn 12264 ℕ₀cn0 12524 ℤcz 12611 ℤ_≥cuz 12876 ℝ⁺crp 13032 ...cfz 13544 ..^cfzo 13691 mod cmo 13906 ♯chash 14366 Word cword 14549 cyclShift ccsh 14823

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230 ax-pre-sup 11231

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ifp 1063 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3378 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-int 4952 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8013 df-2nd 8014 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-1o 8505 df-er 8744 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-sup 9480 df-inf 9481 df-card 9977 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-div 11919 df-nn 12265 df-2 12327 df-n0 12525 df-z 12612 df-uz 12877 df-rp 13033 df-fz 13545 df-fzo 13692 df-fl 13829 df-mod 13907 df-hash 14367 df-word 14550 df-concat 14606 df-substr 14676 df-pfx 14706 df-csh 14824

This theorem is referenced by: crctcshwlkn0lem7 29846

W3C validator