Description: In a generalized Petersen graph G , every outside vertex has exactly three (different) neighbors. (Contributed by AV, 30-Aug-2025)
The proof of gpg3nbgrvtx0 can be shortened using lemma gpg3nbgrvtxlem , but then theorem 2ltceilhalf is required which is based on an "example" ex-ceil . If these theorems were moved to main, the "example" should also be moved up to become a full-fledged theorem. (Proof shortened by AV, 4-Sep-2025) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | gpgnbgr.j | ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) | |
| gpgnbgr.g | ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 ) | ||
| gpgnbgr.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | ||
| gpgnbgr.u | ⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 ) | ||
| Assertion | gpg3nbgrvtx0ALT | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ♯ ‘ 𝑈 ) = 3 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | gpgnbgr.j | ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) | |
| 2 | gpgnbgr.g | ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 ) | |
| 3 | gpgnbgr.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| 4 | gpgnbgr.u | ⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 ) | |
| 5 | 1 2 3 4 | gpgnbgrvtx0 | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → 𝑈 = { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ) |
| 6 | 5 | fveq2d | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ) ) |
| 7 | 0ne1 | ⊢ 0 ≠ 1 | |
| 8 | 7 | a1i | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → 0 ≠ 1 ) |
| 9 | 8 | orcd | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( 0 ≠ 1 ∨ ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ≠ ( 2nd ‘ 𝑋 ) ) ) |
| 10 | c0ex | ⊢ 0 ∈ V | |
| 11 | ovex | ⊢ ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ∈ V | |
| 12 | 10 11 | opthne | ⊢ ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ↔ ( 0 ≠ 1 ∨ ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ≠ ( 2nd ‘ 𝑋 ) ) ) |
| 13 | 9 12 | sylibr | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ) |
| 14 | ax-1ne0 | ⊢ 1 ≠ 0 | |
| 15 | 14 | a1i | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → 1 ≠ 0 ) |
| 16 | 15 | orcd | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( 1 ≠ 0 ∨ ( 2nd ‘ 𝑋 ) ≠ ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ) ) |
| 17 | 1ex | ⊢ 1 ∈ V | |
| 18 | fvex | ⊢ ( 2nd ‘ 𝑋 ) ∈ V | |
| 19 | 17 18 | opthne | ⊢ ( ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ↔ ( 1 ≠ 0 ∨ ( 2nd ‘ 𝑋 ) ≠ ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ) ) |
| 20 | 16 19 | sylibr | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ) |
| 21 | simpll | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) | |
| 22 | 2z | ⊢ 2 ∈ ℤ | |
| 23 | 22 | a1i | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ∈ ℤ ) |
| 24 | eluzelre | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℝ ) | |
| 25 | 24 | rehalfcld | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 / 2 ) ∈ ℝ ) |
| 26 | 25 | ceilcld | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ ) |
| 27 | 2ltceilhalf | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) | |
| 28 | eluz2 | ⊢ ( ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ ∧ 2 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) | |
| 29 | 23 26 27 28 | syl3anbrc | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ( ℤ≥ ‘ 2 ) ) |
| 30 | 29 | adantr | ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ( ℤ≥ ‘ 2 ) ) |
| 31 | 30 | adantr | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ( ℤ≥ ‘ 2 ) ) |
| 32 | fzo1lb | ⊢ ( 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ↔ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ( ℤ≥ ‘ 2 ) ) | |
| 33 | 31 32 | sylibr | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) |
| 34 | eqid | ⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 ) | |
| 35 | 34 1 2 3 | gpgvtxel2 | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( 2nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) ) |
| 36 | 35 | adantrr | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( 2nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) ) |
| 37 | gpg3nbgrvtxlem | ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ∧ ( 2nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ) | |
| 38 | 21 33 36 37 | syl3anc | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ) |
| 39 | 38 | necomd | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ) |
| 40 | 39 | olcd | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( 0 ≠ 0 ∨ ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ) ) |
| 41 | ovex | ⊢ ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ∈ V | |
| 42 | 10 41 | opthne | ⊢ ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ↔ ( 0 ≠ 0 ∨ ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ≠ ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ) ) |
| 43 | 40 42 | sylibr | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ) |
| 44 | 13 20 43 | 3jca | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∧ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ) ) |
| 45 | opex | ⊢ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ V | |
| 46 | opex | ⊢ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∈ V | |
| 47 | opex | ⊢ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ V | |
| 48 | hashtpg | ⊢ ( ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ V ∧ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∈ V ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ V ) → ( ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∧ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ) ↔ ( ♯ ‘ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ) = 3 ) ) | |
| 49 | 45 46 47 48 | mp3an | ⊢ ( ( ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∧ ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∧ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ) ↔ ( ♯ ‘ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ) = 3 ) |
| 50 | 44 49 | sylib | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ♯ ‘ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ) = 3 ) |
| 51 | 6 50 | eqtrd | ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → ( ♯ ‘ 𝑈 ) = 3 ) |