2clwwlk2clwwlk - Metamath Proof Explorer

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

Theorem 2clwwlk2clwwlk 29294

Description: An element of the value of operation 𝐶, i.e., a word being a double loop of length 𝑁 on vertex 𝑋, is composed of two closed walks. (Contributed by AV, 28-Apr-2022.) (Proof shortened by AV, 3-Nov-2022.)

**Hypothesis**
Ref	Expression
2clwwlk.c	⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ_≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})

**Assertion**
Ref	Expression
2clwwlk2clwwlk	⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (𝑊 ∈ (𝑋𝐶𝑁) ↔ ∃𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))∃𝑏 ∈ (𝑋(ClWWalksNOn‘𝐺)2)𝑊 = (𝑎 ++ 𝑏)))

Distinct variable groups: 𝑛,𝐺,𝑣,𝑤 𝑛,𝑁,𝑣,𝑤 𝑛,𝑉,𝑣 𝑛,𝑋,𝑣,𝑤 𝑤,𝑊 𝐶,𝑎,𝑏 𝐺,𝑎,𝑏 𝑁,𝑎,𝑏,𝑤 𝑉,𝑎,𝑏 𝑊,𝑎,𝑏 𝑋,𝑎,𝑏 Allowed substitution hints: 𝐶(𝑤,𝑣,𝑛) 𝑉(𝑤) 𝑊(𝑣,𝑛)

