wrdpmtrlast - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > wrdpmtrlast		Structured version Visualization version GIF version

Theorem wrdpmtrlast 33353

Description: Reorder a word, so that the symbol given at index 𝐼 is at the end. (Contributed by Thierry Arnoux, 27-May-2025.)

**Hypotheses**
Ref	Expression
wrdpmtrlast.1	⊢ 𝐽 = (0..^(♯‘𝑊))
wrdpmtrlast.2	⊢ (𝜑 → 𝐼 ∈ 𝐽)
wrdpmtrlast.3	⊢ (𝜑 → 𝑊 ∈ Word 𝑆)
wrdpmtrlast.4	⊢ 𝑈 = ((𝑊 ∘ 𝑠) prefix ((♯‘𝑊) − 1))

**Assertion**
Ref	Expression
wrdpmtrlast	⊢ (𝜑 → ∃𝑠(𝑠:𝐽–1-1-onto→𝐽 ∧ (𝑊 ∘ 𝑠) = (𝑈 ++ ⟨“(𝑊‘𝐼)”⟩)))

Distinct variable groups: 𝐼,𝑠 𝐽,𝑠 𝑊,𝑠 𝜑,𝑠 Allowed substitution hints: 𝑆(𝑠) 𝑈(𝑠)

**Proof of Theorem wrdpmtrlast**
Step	Hyp	Ref	Expression
1		wrdpmtrlast.1	. . 3 ⊢ 𝐽 = (0..^(♯‘𝑊))
2		wrdpmtrlast.2	. . 3 ⊢ (𝜑 → 𝐼 ∈ 𝐽)
3	1, 2	fzo0pmtrlast 33352	. 2 ⊢ (𝜑 → ∃𝑠(𝑠:𝐽–1-1-onto→𝐽 ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼))
4		simplr 780	. . . . 5 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → 𝑠:𝐽–1-1-onto→𝐽)
5		wrdpmtrlast.4	. . . . . . . 8 ⊢ 𝑈 = ((𝑊 ∘ 𝑠) prefix ((♯‘𝑊) − 1))
6		f1of 6821	. . . . . . . . . . . . . . 15 ⊢ (𝑠:𝐽–1-1-onto→𝐽 → 𝑠:𝐽⟶𝐽)
7	1	feq2i 6698	. . . . . . . . . . . . . . 15 ⊢ (𝑠:𝐽⟶𝐽 ↔ 𝑠:(0..^(♯‘𝑊))⟶𝐽)
8	6, 7	sylib 221	. . . . . . . . . . . . . 14 ⊢ (𝑠:𝐽–1-1-onto→𝐽 → 𝑠:(0..^(♯‘𝑊))⟶𝐽)
9	4, 8	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → 𝑠:(0..^(♯‘𝑊))⟶𝐽)
10		iswrdi 14553	. . . . . . . . . . . . 13 ⊢ (𝑠:(0..^(♯‘𝑊))⟶𝐽 → 𝑠 ∈ Word 𝐽)
11	9, 10	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → 𝑠 ∈ Word 𝐽)
12		eqidd 2770	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (♯‘𝑊) = (♯‘𝑊))
13		wrdpmtrlast.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)
14	13	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → 𝑊 ∈ Word 𝑆)
15	12, 14	wrdfd 14555	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
16	1	feq2i 6698	. . . . . . . . . . . . 13 ⊢ (𝑊:𝐽⟶𝑆 ↔ 𝑊:(0..^(♯‘𝑊))⟶𝑆)
17	15, 16	sylibr 237	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → 𝑊:𝐽⟶𝑆)
18		lenco 14868	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ Word 𝐽 ∧ 𝑊:𝐽⟶𝑆) → (♯‘(𝑊 ∘ 𝑠)) = (♯‘𝑠))
19	11, 17, 18	syl2anc 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (♯‘(𝑊 ∘ 𝑠)) = (♯‘𝑠))
20	9	ffund 6711	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → Fun 𝑠)
21		hashfundm 14478	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ Word 𝐽 ∧ Fun 𝑠) → (♯‘𝑠) = (♯‘dom 𝑠))
22	11, 20, 21	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (♯‘𝑠) = (♯‘dom 𝑠))
23	9	fdmd 6717	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → dom 𝑠 = (0..^(♯‘𝑊)))
24	23	fveq2d 6886	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (♯‘dom 𝑠) = (♯‘(0..^(♯‘𝑊))))
25	2, 1	eleqtrdi 2879	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐼 ∈ (0..^(♯‘𝑊)))
26	25	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → 𝐼 ∈ (0..^(♯‘𝑊)))
27		elfzo0 13728	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 ∈ (0..^(♯‘𝑊)) ↔ (𝐼 ∈ ℕ₀ ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐼 < (♯‘𝑊)))
28	27	simp2bi 1162	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ (0..^(♯‘𝑊)) → (♯‘𝑊) ∈ ℕ)
29	26, 28	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (♯‘𝑊) ∈ ℕ)
30	29	nnnn0d 12564	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (♯‘𝑊) ∈ ℕ₀)
31		hashfzo0 14466	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑊) ∈ ℕ₀ → (♯‘(0..^(♯‘𝑊))) = (♯‘𝑊))
32	30, 31	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (♯‘(0..^(♯‘𝑊))) = (♯‘𝑊))
33	22, 24, 32	3eqtrd 2808	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (♯‘𝑠) = (♯‘𝑊))
34	19, 33	eqtr2d 2805	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (♯‘𝑊) = (♯‘(𝑊 ∘ 𝑠)))
35	34	oveq1d 7426	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → ((♯‘𝑊) − 1) = ((♯‘(𝑊 ∘ 𝑠)) − 1))
36	35	oveq2d 7427	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → ((𝑊 ∘ 𝑠) prefix ((♯‘𝑊) − 1)) = ((𝑊 ∘ 𝑠) prefix ((♯‘(𝑊 ∘ 𝑠)) − 1)))
37	5, 36	eqtrid 2816	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → 𝑈 = ((𝑊 ∘ 𝑠) prefix ((♯‘(𝑊 ∘ 𝑠)) − 1)))
38	26	ne0d 4303	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (0..^(♯‘𝑊)) ≠ ∅)
39		f0dom0 6763	. . . . . . . . . . . . 13 ⊢ (𝑠:(0..^(♯‘𝑊))⟶𝐽 → ((0..^(♯‘𝑊)) = ∅ ↔ 𝑠 = ∅))
40	39	necon3bid 3008	. . . . . . . . . . . 12 ⊢ (𝑠:(0..^(♯‘𝑊))⟶𝐽 → ((0..^(♯‘𝑊)) ≠ ∅ ↔ 𝑠 ≠ ∅))
41	40	biimpa 481	. . . . . . . . . . 11 ⊢ ((𝑠:(0..^(♯‘𝑊))⟶𝐽 ∧ (0..^(♯‘𝑊)) ≠ ∅) → 𝑠 ≠ ∅)
42	9, 38, 41	syl2anc 595	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → 𝑠 ≠ ∅)
43		lswco 14875	. . . . . . . . . 10 ⊢ ((𝑠 ∈ Word 𝐽 ∧ 𝑠 ≠ ∅ ∧ 𝑊:𝐽⟶𝑆) → (lastS‘(𝑊 ∘ 𝑠)) = (𝑊‘(lastS‘𝑠)))
44	11, 42, 17, 43	syl3anc 1396	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (lastS‘(𝑊 ∘ 𝑠)) = (𝑊‘(lastS‘𝑠)))
45		lsw 14600	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ Word 𝐽 → (lastS‘𝑠) = (𝑠‘((♯‘𝑠) − 1)))
46	11, 45	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (lastS‘𝑠) = (𝑠‘((♯‘𝑠) − 1)))
47	33	oveq1d 7426	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → ((♯‘𝑠) − 1) = ((♯‘𝑊) − 1))
48	47	fveq2d 6886	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (𝑠‘((♯‘𝑠) − 1)) = (𝑠‘((♯‘𝑊) − 1)))
49		simpr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (𝑠‘((♯‘𝑊) − 1)) = 𝐼)
50	46, 48, 49	3eqtrd 2808	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (lastS‘𝑠) = 𝐼)
51	50	fveq2d 6886	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (𝑊‘(lastS‘𝑠)) = (𝑊‘𝐼))
52	44, 51	eqtr2d 2805	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (𝑊‘𝐼) = (lastS‘(𝑊 ∘ 𝑠)))
53	52	s1eqd 14638	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → ⟨“(𝑊‘𝐼)”⟩ = ⟨“(lastS‘(𝑊 ∘ 𝑠))”⟩)
54	37, 53	oveq12d 7429	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (𝑈 ++ ⟨“(𝑊‘𝐼)”⟩) = (((𝑊 ∘ 𝑠) prefix ((♯‘(𝑊 ∘ 𝑠)) − 1)) ++ ⟨“(lastS‘(𝑊 ∘ 𝑠))”⟩))
55	1, 4, 14	wrdpmcl 33198	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (𝑊 ∘ 𝑠) ∈ Word 𝑆)
56		fzo0end 13786	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑊) ∈ ℕ → ((♯‘𝑊) − 1) ∈ (0..^(♯‘𝑊)))
57	29, 56	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → ((♯‘𝑊) − 1) ∈ (0..^(♯‘𝑊)))
58	57, 1	eleqtrrdi 2880	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → ((♯‘𝑊) − 1) ∈ 𝐽)
59	17	fdmd 6717	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → dom 𝑊 = 𝐽)
60	58, 59	eleqtrrd 2872	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → ((♯‘𝑊) − 1) ∈ dom 𝑊)
61		dff1o5 6831	. . . . . . . . . . . . 13 ⊢ (𝑠:𝐽–1-1-onto→𝐽 ↔ (𝑠:𝐽–1-1→𝐽 ∧ ran 𝑠 = 𝐽))
62	61	simprbi 502	. . . . . . . . . . . 12 ⊢ (𝑠:𝐽–1-1-onto→𝐽 → ran 𝑠 = 𝐽)
63	4, 62	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → ran 𝑠 = 𝐽)
64	58, 63	eleqtrrd 2872	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → ((♯‘𝑊) − 1) ∈ ran 𝑠)
65	60, 64	elind 4161	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → ((♯‘𝑊) − 1) ∈ (dom 𝑊 ∩ ran 𝑠))
66	65	ne0d 4303	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (dom 𝑊 ∩ ran 𝑠) ≠ ∅)
67		coeq0 6258	. . . . . . . . 9 ⊢ ((𝑊 ∘ 𝑠) = ∅ ↔ (dom 𝑊 ∩ ran 𝑠) = ∅)
68	67	necon3bii 3016	. . . . . . . 8 ⊢ ((𝑊 ∘ 𝑠) ≠ ∅ ↔ (dom 𝑊 ∩ ran 𝑠) ≠ ∅)
69	66, 68	sylibr 237	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (𝑊 ∘ 𝑠) ≠ ∅)
70		pfxlswccat 14749	. . . . . . 7 ⊢ (((𝑊 ∘ 𝑠) ∈ Word 𝑆 ∧ (𝑊 ∘ 𝑠) ≠ ∅) → (((𝑊 ∘ 𝑠) prefix ((♯‘(𝑊 ∘ 𝑠)) − 1)) ++ ⟨“(lastS‘(𝑊 ∘ 𝑠))”⟩) = (𝑊 ∘ 𝑠))
71	55, 69, 70	syl2anc 595	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (((𝑊 ∘ 𝑠) prefix ((♯‘(𝑊 ∘ 𝑠)) − 1)) ++ ⟨“(lastS‘(𝑊 ∘ 𝑠))”⟩) = (𝑊 ∘ 𝑠))
72	54, 71	eqtr2d 2805	. . . . 5 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (𝑊 ∘ 𝑠) = (𝑈 ++ ⟨“(𝑊‘𝐼)”⟩))
73	4, 72	jca 520	. . . 4 ⊢ (((𝜑 ∧ 𝑠:𝐽–1-1-onto→𝐽) ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (𝑠:𝐽–1-1-onto→𝐽 ∧ (𝑊 ∘ 𝑠) = (𝑈 ++ ⟨“(𝑊‘𝐼)”⟩)))
74	73	expl 462	. . 3 ⊢ (𝜑 → ((𝑠:𝐽–1-1-onto→𝐽 ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → (𝑠:𝐽–1-1-onto→𝐽 ∧ (𝑊 ∘ 𝑠) = (𝑈 ++ ⟨“(𝑊‘𝐼)”⟩))))
75	74	eximdv 1944	. 2 ⊢ (𝜑 → (∃𝑠(𝑠:𝐽–1-1-onto→𝐽 ∧ (𝑠‘((♯‘𝑊) − 1)) = 𝐼) → ∃𝑠(𝑠:𝐽–1-1-onto→𝐽 ∧ (𝑊 ∘ 𝑠) = (𝑈 ++ ⟨“(𝑊‘𝐼)”⟩))))
76	3, 75	mpd 16	1 ⊢ (𝜑 → ∃𝑠(𝑠:𝐽–1-1-onto→𝐽 ∧ (𝑊 ∘ 𝑠) = (𝑈 ++ ⟨“(𝑊‘𝐼)”⟩)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1567 ∃wex 1806 ∈ wcel 2149 ≠ wne 2964 ∩ cin 3912 ∅c0 4294 class class class wbr 5113 dom cdm 5662 ran crn 5663 ∘ ccom 5666 Fun wfun 6531 ⟶wf 6533 –1-1→wf1 6534 –1-1-onto→wf1o 6536 ‘cfv 6537 (class class class)co 7411 0cc0 11099 1c1 11100 < clt 11242 − cmin 11440 ℕcn 12232 ℕ₀cn0 12503 ..^cfzo 13681 ♯chash 14365 Word cword 14549 lastSclsw 14598 ++ cconcat 14606 ⟨“cs1 14632 prefix cpfx 14707

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-oadd 8456 df-er 8693 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-dju 9886 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-2 12302 df-n0 12504 df-xnn0 12577 df-z 12591 df-uz 12862 df-fz 13535 df-fzo 13682 df-hash 14366 df-word 14550 df-lsw 14599 df-concat 14607 df-s1 14633 df-substr 14678 df-pfx 14708 df-pmtr 19511

This theorem is referenced by: 1arithidom 33771

W3C validator