Metamath Proof Explorer

Theorem gpgprismgrusgra

Description: The generalized Petersen graphs G(N,1), which are the N-prisms, are simple graphs. (Contributed by AV, 31-Oct-2025)

Ref Expression
Assertion gpgprismgrusgra ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 gPetersenGr 1 ) ∈ USGraph )

Proof

Step Hyp Ref Expression
1 1zzd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ℤ )
2 eluzelre ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℝ )
3 2re ⊢ 2 ∈ ℝ
4 3 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ∈ ℝ )
5 2ne0 ⊢ 2 ≠ 0
6 5 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ≠ 0 )
7 2 4 6 3jca ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 ∈ ℝ ∧ 2 ∈ ℝ ∧ 2 ≠ 0 ) )
8 redivcl ⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ∈ ℝ ∧ 2 ≠ 0 ) → ( 𝑁 / 2 ) ∈ ℝ )
9 7 8 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 / 2 ) ∈ ℝ )
10 9 ceilcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
11 1red ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ℝ )
12 8 ceilcld ⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ∈ ℝ ∧ 2 ≠ 0 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
13 7 12 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
14 13 zred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℝ )
15 1lt2 ⊢ 1 < 2
16 15 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 < 2 )
17 2ltceilhalf ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ≤ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
18 11 4 14 16 17 ltletrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 < ( ⌈ ‘ ( 𝑁 / 2 ) ) )
19 fzolb ⊢ ( 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ↔ ( 1 ∈ ℤ ∧ ( ⌈ ‘ ( 𝑁 / 2 ) ) ∈ ℤ ∧ 1 < ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
20 1 10 18 19 syl3anbrc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
21 gpgusgra ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 1 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 𝑁 gPetersenGr 1 ) ∈ USGraph )
22 20 21 mpdan ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 gPetersenGr 1 ) ∈ USGraph )