We construct an injection from \(\mathbb {Z}/q\mathbb {Z} \sqcup \{ *\} \) into \(\operatorname {PGL}(2,q)\) by sending \(a \in \mathbb {Z}/q\mathbb {Z}\) to the class of the upper unipotent matrix

and sending the single element of \(\{ *\} \) to the class of the swap matrix

We verify injectivity in four cases. If \(\operatorname {projPGL}(U(a)) = \operatorname {projPGL}(U(b))\), then there exists a central element \(z\) in \(\operatorname {GL}(2,q)\) with \(U(a) \cdot z = U(b)\). Since \(z\) is central, it commutes with \(U(1) = \begin{pmatrix} 1 & 1 \\ 0 & 1 \end{pmatrix}\); by expanding the commutation relation at entry \((1,0)\) we obtain \(z_{10} = 0\), and at entry \((0,1)\) we obtain \(z_{00} = z_{11}\). Similarly, commuting with \(E_{21} = \begin{pmatrix} 1 & 0 \\ 1 & 1 \end{pmatrix}\) yields \(z_{01} = 0\). Substituting into the equation \(U(a) \cdot z = U(b)\) and reading off entry \((0,0)\) gives \(z_{00} = 1\), after which entry \((0,1)\) yields \(a \cdot z_{11} = b\). Since \(z_{00} = z_{11} = 1\), we conclude \(a = b\).

If \(\operatorname {projPGL}(S) = \operatorname {projPGL}(U(a))\), then \(S \cdot z = U(a)\) for some central \(z\). The same argument gives \(z_{10} = 0\), \(z_{01} = 0\). Reading entry \((1,0)\) of \(S \cdot z = U(a)\) yields \(-z_{00} = 0\), and entry \((1,1)\) yields \(-z_{01} = 1\); but \(z_{01} = 0\), giving \(0 = 1\), a contradiction. The remaining cases are symmetric or trivial.

Thus the map is injective, and by counting we obtain \(|\operatorname {PGL}(2,q)| \geq |\mathbb {Z}/q\mathbb {Z}| + 1 = q + 1 \geq 6\) for \(q \geq 5\).

We construct an injection from \(\mathbb {Z}/q\mathbb {Z} \sqcup \{ *\} \) into \(\operatorname {PSL}(2,q)\) by sending \(a\) to the class of the upper unipotent \(\operatorname {SL}\) element \(U(a) = \bigl(\begin{smallmatrix} 1 & a \\ 0 & 1 \end{smallmatrix}\bigr)\) and \(*\) to the class of the swap \(\operatorname {SL}\) element \(S = \bigl(\begin{smallmatrix} 0 & 1 \\ -1 & 0 \end{smallmatrix}\bigr)\).

Injectivity is established by the same argument as in \(\operatorname {PGL}\): if \(\operatorname {projPSL}(U(a)) = \operatorname {projPSL}(U(b))\), there is a central \(z \in \operatorname {SL}(2,q)\) with \(U(a) \cdot z = U(b)\). Commuting \(z\) with \(E_{12}\) gives \(z_{10} = 0\) and \(z_{00} = z_{11}\); commuting with \(E_{21}\) gives \(z_{01} = 0\). Expanding \(U(a) \cdot z = U(b)\) then forces \(z_{00} = 1\) and \(a = b\).

The case \(\operatorname {projPSL}(S) = \operatorname {projPSL}(U(a))\) leads to \(z_{01} = 0\) and the equation at entry \((1,1)\) of \(S \cdot z = U(a)\) gives \(-z_{01} = 1\), i.e. \(0 = 1\), a contradiction. Hence the map is injective, so \(|\operatorname {PSL}(2,q)| \geq q + 1 \geq 6\).

We argue by contradiction. Suppose \(q {\lt} 5\), so \(q \leq 4\). Since \(q\) is an odd prime and \(q \leq 4\), we must have \(q = 3\).

Since \(p\) is an odd prime, \(p \geq 3\), hence \((p : \mathbb {R}) \geq 3\). From the hypothesis \(q {\gt} 2\sqrt{p}\) with \(q = 3\), we have \(3 {\gt} 2\sqrt{p}\), so \(9 {\gt} 4p\). But \(4p \geq 12\), giving \(9 {\gt} 12\), a contradiction. Formally, let \(s = \sqrt{p}\); then \(s \geq 0\) and \(s^2 = p \geq 3\). The inequality \(3 {\gt} 2s\) gives \((3 - 2s)^2 {\gt} 0\) and \(9 {\gt} 4s^2 = 4p \geq 12\), which is absurd; this is derived by nonlinear arithmetic from \(\operatorname {nlinarith}\) using \((2\sqrt{p} - 3)^2 \geq 0\).

By Lemma 498, the hypothesis \(q {\gt} 2\sqrt{p}\) together with \(p, q\) odd primes implies \(q \geq 5\). Applying Theorem 496 we obtain \(|\operatorname {PGL}(2,q)| \geq 6 \geq 2\).

By Lemma 498, \(q \geq 5\). Applying Theorem 497 gives \(|\operatorname {PSL}(2,q)| \geq 6 \geq 2\).

blue[Uses hypothesis-based assumptions: Ramanujan property and spectral bound]

We unfold the definition of \(\operatorname {IsRamanujan}\) in the hypothesis \(h_{\mathrm{ram}}\): for every index \(i \in \operatorname {Fin}(|\operatorname {PGL}(2,q)|)\) with \(|\lambda _i| {\lt} p+1\), we have \(|\lambda _i| \leq 2\sqrt{p}\). Set the index \(i = 1\), which is valid since \(|\operatorname {PGL}(2,q)| \geq 2\). Applying \(h_{\mathrm{ram}}\) at \(i = 1\) and using the hypothesis \(h_{\mathrm{spec}} : |\lambda _2| {\lt} p+1\) (after casting naturals to reals), we obtain \(|\lambda _2| \leq 2\sqrt{p}\). Since \(\lambda _2 \leq |\lambda _2|\), we conclude \(\lambda _2 \leq 2\sqrt{p}\).

blue[Uses hypothesis-based assumptions: Ramanujan property and spectral bound]

We unfold the definition of \(\operatorname {IsRamanujan}\) and apply it at index \(i = 1 \in \operatorname {Fin}(|\operatorname {PSL}(2,q)|)\), which is valid since \(|\operatorname {PSL}(2,q)| \geq 2\). From the spectral bound hypothesis \(|\lambda _2| {\lt} p+1\) (after casting), the Ramanujan condition yields \(|\lambda _2| \leq 2\sqrt{p}\). The conclusion \(\lambda _2 \leq 2\sqrt{p}\) follows since \(\lambda _2 \leq |\lambda _2|\).

blue[Uses hypothesis-based assumptions: connectedness and Ramanujan property]

We combine the hypotheses and previously established results. Connectedness follows directly from \(h_{\mathrm{conn}}\). Regularity of degree \(p+1\) follows from Theorem 492. The cardinality bound \(|\operatorname {PGL}(2,q)| \geq 2\) follows from Theorem 499. The Ramanujan property follows from \(h_{\mathrm{ram}}\). We package all four conclusions into a conjunction.

blue[Uses hypothesis-based assumptions: connectedness and Ramanujan property]

We combine the hypotheses and previously established results. Connectedness follows from \(h_{\mathrm{conn}}\). Regularity of degree \(p+1\) follows from Theorem 493. The cardinality bound \(|\operatorname {PSL}(2,q)| \geq 2\) follows from Theorem 500. The Ramanujan property is \(h_{\mathrm{ram}}\). All four conclusions are packaged into a conjunction.