Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad

! This file was ported from Lean 3 source module data.int.lemmas
! leanprover-community/mathlib commit 09597669f02422ed388036273d8848119699c22f
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Set.Function
import Mathlib.Data.Int.Order.Lemmas
import Mathlib.Data.Int.Bitwise
import Mathlib.Data.Nat.Cast.Basic
import Mathlib.Data.Nat.Order.Lemmas

/-!
# Miscellaneous lemmas about the integers

This file contains lemmas about integers, which require further imports than
`Data.Int.Basic` or `Data.Int.Order`.

-/


open Nat

namespace Int

theorem 
le_coe_nat_sub: ∀ (m n : ℕ), ↑m - ↑n ≤ ↑(m - n)
le_coe_nat_sub
(m n :
ℕ: Type
ℕ
) : (m - n :
ℤ: Type
ℤ
) ≤ ↑(m - n :
ℕ: Type
ℕ
) :=

Goals accomplished! 🐙
m, n: ℕ


↑m - ↑n ≤ ↑(m - n)
m, n: ℕ

h: m ≥ n


pos
↑m - ↑n ≤ ↑(m - n)
m, n: ℕ

h: ¬m ≥ n


neg
↑m - ↑n ≤ ↑(m - n)
m, n: ℕ


↑m - ↑n ≤ ↑(m - n)
m, n: ℕ

h: m ≥ n


pos
↑m - ↑n ≤ ↑(m - n)
m, n: ℕ

h: m ≥ n


pos
↑m - ↑n ≤ ↑(m - n)
m, n: ℕ

h: ¬m ≥ n


neg
↑m - ↑n ≤ ↑(m - n)

Goals accomplished! 🐙
m, n: ℕ


↑m - ↑n ≤ ↑(m - n)
m, n: ℕ

h: ¬m ≥ n


neg
↑m - ↑n ≤ ↑(m - n)
m, n: ℕ

h: ¬m ≥ n


neg
↑m - ↑n ≤ ↑(m - n)

Goals accomplished! 🐙
#align int.le_coe_nat_sub
Int.le_coe_nat_sub: ∀ (m n : ℕ), ↑m - ↑n ≤ ↑(m - n)
Int.le_coe_nat_sub
/-! ### `succ` and `pred` -/ -- Porting note: simp can prove this @[simp] theorem
succ_coe_nat_pos: ∀ (n : ℕ), 0 < ↑n + 1
succ_coe_nat_pos
(n :
ℕ: Type
ℕ
) :
0: ?m.1564
0
< (n :
ℤ: Type
ℤ
) +
1: ?m.1624
1
:=
lt_add_one_iff: ∀ {a b : ℤ}, a < b + 1 ↔ a ≤ b
lt_add_one_iff
.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
(

Goals accomplished! 🐙

0 ≤ ↑n

Goals accomplished! 🐙
) #align int.succ_coe_nat_pos
Int.succ_coe_nat_pos: ∀ (n : ℕ), 0 < ↑n + 1
Int.succ_coe_nat_pos
/-! ### `natAbs` -/ variable {a b :
ℤ: Type
ℤ
} {n :
ℕ: Type
ℕ
} theorem
natAbs_eq_iff_sq_eq: ∀ {a b : ℤ}, natAbs a = natAbs b ↔ a ^ 2 = b ^ 2
natAbs_eq_iff_sq_eq
{a b :
ℤ: Type
ℤ
} : a.
natAbs: ℤ → ℕ
natAbs
= b.
natAbs: ℤ → ℕ
natAbs
↔ a ^
2: ?m.1981
2
= b ^
2: ?m.1998
2
:=

Goals accomplished! 🐙
a✝, b✝: ℤ

n: ℕ

a, b: ℤ


natAbs a = natAbs b ↔ a ^ 2 = b ^ 2
a✝, b✝: ℤ

n: ℕ

a, b: ℤ


natAbs a = natAbs b ↔ a ^ 2 = b ^ 2
a✝, b✝: ℤ

n: ℕ

a, b: ℤ


natAbs a = natAbs b ↔ a * a = b ^ 2
a✝, b✝: ℤ

n: ℕ

a, b: ℤ


natAbs a = natAbs b ↔ a ^ 2 = b ^ 2
a✝, b✝: ℤ

n: ℕ

a, b: ℤ


