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

Theorem numclwwlk7 26407
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 frgregordn0 26363 or frrusgraord 26364, 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 empty graph is a friendship graph, see frgra0 26287, as well as k-regular (for any k), see 0vgrargra 26230, but has no closed walk, see clwlk0 26056, this theorem would be false: ((#‘(𝐶𝑃)) mod 𝑃) = 0 ≠ 1, so this case must be excluded. ( (Contributed by Alexander van der Vekens, 1-Sep-2018.)
Assertion
Ref Expression
numclwwlk7 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘((𝑉 ClWWalksN 𝐸)‘𝑃)) mod 𝑃) = 1)

Proof of Theorem numclwwlk7
Dummy variables 𝑚 𝑛 𝑝 𝑞 𝑣 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prmnn 15172 . . . . . . . . 9 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
21nnnn0d 11198 . . . . . . . 8 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ0)
32adantr 479 . . . . . . 7 ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → 𝑃 ∈ ℕ0)
433ad2ant3 1076 . . . . . 6 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑃 ∈ ℕ0)
5 eqid 2609 . . . . . . 7 (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))
65numclwwlkfvc 26370 . . . . . 6 (𝑃 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑃) = ((𝑉 ClWWalksN 𝐸)‘𝑃))
74, 6syl 17 . . . . 5 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑃) = ((𝑉 ClWWalksN 𝐸)‘𝑃))
87eqcomd 2615 . . . 4 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((𝑉 ClWWalksN 𝐸)‘𝑃) = ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑃))
98fveq2d 6092 . . 3 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (#‘((𝑉 ClWWalksN 𝐸)‘𝑃)) = (#‘((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑃)))
109oveq1d 6542 . 2 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘((𝑉 ClWWalksN 𝐸)‘𝑃)) mod 𝑃) = ((#‘((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑃)) mod 𝑃))
11 simpr 475 . . . . 5 ((𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) → 𝑉 ∈ Fin)
1211anim2i 590 . . . 4 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) → ((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ 𝑉 ∈ Fin))
13 df-3an 1032 . . . 4 ((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸𝑉 ∈ Fin) ↔ ((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ 𝑉 ∈ Fin))
1412, 13sylibr 222 . . 3 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) → (⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸𝑉 ∈ Fin))
15 fveq2 6088 . . . . 5 (𝑛 = 𝑚 → ((𝑉 ClWWalksN 𝐸)‘𝑛) = ((𝑉 ClWWalksN 𝐸)‘𝑚))
1615cbvmptv 4672 . . . 4 (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) = (𝑚 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑚))
17 fveq1 6087 . . . . . . . 8 (𝑝 = 𝑞 → (𝑝‘0) = (𝑞‘0))
1817eqeq1d 2611 . . . . . . 7 (𝑝 = 𝑞 → ((𝑝‘0) = 𝑣 ↔ (𝑞‘0) = 𝑣))
1918cbvrabv 3171 . . . . . 6 {𝑝 ∈ ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑚) ∣ (𝑝‘0) = 𝑣} = {𝑞 ∈ ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑚) ∣ (𝑞‘0) = 𝑣}
2019a1i 11 . . . . 5 ((𝑣𝑉𝑚 ∈ ℕ0) → {𝑝 ∈ ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑚) ∣ (𝑝‘0) = 𝑣} = {𝑞 ∈ ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑚) ∣ (𝑞‘0) = 𝑣})
2120mpt2eq3ia 6596 . . . 4 (𝑣𝑉, 𝑚 ∈ ℕ0 ↦ {𝑝 ∈ ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑚) ∣ (𝑝‘0) = 𝑣}) = (𝑣𝑉, 𝑚 ∈ ℕ0 ↦ {𝑞 ∈ ((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑚) ∣ (𝑞‘0) = 𝑣})
2216, 21numclwwlk6 26406 . . 3 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑃)) mod 𝑃) = ((#‘𝑉) mod 𝑃))
2314, 22stoic3 1691 . 2 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘((𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛))‘𝑃)) mod 𝑃) = ((#‘𝑉) mod 𝑃))
24 simp2 1054 . . . . . 6 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin))
2524ancomd 465 . . . . 5 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅))
26 simp1 1053 . . . . . 6 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸))
2726ancomd 465 . . . . 5 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑉 FriendGrph 𝐸 ∧ ⟨𝑉, 𝐸⟩ RegUSGrph 𝐾))
28 frrusgraord 26364 . . . . 5 ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝑉 FriendGrph 𝐸 ∧ ⟨𝑉, 𝐸⟩ RegUSGrph 𝐾) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)))
2925, 27, 28sylc 62 . . . 4 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))
3029oveq1d 6542 . . 3 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘𝑉) mod 𝑃) = (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃))
31 rusgraprop 26222 . . . . . . 7 (⟨𝑉, 𝐸⟩ RegUSGrph 𝐾 → (𝑉 USGrph 𝐸𝐾 ∈ ℕ0 ∧ ∀𝑥𝑉 ((𝑉 VDeg 𝐸)‘𝑥) = 𝐾))
32 nn0cn 11149 . . . . . . . . . . . . . . . 16 (𝐾 ∈ ℕ0𝐾 ∈ ℂ)
33 peano2cnm 10198 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ ℂ → (𝐾 − 1) ∈ ℂ)
3432, 33syl 17 . . . . . . . . . . . . . . . 16 (𝐾 ∈ ℕ0 → (𝐾 − 1) ∈ ℂ)
3532, 34mulcomd 9917 . . . . . . . . . . . . . . 15 (𝐾 ∈ ℕ0 → (𝐾 · (𝐾 − 1)) = ((𝐾 − 1) · 𝐾))
3635oveq1d 6542 . . . . . . . . . . . . . 14 (𝐾 ∈ ℕ0 → ((𝐾 · (𝐾 − 1)) mod 𝑃) = (((𝐾 − 1) · 𝐾) mod 𝑃))
3736adantr 479 . . . . . . . . . . . . 13 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((𝐾 · (𝐾 − 1)) mod 𝑃) = (((𝐾 − 1) · 𝐾) mod 𝑃))
381ad2antrl 759 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑃 ∈ ℕ)
39 nn0z 11233 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ ℕ0𝐾 ∈ ℤ)
40 peano2zm 11253 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
4139, 40syl 17 . . . . . . . . . . . . . . . 16 (𝐾 ∈ ℕ0 → (𝐾 − 1) ∈ ℤ)
4241adantr 479 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝐾 − 1) ∈ ℤ)
4339adantr 479 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝐾 ∈ ℤ)
4438, 42, 433jca 1234 . . . . . . . . . . . . . 14 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑃 ∈ ℕ ∧ (𝐾 − 1) ∈ ℤ ∧ 𝐾 ∈ ℤ))
45 simprr 791 . . . . . . . . . . . . . 14 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑃 ∥ (𝐾 − 1))
46 mulmoddvds 14835 . . . . . . . . . . . . . 14 ((𝑃 ∈ ℕ ∧ (𝐾 − 1) ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑃 ∥ (𝐾 − 1) → (((𝐾 − 1) · 𝐾) mod 𝑃) = 0))
4744, 45, 46sylc 62 . . . . . . . . . . . . 13 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (((𝐾 − 1) · 𝐾) mod 𝑃) = 0)
4837, 47eqtrd 2643 . . . . . . . . . . . 12 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((𝐾 · (𝐾 − 1)) mod 𝑃) = 0)
491nnred 10882 . . . . . . . . . . . . . . 15 (𝑃 ∈ ℙ → 𝑃 ∈ ℝ)
50 prmgt1 15193 . . . . . . . . . . . . . . 15 (𝑃 ∈ ℙ → 1 < 𝑃)
5149, 50jca 552 . . . . . . . . . . . . . 14 (𝑃 ∈ ℙ → (𝑃 ∈ ℝ ∧ 1 < 𝑃))
5251ad2antrl 759 . . . . . . . . . . . . 13 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝑃 ∈ ℝ ∧ 1 < 𝑃))
53 1mod 12519 . . . . . . . . . . . . 13 ((𝑃 ∈ ℝ ∧ 1 < 𝑃) → (1 mod 𝑃) = 1)
5452, 53syl 17 . . . . . . . . . . . 12 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (1 mod 𝑃) = 1)
5548, 54oveq12d 6545 . . . . . . . . . . 11 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (((𝐾 · (𝐾 − 1)) mod 𝑃) + (1 mod 𝑃)) = (0 + 1))
5655oveq1d 6542 . . . . . . . . . 10 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((((𝐾 · (𝐾 − 1)) mod 𝑃) + (1 mod 𝑃)) mod 𝑃) = ((0 + 1) mod 𝑃))
57 nn0re 11148 . . . . . . . . . . . . 13 (𝐾 ∈ ℕ0𝐾 ∈ ℝ)
58 peano2rem 10199 . . . . . . . . . . . . . 14 (𝐾 ∈ ℝ → (𝐾 − 1) ∈ ℝ)
5957, 58syl 17 . . . . . . . . . . . . 13 (𝐾 ∈ ℕ0 → (𝐾 − 1) ∈ ℝ)
6057, 59remulcld 9926 . . . . . . . . . . . 12 (𝐾 ∈ ℕ0 → (𝐾 · (𝐾 − 1)) ∈ ℝ)
6160adantr 479 . . . . . . . . . . 11 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (𝐾 · (𝐾 − 1)) ∈ ℝ)
62 1red 9911 . . . . . . . . . . 11 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 1 ∈ ℝ)
631nnrpd 11702 . . . . . . . . . . . 12 (𝑃 ∈ ℙ → 𝑃 ∈ ℝ+)
6463ad2antrl 759 . . . . . . . . . . 11 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → 𝑃 ∈ ℝ+)
65 modaddabs 12525 . . . . . . . . . . 11 (((𝐾 · (𝐾 − 1)) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑃 ∈ ℝ+) → ((((𝐾 · (𝐾 − 1)) mod 𝑃) + (1 mod 𝑃)) mod 𝑃) = (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃))
6661, 62, 64, 65syl3anc 1317 . . . . . . . . . 10 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((((𝐾 · (𝐾 − 1)) mod 𝑃) + (1 mod 𝑃)) mod 𝑃) = (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃))
67 0p1e1 10979 . . . . . . . . . . . 12 (0 + 1) = 1
6867oveq1i 6537 . . . . . . . . . . 11 ((0 + 1) mod 𝑃) = (1 mod 𝑃)
6949, 50, 53syl2anc 690 . . . . . . . . . . . 12 (𝑃 ∈ ℙ → (1 mod 𝑃) = 1)
7069ad2antrl 759 . . . . . . . . . . 11 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (1 mod 𝑃) = 1)
7168, 70syl5eq 2655 . . . . . . . . . 10 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((0 + 1) mod 𝑃) = 1)
7256, 66, 713eqtr3d 2651 . . . . . . . . 9 ((𝐾 ∈ ℕ0 ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃) = 1)
7372ex 448 . . . . . . . 8 (𝐾 ∈ ℕ0 → ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃) = 1))
74733ad2ant2 1075 . . . . . . 7 ((𝑉 USGrph 𝐸𝐾 ∈ ℕ0 ∧ ∀𝑥𝑉 ((𝑉 VDeg 𝐸)‘𝑥) = 𝐾) → ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃) = 1))
7531, 74syl 17 . . . . . 6 (⟨𝑉, 𝐸⟩ RegUSGrph 𝐾 → ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃) = 1))
7675adantr 479 . . . . 5 ((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) → ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1)) → (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃) = 1))
7776imp 443 . . . 4 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃) = 1)
78773adant2 1072 . . 3 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → (((𝐾 · (𝐾 − 1)) + 1) mod 𝑃) = 1)
7930, 78eqtrd 2643 . 2 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘𝑉) mod 𝑃) = 1)
8010, 23, 793eqtrd 2647 1 (((⟨𝑉, 𝐸⟩ RegUSGrph 𝐾𝑉 FriendGrph 𝐸) ∧ (𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) ∧ (𝑃 ∈ ℙ ∧ 𝑃 ∥ (𝐾 − 1))) → ((#‘((𝑉 ClWWalksN 𝐸)‘𝑃)) mod 𝑃) = 1)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wral 2895  {crab 2899  c0 3873  cop 4130   class class class wbr 4577  cmpt 4637  cfv 5790  (class class class)co 6527  cmpt2 6529  Fincfn 7818  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797   < clt 9930  cmin 10117  cn 10867  0cn0 11139  cz 11210  +crp 11664   mod cmo 12485  #chash 12934  cdvds 14767  cprime 15169   USGrph cusg 25625   ClWWalksN cclwwlkn 26043   VDeg cvdg 26186   RegUSGrph crusgra 26216   FriendGrph cfrgra 26281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-inf2 8398  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-ot 4133  df-uni 4367  df-int 4405  df-iun 4451  df-disj 4548  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-n0 11140  df-z 11211  df-uz 11520  df-rp 11665  df-xadd 11779  df-fz 12153  df-fzo 12290  df-fl 12410  df-mod 12486  df-seq 12619  df-exp 12678  df-hash 12935  df-word 13100  df-lsw 13101  df-concat 13102  df-s1 13103  df-substr 13104  df-s2 13390  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-abs 13770  df-clim 14013  df-sum 14211  df-dvds 14768  df-gcd 15001  df-prm 15170  df-phi 15255  df-usgra 25628  df-nbgra 25715  df-wlk 25802  df-trail 25803  df-pth 25804  df-spth 25805  df-wlkon 25808  df-spthon 25811  df-wwlk 25973  df-wwlkn 25974  df-clwwlk 26045  df-clwwlkn 26046  df-2wlkonot 26151  df-2spthonot 26153  df-2spthsot 26154  df-vdgr 26187  df-rgra 26217  df-rusgra 26218  df-frgra 26282
This theorem is referenced by:  frgrareggt1  26409
  Copyright terms: Public domain W3C validator