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 29901

Description: Lemma for crctcshwlkn0 29907. (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 7363	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1))
2		0p1e1 12289	. . . . . . . . 9 ⊢ (0 + 1) = 1
3	1, 2	eqtrdi 2790	. . . . . . . 8 ⊢ (𝑖 = 0 → (𝑖 + 1) = 1)
4		wkslem2 29695	. . . . . . . 8 ⊢ ((𝑖 = 0 ∧ (𝑖 + 1) = 1) → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))))
5	3, 4	mpdan 693	. . . . . . 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 13658	. . . . . . . . . 10 ⊢ (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁))
9		simp2 1143	. . . . . . . . . 10 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ∈ ℕ)
10	8, 9	sylbi 218	. . . . . . . . 9 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℕ)
11	7, 10	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
12		lbfzo0 13645	. . . . . . . 8 ⊢ (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
13	11, 12	sylibr 235	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝑁))
14	5, 6, 13	rspcdva 3561	. . . . . 6 ⊢ (𝜑 → if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
15		crctcshwlkn0lem.e	. . . . . . 7 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))
16		eqeq1 2743	. . . . . . . 8 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → ((𝑃‘𝑁) = (𝑃‘1) ↔ (𝑃‘0) = (𝑃‘1)))
17		sneq 4565	. . . . . . . . 9 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → {(𝑃‘𝑁)} = {(𝑃‘0)})
18	17	eqeq2d 2750	. . . . . . . 8 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → ((𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)} ↔ (𝐼‘(𝐹‘0)) = {(𝑃‘0)}))
19		preq1 4665	. . . . . . . . 9 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → {(𝑃‘𝑁), (𝑃‘1)} = {(𝑃‘0), (𝑃‘1)})
20	19	sseq1d 3946	. . . . . . . 8 ⊢ ((𝑃‘𝑁) = (𝑃‘0) → ({(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ↔ {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
21	16, 18, 20	ifpbi123d 1084	. . . . . . 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 258	. . . . 5 ⊢ (𝜑 → if-((𝑃‘𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
24		nncn 12173	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
25		nncn 12173	. . . . . . . . . 10 ⊢ (𝑆 ∈ ℕ → 𝑆 ∈ ℂ)
26		npcan 11393	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℂ ∧ 𝑆 ∈ ℂ) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
27	24, 25, 26	syl2anr 603	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
28		simpr 485	. . . . . . . . . 10 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
29		oveq1 7363	. . . . . . . . . . 11 ⊢ (((𝑁 − 𝑆) + 𝑆) = 𝑁 → (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = (𝑁 mod (♯‘𝐹)))
30		crctcshwlkn0lem.n	. . . . . . . . . . . . . . 15 ⊢ 𝑁 = (♯‘𝐹)
31	30	eqcomi 2748	. . . . . . . . . . . . . 14 ⊢ (♯‘𝐹) = 𝑁
32	31	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (♯‘𝐹) = 𝑁)
33	32	oveq2d 7372	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod (♯‘𝐹)) = (𝑁 mod 𝑁))
34		nnrp 12945	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ⁺)
35		modid0 13847	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℝ⁺ → (𝑁 mod 𝑁) = 0)
36	34, 35	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑁 mod 𝑁) = 0)
37	36	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod 𝑁) = 0)
38	33, 37	eqtrd 2774	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod (♯‘𝐹)) = 0)
39	29, 38	sylan9eqr 2796	. . . . . . . . . 10 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0)
40		simpl 483	. . . . . . . . . 10 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ))
41	28, 39, 40	3jca 1134	. . . . . . . . 9 ⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
42	27, 41	mpdan 693	. . . . . . . 8 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
43	42	3adant3 1138	. . . . . . 7 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
44	8, 43	sylbi 218	. . . . . 6 ⊢ (𝑆 ∈ (1..^𝑁) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)))
45		simp1 1142	. . . . . . . . 9 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑁 − 𝑆) + 𝑆) = 𝑁)
46	45	fveq2d 6831	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘𝑁))
47	46	eqeq1d 2741	. . . . . . 7 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1) ↔ (𝑃‘𝑁) = (𝑃‘1)))
48		simp2 1143	. . . . . . . . . 10 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0)
49	48	fveq2d 6831	. . . . . . . . 9 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))) = (𝐹‘0))
50	49	fveq2d 6831	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = (𝐼‘(𝐹‘0)))
51	46	sneqd 4567	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → {(𝑃‘((𝑁 − 𝑆) + 𝑆))} = {(𝑃‘𝑁)})
52	50, 51	eqeq12d 2755	. . . . . . 7 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))} ↔ (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}))
53	46	preq1d 4671	. . . . . . . 8 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} = {(𝑃‘𝑁), (𝑃‘1)})
54	53, 50	sseq12d 3948	. . . . . . 7 ⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ({(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) ↔ {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))
55	47, 52, 54	ifpbi123d 1084	. . . . . 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 258	. . . 4 ⊢ (𝜑 → if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))))
58		nnsub 12212	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑆 < 𝑁 ↔ (𝑁 − 𝑆) ∈ ℕ))
59	58	biimp3a 1477	. . . . . . . . . 10 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 𝑆) ∈ ℕ)
60	59	nnnn0d 12489	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 𝑆) ∈ ℕ₀)
61	8, 60	sylbi 218	. . . . . . . 8 ⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈ ℕ₀)
62	7, 61	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑁 − 𝑆) ∈ ℕ₀)
63		nn0fz0 13570	. . . . . . 7 ⊢ ((𝑁 − 𝑆) ∈ ℕ₀ ↔ (𝑁 − 𝑆) ∈ (0...(𝑁 − 𝑆)))
64	62, 63	sylib 219	. . . . . 6 ⊢ (𝜑 → (𝑁 − 𝑆) ∈ (0...(𝑁 − 𝑆)))
65		crctcshwlkn0lem.q	. . . . . . 7 ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))
66	7, 65	crctcshwlkn0lem2 29897	. . . . . 6 ⊢ ((𝜑 ∧ (𝑁 − 𝑆) ∈ (0...(𝑁 − 𝑆))) → (𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)))
67	64, 66	mpdan 693	. . . . 5 ⊢ (𝜑 → (𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)))
68		elfzoel2 13603	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℤ)
69		elfzoelz 13604	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ ℤ)
70	68, 69	zsubcld 12629	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈ ℤ)
71	70	peano2zd 12627	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1..^𝑁) → ((𝑁 − 𝑆) + 1) ∈ ℤ)
72		nnre 12172	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
73	72	anim1i 621	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝑆 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ))
74	73	ancoms 459	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ))
75		crctcshwlkn0lem1 29896	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
76	74, 75	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
77	76	3adant3 1138	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
78	8, 77	sylbi 218	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1..^𝑁) → ((𝑁 − 𝑆) + 1) ≤ 𝑁)
79	71, 68, 78	3jca 1134	. . . . . . . . . 10 ⊢ (𝑆 ∈ (1..^𝑁) → (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁))
80	7, 79	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁))
81		eluz2 12785	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘((𝑁 − 𝑆) + 1)) ↔ (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁))
82	80, 81	sylibr 235	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘((𝑁 − 𝑆) + 1)))
83		eluzfz1 13476	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘((𝑁 − 𝑆) + 1)) → ((𝑁 − 𝑆) + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁))
84	82, 83	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑁 − 𝑆) + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁))
85	7, 65	crctcshwlkn0lem3 29898	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑁 − 𝑆) + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁)) → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁)))
86	84, 85	mpdan 693	. . . . . 6 ⊢ (𝜑 → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁)))
87		subcl 11383	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑁 − 𝑆) ∈ ℂ)
88	87	ancoms 459	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑁 − 𝑆) ∈ ℂ)
89		ax-1cn 11087	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
90		pncan2 11391	. . . . . . . . . . . . . 14 ⊢ (((𝑁 − 𝑆) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)) = 1)
91	90	eqcomd 2745	. . . . . . . . . . . . 13 ⊢ (((𝑁 − 𝑆) ∈ ℂ ∧ 1 ∈ ℂ) → 1 = (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)))
92	88, 89, 91	sylancl 592	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 1 = (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)))
93		peano2cn 11309	. . . . . . . . . . . . . 14 ⊢ ((𝑁 − 𝑆) ∈ ℂ → ((𝑁 − 𝑆) + 1) ∈ ℂ)
94	88, 93	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑁 − 𝑆) + 1) ∈ ℂ)
95		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 𝑁 ∈ ℂ)
96		simpl 483	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 𝑆 ∈ ℂ)
97	94, 95, 96	subsub3d 11526	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)) = ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁))
98	92, 97	eqtr2d 2775	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
99	25, 24, 98	syl2an 602	. . . . . . . . . 10 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
100	99	3adant3 1138	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
101	8, 100	sylbi 218	. . . . . . . 8 ⊢ (𝑆 ∈ (1..^𝑁) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
102	7, 101	syl 17	. . . . . . 7 ⊢ (𝜑 → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1)
103	102	fveq2d 6831	. . . . . 6 ⊢ (𝜑 → (𝑃‘((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁)) = (𝑃‘1))
104	86, 103	eqtrd 2774	. . . . 5 ⊢ (𝜑 → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1))
105		crctcshwlkn0lem.h	. . . . . . 7 ⊢ 𝐻 = (𝐹 cyclShift 𝑆)
106	105	fveq1i 6828	. . . . . 6 ⊢ (𝐻‘(𝑁 − 𝑆)) = ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆))
107		crctcshwlkn0lem.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ Word 𝐴)
108	107	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → 𝐹 ∈ Word 𝐴)
109	69	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → 𝑆 ∈ ℤ)
110		elfzofz 13621	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ (1...𝑁))
111		ubmelfzo 13676	. . . . . . . . . . 11 ⊢ (𝑆 ∈ (1...𝑁) → (𝑁 − 𝑆) ∈ (0..^𝑁))
112	110, 111	syl 17	. . . . . . . . . 10 ⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈ (0..^𝑁))
113	112	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → (𝑁 − 𝑆) ∈ (0..^𝑁))
114	31	oveq2i 7367	. . . . . . . . 9 ⊢ (0..^(♯‘𝐹)) = (0..^𝑁)
115	113, 114	eleqtrrdi 2850	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → (𝑁 − 𝑆) ∈ (0..^(♯‘𝐹)))
116		cshwidxmod 14756	. . . . . . . 8 ⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ (𝑁 − 𝑆) ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
117	108, 109, 115, 116	syl3anc 1379	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
118	7, 117	mpdan 693	. . . . . 6 ⊢ (𝜑 → ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
119	106, 118	eqtrid 2786	. . . . 5 ⊢ (𝜑 → (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
120		simp1 1142	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)))
121		simp2 1143	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1))
122	120, 121	eqeq12d 2755	. . . . . 6 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → ((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)) ↔ (𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1)))
123		simp3 1144	. . . . . . . 8 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))
124	123	fveq2d 6831	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝐼‘(𝐻‘(𝑁 − 𝑆))) = (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))))
125	120	sneqd 4567	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → {(𝑄‘(𝑁 − 𝑆))} = {(𝑃‘((𝑁 − 𝑆) + 𝑆))})
126	124, 125	eqeq12d 2755	. . . . . 6 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → ((𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))} ↔ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}))
127	120, 121	preq12d 4673	. . . . . . 7 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} = {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)})
128	127, 124	sseq12d 3948	. . . . . 6 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → ({(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))) ↔ {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))))
129	122, 126, 128	ifpbi123d 1084	. . . . 5 ⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))) ↔ if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))))))
130	67, 104, 119, 129	syl3anc 1379	. . . 4 ⊢ (𝜑 → (if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))) ↔ if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))))))
131	57, 130	mpbird 258	. . 3 ⊢ (𝜑 → if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))))
132	131	adantr 481	. 2 ⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))))
133		wkslem1 29694	. . 3 ⊢ (𝐽 = (𝑁 − 𝑆) → (if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))) ↔ if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))))))
134	133	adantl 482	. 2 ⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → (if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))) ↔ if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))))))
135	132, 134	mpbird 258	1 ⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 if-wif 1068 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ∀wral 3053 ⊆ wss 3883 ifcif 4454 {csn 4555 {cpr 4557 class class class wbr 5072 ↦ cmpt 5153 ‘cfv 6485 (class class class)co 7356 ℂcc 11027 ℝcr 11028 0cc0 11029 1c1 11030 + caddc 11032 < clt 11170 ≤ cle 11171 − cmin 11368 ℕcn 12165 ℕ₀cn0 12428 ℤcz 12515 ℤ_≥cuz 12779 ℝ⁺crp 12933 ...cfz 13452 ..^cfzo 13599 mod cmo 13819 ♯chash 14283 Word cword 14466 cyclShift ccsh 14741

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 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-ifp 1069 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8633 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9345 df-inf 9346 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-n0 12429 df-z 12516 df-uz 12780 df-rp 12934 df-fz 13453 df-fzo 13600 df-fl 13742 df-mod 13820 df-hash 14284 df-word 14467 df-concat 14524 df-substr 14595 df-pfx 14625 df-csh 14742

This theorem is referenced by: crctcshwlkn0lem7 29902

W3C validator