natAbs a = natAbs b ↔ a * a = b * b
a✝, b✝: ℤ

n: ℕ

a, b: ℤ


natAbs a = natAbs b ↔ a * a = b * b
a✝, b✝: ℤ

n: ℕ

a, b: ℤ


natAbs a = natAbs b ↔ a ^ 2 = b ^ 2

Goals accomplished! 🐙
#align int.nat_abs_eq_iff_sq_eq
Int.natAbs_eq_iff_sq_eq: ∀ {a b : ℤ}, natAbs a = natAbs b ↔ a ^ 2 = b ^ 2
Int.natAbs_eq_iff_sq_eq
theorem
natAbs_lt_iff_sq_lt: ∀ {a b : ℤ}, natAbs a < natAbs b ↔ a ^ 2 < b ^ 2
natAbs_lt_iff_sq_lt
{a b :
ℤ: Type
ℤ
} : a.
natAbs: ℤ → ℕ
natAbs
< b.
natAbs: ℤ → ℕ
natAbs
↔ a ^
2: ?m.2435
2
< b ^
2: ?m.2452
2
:=

Goals accomplished! 🐙
a✝, b✝: ℤ

n: ℕ

a, b: ℤ


natAbs a < natAbs b ↔ a ^ 2 < b ^ 2
a✝, b✝: ℤ

n: ℕ

a, b: ℤ


natAbs a < natAbs b ↔ a ^ 2 < b ^ 2
a✝, b✝: ℤ

n: ℕ

a, b: ℤ


natAbs a < natAbs b ↔ a * a < b ^ 2
a✝, b✝: ℤ

n: ℕ

a, b: ℤ


natAbs a < natAbs b ↔ a ^ 2 < b ^ 2
a✝, b✝: ℤ

n: ℕ

a, b: ℤ


natAbs a < natAbs b ↔ a * a < b * b
a✝, b✝: ℤ

n: ℕ

a, b: ℤ


natAbs a < natAbs b ↔ a * a < b * b
a✝, b✝: ℤ

n: ℕ

a, b: ℤ


natAbs a < natAbs b ↔ a ^ 2 < b ^ 2

Goals accomplished! 🐙
#align int.nat_abs_lt_iff_sq_lt
Int.natAbs_lt_iff_sq_lt: ∀ {a b : ℤ}, natAbs a < natAbs b ↔ a ^ 2 < b ^ 2
Int.natAbs_lt_iff_sq_lt
theorem
natAbs_le_iff_sq_le: ∀ {a b : ℤ}, natAbs a ≤ natAbs b ↔ a ^ 2 ≤ b ^ 2
natAbs_le_iff_sq_le
{a b :
ℤ: Type
ℤ
} : a.
natAbs: ℤ → ℕ
natAbs
≤ b.
natAbs: ℤ → ℕ
natAbs
↔ a ^
2: ?m.2948
2
≤ b ^
2: ?m.2965
2
:=

Goals accomplished! 🐙
a✝, b✝: ℤ

n: ℕ

a, b: ℤ


a✝, b✝: ℤ

n: ℕ

a, b: ℤ


a✝, b✝: ℤ

n: ℕ

a, b: ℤ


a✝, b✝: ℤ

n: ℕ

a, b: ℤ


a✝, b✝: ℤ

n: ℕ

a, b: ℤ


a✝, b✝: ℤ

n: ℕ

a, b: ℤ


a✝, b✝: ℤ

n: ℕ

a, b: ℤ



Goals accomplished! 🐙
#align int.nat_abs_le_iff_sq_le
Int.natAbs_le_iff_sq_le: ∀ {a b : ℤ}, natAbs a ≤ natAbs b ↔ a ^ 2 ≤ b ^ 2
Int.natAbs_le_iff_sq_le
theorem
natAbs_inj_of_nonneg_of_nonneg: ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → (natAbs a = natAbs b ↔ a = b)
natAbs_inj_of_nonneg_of_nonneg
{a b :
ℤ: Type
ℤ
} (
ha: 0 ≤ a
ha
:
0: ?m.3462
0
≤ a) (
hb: 0 ≤ b
hb
:
0: ?m.3499
0
≤ b) :
natAbs: ℤ → ℕ
natAbs
a =
natAbs: ℤ → ℕ
natAbs
b ↔ a = b :=

Goals accomplished! 🐙
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: 0 ≤ a

hb: 0 ≤ b


