8 有理数

8.1 有理数と分数

word(,s) … \(\mathbb{Q}\)
word(ss,s) … \(/\)
ℚ. … \(\mathbb{Q} = \{ a / b \mid a \in \mathbb{Z} , b \in \mathbb{N} \}\)
÷ℚ … \(\begin{cases} a , c \in \mathbb{Z} , b , d \in \mathbb{N} \Longrightarrow ( a / b = c / d \Longleftrightarrow a \cdot d = c \cdot b ) \\ a \in \mathbb{Z} \Longrightarrow a / 1 = a \\ a \in \mathbb{Z} , b \in \mathbb{N} \Longrightarrow - ( a / b ) = ( - a ) / b \end{cases}\)
+ℚ … +ℤ \(, ( a , c \in \mathbb{Z} , b , d \in \mathbb{N} \Longrightarrow ( a / b ) + ( c / d ) = ( a \cdot d + c \cdot b ) / ( b \cdot d ) )\)
⋅ℚ … ⋅ℤ \(, ( a , c \in \mathbb{Z} , b , d \in \mathbb{N} \Longrightarrow ( a / b ) \cdot ( c / d ) = ( a \cdot c ) / ( b \cdot d ) )\)
ℤ⊂ℚ … \(a \in \mathbb{Z} \Longrightarrow a \in \mathbb{Q}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ
+∈ℚ … \(x , y \in \mathbb{Q} \Longrightarrow x + y \in \mathbb{Q}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ
⋅∈ℚ … \(x , y \in \mathbb{Q} \Longrightarrow x \cdot y \in \mathbb{Q}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ
↑∈ℚ … \(x \in \mathbb{Q} , n \in \mathbb{M} \Longrightarrow x ^ n \in \mathbb{Q}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，↑𝕄

8.2 有理数の演算の性質

\(0 \in \text{unit} ( \mathbb{Q} , [+] )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，ℤ⊂ℚ
\(1 \in \text{unit} ( \mathbb{Q} , [\cdot] )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，ℤ⊂ℚ
\(( \mathbb{Q} , [+] ) :\underline{2}\mathsf{C}\mathsf{A}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ
\(( \mathbb{Q} , [\cdot] ) :\underline{2}\mathsf{C}\mathsf{A}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ

8.3 有理数の順序

≤ℚ … \(x , y \in \mathbb{Q} \Longrightarrow ( x \le y \Longleftrightarrow \exists a , b \, a \in \mathbb{M} , b \in \mathbb{N} , y + ( - x ) = a / b )\)
ℚ も可換半環（csemiring）。
\(( \mathbb{Q} , [+] , [\cdot] ) \text{csemiring}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ
≤ℚ:R … \(x \in \mathbb{Q} \Longrightarrow x \le x\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
≤ℚ:T … \(x , y , z \in \mathbb{Q} , x \le y , y \le z \Longrightarrow x \le z\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
≤ℚ:A … \(x , y \in \mathbb{Q} , x \le y , y \le x \Longrightarrow x = y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
≤ℚ:tot … \(x , y \in \mathbb{Q} \Longrightarrow x \le y \mathbin{\rm o\!r} y \le x\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
≤ℚ+ … \(x , y , z \in \mathbb{Q} , x \le y \Longrightarrow x + z \le y + z\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
≤ℚ⋅ … \(x , y , z \in \mathbb{Q} , 0 \le z , x \le y \Longrightarrow x \cdot z \le y \cdot z\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