gpg3nbgrvtx0

Description: In a generalized Petersen graph G , every outside vertex has exactly three (different) neighbors. (Contributed by AV, 30-Aug-2025)

	Ref	Expression
Hypotheses	gpgnbgr.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
	gpgnbgr.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
	gpgnbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	gpgnbgr.u	⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
Assertion	gpg3nbgrvtx0	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ♯ ‘ 𝑈 ) = 3 )

Proof

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 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 𝑈 = { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } )
6	5	fveq2d	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ) )
7		0ne1	⊢ 0 ≠ 1
8	7	a1i	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 0 ≠ 1 )
9	8	orcd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( 0 ≠ 1 ∨ ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ≠ ( 2^nd ‘ 𝑋 ) ) )
10		c0ex	⊢ 0 ∈ V
11		ovex	⊢ ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ∈ V
12	10 11	opthne	⊢ ( ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ↔ ( 0 ≠ 1 ∨ ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ≠ ( 2^nd ‘ 𝑋 ) ) )
13	9 12	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ )
14		ax-1ne0	⊢ 1 ≠ 0
15	14	a1i	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 1 ≠ 0 )
16	15	orcd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( 1 ≠ 0 ∨ ( 2^nd ‘ 𝑋 ) ≠ ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ) )
17		1ex	⊢ 1 ∈ V
18		fvex	⊢ ( 2^nd ‘ 𝑋 ) ∈ V
19	17 18	opthne	⊢ ( ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ↔ ( 1 ≠ 0 ∨ ( 2^nd ‘ 𝑋 ) ≠ ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ) )
20	16 19	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ )
21		simpl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) → 𝑋 ∈ 𝑉 )
22	21	anim2i	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) )
23		eqid	⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
24	23 1 2 3	gpgvtxel2	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑋 ∈ 𝑉 ) → ( 2^nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) )
25		elfzoelz	⊢ ( ( 2^nd ‘ 𝑋 ) ∈ ( 0 ..^ 𝑁 ) → ( 2^nd ‘ 𝑋 ) ∈ ℤ )
26	22 24 25	3syl	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( 2^nd ‘ 𝑋 ) ∈ ℤ )
27	26	zcnd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( 2^nd ‘ 𝑋 ) ∈ ℂ )
28		1cnd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 1 ∈ ℂ )
29		2cnd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 2 ∈ ℂ )
30	27 28 29	subadd23d	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( ( 2^nd ‘ 𝑋 ) − 1 ) + 2 ) = ( ( 2^nd ‘ 𝑋 ) + ( 2 − 1 ) ) )
31		2m1e1	⊢ ( 2 − 1 ) = 1
32	31	a1i	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( 2 − 1 ) = 1 )
33	32	oveq2d	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( 2^nd ‘ 𝑋 ) + ( 2 − 1 ) ) = ( ( 2^nd ‘ 𝑋 ) + 1 ) )
34	30 33	eqtrd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( ( 2^nd ‘ 𝑋 ) − 1 ) + 2 ) = ( ( 2^nd ‘ 𝑋 ) + 1 ) )
35	34	eqcomd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( 2^nd ‘ 𝑋 ) + 1 ) = ( ( ( 2^nd ‘ 𝑋 ) − 1 ) + 2 ) )
36	35	oveq1d	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) = ( ( ( ( 2^nd ‘ 𝑋 ) − 1 ) + 2 ) mod 𝑁 ) )
37		1zzd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 1 ∈ ℤ )
38	26 37	zsubcld	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( 2^nd ‘ 𝑋 ) − 1 ) ∈ ℤ )
39	38	zred	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( 2^nd ‘ 𝑋 ) − 1 ) ∈ ℝ )
40		2re	⊢ 2 ∈ ℝ
41	40	a1i	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 2 ∈ ℝ )
42		eluz3nn	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → 𝑁 ∈ ℕ )
43	42	nnrpd	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → 𝑁 ∈ ℝ⁺ )
44	43	ad2antrr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 𝑁 ∈ ℝ⁺ )
45		modaddabs	⊢ ( ( ( ( 2^nd ‘ 𝑋 ) − 1 ) ∈ ℝ ∧ 2 ∈ ℝ ∧ 𝑁 ∈ ℝ⁺ ) → ( ( ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) + ( 2 mod 𝑁 ) ) mod 𝑁 ) = ( ( ( ( 2^nd ‘ 𝑋 ) − 1 ) + 2 ) mod 𝑁 ) )
46	39 41 44 45	syl3anc	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) + ( 2 mod 𝑁 ) ) mod 𝑁 ) = ( ( ( ( 2^nd ‘ 𝑋 ) − 1 ) + 2 ) mod 𝑁 ) )
47	46	eqcomd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( ( ( 2^nd ‘ 𝑋 ) − 1 ) + 2 ) mod 𝑁 ) = ( ( ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) + ( 2 mod 𝑁 ) ) mod 𝑁 ) )
48	36 47	eqtrd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) = ( ( ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) + ( 2 mod 𝑁 ) ) mod 𝑁 ) )
49	42	ad2antrr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → 𝑁 ∈ ℕ )
50	38 49	zmodcld	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ∈ ℕ₀ )
51		modlt	⊢ ( ( ( ( 2^nd ‘ 𝑋 ) − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ⁺ ) → ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) < 𝑁 )
52	39 44 51	syl2anc	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) < 𝑁 )
53	50 52	jca	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ∈ ℕ₀ ∧ ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) < 𝑁 ) )
54		2nn0	⊢ 2 ∈ ℕ₀
55	54	a1i	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → 2 ∈ ℕ₀ )
56		eluz2	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) )
57	40	a1i	⊢ ( ( 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 2 ∈ ℝ )
58		3re	⊢ 3 ∈ ℝ
59	58	a1i	⊢ ( ( 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 3 ∈ ℝ )
60		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
61	60	adantr	⊢ ( ( 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
62		2lt3	⊢ 2 < 3
63	62	a1i	⊢ ( ( 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 2 < 3 )
64		simpr	⊢ ( ( 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 3 ≤ 𝑁 )
65	57 59 61 63 64	ltletrd	⊢ ( ( 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 2 < 𝑁 )
66	65	3adant1	⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 2 < 𝑁 )
67	56 66	sylbi	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → 2 < 𝑁 )
68		elfzo0	⊢ ( 2 ∈ ( 0 ..^ 𝑁 ) ↔ ( 2 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁 ) )
69	55 42 67 68	syl3anbrc	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → 2 ∈ ( 0 ..^ 𝑁 ) )
70		zmodidfzoimp	⊢ ( 2 ∈ ( 0 ..^ 𝑁 ) → ( 2 mod 𝑁 ) = 2 )
71	69 70	syl	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ( 2 mod 𝑁 ) = 2 )
72		2nn	⊢ 2 ∈ ℕ
73	71 72	eqeltrdi	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ( 2 mod 𝑁 ) ∈ ℕ )
74	40	a1i	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → 2 ∈ ℝ )
75		modlt	⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℝ⁺ ) → ( 2 mod 𝑁 ) < 𝑁 )
76	74 43 75	syl2anc	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ( 2 mod 𝑁 ) < 𝑁 )
77	73 76	jca	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) → ( ( 2 mod 𝑁 ) ∈ ℕ ∧ ( 2 mod 𝑁 ) < 𝑁 ) )
78	77	ad2antrr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( 2 mod 𝑁 ) ∈ ℕ ∧ ( 2 mod 𝑁 ) < 𝑁 ) )
79		addmodne	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ∈ ℕ₀ ∧ ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) < 𝑁 ) ∧ ( ( 2 mod 𝑁 ) ∈ ℕ ∧ ( 2 mod 𝑁 ) < 𝑁 ) ) → ( ( ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) + ( 2 mod 𝑁 ) ) mod 𝑁 ) ≠ ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) )
80	49 53 78 79	syl3anc	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) + ( 2 mod 𝑁 ) ) mod 𝑁 ) ≠ ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) )
81	48 80	eqnetrd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ≠ ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) )
82	81	necomd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ≠ ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) )
83	82	olcd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( 0 ≠ 0 ∨ ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ≠ ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ) )
84		ovex	⊢ ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ∈ V
85	10 84	opthne	⊢ ( ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ↔ ( 0 ≠ 0 ∨ ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ≠ ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ) )
86	83 85	sylibr	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ )
87	13 20 86	3jca	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∧ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ) )
88		opex	⊢ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ V
89		opex	⊢ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ V
90		opex	⊢ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ V
91		hashtpg	⊢ ( ( ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ∈ V ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∈ V ∧ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∈ V ) → ( ( ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∧ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ) ↔ ( ♯ ‘ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ) = 3 ) )
92	88 89 90 91	mp3an	⊢ ( ( ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∧ ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ≠ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ∧ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ ) ↔ ( ♯ ‘ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ) = 3 )
93	87 92	sylib	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ♯ ‘ { ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 𝑁 ) ⟩ , ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 𝑁 ) ⟩ } ) = 3 )
94	6 93	eqtrd	⊢ ( ( ( 𝑁 ∈ ( ℤ_≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑋 ) = 0 ) ) → ( ♯ ‘ 𝑈 ) = 3 )

Metamath Proof Explorer

Theorem gpg3nbgrvtx0

Proof