Metamath Proof Explorer

Theorem numclwwlk5lem

Description: Lemma for numclwwlk5 . (Contributed by Alexander van der Vekens, 7-Oct-2018) (Revised by AV, 2-Jun-2021) (Revised by AV, 7-Mar-2022)

Ref Expression
Hypothesis numclwwlk3.v 
|- V = ( Vtx ` G )
Assertion numclwwlk5lem 
|- ( ( G RegUSGraph K /\ X e. V /\ K e. NN0 ) -> ( 2 || ( K - 1 ) -> ( ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) mod 2 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 numclwwlk3.v 
 |-  V = ( Vtx ` G )
2 1 eleq2i 
 |-  ( X e. V <-> X e. ( Vtx ` G ) )
3 clwwlknon2num 
 |-  ( ( G RegUSGraph K /\ X e. ( Vtx ` G ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) = K )
4 2 3 sylan2b 
 |-  ( ( G RegUSGraph K /\ X e. V ) -> ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) = K )
5 4 3adant3 
 |-  ( ( G RegUSGraph K /\ X e. V /\ K e. NN0 ) -> ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) = K )
6 oveq1 
 |-  ( ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) = K -> ( ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) mod 2 ) = ( K mod 2 ) )
7 6 ad2antrr 
 |-  ( ( ( ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) = K /\ ( G RegUSGraph K /\ X e. V /\ K e. NN0 ) ) /\ 2 || ( K - 1 ) ) -> ( ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) mod 2 ) = ( K mod 2 ) )
8 2prm 
 |-  2 e. Prime
9 nn0z 
 |-  ( K e. NN0 -> K e. ZZ )
10 modprm1div 
 |-  ( ( 2 e. Prime /\ K e. ZZ ) -> ( ( K mod 2 ) = 1 <-> 2 || ( K - 1 ) ) )
11 8 9 10 sylancr 
 |-  ( K e. NN0 -> ( ( K mod 2 ) = 1 <-> 2 || ( K - 1 ) ) )
12 11 biimprd 
 |-  ( K e. NN0 -> ( 2 || ( K - 1 ) -> ( K mod 2 ) = 1 ) )
13 12 3ad2ant3 
 |-  ( ( G RegUSGraph K /\ X e. V /\ K e. NN0 ) -> ( 2 || ( K - 1 ) -> ( K mod 2 ) = 1 ) )
14 13 adantl 
 |-  ( ( ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) = K /\ ( G RegUSGraph K /\ X e. V /\ K e. NN0 ) ) -> ( 2 || ( K - 1 ) -> ( K mod 2 ) = 1 ) )
15 14 imp 
 |-  ( ( ( ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) = K /\ ( G RegUSGraph K /\ X e. V /\ K e. NN0 ) ) /\ 2 || ( K - 1 ) ) -> ( K mod 2 ) = 1 )
16 7 15 eqtrd 
 |-  ( ( ( ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) = K /\ ( G RegUSGraph K /\ X e. V /\ K e. NN0 ) ) /\ 2 || ( K - 1 ) ) -> ( ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) mod 2 ) = 1 )
17 16 ex 
 |-  ( ( ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) = K /\ ( G RegUSGraph K /\ X e. V /\ K e. NN0 ) ) -> ( 2 || ( K - 1 ) -> ( ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) mod 2 ) = 1 ) )
18 5 17 mpancom 
 |-  ( ( G RegUSGraph K /\ X e. V /\ K e. NN0 ) -> ( 2 || ( K - 1 ) -> ( ( # ` ( X ( ClWWalksNOn ` G ) 2 ) ) mod 2 ) = 1 ) )