a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: 0 ≤ a

hb: 0 ≤ b


a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: 0 ≤ a

hb: 0 ≤ b


natAbs a = natAbs b ↔ a ^ 2 = b ^ 2
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: 0 ≤ a

hb: 0 ≤ b


a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: 0 ≤ a

hb: 0 ≤ b



Goals accomplished! 🐙
#align int.nat_abs_inj_of_nonneg_of_nonneg
Int.natAbs_inj_of_nonneg_of_nonneg: ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → (natAbs a = natAbs b ↔ a = b)
Int.natAbs_inj_of_nonneg_of_nonneg
theorem
natAbs_inj_of_nonpos_of_nonpos: ∀ {a b : ℤ}, a ≤ 0 → b ≤ 0 → (natAbs a = natAbs b ↔ a = b)
natAbs_inj_of_nonpos_of_nonpos
{a b :
ℤ: Type
ℤ
} (
ha: a ≤ 0
ha
: a ≤
0: ?m.3661
0
) (
hb: b ≤ 0
hb
: b ≤
0: ?m.3693
0
) :
natAbs: ℤ → ℕ
natAbs
a =
natAbs: ℤ → ℕ
natAbs
b ↔ a = b :=

Goals accomplished! 🐙
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: a ≤ 0

hb: b ≤ 0



Goals accomplished! 🐙
#align int.nat_abs_inj_of_nonpos_of_nonpos
Int.natAbs_inj_of_nonpos_of_nonpos: ∀ {a b : ℤ}, a ≤ 0 → b ≤ 0 → (natAbs a = natAbs b ↔ a = b)
Int.natAbs_inj_of_nonpos_of_nonpos
theorem
natAbs_inj_of_nonneg_of_nonpos: ∀ {a b : ℤ}, 0 ≤ a → b ≤ 0 → (natAbs a = natAbs b ↔ a = -b)
natAbs_inj_of_nonneg_of_nonpos
{a b :
ℤ: Type
ℤ
} (
ha: 0 ≤ a
ha
:
0: ?m.4076
0
≤ a) (
hb: b ≤ 0
hb
: b ≤
0: ?m.4113
0
) :
natAbs: ℤ → ℕ
natAbs
a =
natAbs: ℤ → ℕ
natAbs
b ↔ a = -b :=

Goals accomplished! 🐙
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: 0 ≤ a

hb: b ≤ 0



Goals accomplished! 🐙
#align int.nat_abs_inj_of_nonneg_of_nonpos
Int.natAbs_inj_of_nonneg_of_nonpos: ∀ {a b : ℤ}, 0 ≤ a → b ≤ 0 → (natAbs a = natAbs b ↔ a = -b)
Int.natAbs_inj_of_nonneg_of_nonpos
theorem
natAbs_inj_of_nonpos_of_nonneg: ∀ {a b : ℤ}, a ≤ 0 → 0 ≤ b → (natAbs a = natAbs b ↔ -a = b)
natAbs_inj_of_nonpos_of_nonneg
{a b :
ℤ: Type
ℤ
} (
ha: a ≤ 0
ha
: a ≤
0: ?m.4391
0
) (
hb: 0 ≤ b
hb
:
0: ?m.4423
0
≤ b) :
natAbs: ℤ → ℕ
natAbs
a =
natAbs: ℤ → ℕ
natAbs
b ↔ -a = b :=

Goals accomplished! 🐙
a✝, b✝: ℤ

n: ℕ

a, b: ℤ

ha: a ≤ 0

hb: 0 ≤ b



