¬∃x∈ℚ ( x·x = 2 )
  If ∃x∈ℚ ( x·x = 2 ):
    Let a ∈ ℚ such that a·a = 2
    ∀x∈ℚ ∃p,q∈ℤ ( q ≠ 0 ∧ p = q·x )
    ∃p,q∈ℤ ( q ≠ 0 ∧ p = q·a )
    Let p',q' ∈ ℤ such that q' ≠ 0 ∧ p' = q'·a
    p' ∈ ℕ ∨ –p' ∈ ℕ [ℤ=ℕ⋃−ℕ]
    q' ∈ ℕ ∨ –q' ∈ ℕ [ℤ=ℕ⋃−ℕ]
    If p' ∈ ℕ:
      If q' ∈ ℕ:
        p' = q'·a
        q'·q'·a·a = q'·q'·2
        q'·a·q'·a = q'·q'·2
        p'·p' = q'·q'·2
        ∀k,m∈ℕ ( k·k = m·m·2 ⇒ k = 0 ) [PA4]
        p'·p' = q'·q'·2 ⇒ p' = 0
        p' = 0
        0 = q'·a
        0 = q'·0