**Proof of Theorem 2clwwlk2clwwlk**
Step	Hyp	Ref	Expression
1		uzuzle23 12814	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ (ℤ_≥‘2))
2		2clwwlk.c	. . . . . 6 ⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ_≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})
3	2	2clwwlkel 29293	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → (𝑊 ∈ (𝑋𝐶𝑁) ↔ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)))
4	1, 3	sylan2 593	. . . 4 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (𝑊 ∈ (𝑋𝐶𝑁) ↔ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)))
5		simpr 485	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → 𝑁 ∈ (ℤ_≥‘3))
6	5	anim1i 615	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)) → (𝑁 ∈ (ℤ_≥‘3) ∧ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)))
7		3anass 1095	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋) ↔ (𝑁 ∈ (ℤ_≥‘3) ∧ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)))
8	6, 7	sylibr 233	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)) → (𝑁 ∈ (ℤ_≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋))
9		clwwnonrepclwwnon 29289	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋) → (𝑊 prefix (𝑁 − 2)) ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))
10	8, 9	syl 17	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)) → (𝑊 prefix (𝑁 − 2)) ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))
11	5	adantr 481	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)) → 𝑁 ∈ (ℤ_≥‘3))
12		simprl 769	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)) → 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁))
13		simprr 771	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)) → (𝑊‘(𝑁 − 2)) = 𝑋)
14		isclwwlknon 29035	. . . . . . . . . 10 ⊢ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋))
15		simpr 485	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → (𝑊‘0) = 𝑋)
16	15	eqcomd 2742	. . . . . . . . . 10 ⊢ ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → 𝑋 = (𝑊‘0))
17	14, 16	sylbi 216	. . . . . . . . 9 ⊢ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) → 𝑋 = (𝑊‘0))
18	17	ad2antrl 726	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)) → 𝑋 = (𝑊‘0))
19	13, 18	eqtrd 2776	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)) → (𝑊‘(𝑁 − 2)) = (𝑊‘0))
20		2clwwlk2clwwlklem 29290	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩) ∈ (𝑋(ClWWalksNOn‘𝐺)2))
21	11, 12, 19, 20	syl3anc 1371	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)) → (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩) ∈ (𝑋(ClWWalksNOn‘𝐺)2))
22		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
23	22	clwwlknbp 28979	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁))
24		opeq2 4831	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 = (♯‘𝑊) → ⟨(𝑁 − 2), 𝑁⟩ = ⟨(𝑁 − 2), (♯‘𝑊)⟩)
25	24	oveq2d 7373	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 = (♯‘𝑊) → (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩) = (𝑊 substr ⟨(𝑁 − 2), (♯‘𝑊)⟩))
26	25	oveq2d 7373	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 = (♯‘𝑊) → ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩)) = ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), (♯‘𝑊)⟩)))
27	26	eqcoms 2744	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑊) = 𝑁 → ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩)) = ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), (♯‘𝑊)⟩)))
28	27	ad2antlr 725	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3))) → ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩)) = ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), (♯‘𝑊)⟩)))
29		simpl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) → 𝑊 ∈ Word (Vtx‘𝐺))
30		fz1ssfz0 13537	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑁) ⊆ (0...𝑁)
31		ige3m2fz 13465	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑁 − 2) ∈ (1...𝑁))
32	30, 31	sselid 3942	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑁 − 2) ∈ (0...𝑁))
33	32	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (𝑁 − 2) ∈ (0...𝑁))
34	33	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3))) → (𝑁 − 2) ∈ (0...𝑁))
35		oveq2 7365	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑊) = 𝑁 → (0...(♯‘𝑊)) = (0...𝑁))
36	35	eleq2d 2823	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑊) = 𝑁 → ((𝑁 − 2) ∈ (0...(♯‘𝑊)) ↔ (𝑁 − 2) ∈ (0...𝑁)))
37	36	ad2antlr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3))) → ((𝑁 − 2) ∈ (0...(♯‘𝑊)) ↔ (𝑁 − 2) ∈ (0...𝑁)))
38	34, 37	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3))) → (𝑁 − 2) ∈ (0...(♯‘𝑊)))
39		pfxcctswrd 14598	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 − 2) ∈ (0...(♯‘𝑊))) → ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), (♯‘𝑊)⟩)) = 𝑊)
40	29, 38, 39	syl2an2r 683	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3))) → ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), (♯‘𝑊)⟩)) = 𝑊)
41	28, 40	eqtrd 2776	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = 𝑁) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3))) → ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩)) = 𝑊)
42	23, 41	sylan 580	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3))) → ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩)) = 𝑊)
43	42	ex 413	. . . . . . . . . . 11 ⊢ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩)) = 𝑊))
44	43	adantr 481	. . . . . . . . . 10 ⊢ ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩)) = 𝑊))
45	14, 44	sylbi 216	. . . . . . . . 9 ⊢ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩)) = 𝑊))
46	45	adantr 481	. . . . . . . 8 ⊢ ((𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩)) = 𝑊))
47	46	impcom 408	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)) → ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩)) = 𝑊)
48	47	eqcomd 2742	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)) → 𝑊 = ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩)))
49	10, 21, 48	3jca 1128	. . . . 5 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)) → ((𝑊 prefix (𝑁 − 2)) ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∧ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩) ∈ (𝑋(ClWWalksNOn‘𝐺)2) ∧ 𝑊 = ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩))))
50	49	ex 413	. . . 4 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋) → ((𝑊 prefix (𝑁 − 2)) ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∧ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩) ∈ (𝑋(ClWWalksNOn‘𝐺)2) ∧ 𝑊 = ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩)))))
51	4, 50	sylbid 239	. . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (𝑊 ∈ (𝑋𝐶𝑁) → ((𝑊 prefix (𝑁 − 2)) ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∧ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩) ∈ (𝑋(ClWWalksNOn‘𝐺)2) ∧ 𝑊 = ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩)))))
52		rspceov 7404	. . 3 ⊢ (((𝑊 prefix (𝑁 − 2)) ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∧ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩) ∈ (𝑋(ClWWalksNOn‘𝐺)2) ∧ 𝑊 = ((𝑊 prefix (𝑁 − 2)) ++ (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩))) → ∃𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))∃𝑏 ∈ (𝑋(ClWWalksNOn‘𝐺)2)𝑊 = (𝑎 ++ 𝑏))
53	51, 52	syl6 35	. 2 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (𝑊 ∈ (𝑋𝐶𝑁) → ∃𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))∃𝑏 ∈ (𝑋(ClWWalksNOn‘𝐺)2)𝑊 = (𝑎 ++ 𝑏)))
54		eluzelcn 12775	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 𝑁 ∈ ℂ)
55		2cnd 12231	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘3) → 2 ∈ ℂ)
56	54, 55	npcand 11516	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘3) → ((𝑁 − 2) + 2) = 𝑁)
57	56	adantl 482	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑁 − 2) + 2) = 𝑁)
58	57	oveq2d 7373	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (𝑋(ClWWalksNOn‘𝐺)((𝑁 − 2) + 2)) = (𝑋(ClWWalksNOn‘𝐺)𝑁))
59	58	eleq2d 2823	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑎 ++ 𝑏) ∈ (𝑋(ClWWalksNOn‘𝐺)((𝑁 − 2) + 2)) ↔ (𝑎 ++ 𝑏) ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁)))
60	59	biimpd 228	. . . . . 6 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑎 ++ 𝑏) ∈ (𝑋(ClWWalksNOn‘𝐺)((𝑁 − 2) + 2)) → (𝑎 ++ 𝑏) ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁)))
61		clwwlknonccat 29040	. . . . . 6 ⊢ ((𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∧ 𝑏 ∈ (𝑋(ClWWalksNOn‘𝐺)2)) → (𝑎 ++ 𝑏) ∈ (𝑋(ClWWalksNOn‘𝐺)((𝑁 − 2) + 2)))
62	60, 61	impel 506	. . . . 5 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∧ 𝑏 ∈ (𝑋(ClWWalksNOn‘𝐺)2))) → (𝑎 ++ 𝑏) ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁))
63		isclwwlknon 29035	. . . . . . . 8 ⊢ (𝑏 ∈ (𝑋(ClWWalksNOn‘𝐺)2) ↔ (𝑏 ∈ (2 ClWWalksN 𝐺) ∧ (𝑏‘0) = 𝑋))
64		clwwlkn2 28988	. . . . . . . . . 10 ⊢ (𝑏 ∈ (2 ClWWalksN 𝐺) ↔ ((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺) ∧ {(𝑏‘0), (𝑏‘1)} ∈ (Edg‘𝐺)))
65		isclwwlknon 29035	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ↔ (𝑎 ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋))
66	22	clwwlknbp 28979	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ((𝑁 − 2) ClWWalksN 𝐺) → (𝑎 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑎) = (𝑁 − 2)))
67		simpl 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺))) → 𝑎 ∈ Word (Vtx‘𝐺))
68		simprr 771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺))) → 𝑏 ∈ Word (Vtx‘𝐺))
69		2nn 12226	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2 ∈ ℕ
70		lbfzo0 13612	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 ∈ (0..^2) ↔ 2 ∈ ℕ)
71	69, 70	mpbir 230	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 0 ∈ (0..^2)
72		oveq2 7365	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘𝑏) = 2 → (0..^(♯‘𝑏)) = (0..^2))
73	71, 72	eleqtrrid 2845	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘𝑏) = 2 → 0 ∈ (0..^(♯‘𝑏)))
74	73	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺))) → 0 ∈ (0..^(♯‘𝑏)))
75	67, 68, 74	3jca 1128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺))) → (𝑎 ∈ Word (Vtx‘𝐺) ∧ 𝑏 ∈ Word (Vtx‘𝐺) ∧ 0 ∈ (0..^(♯‘𝑏))))
76	75	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺))) ∧ ((𝑏‘0) = 𝑋 ∧ (♯‘𝑎) = (𝑁 − 2))) → (𝑎 ∈ Word (Vtx‘𝐺) ∧ 𝑏 ∈ Word (Vtx‘𝐺) ∧ 0 ∈ (0..^(♯‘𝑏))))
77	76	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺))) ∧ ((𝑏‘0) = 𝑋 ∧ (♯‘𝑎) = (𝑁 − 2))) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3))) → (𝑎 ∈ Word (Vtx‘𝐺) ∧ 𝑏 ∈ Word (Vtx‘𝐺) ∧ 0 ∈ (0..^(♯‘𝑏))))
78		ccatval3 14467	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ Word (Vtx‘𝐺) ∧ 𝑏 ∈ Word (Vtx‘𝐺) ∧ 0 ∈ (0..^(♯‘𝑏))) → ((𝑎 ++ 𝑏)‘(0 + (♯‘𝑎))) = (𝑏‘0))
79	77, 78	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺))) ∧ ((𝑏‘0) = 𝑋 ∧ (♯‘𝑎) = (𝑁 − 2))) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3))) → ((𝑎 ++ 𝑏)‘(0 + (♯‘𝑎))) = (𝑏‘0))
80		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑏‘0) = 𝑋 ∧ (♯‘𝑎) = (𝑁 − 2)) → (♯‘𝑎) = (𝑁 − 2))
81	80	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑏‘0) = 𝑋 ∧ (♯‘𝑎) = (𝑁 − 2)) → (0 + (♯‘𝑎)) = (0 + (𝑁 − 2)))
82	81	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑎 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺))) ∧ ((𝑏‘0) = 𝑋 ∧ (♯‘𝑎) = (𝑁 − 2))) → (0 + (♯‘𝑎)) = (0 + (𝑁 − 2)))
83	54, 55	subcld 11512	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (𝑁 − 2) ∈ ℂ)
84	83	addid2d 11356	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ (ℤ_≥‘3) → (0 + (𝑁 − 2)) = (𝑁 − 2))
85	84	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (0 + (𝑁 − 2)) = (𝑁 − 2))
86	82, 85	sylan9eq 2796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑎 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺))) ∧ ((𝑏‘0) = 𝑋 ∧ (♯‘𝑎) = (𝑁 − 2))) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3))) → (0 + (♯‘𝑎)) = (𝑁 − 2))
87	86	eqcomd 2742	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺))) ∧ ((𝑏‘0) = 𝑋 ∧ (♯‘𝑎) = (𝑁 − 2))) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3))) → (𝑁 − 2) = (0 + (♯‘𝑎)))
88	87	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺))) ∧ ((𝑏‘0) = 𝑋 ∧ (♯‘𝑎) = (𝑁 − 2))) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3))) → ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = ((𝑎 ++ 𝑏)‘(0 + (♯‘𝑎))))
89		simpl 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑏‘0) = 𝑋 ∧ (♯‘𝑎) = (𝑁 − 2)) → (𝑏‘0) = 𝑋)
90	89	eqcomd 2742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑏‘0) = 𝑋 ∧ (♯‘𝑎) = (𝑁 − 2)) → 𝑋 = (𝑏‘0))
91	90	ad2antlr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺))) ∧ ((𝑏‘0) = 𝑋 ∧ (♯‘𝑎) = (𝑁 − 2))) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3))) → 𝑋 = (𝑏‘0))
92	79, 88, 91	3eqtr4d 2786	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑎 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺))) ∧ ((𝑏‘0) = 𝑋 ∧ (♯‘𝑎) = (𝑁 − 2))) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3))) → ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋)
93	92	exp53 448	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ Word (Vtx‘𝐺) → (((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺)) → ((𝑏‘0) = 𝑋 → ((♯‘𝑎) = (𝑁 − 2) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋)))))
94	93	com24 95	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ Word (Vtx‘𝐺) → ((♯‘𝑎) = (𝑁 − 2) → ((𝑏‘0) = 𝑋 → (((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋)))))
95	94	imp 407	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑎) = (𝑁 − 2)) → ((𝑏‘0) = 𝑋 → (((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋))))
96	66, 95	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ((𝑁 − 2) ClWWalksN 𝐺) → ((𝑏‘0) = 𝑋 → (((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋))))
97	96	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ((𝑁 − 2) ClWWalksN 𝐺) ∧ (𝑎‘0) = 𝑋) → ((𝑏‘0) = 𝑋 → (((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋))))
98	65, 97	sylbi 216	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) → ((𝑏‘0) = 𝑋 → (((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋))))
99	98	com13 88	. . . . . . . . . . 11 ⊢ (((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺)) → ((𝑏‘0) = 𝑋 → (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋))))
100	99	3adant3 1132	. . . . . . . . . 10 ⊢ (((♯‘𝑏) = 2 ∧ 𝑏 ∈ Word (Vtx‘𝐺) ∧ {(𝑏‘0), (𝑏‘1)} ∈ (Edg‘𝐺)) → ((𝑏‘0) = 𝑋 → (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋))))
101	64, 100	sylbi 216	. . . . . . . . 9 ⊢ (𝑏 ∈ (2 ClWWalksN 𝐺) → ((𝑏‘0) = 𝑋 → (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋))))
102	101	imp 407	. . . . . . . 8 ⊢ ((𝑏 ∈ (2 ClWWalksN 𝐺) ∧ (𝑏‘0) = 𝑋) → (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋)))
103	63, 102	sylbi 216	. . . . . . 7 ⊢ (𝑏 ∈ (𝑋(ClWWalksNOn‘𝐺)2) → (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋)))
104	103	impcom 408	. . . . . 6 ⊢ ((𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∧ 𝑏 ∈ (𝑋(ClWWalksNOn‘𝐺)2)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋))
105	104	impcom 408	. . . . 5 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∧ 𝑏 ∈ (𝑋(ClWWalksNOn‘𝐺)2))) → ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋)
106	2	2clwwlkel 29293	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘2)) → ((𝑎 ++ 𝑏) ∈ (𝑋𝐶𝑁) ↔ ((𝑎 ++ 𝑏) ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋)))
107	1, 106	sylan2 593	. . . . . 6 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → ((𝑎 ++ 𝑏) ∈ (𝑋𝐶𝑁) ↔ ((𝑎 ++ 𝑏) ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋)))
108	107	adantr 481	. . . . 5 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∧ 𝑏 ∈ (𝑋(ClWWalksNOn‘𝐺)2))) → ((𝑎 ++ 𝑏) ∈ (𝑋𝐶𝑁) ↔ ((𝑎 ++ 𝑏) ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ ((𝑎 ++ 𝑏)‘(𝑁 − 2)) = 𝑋)))
109	62, 105, 108	mpbir2and 711	. . . 4 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∧ 𝑏 ∈ (𝑋(ClWWalksNOn‘𝐺)2))) → (𝑎 ++ 𝑏) ∈ (𝑋𝐶𝑁))
110		eleq1 2825	. . . 4 ⊢ (𝑊 = (𝑎 ++ 𝑏) → (𝑊 ∈ (𝑋𝐶𝑁) ↔ (𝑎 ++ 𝑏) ∈ (𝑋𝐶𝑁)))
111	109, 110	syl5ibrcom 246	. . 3 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) ∧ (𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∧ 𝑏 ∈ (𝑋(ClWWalksNOn‘𝐺)2))) → (𝑊 = (𝑎 ++ 𝑏) → 𝑊 ∈ (𝑋𝐶𝑁)))
112	111	rexlimdvva 3205	. 2 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (∃𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))∃𝑏 ∈ (𝑋(ClWWalksNOn‘𝐺)2)𝑊 = (𝑎 ++ 𝑏) → 𝑊 ∈ (𝑋𝐶𝑁)))
113	53, 112	impbid 211	1 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ_≥‘3)) → (𝑊 ∈ (𝑋𝐶𝑁) ↔ ∃𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))∃𝑏 ∈ (𝑋(ClWWalksNOn‘𝐺)2)𝑊 = (𝑎 ++ 𝑏)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∃wrex 3073 {crab 3407 {cpr 4588 ⟨cop 4592 ‘cfv 6496 (class class class)co 7357 ∈ cmpo 7359 0cc0 11051 1c1 11052 + caddc 11054 − cmin 11385 ℕcn 12153 2c2 12208 3c3 12209 ℤ_≥cuz 12763 ...cfz 13424 ..^cfzo 13567 ♯chash 14230 Word cword 14402 ++ cconcat 14458 substr csubstr 14528 prefix cpfx 14558 Vtxcvtx 27947 Edgcedg 27998 ClWWalksN cclwwlkn 28968 ClWWalksNOncclwwlknon 29031

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-oadd 8416 df-er 8648 df-map 8767 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-nn 12154 df-2 12216 df-3 12217 df-n0 12414 df-xnn0 12486 df-z 12500 df-uz 12764 df-rp 12916 df-fz 13425 df-fzo 13568 df-hash 14231 df-word 14403 df-lsw 14451 df-concat 14459 df-s1 14484 df-substr 14529 df-pfx 14559 df-s2 14737 df-wwlks 28775 df-wwlksn 28776 df-clwwlk 28926 df-clwwlkn 28969 df-clwwlknon 29032

This theorem is referenced by: (None)

W3C validator