no goals
d : ℕ
dnsq : Nonsquare d
x : ℕ
xy : Nonneg { re := -[x+1], im := 0 }
x✝ : Nonneg (-{ re := -[x+1], im := 0 })
⊢ 0 < 1
decide
no goals
d : ℕ
dnsq : Nonsquare d
x : ℕ
x✝ : Nonneg { re := ↑(x + 1), im := 0 }
yx : Nonneg (-{ re := ↑(x + 1), im := 0 })
⊢ 0 < 1
decide
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (Nat.add x 0 + 1) 1 (Nat.succ y) d
t : 1 * (Nat.add x 0 + 1) * (Nat.add x 0 + 1) = d * Nat.succ y * Nat.succ y := le_antisymm yx xy
⊢ { re := ↑(x + 1), im := -[y+1] } = 0
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (Nat.add x 0 + 1) 1 (Nat.succ y) d
⊢ { re := ↑(x + 1), im := -[y+1] } = 0
let t := le_antisymm yx xy
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (Nat.add x 0 + 1) 1 (Nat.succ y) d
t : (Nat.add x 0 + 1) * (Nat.add x 0 + 1) = d * Nat.succ y * Nat.succ y
⊢ { re := ↑(x + 1), im := -[y+1] } = 0
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (Nat.add x 0 + 1) 1 (Nat.succ y) d
t : 1 * (Nat.add x 0 + 1) * (Nat.add x 0 + 1) = d * Nat.succ y * Nat.succ y := le_antisymm yx xy
⊢ { re := ↑(x + 1), im := -[y+1] } = 0
rw [one_mul] at t
no goals
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (Nat.add x 0 + 1) 1 (Nat.succ y) d
t : (Nat.add x 0 + 1) * (Nat.add x 0 + 1) = d * Nat.succ y * Nat.succ y
⊢ { re := ↑(x + 1), im := -[y+1] } = 0
exact absurd t (not_divides_sq _ _)
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (Nat.add y 0 + 1) d (Nat.succ x) 1
t : 1 * (x + 1) * (x + 1) = d * (y + 1) * (y + 1) := le_antisymm xy yx
⊢ { re := -[x+1], im := ↑(y + 1) } = 0
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (Nat.add y 0 + 1) d (Nat.succ x) 1
⊢ { re := -[x+1], im := ↑(y + 1) } = 0
let t := le_antisymm xy yx
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (Nat.add y 0 + 1) d (Nat.succ x) 1
t : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
⊢ { re := -[x+1], im := ↑(y + 1) } = 0
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (Nat.add y 0 + 1) d (Nat.succ x) 1
t : 1 * (x + 1) * (x + 1) = d * (y + 1) * (y + 1) := le_antisymm xy yx
⊢ { re := -[x+1], im := ↑(y + 1) } = 0
rw [one_mul] at t
no goals
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (Nat.add y 0 + 1) d (Nat.succ x) 1
t : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
⊢ { re := -[x+1], im := ↑(y + 1) } = 0
exact absurd t (not_divides_sq _ _)