Goals accomplished! 🐙
#align int.nat_abs_inj_of_nonpos_of_nonneg
Int.natAbs_inj_of_nonpos_of_nonneg: ∀ {a b : ℤ}, a ≤ 0 → 0 ≤ b → (natAbs a = natAbs b ↔ -a = b)
Int.natAbs_inj_of_nonpos_of_nonneg
section Intervals open Set theorem
strictMonoOn_natAbs: StrictMonoOn natAbs (Ici 0)
strictMonoOn_natAbs
:
StrictMonoOn: {α : Type ?u.4705} → {β : Type ?u.4704} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → Prop
StrictMonoOn
natAbs: ℤ → ℕ
natAbs
(
Ici: {α : Type ?u.4753} → [inst : Preorder α] → α → Set α
Ici
0: ?m.4779
0
) := fun
_: ?m.4869
_
ha: ?m.4872
ha
_: ?m.4875
_
_: ?m.4878
_
hab: ?m.4881
hab
=>
natAbs_lt_natAbs_of_nonneg_of_lt: ∀ {a b : ℤ}, 0 ≤ a → a < b → natAbs a < natAbs b
natAbs_lt_natAbs_of_nonneg_of_lt
ha: ?m.4872
ha
hab: ?m.4881
hab
#align int.strict_mono_on_nat_abs
Int.strictMonoOn_natAbs: StrictMonoOn natAbs (Ici 0)
Int.strictMonoOn_natAbs
theorem
strictAntiOn_natAbs: StrictAntiOn natAbs (Iic 0)
strictAntiOn_natAbs
:
StrictAntiOn: {α : Type ?u.4915} → {β : Type ?u.4914} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Set α → Prop
StrictAntiOn
natAbs: ℤ → ℕ
natAbs
(
Iic: {α : Type ?u.4963} → [inst : Preorder α] → α → Set α
Iic
0: ?m.4989
0
) := fun
a: ?m.5079
a
_: ?m.5082
_
b: ?m.5085
b
hb: ?m.5088
hb
hab: ?m.5091
hab
=>

Goals accomplished! 🐙
a✝, b✝: ℤ

n: ℕ

a: ℤ

x✝: a ∈ Iic 0

b: ℤ

hb: b ∈ Iic 0

hab: a < b



Goals accomplished! 🐙
#align int.strict_anti_on_nat_abs
Int.strictAntiOn_natAbs: StrictAntiOn natAbs (Iic 0)
Int.strictAntiOn_natAbs
theorem
injOn_natAbs_Ici: InjOn natAbs (Ici 0)
injOn_natAbs_Ici
:
InjOn: {α : Type ?u.6773} → {β : Type ?u.6772} → (α → β) → Set α → Prop
InjOn
natAbs: ℤ → ℕ
natAbs
(
Ici: {α : Type ?u.6779} → [inst : Preorder α] → α → Set α
Ici
0: ?m.6805
0
) :=
strictMonoOn_natAbs: StrictMonoOn natAbs (Ici 0)
strictMonoOn_natAbs
.
injOn: ∀ {α : Type ?u.6854} {β : Type ?u.6855} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α}, StrictMonoOn f s → InjOn f s
injOn
#align int.inj_on_nat_abs_Ici
Int.injOn_natAbs_Ici: InjOn natAbs (Ici 0)
Int.injOn_natAbs_Ici
theorem
injOn_natAbs_Iic: InjOn natAbs (Iic 0)
injOn_natAbs_Iic
:
InjOn: {α : Type ?u.6957} → {β : Type ?u.6956} → (α → β) → Set α → Prop
InjOn
natAbs: ℤ → ℕ
natAbs
(
Iic: {α : Type ?u.6963} → [inst : Preorder α] → α → Set α
Iic
0: ?m.6989
0
) :=
strictAntiOn_natAbs: StrictAntiOn natAbs (Iic 0)
strictAntiOn_natAbs
.
injOn: ∀ {α : Type ?u.7038} {β : Type ?u.7039} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α}, StrictAntiOn f s → InjOn f s
injOn
#align int.inj_on_nat_abs_Iic
Int.injOn_natAbs_Iic: InjOn natAbs (Iic 0)
Int.injOn_natAbs_Iic
end Intervals /-! ### `toNat` -/ theorem
toNat_of_nonpos: ∀ {z : ℤ}, z ≤ 0 → toNat z = 0
toNat_of_nonpos
: ∀ {z :
ℤ: Type
ℤ
}, z ≤
0: ?m.7146
0
→ z.
toNat: ℤ → ℕ
toNat
=
0: ?m.7178
0
| 0, _ =>
rfl: ∀ {α : Sort ?u.7219} {a : α}, a = a
rfl
| (n + 1 : ℕ),
h: ↑(n + 1) ≤ 0
h
=> (
h: ↑(n + 1) ≤ 0
h
.
not_lt: ∀ {α : Type ?u.7366} [inst : Preorder α] {a b : α}, a ≤ b → ¬b < a
not_lt
(

Goals accomplished! 🐙
a, b: ℤ

n✝, n: ℕ

h: ↑(n + 1) ≤ 0


0 < ↑(n + 1)

Goals accomplished! 🐙
)).
elim: ∀ {C : Sort ?u.7423}, False → C
elim
| -[n+1], _ =>
rfl: ∀ {α : Sort ?u.7445} {a : α}, a = a
rfl
#align int.to_nat_of_nonpos
Int.toNat_of_nonpos: ∀ {z : ℤ}, z ≤ 0 → toNat z = 0
Int.toNat_of_nonpos
/-! ### bitwise ops This lemma is orphaned from `Data.Int.Bitwise` as it also requires material from `Data.Int.Order`. -/ attribute [local simp]
Int.zero_div: ∀ (b : ℤ), div 0 b = 0
Int.zero_div
@[simp] theorem
div2_bit: ∀ (b : Bool) (n : ℤ), div2 (bit b n) = n
div2_bit
(
b: Bool
b
n: ?m.8026
n
) :
div2: ℤ → ℤ
div2
(
bit: Bool → ℤ → ℤ
bit
b: ?m.8023
b
n: ?m.8026
n
) =
n: ?m.8026
n
:=

