[proofplan] Associate to the irreducible reduced finite root system its Dynkin diagram. Irreducibility makes this diagram connected, finiteness makes its Cartan form positive definite, and reducedness restricts all bonds to the ordinary finite Dynkin possibilities. The classification of connected finite Dynkin diagrams gives precisely the displayed list, and the standard coordinate constructions show that every listed diagram is realised by a reduced irreducible finite root system. Uniqueness follows because the Dynkin diagram determines a reduced finite root system up to isomorphism. [/proofplan]

[step:Pass from the root system to a connected finite Dynkin diagram] Let $\Phi$ denote the given irreducible reduced finite root system in a finite-dimensional real [inner product space](/page/Inner%20Product%20Space) $V$. Choose a base $\Delta \subset \Phi$, and let $\Gamma(\Phi,\Delta)$ denote the Dynkin diagram whose vertices are the simple roots in $\Delta$ and whose bonds are determined by the Cartan integers \begin{align*} \langle \alpha,\beta^\vee\rangle = \frac{2(\alpha,\beta)_V}{(\beta,\beta)_V}, \qquad \alpha,\beta \in \Delta. \end{align*} By the [Dynkin Diagram of a Reduced Root System](/page/Dynkin%20Diagram), the reducedness hypothesis ensures that this construction gives an ordinary finite Dynkin diagram, with no non-reduced vertex labels. Since $\Phi$ is finite, the Cartan matrix attached to $\Delta$ is positive definite. Since $\Phi$ is irreducible, the diagram $\Gamma(\Phi,\Delta)$ is connected; otherwise a decomposition of the vertex set into two disconnected parts would split $\Phi$ as an orthogonal union of two nonempty root subsystems, contradicting irreducibility. [/step]

[step:Apply the classification of connected finite Dynkin diagrams]The [Classification of Connected Finite Dynkin Diagrams](/page/Classification%20of%20Connected%20Finite%20Dynkin%20Diagrams) applies to $\Gamma(\Phi,\Delta)$ because the preceding step verified that the diagram is connected and of finite positive-definite type. Therefore $\Gamma(\Phi,\Delta)$ is isomorphic to exactly one diagram in the list \begin{align*} A_n \ (n\ge 1),\quad B_n \ (n\ge 2),\quad C_n \ (n\ge 3),\quad D_n \ (n\ge 4),\quad E_6,E_7,E_8,F_4,G_2. \end{align*} The small-rank coincidences are excluded by the stated index ranges: $B_1$ and $C_1$ are $A_1$, $D_2$ is reducible, $D_3$ is $A_3$, and $C_2$ has the same diagram type as $B_2$ after reversing root lengths.[/step]

[guided]The purpose of passing to $\Gamma(\Phi,\Delta)$ is that the classification problem becomes a finite graph problem with a positive-definite Cartan matrix. The classification theorem requires two hypotheses: connectedness and finite positive-definite type. Connectedness was obtained from irreducibility of $\Phi$, and finite positive-definite type was obtained from finiteness of the root system and positive-definiteness of the ambient inner product on $V$. Applying the [Classification of Connected Finite Dynkin Diagrams](/page/Classification%20of%20Connected%20Finite%20Dynkin%20Diagrams), the diagram $\Gamma(\Phi,\Delta)$ must be isomorphic to exactly one of \begin{align*} A_n \ (n\ge 1),\quad B_n \ (n\ge 2),\quad C_n \ (n\ge 3),\quad D_n \ (n\ge 4),\quad E_6,E_7,E_8,F_4,G_2. \end{align*} The restrictions on $n$ are part of the uniqueness convention for the classification. They remove duplicate or degenerate names: $B_1$ and $C_1$ give the one-node diagram $A_1$, $D_2$ splits into two disconnected nodes, $D_3$ is the same type as $A_3$, and $C_2$ is identified with $B_2$ after exchanging long and short roots.[/guided]

[step:Realise every diagram in the list by a reduced irreducible finite root system] For each diagram in the displayed list, the [Existence of Finite Root Systems of Dynkin Type](/page/Finite%20Root%20Systems%20of%20Dynkin%20Type) constructs a reduced finite root system with that diagram: the classical systems $A_n,B_n,C_n,D_n$ are realised in Euclidean space by their standard coordinate root sets, and the exceptional systems $E_6,E_7,E_8,F_4,G_2$ are realised by their standard exceptional coordinate models. In each case the constructed diagram is connected, so the corresponding root system is irreducible. Thus every listed type occurs. [/step]

[step:Use the diagram to identify the root system uniquely] By the [Isomorphism Theorem for Reduced Finite Root Systems](/page/Isomorphism%20Theorem%20for%20Reduced%20Finite%20Root%20Systems), a reduced finite root system is determined up to isomorphism by its Dynkin diagram. The theorem applies to $\Phi$ because $\Phi$ is reduced and finite. Hence two irreducible reduced finite root systems with the same Dynkin diagram from the list are isomorphic, while two with non-isomorphic diagrams are not isomorphic. Combining this uniqueness with the existence step proves that every irreducible reduced finite root system is isomorphic to exactly one of the stated types. [/step]