Theorem numclwwlk3lem 25829

Description: Lemma for numclwwlk3 25830. (Contributed by Alexander van der Vekens, 6-Oct-2018.)

Hypotheses

Ref	Expression
numclwwlk.c	|- C = ( n e. NN0 |-> ( ( V ClWWalksN E ) ` n ) )
numclwwlk.f	|- F = ( v e. V , n e. NN0 |-> { w e. ( C ` n ) | ( w ` 0 ) = v } )
numclwwlk.g	|- G = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( C ` n ) | ( ( w ` 0 ) = v /\ ( w ` ( n - 2 ) ) = ( w ` 0 ) ) } )
numclwwlk.q	|- Q = ( v e. V , n e. NN0 |-> { w e. ( ( V WWalksN E ) ` n ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
numclwwlk.h	|- H = ( v e. V , n e. NN0 |-> { w e. ( C ` n ) | ( ( w ` 0 ) = v /\ ( w ` ( n - 2 ) ) =/= ( w ` 0 ) ) } )

Assertion

Ref	Expression
numclwwlk3lem	|- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( # ` ( X F N ) ) = ( ( # ` ( X H N ) ) + ( # ` ( X G N ) ) ) )

Distinct variable groups:   n, E   n, N   n, V   w, C   w, N   C, n, v, w   v, N   n, X, v, w   v, V   w, E   w, V   w, F   w, Q   w, G   v, E   v, H, w

Allowed substitution hints:   Q( v, n)   F( v, n)   G( v, n)   H( n)

Proof of Theorem numclwwlk3lem

Step	Hyp	Ref	Expression
1		simp3 1009	. . . . 5 |- ( ( V USGrph E /\ V e. Fin /\ X e. V ) -> X e. V )
2		eluzge2nn0 11195	. . . . 5 |- ( N e. ( ZZ>= ` 2 ) -> N e. NN0 )
3		numclwwlk.c	. . . . . 6 |- C = ( n e. NN0 |-> ( ( V ClWWalksN E ) ` n ) )
4		numclwwlk.f	. . . . . 6 |- F = ( v e. V , n e. NN0 |-> { w e. ( C ` n ) | ( w ` 0 ) = v } )
5	3, 4	numclwwlkovf 25802	. . . . 5 |- ( ( X e. V /\ N e. NN0 ) -> ( X F N ) = { w e. ( C ` N ) | ( w ` 0 ) = X } )
6	1, 2, 5	syl2an 480	. . . 4 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( X F N ) = { w e. ( C ` N ) | ( w ` 0 ) = X } )
7	6	fveq2d 5867	. . 3 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( # ` ( X F N ) ) = ( # ` { w e. ( C ` N ) | ( w ` 0 ) = X } ) )
8		pm4.42 970	. . . . . . . 8 |- ( ( w ` 0 ) = X <-> ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) \/ ( ( w ` 0 ) = X /\ -. ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) ) )
9		nne 2627	. . . . . . . . . 10 |- ( -. ( w ` ( N - 2 ) ) =/= ( w ` 0 ) <-> ( w ` ( N - 2 ) ) = ( w ` 0 ) )
10	9	anbi2i 699	. . . . . . . . 9 |- ( ( ( w ` 0 ) = X /\ -. ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) <-> ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) )
11	10	orbi2i 522	. . . . . . . 8 |- ( ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) \/ ( ( w ` 0 ) = X /\ -. ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) ) <-> ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) \/ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) ) )
12	8, 11	bitri 253	. . . . . . 7 |- ( ( w ` 0 ) = X <-> ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) \/ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) ) )
13	12	a1i 11	. . . . . 6 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( ( w ` 0 ) = X <-> ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) \/ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) ) ) )
14	13	rabbidv 3035	. . . . 5 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> { w e. ( C ` N ) | ( w ` 0 ) = X } = { w e. ( C ` N ) | ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) \/ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) ) } )
15		unrab 3713	. . . . 5 |- ( { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } u. { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } ) = { w e. ( C ` N ) | ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) \/ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) ) }
16	14, 15	syl6eqr 2502	. . . 4 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> { w e. ( C ` N ) | ( w ` 0 ) = X } = ( { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } u. { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } ) )
17	16	fveq2d 5867	. . 3 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( # ` { w e. ( C ` N ) | ( w ` 0 ) = X } ) = ( # ` ( { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } u. { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } ) ) )
18	3	numclwwlkfvc 25798	. . . . . . . 8 |- ( N e. NN0 -> ( C ` N ) = ( ( V ClWWalksN E ) ` N ) )
19	2, 18	syl 17	. . . . . . 7 |- ( N e. ( ZZ>= ` 2 ) -> ( C ` N ) = ( ( V ClWWalksN E ) ` N ) )
20	19	adantl 468	. . . . . 6 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( C ` N ) = ( ( V ClWWalksN E ) ` N ) )
21		simpl2 1011	. . . . . . 7 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> V e. Fin )
22		usgrav 25058	. . . . . . . . . 10 |- ( V USGrph E -> ( V e. _V /\ E e. _V ) )
23	22	simprd 465	. . . . . . . . 9 |- ( V USGrph E -> E e. _V )
24	23	3ad2ant1 1028	. . . . . . . 8 |- ( ( V USGrph E /\ V e. Fin /\ X e. V ) -> E e. _V )
25	24	adantr 467	. . . . . . 7 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> E e. _V )
26	2	adantl 468	. . . . . . 7 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> N e. NN0 )
27		clwwlknfi 25499	. . . . . . 7 |- ( ( V e. Fin /\ E e. _V /\ N e. NN0 ) -> ( ( V ClWWalksN E ) ` N ) e. Fin )
28	21, 25, 26, 27	syl3anc 1267	. . . . . 6 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( ( V ClWWalksN E ) ` N ) e. Fin )
29	20, 28	eqeltrd 2528	. . . . 5 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( C ` N ) e. Fin )
30		rabfi 7793	. . . . 5 |- ( ( C ` N ) e. Fin -> { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } e. Fin )
31	29, 30	syl 17	. . . 4 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } e. Fin )
32		rabfi 7793	. . . . 5 |- ( ( C ` N ) e. Fin -> { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } e. Fin )
33	29, 32	syl 17	. . . 4 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } e. Fin )
34		inrab 3714	. . . . 5 |- ( { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } i^i { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } ) = { w e. ( C ` N ) | ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) ) }
35		df-ne 2623	. . . . . . . . . . . . 13 |- ( ( w ` ( N - 2 ) ) =/= ( w ` 0 ) <-> -. ( w ` ( N - 2 ) ) = ( w ` 0 ) )
36	35	biimpi 198	. . . . . . . . . . . 12 |- ( ( w ` ( N - 2 ) ) =/= ( w ` 0 ) -> -. ( w ` ( N - 2 ) ) = ( w ` 0 ) )
37	36	adantl 468	. . . . . . . . . . 11 |- ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) -> -. ( w ` ( N - 2 ) ) = ( w ` 0 ) )
38	37	intnand 926	. . . . . . . . . 10 |- ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) -> -. ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) )
39	38	imori 415	. . . . . . . . 9 |- ( -. ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) \/ -. ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) )
40		ianor 491	. . . . . . . . 9 |- ( -. ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) ) <-> ( -. ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) \/ -. ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) ) )
41	39, 40	mpbir 213	. . . . . . . 8 |- -. ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) )
42	41	a1i 11	. . . . . . 7 |- ( ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) /\ w e. ( C ` N ) ) -> -. ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) ) )
43	42	ralrimiva 2801	. . . . . 6 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> A. w e. ( C ` N ) -. ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) ) )
44		rabeq0 3753	. . . . . 6 |- ( { w e. ( C ` N ) | ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) ) } = (/) <-> A. w e. ( C ` N ) -. ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) ) )
45	43, 44	sylibr 216	. . . . 5 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> { w e. ( C ` N ) | ( ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) /\ ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) ) } = (/) )
46	34, 45	syl5eq 2496	. . . 4 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } i^i { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } ) = (/) )
47		hashun 12558	. . . 4 |- ( ( { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } e. Fin /\ { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } e. Fin /\ ( { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } i^i { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } ) = (/) ) -> ( # ` ( { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } u. { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } ) ) = ( ( # ` { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } ) + ( # ` { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } ) ) )
48	31, 33, 46, 47	syl3anc 1267	. . 3 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( # ` ( { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } u. { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } ) ) = ( ( # ` { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } ) + ( # ` { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } ) ) )
49	7, 17, 48	3eqtrd 2488	. 2 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( # ` ( X F N ) ) = ( ( # ` { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } ) + ( # ` { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } ) ) )
50		numclwwlk.g	. . . . . 6 |- G = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( C ` n ) | ( ( w ` 0 ) = v /\ ( w ` ( n - 2 ) ) = ( w ` 0 ) ) } )
51		numclwwlk.q	. . . . . 6 |- Q = ( v e. V , n e. NN0 |-> { w e. ( ( V WWalksN E ) ` n ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
52		numclwwlk.h	. . . . . 6 |- H = ( v e. V , n e. NN0 |-> { w e. ( C ` n ) | ( ( w ` 0 ) = v /\ ( w ` ( n - 2 ) ) =/= ( w ` 0 ) ) } )
53	3, 4, 50, 51, 52	numclwwlkovh 25822	. . . . 5 |- ( ( X e. V /\ N e. NN0 ) -> ( X H N ) = { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } )
54	1, 2, 53	syl2an 480	. . . 4 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( X H N ) = { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } )
55	54	fveq2d 5867	. . 3 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( # ` ( X H N ) ) = ( # ` { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } ) )
56	3, 4, 50	numclwwlkovg 25808	. . . . 5 |- ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( X G N ) = { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } )
57	1, 56	sylan 474	. . . 4 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( X G N ) = { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } )
58	57	fveq2d 5867	. . 3 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( # ` ( X G N ) ) = ( # ` { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } ) )
59	55, 58	oveq12d 6306	. 2 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( ( # ` ( X H N ) ) + ( # ` ( X G N ) ) ) = ( ( # ` { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) =/= ( w ` 0 ) ) } ) + ( # ` { w e. ( C ` N ) | ( ( w ` 0 ) = X /\ ( w ` ( N - 2 ) ) = ( w ` 0 ) ) } ) ) )
60	49, 59	eqtr4d 2487	1 |- ( ( ( V USGrph E /\ V e. Fin /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( # ` ( X F N ) ) = ( ( # ` ( X H N ) ) + ( # ` ( X G N ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   /\ w3a 984   = wceq 1443   e. wcel 1886   =/= wne 2621   A.wral 2736   {crab 2740   _Vcvv 3044   u. cun 3401   i^i cin 3402   (/)c0 3730   class class class wbr 4401   |-> cmpt 4460   ` cfv 5581  (class class class)co 6288   |-> cmpt2 6290   Fincfn 7566   0cc0 9536   + caddc 9539   - cmin 9857   2c2 10656   NN0cn0 10866   ZZ>=cuz 11156   #chash 12512   lastS clsw 12654   USGrph cusg 25050   WWalksN cwwlkn 25399   ClWWalksN cclwwlkn 25470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-2o 7180  df-oadd 7183  df-er 7360  df-map 7471  df-pm 7472  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570  df-card 8370  df-cda 8595  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-nn 10607  df-2 10665  df-n0 10867  df-z 10935  df-uz 11157  df-fz 11782  df-fzo 11913  df-seq 12211  df-exp 12270  df-hash 12513  df-word 12661  df-usgra 25053  df-clwwlk 25472  df-clwwlkn 25473

This theorem is referenced by:  numclwwlk3  25830