Goals accomplished! 🐙
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


div2 (bit b n) = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


div2 (bit b n) = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


div2 (2 * n + bif b then 1 else 0) = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


div2 (bit b n) = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


(2 * n + bif b then 1 else 0) / 2 = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


div2 (bit b n) = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


((bif b then 1 else 0) + 2 * n) / 2 = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


div2 (bit b n) = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


(bif b then 1 else 0) / 2 + n = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


H
2 ≠ 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


div2 (bit b n) = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


0 + n = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


(bif b then 1 else 0) / 2 = 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


H
2 ≠ 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


div2 (bit b n) = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


n = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


(bif b then 1 else 0) / 2 = 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


H
2 ≠ 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


(bif b then 1 else 0) / 2 = 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


H
2 ≠ 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


div2 (bit b n) = n
a, b: ℤ

n✝: ℕ

n: ℤ


false
(bif false then 1 else 0) / 2 = 0
a, b: ℤ

n✝: ℕ

n: ℤ


true
(bif true then 1 else 0) / 2 = 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


H
2 ≠ 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


div2 (bit b n) = n
a, b: ℤ

n✝: ℕ

n: ℤ


false
(bif false then 1 else 0) / 2 = 0
a, b: ℤ

n✝: ℕ

n: ℤ


false
(bif false then 1 else 0) / 2 = 0
a, b: ℤ

n✝: ℕ

n: ℤ


true
(bif true then 1 else 0) / 2 = 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


H
2 ≠ 0

Goals accomplished! 🐙
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


div2 (bit b n) = n
a, b: ℤ

n✝: ℕ

n: ℤ


true
(bif true then 1 else 0) / 2 = 0
a, b: ℤ

n✝: ℕ

n: ℤ


true
(bif true then 1 else 0) / 2 = 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


H
2 ≠ 0
a, b: ℤ

n✝: ℕ

n: ℤ


true
ofNat (1 / 2) = 0
a, b: ℤ

n✝: ℕ

n: ℤ


true
(bif true then 1 else 0) / 2 = 0
a, b: ℤ

n✝: ℕ

n: ℤ


true
ofNat (1 / 2) = 0
a, b: ℤ

n✝: ℕ

n: ℤ


true
ofNat 0 = 0
a, b: ℤ

n✝: ℕ

n: ℤ


true
1 < 2
a, b: ℤ

n✝: ℕ

n: ℤ


true
ofNat 0 = 0
a, b: ℤ

n✝: ℕ

n: ℤ


true
1 < 2
a, b: ℤ

n✝: ℕ

n: ℤ


true
ofNat (1 / 2) = 0
a, b: ℤ

n✝: ℕ

n: ℤ


true
ofNat 0 = 0
a, b: ℤ

n✝: ℕ

n: ℤ


true
1 < 2
a, b: ℤ

n✝: ℕ

n: ℤ


true
ofNat (1 / 2) = 0

Goals accomplished! 🐙
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


div2 (bit b n) = n
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


H
2 ≠ 0
a, b✝: ℤ

n✝: ℕ

b: Bool

n: ℤ


H
2 ≠ 0

Goals accomplished! 🐙
#align int.div2_bit
Int.div2_bit: ∀ (b : Bool) (n : ℤ), div2 (bit b n) = n
Int.div2_bit
end Int