Metamath Proof Explorer

Theorem numclwwlk7

Description: Statement 14 in Huneke p. 2: "The total number of closed walks of length p [in a friendship graph] is (k(k-1)+1)f(p)=1 (mod p)", since the number of vertices in a friendship graph is (k(k-1)+1), see frrusgrord0 or frrusgrord , and p divides (k-1), i.e. (k-1) mod p = 0 => k(k-1) mod p = 0 => k(k-1)+1 mod p = 1. Since the null graph is a friendship graph, see frgr0 , as well as k-regular (for any k), see 0vtxrgr , but has no closed walk, see 0clwlk0 , this theorem would be false for a null graph: ( ( #( P ClWWalksN G ) ) mod P ) = 0 =/= 1 , so this case must be excluded (by assuming V =/= (/) ). (Contributed by Alexander van der Vekens, 1-Sep-2018) (Revised by AV, 3-Jun-2021)

Ref Expression
Hypothesis numclwwlk6.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion numclwwlk7 ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) mod 𝑃 ) = 1 )

Proof

Step Hyp Ref Expression
1 numclwwlk6.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 simpll ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → 𝐺 RegUSGraph 𝐾 )
3 simplr ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → 𝐺 ∈ FriendGraph )
4 simprr ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → 𝑉 ∈ Fin )
5 2 3 4 3jca ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) )
6 1 numclwwlk6 ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) mod 𝑃 ) = ( ( ♯ ‘ 𝑉 ) mod 𝑃 ) )
7 5 6 stoic3 ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) mod 𝑃 ) = ( ( ♯ ‘ 𝑉 ) mod 𝑃 ) )
8 simp2 ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) )
9 8 ancomd ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) )
10 simp1 ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) )
11 10 ancomd ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) )
12 1 frrusgrord ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) )
13 9 11 12 sylc ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) )
14 13 oveq1d ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ 𝑉 ) mod 𝑃 ) = ( ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) mod 𝑃 ) )
15 1 numclwwlk7lem ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → 𝐾 ∈ ℕ0 )
16 nn0cn ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℂ )
17 peano2cnm ⊢ ( 𝐾 ∈ ℂ → ( 𝐾 − 1 ) ∈ ℂ )
18 16 17 syl ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 − 1 ) ∈ ℂ )
19 16 18 mulcomd ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 · ( 𝐾 − 1 ) ) = ( ( 𝐾 − 1 ) · 𝐾 ) )
20 19 oveq1d ⊢ ( 𝐾 ∈ ℕ0 → ( ( 𝐾 · ( 𝐾 − 1 ) ) mod 𝑃 ) = ( ( ( 𝐾 − 1 ) · 𝐾 ) mod 𝑃 ) )
21 20 adantr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( 𝐾 · ( 𝐾 − 1 ) ) mod 𝑃 ) = ( ( ( 𝐾 − 1 ) · 𝐾 ) mod 𝑃 ) )
22 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
23 22 ad2antrl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → 𝑃 ∈ ℕ )
24 nn0z ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℤ )
25 peano2zm ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 − 1 ) ∈ ℤ )
26 24 25 syl ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 − 1 ) ∈ ℤ )
27 26 adantr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝐾 − 1 ) ∈ ℤ )
28 24 adantr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → 𝐾 ∈ ℤ )
29 23 27 28 3jca ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝑃 ∈ ℕ ∧ ( 𝐾 − 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) )
30 simprr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → 𝑃 ∥ ( 𝐾 − 1 ) )
31 mulmoddvds ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝐾 − 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑃 ∥ ( 𝐾 − 1 ) → ( ( ( 𝐾 − 1 ) · 𝐾 ) mod 𝑃 ) = 0 ) )
32 29 30 31 sylc ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ( 𝐾 − 1 ) · 𝐾 ) mod 𝑃 ) = 0 )
33 21 32 eqtrd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( 𝐾 · ( 𝐾 − 1 ) ) mod 𝑃 ) = 0 )
34 22 nnred ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ )
35 prmgt1 ⊢ ( 𝑃 ∈ ℙ → 1 < 𝑃 )
36 34 35 jca ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) )
37 36 ad2antrl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) )
38 1mod ⊢ ( ( 𝑃 ∈ ℝ ∧ 1 < 𝑃 ) → ( 1 mod 𝑃 ) = 1 )
39 37 38 syl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 1 mod 𝑃 ) = 1 )
40 33 39 oveq12d ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ( 𝐾 · ( 𝐾 − 1 ) ) mod 𝑃 ) + ( 1 mod 𝑃 ) ) = ( 0 + 1 ) )
41 40 oveq1d ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ( ( 𝐾 · ( 𝐾 − 1 ) ) mod 𝑃 ) + ( 1 mod 𝑃 ) ) mod 𝑃 ) = ( ( 0 + 1 ) mod 𝑃 ) )
42 nn0re ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
43 peano2rem ⊢ ( 𝐾 ∈ ℝ → ( 𝐾 − 1 ) ∈ ℝ )
44 42 43 syl ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 − 1 ) ∈ ℝ )
45 42 44 remulcld ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℝ )
46 45 adantr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℝ )
47 1red ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → 1 ∈ ℝ )
48 22 nnrpd ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ+ )
49 48 ad2antrl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → 𝑃 ∈ ℝ+ )
50 modaddabs ⊢ ( ( ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ( ( 𝐾 · ( 𝐾 − 1 ) ) mod 𝑃 ) + ( 1 mod 𝑃 ) ) mod 𝑃 ) = ( ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) mod 𝑃 ) )
51 46 47 49 50 syl3anc ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ( ( 𝐾 · ( 𝐾 − 1 ) ) mod 𝑃 ) + ( 1 mod 𝑃 ) ) mod 𝑃 ) = ( ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) mod 𝑃 ) )
52 0p1e1 ⊢ ( 0 + 1 ) = 1
53 52 oveq1i ⊢ ( ( 0 + 1 ) mod 𝑃 ) = ( 1 mod 𝑃 )
54 34 35 38 syl2anc ⊢ ( 𝑃 ∈ ℙ → ( 1 mod 𝑃 ) = 1 )
55 54 ad2antrl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( 1 mod 𝑃 ) = 1 )
56 53 55 syl5eq ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( 0 + 1 ) mod 𝑃 ) = 1 )
57 41 51 56 3eqtr3d ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) mod 𝑃 ) = 1 )
58 15 57 stoic3 ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) mod 𝑃 ) = 1 )
59 7 14 58 3eqtrd ⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ∧ ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ ( 𝐾 − 1 ) ) ) → ( ( ♯ ‘ ( 𝑃 ClWWalksN 𝐺 ) ) mod 𝑃 ) = 1 )