自然数には引き算も割り算も無いので、和の公式は分母を払って足し算で述べる。和は \(f\ \mathrm{sum}\ n\)（第 0 項から第 \(n-1\) 項まで）。
ガウスの和：\(2 \sum_{iRga … \(S , n \in \mathbb{M} \Longrightarrow 2 \cdot ( S + ( n ) ) + ( n + 1 ) = 2 \cdot S + n + ( 2 \cdot n + 1 )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\)
Rgb … \(n \in \mathbb{M} \Longrightarrow n \cdot n + ( 2 \cdot n + 1 ) = ( n + 1 ) \cdot ( n + 1 )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\)
LMg … \(\forall i \in \mathbb{M} . f ( i ) = i \Longrightarrow \forall i \in \mathbb{M} . f ( i ) \in \mathbb{M}\) \(\blacktriangleleft\) \(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\)
LBg … \(\forall i \in \mathbb{M} . f ( i ) = i \Longrightarrow 2 \cdot ( f \sum 0 ) + 0 = 0 \cdot 0\) \(\blacktriangleleft\) \(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，⋅𝕄:C ，\(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\) ，sum𝕄
LSg … \(\forall i \in \mathbb{M} . f ( i ) = i , n \in \mathbb{M} , 2 \cdot ( f \sum n ) + n = n \cdot n \Longrightarrow 2 \cdot ( f \sum ( n + 1 ) ) + ( n + 1 ) = ( n + 1 ) \cdot ( n + 1 )\) \(\blacktriangleleft\) \(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，LMg ，sum∈𝕄 ，Rga ，Rgb ，\(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\) ，sum𝕄
Lindg … \(\forall i \in \mathbb{M} . f ( i ) = i \Longrightarrow \forall n \in \mathbb{M} . 2 \cdot ( f \sum n ) + n = n \cdot n\) \(\blacktriangleleft\) LBg ，LSg ，\(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\) ，sum𝕄
連続2整数の積の和：\(3 \sum_{iRpa … \(S , n \in \mathbb{M} \Longrightarrow 3 \cdot ( S + ( n \cdot ( n + 1 ) ) ) + ( n + 1 ) = 3 \cdot S + n + ( ( 3 \cdot ( n \cdot n ) + 3 \cdot n ) + 1 )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\)
Rpb … \(n \in \mathbb{M} \Longrightarrow n \cdot ( n \cdot n ) + ( ( 3 \cdot ( n \cdot n ) + 3 \cdot n ) + 1 ) = ( n + 1 ) \cdot ( ( n + 1 ) \cdot ( n + 1 ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\)
LMp … \(\forall i \in \mathbb{M} . f ( i ) = i \cdot ( i + 1 ) \Longrightarrow \forall i \in \mathbb{M} . f ( i ) \in \mathbb{M}\) \(\blacktriangleleft\) \(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\)
LBp … \(\forall i \in \mathbb{M} . f ( i ) = i \cdot ( i + 1 ) \Longrightarrow 3 \cdot ( f \sum 0 ) + 0 = 0 \cdot ( 0 \cdot 0 )\) \(\blacktriangleleft\) \(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，⋅𝕄:C ，\(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\) ，sum𝕄
LSp … \(\forall i \in \mathbb{M} . f ( i ) = i \cdot ( i + 1 ) , n \in \mathbb{M} , 3 \cdot ( f \sum n ) + n = n \cdot ( n \cdot n ) \Longrightarrow 3 \cdot ( f \sum ( n + 1 ) ) + ( n + 1 ) = ( n + 1 ) \cdot ( ( n + 1 ) \cdot ( n + 1 ) )\) \(\blacktriangleleft\) \(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，LMp ，sum∈𝕄 ，Rpa ，Rpb ，\(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\) ，sum𝕄
Lindp … \(\forall i \in \mathbb{M} . f ( i ) = i \cdot ( i + 1 ) \Longrightarrow \forall n \in \mathbb{M} . 3 \cdot ( f \sum n ) + n = n \cdot ( n \cdot n )\) \(\blacktriangleleft\) LBp ，LSp ，\(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\) ，sum𝕄
立方の階差の和：\(\sum_{iRca … \(S , n \in \mathbb{M} \Longrightarrow ( S + ( ( 3 \cdot ( n \cdot n ) + 3 \cdot n ) + 1 ) ) = S + ( ( 3 \cdot ( n \cdot n ) + 3 \cdot n ) + 1 )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\)
Rcb … \(n \in \mathbb{M} \Longrightarrow n \cdot ( n \cdot n ) + ( ( 3 \cdot ( n \cdot n ) + 3 \cdot n ) + 1 ) = ( n + 1 ) \cdot ( ( n + 1 ) \cdot ( n + 1 ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\)
LMc … \(\forall i \in \mathbb{M} . f ( i ) = ( 3 \cdot ( i \cdot i ) + 3 \cdot i ) + 1 \Longrightarrow \forall i \in \mathbb{M} . f ( i ) \in \mathbb{M}\) \(\blacktriangleleft\) \(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\)
LBc … \(\forall i \in \mathbb{M} . f ( i ) = ( 3 \cdot ( i \cdot i ) + 3 \cdot i ) + 1 \Longrightarrow ( f \sum 0 ) = 0 \cdot ( 0 \cdot 0 )\) \(\blacktriangleleft\) \(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，⋅𝕄:C ，\(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\) ，sum𝕄
LSc … \(\forall i \in \mathbb{M} . f ( i ) = ( 3 \cdot ( i \cdot i ) + 3 \cdot i ) + 1 , n \in \mathbb{M} , ( f \sum n ) = n \cdot ( n \cdot n ) \Longrightarrow ( f \sum ( n + 1 ) ) = ( n + 1 ) \cdot ( ( n + 1 ) \cdot ( n + 1 ) )\) \(\blacktriangleleft\) \(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，LMc ，sum∈𝕄 ，Rca ，Rcb ，\(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\) ，sum𝕄
Lindc … \(\forall i \in \mathbb{M} . f ( i ) = ( 3 \cdot ( i \cdot i ) + 3 \cdot i ) + 1 \Longrightarrow \forall n \in \mathbb{M} . ( f \sum n ) = n \cdot ( n \cdot n )\) \(\blacktriangleleft\) LBc ，LSc ，\(\mathbb{W}.\) ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\) ，sum𝕄