互いに素な \(v, w\) の積 \(vw\) が平方数なら、\(v\) も平方数（23 の準備）。

1 準備

素数 \(p\) が \(k^2\) を割れば \(k\) を割る（∣k）。\(d \mid v\) なら \(d \mid vw\)（∣M）。
\(p \in \mathbb{P} , k \in \mathbb{M} , p \mid k ^ 2 \Longrightarrow p \mid k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，Ldiv ，LG ，Euclid ，∣k⋅

2 主定理

共通の素因数を持たない \(v, w\) について、\(vw = k^2\) なら \(v\) は平方数（Sq）。\(v\) についての強い帰納法で示します。
\(v \ge 2\) なら素因数 \(p\) をとると、\(p \mid k\) で \(p \nmid w\) なので \(v = p^2 u\)・\(uw = j^2\)（Dn）。\(u < v\) なので \(u\) は平方数、よって \(v\) も。
\(p \in \mathbb{P} , v , w , k \in \mathbb{M} , p \mid v , \neg p \mid w , v \cdot w = k ^ 2 \Longrightarrow \exists u \in \mathbb{M} . \exists j \in \mathbb{M} . v = p ^ 2 \cdot u , u \cdot w = j ^ 2\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，Ldiv ，LG ，Euclid ，∣k⋅ ，\(p \in \mathbb{P} , k \in \mathbb{M} , p \mid k ^ 2 \Longrightarrow p \mid k\) ，Dn⋅
\(v , w , k \in \mathbb{M} , v \cdot w = k ^ 2 , \neg \exists q \in \mathbb{P} . q \mid v , q \mid w \Longrightarrow \exists n \in \mathbb{M} . v = n ^ 2\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，Ldiv ，LG ，Euclid ，∣k⋅ ，\(p \in \mathbb{P} , k \in \mathbb{M} , p \mid k ^ 2 \Longrightarrow p \mid k\) ，Dn⋅ ，\(p \in \mathbb{P} , v , w , k \in \mathbb{M} , p \mid v , \neg p \mid w , v \cdot w = k ^ 2 \Longrightarrow \exists u \in \mathbb{M} . \exists j \in \mathbb{M} . v = p ^ 2 \cdot u , u \cdot w = j ^ 2\) ，Sq⋅