23/03/10 10:19:42.73 awDuHvXz.net
1, (a^2≦2b) ∨ (2b≧0 ∧ |a|<0) ・・・仮定
2, (2b≧0 ∧ |a|<0) ・・・・・・・・・・1の後の選言肢を仮定
3, |a|<0 ・・・・・・・・・・・・・・・・2より∧除去
4, 矛盾 ・・・・・・・・・・・・・・・・・3より矛盾
5, (a^2≦2b) ・・・・・・・・・・・・・・4の矛盾から導出
6, (a^2≦2b) ・・・・・・・・・・・・・・1の最初の選言肢を仮定
7, (a^2≦2b) ・・・・・・・・・・・・・・1と5と6より1の∨除去
8, {(a^2≦2b) ∨ (2b≧0 ∧ |a|<0)}→(a^2≦2b) ・・1,7より→導入
9, (a^2≦2b) ・・・・・・・・・・・・・・仮定
10, (a^2≦2b) ∨ (2b≧0 ∧ |a|<0) ・・9より∨導入
11, (a^2≦2b)→{(a^2≦2b) ∨ (2b≧0 ∧ |a|<0)} ・・9,10より→導入
12, (a^2≦2b)↔{(a^2≦2b) ∨ (2b≧0 ∧ |a|<0)} ・・8,11より↔導入