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) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro

! This file was ported from Lean 3 source module data.nat.prime
! leanprover-community/mathlib commit 8631e2d5ea77f6c13054d9151d82b83069680cb1
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Associated
import Mathlib.Algebra.Parity
import Mathlib.Data.Int.Dvd.Basic
import Mathlib.Data.Int.Units
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Data.Nat.Sqrt
import Mathlib.Order.Bounds.Basic

/-!
# Prime numbers

This file deals with prime numbers: natural numbers `p β‰₯ 2` whose only divisors are `p` and `1`.

## Important declarations

- `Nat.Prime`: the predicate that expresses that a natural number `p` is prime
- `Nat.Primes`: the subtype of natural numbers that are prime
- `Nat.minFac n`: the minimal prime factor of a natural number `n β‰  1`
- `Nat.exists_infinite_primes`: Euclid's theorem that there exist infinitely many prime numbers.
  This also appears as `Nat.not_bddAbove_setOf_prime` and `Nat.infinite_setOf_prime` (the latter
  in `Data.Nat.PrimeFin`).
- `Nat.prime_iff`: `Nat.Prime` coincides with the general definition of `Prime`
- `Nat.irreducible_iff_nat_prime`: a non-unit natural number is
                                  only divisible by `1` iff it is prime

-/


open Bool Subtype

open Nat

namespace Nat

/-- `Nat.Prime p` means that `p` is a prime number, that is, a natural number
  at least 2 whose only divisors are `p` and `1`. -/
-- Porting note: removed @[pp_nodot]
def 
Prime: (p : β„•) β†’ ?m.5 p
Prime
(p :
β„•: Type
β„•
) :=
Irreducible: {Ξ± : Type ?u.8} β†’ [inst : Monoid Ξ±] β†’ Ξ± β†’ Prop
Irreducible
p #align nat.prime
Nat.Prime: β„• β†’ Prop
Nat.Prime
theorem
irreducible_iff_nat_prime: βˆ€ (a : β„•), Irreducible a ↔ Prime a
irreducible_iff_nat_prime
(a :
β„•: Type
β„•
) :
Irreducible: {Ξ± : Type ?u.44} β†’ [inst : Monoid Ξ±] β†’ Ξ± β†’ Prop
Irreducible
a ↔
Nat.Prime: β„• β†’ Prop
Nat.Prime
a :=
Iff.rfl: βˆ€ {a : Prop}, a ↔ a
Iff.rfl
#align irreducible_iff_nat_prime
Nat.irreducible_iff_nat_prime: βˆ€ (a : β„•), Irreducible a ↔ Prime a
Nat.irreducible_iff_nat_prime
theorem
not_prime_zero: Β¬Prime 0
not_prime_zero
: Β¬
Prime: β„• β†’ Prop
Prime
0: ?m.62
0
|
h: ?m.77
h
=>
h: ?m.77
h
.
ne_zero: βˆ€ {Ξ± : Type ?u.79} [inst : MonoidWithZero Ξ±] {p : Ξ±}, Irreducible p β†’ p β‰  0
ne_zero
rfl: βˆ€ {Ξ± : Sort ?u.130} {a : Ξ±}, a = a
rfl
#align nat.not_prime_zero
Nat.not_prime_zero: Β¬Prime 0
Nat.not_prime_zero
theorem
not_prime_one: Β¬Prime 1
not_prime_one
: Β¬
Prime: β„• β†’ Prop
Prime
1: ?m.143
1
|
h: ?m.158
h
=>
h: ?m.158
h
.
ne_one: βˆ€ {Ξ± : Type ?u.160} [inst : Monoid Ξ±] {p : Ξ±}, Irreducible p β†’ p β‰  1
ne_one
rfl: βˆ€ {Ξ± : Sort ?u.179} {a : Ξ±}, a = a
rfl
#align nat.not_prime_one
Nat.not_prime_one: Β¬Prime 1
Nat.not_prime_one
theorem
Prime.ne_zero: βˆ€ {n : β„•}, Prime n β†’ n β‰  0
Prime.ne_zero
{n :
β„•: Type
β„•
} (
h: Prime n
h
:
Prime: β„• β†’ Prop
Prime
n) : n β‰ 
0: ?m.198
0
:=
Irreducible.ne_zero: βˆ€ {Ξ± : Type ?u.213} [inst : MonoidWithZero Ξ±] {p : Ξ±}, Irreducible p β†’ p β‰  0
Irreducible.ne_zero
h: Prime n
h
#align nat.prime.ne_zero
Nat.Prime.ne_zero: βˆ€ {n : β„•}, Prime n β†’ n β‰  0
Nat.Prime.ne_zero
theorem
Prime.pos: βˆ€ {p : β„•}, Prime p β†’ 0 < p
Prime.pos
{p :
β„•: Type
β„•
} (
pp: Prime p
pp
:
Prime: β„• β†’ Prop
Prime
p) :
0: ?m.291
0
< p :=
Nat.pos_of_ne_zero: βˆ€ {n : β„•}, n β‰  0 β†’ 0 < n
Nat.pos_of_ne_zero
pp: Prime p
pp
.
ne_zero: βˆ€ {n : β„•}, Prime n β†’ n β‰  0
ne_zero
#align nat.prime.pos
Nat.Prime.pos: βˆ€ {p : β„•}, Prime p β†’ 0 < p
Nat.Prime.pos
theorem
Prime.two_le: βˆ€ {p : β„•}, Prime p β†’ 2 ≀ p
Prime.two_le
: βˆ€ {p :
β„•: Type
β„•
},
Prime: β„• β†’ Prop
Prime
p β†’
2: ?m.353
2
≀ p | 0,
h: Prime 0
h
=> (
not_prime_zero: Β¬Prime 0
not_prime_zero
h: Prime 0
h
).
elim: βˆ€ {C : Sort ?u.412}, False β†’ C
elim
| 1,
h: Prime 1
h
=> (
not_prime_one: Β¬Prime 1
not_prime_one
h: Prime 1
h
).
elim: βˆ€ {C : Sort ?u.436}, False β†’ C
elim
| _ + 2, _ =>
le_add_self: βˆ€ {Ξ± : Type ?u.528} [inst : CanonicallyOrderedAddMonoid Ξ±] {a b : Ξ±}, a ≀ b + a
le_add_self
#align nat.prime.two_le
Nat.Prime.two_le: βˆ€ {p : β„•}, Prime p β†’ 2 ≀ p
Nat.Prime.two_le
theorem
Prime.one_lt: βˆ€ {p : β„•}, Prime p β†’ 1 < p
Prime.one_lt
{p :
β„•: Type
β„•
} :
Prime: β„• β†’ Prop
Prime
p β†’
1: ?m.722
1
< p :=
Prime.two_le: βˆ€ {p : β„•}, Prime p β†’ 2 ≀ p
Prime.two_le
#align nat.prime.one_lt
Nat.Prime.one_lt: βˆ€ {p : β„•}, Prime p β†’ 1 < p
Nat.Prime.one_lt
instance
Prime.one_lt': βˆ€ (p : β„•) [hp : Fact (Prime p)], Fact (1 < p)
Prime.one_lt'
(p :
β„•: Type
β„•
) [
hp: Fact (Prime p)
hp
:
Fact: Prop β†’ Prop
Fact
p.
Prime: β„• β†’ Prop
Prime
] :
Fact: Prop β†’ Prop
Fact
(
1: ?m.775
1
< p) := ⟨
hp: Fact (Prime p)
hp
.
1: βˆ€ {p : Prop} [self : Fact p], p
1
.
one_lt: βˆ€ {p : β„•}, Prime p β†’ 1 < p
one_lt
⟩ #align nat.prime.one_lt'
Nat.Prime.one_lt': βˆ€ (p : β„•) [hp : Fact (Prime p)], Fact (1 < p)
Nat.Prime.one_lt'
theorem
Prime.ne_one: βˆ€ {p : β„•}, Prime p β†’ p β‰  1
Prime.ne_one
{p :
β„•: Type
β„•
} (
hp: Prime p
hp
: p.
Prime: β„• β†’ Prop
Prime
) : p β‰ 
1: ?m.849
1
:=
hp: Prime p
hp
.
one_lt: βˆ€ {p : β„•}, Prime p β†’ 1 < p
one_lt
.
ne': βˆ€ {Ξ± : Type ?u.866} [inst : Preorder Ξ±] {x y : Ξ±}, x < y β†’ y β‰  x
ne'
#align nat.prime.ne_one
Nat.Prime.ne_one: βˆ€ {p : β„•}, Prime p β†’ p β‰  1
Nat.Prime.ne_one
theorem
Prime.eq_one_or_self_of_dvd: βˆ€ {p : β„•}, Prime p β†’ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p
Prime.eq_one_or_self_of_dvd
{p :
β„•: Type
β„•
} (
pp: Prime p
pp
: p.
Prime: β„• β†’ Prop
Prime
) (m :
β„•: Type
β„•
) (
hm: m ∣ p
hm
: m ∣ p) : m =
1: ?m.955
1
∨ m = p :=

Goals accomplished! πŸ™
p: β„•

pp: Prime p

m: β„•

hm: m ∣ p


m = 1 ∨ m = p
p: β„•

pp: Prime p

m, n: β„•

hn: p = m * n


intro
m = 1 ∨ m = p
p: β„•

pp: Prime p

m: β„•

hm: m ∣ p


m = 1 ∨ m = p
p: β„•

pp: Prime p

m, n: β„•

hn: p = m * n

this: IsUnit m ∨ IsUnit n


intro
m = 1 ∨ m = p
p: β„•

pp: Prime p

m: β„•

hm: m ∣ p


m = 1 ∨ m = p
p: β„•

pp: Prime p

m, n: β„•

hn: p = m * n

this: IsUnit m ∨ IsUnit n


intro
m = 1 ∨ m = p
p: β„•

pp: Prime p

m, n: β„•

hn: p = m * n

this: m = 1 ∨ IsUnit n


intro
m = 1 ∨ m = p
p: β„•

pp: Prime p

m, n: β„•

hn: p = m * n

this: IsUnit m ∨ IsUnit n


intro
m = 1 ∨ m = p
p: β„•

pp: Prime p

m, n: β„•

hn: p = m * n

this: m = 1 ∨ n = 1


intro
m = 1 ∨ m = p
p: β„•

pp: Prime p

m, n: β„•

hn: p = m * n

this: m = 1 ∨ n = 1


intro
m = 1 ∨ m = p
p: β„•

pp: Prime p

m, n: β„•

hn: p = m * n

this: m = 1 ∨ n = 1


intro
m = 1 ∨ m = p
p: β„•

pp: Prime p

m: β„•

hm: m ∣ p


m = 1 ∨ m = p
p: β„•

pp: Prime p

m, n: β„•

hn: p = m * n

this: m = 1 ∨ n = 1


n = 1 β†’ m = p
p: β„•

pp: Prime p

m: β„•

hm: m ∣ p


m = 1 ∨ m = p
p: β„•

pp: Prime p

m: β„•

hn: p = m * 1

this: m = 1 ∨ 1 = 1


m = p
p: β„•

pp: Prime p

m: β„•

hm: m ∣ p


m = 1 ∨ m = p
p: β„•

pp: Prime p

m: β„•

hn: p = m * 1

this: m = 1 ∨ 1 = 1


m = p
p: β„•

pp: Prime p

m: β„•

hn: p = m * 1

this: m = 1 ∨ 1 = 1


m = m * 1
p: β„•

pp: Prime p

m: β„•

hn: p = m * 1

this: m = 1 ∨ 1 = 1


m = p
p: β„•

pp: Prime p

m: β„•

hn: p = m * 1

this: m = 1 ∨ 1 = 1


m = m

Goals accomplished! πŸ™
#align nat.prime.eq_one_or_self_of_dvd
Nat.Prime.eq_one_or_self_of_dvd: βˆ€ {p : β„•}, Prime p β†’ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p
Nat.Prime.eq_one_or_self_of_dvd
theorem
prime_def_lt'': βˆ€ {p : β„•}, Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p
prime_def_lt''
{p :
β„•: Type
β„•
} :
Prime: β„• β†’ Prop
Prime
p ↔
2: ?m.1212
2
≀ p ∧ βˆ€ (
m: ?m.1242
m
) (
_: m ∣ p
_
:
m: ?m.1242
m
∣ p),
m: ?m.1242
m
=
1: ?m.1258
1
∨
m: ?m.1242
m
= p :=

Goals accomplished! πŸ™

Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p



Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p

h1: 1 < p



Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p

h1: 1 < p

a, b: β„•

hab: p = a * b



Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p

h1: 1 < p

a, b: β„•

hab: p = a * b


a = 1 ∨ b = 1

Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p

h1: 1 < p

a, b: β„•

hab: p = a * b


a = p β†’ b = 1
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p

h1: 1 < p

a, b: β„•

hab: p = a * b


a ∣ p

Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p

h1: 1 < p

a, b: β„•

hab: p = a * b


a = p β†’ b = 1
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p

h1: 1 < p

a, b: β„•

hab: p = a * b


a = p β†’ b = 1
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p

h1: 1 < p

a, b: β„•

hab: p = a * b


a ∣ p
a, b: β„•

h: 2 ≀ a ∧ βˆ€ (m : β„•), m ∣ a β†’ m = 1 ∨ m = a

h1: 1 < a

hab: a = a * b


b = 1
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p

h1: 1 < p

a, b: β„•

hab: p = a * b


a = p β†’ b = 1
a, b: β„•

h: 2 ≀ a ∧ βˆ€ (m : β„•), m ∣ a β†’ m = 1 ∨ m = a

h1: 1 < a

hab: a = a * b


b = 1
a, b: β„•

h: 2 ≀ a ∧ βˆ€ (m : β„•), m ∣ a β†’ m = 1 ∨ m = a

h1: 1 < a

hab: a = a * b


a * b = a * 1
a, b: β„•

h: 2 ≀ a ∧ βˆ€ (m : β„•), m ∣ a β†’ m = 1 ∨ m = a

h1: 1 < a

hab: a = a * b


b = 1
a, b: β„•

h: 2 ≀ a ∧ βˆ€ (m : β„•), m ∣ a β†’ m = 1 ∨ m = a

h1: 1 < a

hab: a = a * b


a = a * 1
a, b: β„•

h: 2 ≀ a ∧ βˆ€ (m : β„•), m ∣ a β†’ m = 1 ∨ m = a

h1: 1 < a

hab: a = a * b


b = 1
a, b: β„•

h: 2 ≀ a ∧ βˆ€ (m : β„•), m ∣ a β†’ m = 1 ∨ m = a

h1: 1 < a

hab: a = a * b


a = a

Goals accomplished! πŸ™

Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p

h1: 1 < p

a, b: β„•

hab: p = a * b


a ∣ p
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p

h1: 1 < p

a, b: β„•

hab: p = a * b


a ∣ p
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p

h1: 1 < p

a, b: β„•

hab: p = a * b


a ∣ p
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p

h1: 1 < p

a, b: β„•

hab: p = a * b


a ∣ a * b
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p

h1: 1 < p

a, b: β„•

hab: p = a * b


a ∣ a * b
p: β„•

h: 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p

h1: 1 < p

a, b: β„•

hab: p = a * b


a ∣ p

Goals accomplished! πŸ™
#align nat.prime_def_lt''
Nat.prime_def_lt'': βˆ€ {p : β„•}, Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p
Nat.prime_def_lt''
theorem
prime_def_lt: βˆ€ {p : β„•}, Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), m < p β†’ m ∣ p β†’ m = 1
prime_def_lt
{p :
β„•: Type
β„•
} :
Prime: β„• β†’ Prop
Prime
p ↔
2: ?m.2274
2
≀ p ∧ βˆ€
m: ?m.2304
m
< p,
m: ?m.2304
m
∣ p β†’
m: ?m.2304
m
=
1: ?m.2328
1
:=
prime_def_lt'': βˆ€ {p : β„•}, Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p
prime_def_lt''
.
trans: βˆ€ {a b c : Prop}, (a ↔ b) β†’ (b ↔ c) β†’ (a ↔ c)
trans
<|
and_congr_right: βˆ€ {a b c : Prop}, (a β†’ (b ↔ c)) β†’ (a ∧ b ↔ a ∧ c)
and_congr_right
fun
p2: ?m.2376
p2
=>
forall_congr': βˆ€ {Ξ± : Sort ?u.2378} {p q : Ξ± β†’ Prop}, (βˆ€ (a : Ξ±), p a ↔ q a) β†’ ((βˆ€ (a : Ξ±), p a) ↔ βˆ€ (a : Ξ±), q a)
forall_congr'
fun
_: ?m.2392
_
=> ⟨fun
h: ?m.2404
h
l: ?m.2407
l
d: ?m.2410
d
=> (
h: ?m.2404
h
d: ?m.2410
d
).
resolve_right: βˆ€ {a b : Prop}, a ∨ b β†’ Β¬b β†’ a
resolve_right
(
ne_of_lt: βˆ€ {a b : β„•}, a < b β†’ a β‰  b
ne_of_lt
l: ?m.2407
l
), fun
h: ?m.2433
h
d: ?m.2436
d
=> (
le_of_dvd: βˆ€ {m n : β„•}, 0 < n β†’ m ∣ n β†’ m ≀ n
le_of_dvd
(
le_of_succ_le: βˆ€ {n m : β„•}, succ n ≀ m β†’ n ≀ m
le_of_succ_le
p2: ?m.2376
p2
)
d: ?m.2436
d
).
lt_or_eq_dec: βˆ€ {Ξ± : Type ?u.2452} [inst : PartialOrder Ξ±] [inst_1 : DecidableRel fun x x_1 => x ≀ x_1] {a b : Ξ±}, a ≀ b β†’ a < b ∨ a = b
lt_or_eq_dec
.
imp_left: βˆ€ {a b c : Prop}, (a β†’ b) β†’ a ∨ c β†’ b ∨ c
imp_left
fun
l: ?m.2546
l
=>
h: ?m.2433
h
l: ?m.2546
l
d: ?m.2436
d
⟩ #align nat.prime_def_lt
Nat.prime_def_lt: βˆ€ {p : β„•}, Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), m < p β†’ m ∣ p β†’ m = 1
Nat.prime_def_lt
theorem
prime_def_lt': βˆ€ {p : β„•}, Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), 2 ≀ m β†’ m < p β†’ Β¬m ∣ p
prime_def_lt'
{p :
β„•: Type
β„•
} :
Prime: β„• β†’ Prop
Prime
p ↔
2: ?m.2586
2
≀ p ∧ βˆ€
m: ?m.2616
m
,
2: ?m.2622
2
≀
m: ?m.2616
m
β†’
m: ?m.2616
m
< p β†’ Β¬
m: ?m.2616
m
∣ p :=
prime_def_lt: βˆ€ {p : β„•}, Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), m < p β†’ m ∣ p β†’ m = 1
prime_def_lt
.
trans: βˆ€ {a b c : Prop}, (a ↔ b) β†’ (b ↔ c) β†’ (a ↔ c)
trans
<|
and_congr_right: βˆ€ {a b c : Prop}, (a β†’ (b ↔ c)) β†’ (a ∧ b ↔ a ∧ c)
and_congr_right
fun
p2: ?m.2745
p2
=>
forall_congr': βˆ€ {Ξ± : Sort ?u.2747} {p q : Ξ± β†’ Prop}, (βˆ€ (a : Ξ±), p a ↔ q a) β†’ ((βˆ€ (a : Ξ±), p a) ↔ βˆ€ (a : Ξ±), q a)
forall_congr'
fun
m: ?m.2762
m
=> ⟨fun
h: ?m.2775
h
m2: ?m.2778
m2
l: ?m.2781
l
d: ?m.2784
d
=>
not_lt_of_ge: βˆ€ {Ξ± : Type ?u.2786} [inst : Preorder Ξ±] {a b : Ξ±}, a β‰₯ b β†’ Β¬a < b
not_lt_of_ge
m2: ?m.2778
m2
((
h: ?m.2775
h
l: ?m.2781
l
d: ?m.2784
d
).
symm: βˆ€ {Ξ± : Sort ?u.2842} {a b : Ξ±}, a = b β†’ b = a
symm
β–Έ

Goals accomplished! πŸ™
p: β„•

p2: 2 ≀ p

m: β„•

h: m < p β†’ m ∣ p β†’ m = 1

m2: 2 ≀ m

l: m < p

d: m ∣ p


1 < 2

Goals accomplished! πŸ™
), fun
h: ?m.2869
h
l: ?m.2874
l
d: ?m.2877
d
=>

Goals accomplished! πŸ™
p: β„•

p2: 2 ≀ p

m: β„•

h: 2 ≀ m β†’ m < p β†’ Β¬m ∣ p

l: m < p

d: m ∣ p


m = 1
p: β„•

p2: 2 ≀ p

h: 2 ≀ zero β†’ zero < p β†’ Β¬zero ∣ p

l: zero < p

d: zero ∣ p


zero
p: β„•

p2: 2 ≀ p

h: 2 ≀ succ zero β†’ succ zero < p β†’ Β¬succ zero ∣ p

l: succ zero < p

d: succ zero ∣ p


succ.zero
p: β„•

p2: 2 ≀ p

m: β„•

h: 2 ≀ succ (succ m) β†’ succ (succ m) < p β†’ Β¬succ (succ m) ∣ p

l: succ (succ m) < p

d: succ (succ m) ∣ p


succ.succ
succ (succ m) = 1
p: β„•

p2: 2 ≀ p

m: β„•

h: 2 ≀ m β†’ m < p β†’ Β¬m ∣ p

l: m < p

d: m ∣ p


m = 1
p: β„•

p2: 2 ≀ p

h: 2 ≀ zero β†’ zero < p β†’ Β¬zero ∣ p

l: zero < p

d: zero ∣ p


zero
p: β„•

p2: 2 ≀ p

h: 2 ≀ zero β†’ zero < p β†’ Β¬zero ∣ p

l: zero < p

d: zero ∣ p


zero
p: β„•

p2: 2 ≀ p

h: 2 ≀ succ zero β†’ succ zero < p β†’ Β¬succ zero ∣ p

l: succ zero < p

d: succ zero ∣ p


succ.zero
p: β„•

p2: 2 ≀ p

m: β„•

h: 2 ≀ succ (succ m) β†’ succ (succ m) < p β†’ Β¬succ (succ m) ∣ p

l: succ (succ m) < p

d: succ (succ m) ∣ p


succ.succ
succ (succ m) = 1
p: β„•

p2: 2 ≀ p

h: 2 ≀ zero β†’ zero < p β†’ Β¬zero ∣ p

l: zero < p

d: zero ∣ p


zero
p: β„•

p2: 2 ≀ 0

h: 2 ≀ zero β†’ zero < p β†’ Β¬zero ∣ p

l: zero < p

d: zero ∣ p


zero
p: β„•

p2: 2 ≀ 0

h: 2 ≀ zero β†’ zero < p β†’ Β¬zero ∣ p

l: zero < p

d: zero ∣ p


zero
p: β„•

p2: 2 ≀ 0

h: 2 ≀ zero β†’ zero < p β†’ Β¬zero ∣ p

l: zero < p

d: zero ∣ p


zero
p: β„•

p2: 2 ≀ p

h: 2 ≀ zero β†’ zero < p β†’ Β¬zero ∣ p

l: zero < p

d: zero ∣ p


zero
p: β„•

h: 2 ≀ zero β†’ zero < p β†’ Β¬zero ∣ p

l: zero < p

d: zero ∣ p


zero
2 ≀ 0 β†’ zero = 1
p: β„•

p2: 2 ≀ p

h: 2 ≀ zero β†’ zero < p β†’ Β¬zero ∣ p

l: zero < p

d: zero ∣ p


zero

Goals accomplished! πŸ™
p: β„•

p2: 2 ≀ p

m: β„•

h: 2 ≀ m β†’ m < p β†’ Β¬m ∣ p

l: m < p

d: m ∣ p


m = 1
p: β„•

p2: 2 ≀ p

h: 2 ≀ succ zero β†’ succ zero < p β†’ Β¬succ zero ∣ p

l: succ zero < p

d: succ zero ∣ p


succ.zero
p: β„•

p2: 2 ≀ p

h: 2 ≀ succ zero β†’ succ zero < p β†’ Β¬succ zero ∣ p

l: succ zero < p

d: succ zero ∣ p


succ.zero
p: β„•

p2: 2 ≀ p

m: β„•

h: 2 ≀ succ (succ m) β†’ succ (succ m) < p β†’ Β¬succ (succ m) ∣ p

l: succ (succ m) < p

d: succ (succ m) ∣ p


succ.succ
succ (succ m) = 1

Goals accomplished! πŸ™
p: β„•

p2: 2 ≀ p

m: β„•

h: 2 ≀ m β†’ m < p β†’ Β¬m ∣ p

l: m < p

d: m ∣ p


m = 1
p: β„•

p2: 2 ≀ p

m: β„•

h: 2 ≀ succ (succ m) β†’ succ (succ m) < p β†’ Β¬succ (succ m) ∣ p

l: succ (succ m) < p

d: succ (succ m) ∣ p


succ.succ
succ (succ m) = 1
p: β„•

p2: 2 ≀ p

m: β„•

h: 2 ≀ succ (succ m) β†’ succ (succ m) < p β†’ Β¬succ (succ m) ∣ p

l: succ (succ m) < p

d: succ (succ m) ∣ p


succ.succ
succ (succ m) = 1

Goals accomplished! πŸ™
⟩ #align nat.prime_def_lt'
Nat.prime_def_lt': βˆ€ {p : β„•}, Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), 2 ≀ m β†’ m < p β†’ Β¬m ∣ p
Nat.prime_def_lt'
theorem
prime_def_le_sqrt: βˆ€ {p : β„•}, Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p
prime_def_le_sqrt
{p :
β„•: Type
β„•
} :
Prime: β„• β†’ Prop
Prime
p ↔
2: ?m.3321
2
≀ p ∧ βˆ€
m: ?m.3351
m
,
2: ?m.3357
2
≀
m: ?m.3351
m
β†’
m: ?m.3351
m
≀
sqrt: β„• β†’ β„•
sqrt
p β†’ Β¬
m: ?m.3351
m
∣ p :=
prime_def_lt': βˆ€ {p : β„•}, Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), 2 ≀ m β†’ m < p β†’ Β¬m ∣ p
prime_def_lt'
.
trans: βˆ€ {a b c : Prop}, (a ↔ b) β†’ (b ↔ c) β†’ (a ↔ c)
trans
<|
and_congr_right: βˆ€ {a b c : Prop}, (a β†’ (b ↔ c)) β†’ (a ∧ b ↔ a ∧ c)
and_congr_right
fun
p2: ?m.3477
p2
=> ⟨fun
a: ?m.3486
a
m: ?m.3492
m
m2: ?m.3495
m2
l: ?m.3498
l
=>
a: ?m.3486
a
m: ?m.3492
m
m2: ?m.3495
m2
<|
lt_of_le_of_lt: βˆ€ {Ξ± : Type ?u.3501} [inst : Preorder Ξ±] {a b c : Ξ±}, a ≀ b β†’ b < c β†’ a < c
lt_of_le_of_lt
l: ?m.3498
l
<|
sqrt_lt_self: βˆ€ {n : β„•}, 1 < n β†’ sqrt n < n
sqrt_lt_self
p2: ?m.3477
p2
, fun
a: ?m.3600
a
=> have : βˆ€ {m k :
β„•: Type
β„•
}, m ≀ k β†’
1: ?m.3619
1
< m β†’ p β‰  m * k := fun {
m: ?m.3700
m
k: ?m.3703
k
}
mk: ?m.3706
mk
m1: ?m.3709
m1
e: ?m.3712
e
=>
a: ?m.3600
a
m: ?m.3700
m
m1: ?m.3709
m1
(
le_sqrt: βˆ€ {m n : β„•}, m ≀ sqrt n ↔ m * m ≀ n
le_sqrt
.
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
(
e: ?m.3712
e
.
symm: βˆ€ {Ξ± : Sort ?u.3718} {a b : Ξ±}, a = b β†’ b = a
symm
β–Έ
Nat.mul_le_mul_left: βˆ€ {n m : β„•} (k : β„•), n ≀ m β†’ k * n ≀ k * m
Nat.mul_le_mul_left
m: ?m.3700
m
mk: ?m.3706
mk
)) ⟨
k: ?m.3703
k
,
e: ?m.3712
e
⟩ fun
m: ?m.3770
m
m2: ?m.3773
m2
l: ?m.3776
l
⟨k,
e: p = m * k
e
⟩ =>

Goals accomplished! πŸ™
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = m * k


p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = m * k

mk: m ≀ k


inl
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = m * k

km: k ≀ m


inr
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = m * k


p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = m * k

mk: m ≀ k


inl
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = m * k

mk: m ≀ k


inl
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = m * k

km: k ≀ m


inr

Goals accomplished! πŸ™
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = m * k


p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = m * k

km: k ≀ m


inr
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = m * k

km: k ≀ m


inr
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = m * k

km: k ≀ m


inr
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = k * m

km: k ≀ m


inr
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = k * m

km: k ≀ m


inr
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = k * m

km: k ≀ m


inr
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = m * k

km: k ≀ m


inr
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = k * m

km: k ≀ m


inr
1 * m < k * m
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = m * k

km: k ≀ m


inr
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = k * m

km: k ≀ m


inr
1 * m < k * m
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = k * m

km: k ≀ m


inr
m < k * m
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = k * m

km: k ≀ m


inr
1 * m < k * m
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = k * m

km: k ≀ m


inr
m < p
p: β„•

p2: 2 ≀ p

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p

this: βˆ€ {m k : β„•}, m ≀ k β†’ 1 < m β†’ p β‰  m * k

m: β„•

m2: 2 ≀ m

l: m < p

x✝: m ∣ p

k: β„•

e: p = k * m

km: k ≀ m


inr
m < p
⟩ #align nat.prime_def_le_sqrt
Nat.prime_def_le_sqrt: βˆ€ {p : β„•}, Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), 2 ≀ m β†’ m ≀ sqrt p β†’ Β¬m ∣ p
Nat.prime_def_le_sqrt
theorem
prime_of_coprime: βˆ€ (n : β„•), 1 < n β†’ (βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m) β†’ Prime n
prime_of_coprime
(n :
β„•: Type
β„•
) (
h1: 1 < n
h1
:
1: ?m.4503
1
< n) (
h: βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m
h
: βˆ€
m: ?m.4539
m
< n,
m: ?m.4539
m
β‰ 
0: ?m.4551
0
β†’ n.
coprime: β„• β†’ β„• β†’ Prop
coprime
m: ?m.4539
m
) :
Prime: β„• β†’ Prop
Prime
n :=

Goals accomplished! πŸ™
n: β„•

h1: 1 < n

h: βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m


n: β„•

h1: 1 < n

h: βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m

m: β„•

mlt: m < n

mdvd: m ∣ n


m = 1
n: β„•

h1: 1 < n

h: βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m


n: β„•

h1: 1 < n

h: βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m

m: β„•

mlt: m < n

mdvd: m ∣ n


m = 1

Goals accomplished! πŸ™
n: β„•

h1: 1 < n

h: βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m

m: β„•

mlt: m < n

mdvd: m ∣ n


m β‰  0
n: β„•

h1: 1 < n

h: βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m

mlt: 0 < n

mdvd: 0 ∣ n


n: β„•

h1: 1 < n

h: βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m

m: β„•

mlt: m < n

mdvd: m ∣ n


m β‰  0
n: β„•

h1: 1 < n

h: βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m

mlt: 0 < n

mdvd: 0 ∣ n


n: β„•

h1: 1 < n

h: βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m

mlt: 0 < n

mdvd: n = 0


n: β„•

h1: 1 < n

h: βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m

mlt: 0 < n

mdvd: n = 0


n: β„•

h1: 1 < n

h: βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m

mlt: 0 < n

mdvd: n = 0


n: β„•

h1: 1 < n

h: βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m

m: β„•

mlt: m < n

mdvd: m ∣ n


m β‰  0

Goals accomplished! πŸ™
n: β„•

h1: 1 < n

h: βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m



Goals accomplished! πŸ™
#align nat.prime_of_coprime
Nat.prime_of_coprime: βˆ€ (n : β„•), 1 < n β†’ (βˆ€ (m : β„•), m < n β†’ m β‰  0 β†’ coprime n m) β†’ Prime n
Nat.prime_of_coprime
section /-- This instance is slower than the instance `decidablePrime` defined below, but has the advantage that it works in the kernel for small values. If you need to prove that a particular number is prime, in any case you should not use `by decide`, but rather `by norm_num`, which is much faster. -/ @[local instance] def
decidablePrime1: (p : β„•) β†’ Decidable (Prime p)
decidablePrime1
(p :
β„•: Type
β„•
) :
Decidable: Prop β†’ Type
Decidable
(
Prime: β„• β†’ Prop
Prime
p) :=
decidable_of_iff': {a : Prop} β†’ (b : Prop) β†’ (a ↔ b) β†’ [inst : Decidable b] β†’ Decidable a
decidable_of_iff'
_: Prop
_
prime_def_lt': βˆ€ {p : β„•}, Prime p ↔ 2 ≀ p ∧ βˆ€ (m : β„•), 2 ≀ m β†’ m < p β†’ Β¬m ∣ p
prime_def_lt'
#align nat.decidable_prime_1
Nat.decidablePrime1: (p : β„•) β†’ Decidable (Prime p)
Nat.decidablePrime1
theorem
prime_two: Prime 2
prime_two
:
Prime: β„• β†’ Prop
Prime
2: ?m.5130
2
:=

Goals accomplished! πŸ™

Goals accomplished! πŸ™
#align nat.prime_two
Nat.prime_two: Prime 2
Nat.prime_two
theorem
prime_three: Prime 3
prime_three
:
Prime: β„• β†’ Prop
Prime
3: ?m.5176
3
:=

Goals accomplished! πŸ™

Goals accomplished! πŸ™
#align nat.prime_three
Nat.prime_three: Prime 3
Nat.prime_three
theorem
Prime.five_le_of_ne_two_of_ne_three: βˆ€ {p : β„•}, Prime p β†’ p β‰  2 β†’ p β‰  3 β†’ 5 ≀ p
Prime.five_le_of_ne_two_of_ne_three
{p :
β„•: Type
β„•
} (
hp: Prime p
hp
: p.
Prime: β„• β†’ Prop
Prime
) (
h_two: p β‰  2
h_two
: p β‰ 
2: ?m.5251
2
) (
h_three: p β‰  3
h_three
: p β‰ 
3: ?m.5265
3
) :
5: ?m.5274
5
≀ p :=

Goals accomplished! πŸ™
p: β„•

hp: Prime p

h_two: p β‰  2

h_three: p β‰  3


p: β„•

hp: Prime p

h_two: p β‰  2

h_three: p β‰  3

h: p < 5


p: β„•

hp: Prime p

h_two: p β‰  2

h_three: p β‰  3


p: β„•

h: p < 5


Prime p β†’ p β‰  2 β†’ p β‰  3 β†’ False
p: β„•

hp: Prime p

h_two: p β‰  2

h_three: p β‰  3


p: β„•

h: p < 5


Prime p β†’ p β‰  2 β†’ p β‰  3 β†’ False
p: β„•

h: 0 < 5


Prime 0 β†’ 0 β‰  2 β†’ 0 β‰  3 β†’ False
p: β„•

h: p < 5


Prime p β†’ p β‰  2 β†’ p β‰  3 β†’ False

Goals accomplished! πŸ™
p: β„•

h: p < 5


Prime p β†’ p β‰  2 β†’ p β‰  3 β†’ False
p: β„•

h: 1 < 5


Prime 1 β†’ 1 β‰  2 β†’ 1 β‰  3 β†’ False
p: β„•

h: p < 5


Prime p β†’ p β‰  2 β†’ p β‰  3 β†’ False

Goals accomplished! πŸ™
p: β„•

h: p < 5


Prime p β†’ p β‰  2 β†’ p β‰  3 β†’ False
p: β„•

h: 2 < 5


Prime 2 β†’ 2 β‰  2 β†’ 2 β‰  3 β†’ False
p: β„•

h: p < 5


Prime p β†’ p β‰  2 β†’ p β‰  3 β†’ False

Goals accomplished! πŸ™
p: β„•

h: p < 5


Prime p β†’ p β‰  2 β†’ p β‰  3 β†’ False
p: β„•

h: 3 < 5


Prime 3 β†’ 3 β‰  2 β†’ 3 β‰  3 β†’ False
p: β„•

h: p < 5


Prime p β†’ p β‰  2 β†’ p β‰  3 β†’ False

Goals accomplished! πŸ™
p: β„•

h: p < 5


Prime p β†’ p β‰  2 β†’ p β‰  3 β†’ False
p: β„•

h: 4 < 5


Prime 4 β†’ 4 β‰  2 β†’ 4 β‰  3 β†’ False
p: β„•

h: p < 5


Prime p β†’ p β‰  2 β†’ p β‰  3 β†’ False

Goals accomplished! πŸ™
p: β„•

h: p < 5


Prime p β†’ p β‰  2 β†’ p β‰  3 β†’ False
p, n: β„•

h: n + 5 < 5


Prime (n + 5) β†’ n + 5 β‰  2 β†’ n + 5 β‰  3 β†’ False
p: β„•

h: p < 5


Prime p β†’ p β‰  2 β†’ p β‰  3 β†’ False

Goals accomplished! πŸ™
#align nat.prime.five_le_of_ne_two_of_ne_three
Nat.Prime.five_le_of_ne_two_of_ne_three: βˆ€ {p : β„•}, Prime p β†’ p β‰  2 β†’ p β‰  3 β†’ 5 ≀ p
Nat.Prime.five_le_of_ne_two_of_ne_three
end theorem
Prime.pred_pos: βˆ€ {p : β„•}, Prime p β†’ 0 < pred p
Prime.pred_pos
{p :
β„•: Type
β„•
} (
pp: Prime p
pp
:
Prime: β„• β†’ Prop
Prime
p) :
0: ?m.7513
0
<
pred: β„• β†’ β„•
pred
p :=
lt_pred_iff: βˆ€ {m n : β„•}, n < pred m ↔ succ n < m
lt_pred_iff
.
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
pp: Prime p
pp
.
one_lt: βˆ€ {p : β„•}, Prime p β†’ 1 < p
one_lt
#align nat.prime.pred_pos
Nat.Prime.pred_pos: βˆ€ {p : β„•}, Prime p β†’ 0 < pred p
Nat.Prime.pred_pos
theorem
succ_pred_prime: βˆ€ {p : β„•}, Prime p β†’ succ (pred p) = p
succ_pred_prime
{p :
β„•: Type
β„•
} (
pp: Prime p
pp
:
Prime: β„• β†’ Prop
Prime
p) :
succ: β„• β†’ β„•
succ
(
pred: β„• β†’ β„•
pred
p) = p :=
succ_pred_eq_of_pos: βˆ€ {n : β„•}, 0 < n β†’ succ (pred n) = n
succ_pred_eq_of_pos
pp: Prime p
pp
.
pos: βˆ€ {p : β„•}, Prime p β†’ 0 < p
pos
#align nat.succ_pred_prime
Nat.succ_pred_prime: βˆ€ {p : β„•}, Prime p β†’ succ (pred p) = p
Nat.succ_pred_prime
theorem
dvd_prime: βˆ€ {p m : β„•}, Prime p β†’ (m ∣ p ↔ m = 1 ∨ m = p)
dvd_prime
{p m :
β„•: Type
β„•
} (
pp: Prime p
pp
:
Prime: β„• β†’ Prop
Prime
p) : m ∣ p ↔ m =
1: ?m.7606
1
∨ m = p := ⟨fun
d: ?m.7645
d
=>
pp: Prime p
pp
.
eq_one_or_self_of_dvd: βˆ€ {p : β„•}, Prime p β†’ βˆ€ (m : β„•), m ∣ p β†’ m = 1 ∨ m = p
eq_one_or_self_of_dvd
m
d: ?m.7645
d
, fun
h: ?m.7658
h
=>
h: ?m.7658
h
.
elim: βˆ€ {a b c : Prop}, a ∨ b β†’ (a β†’ c) β†’ (b β†’ c) β†’ c
elim
(fun
e: ?m.7670
e
=>
e: ?m.7670
e
.
symm: βˆ€ {Ξ± : Sort ?u.7672} {a b : Ξ±}, a = b β†’ b = a
symm
β–Έ
one_dvd: βˆ€ {Ξ± : Type ?u.7683} [inst : Monoid Ξ±] (a : Ξ±), 1 ∣ a
one_dvd
_: ?m.7684
_
) fun
e: ?m.7744
e
=>
e: ?m.7744
e
.
symm: βˆ€ {Ξ± : Sort ?u.7746} {a b : Ξ±}, a = b β†’ b = a
symm
β–Έ
dvd_rfl: βˆ€ {Ξ± : Type ?u.7754} [inst : Monoid Ξ±] {a : Ξ±}, a ∣ a
dvd_rfl
⟩ #align nat.dvd_prime
Nat.dvd_prime: βˆ€ {p m : β„•}, Prime p β†’ (m ∣ p ↔ m = 1 ∨ m = p)
Nat.dvd_prime
theorem
dvd_prime_two_le: βˆ€ {p m : β„•}, Prime p β†’ 2 ≀ m β†’ (m ∣ p ↔ m = p)
dvd_prime_two_le
{p m :
β„•: Type
β„•
} (
pp: Prime p
pp
:
Prime: β„• β†’ Prop
Prime
p) (
H: 2 ≀ m
H
:
2: ?m.7819
2
≀ m) : m ∣ p ↔ m = p := (
dvd_prime: βˆ€ {p m : β„•}, Prime p β†’ (m ∣ p ↔ m = 1 ∨ m = p)
dvd_prime
pp: Prime p
pp
).
trans: βˆ€ {a b c : Prop}, (a ↔ b) β†’ (b ↔ c) β†’ (a ↔ c)
trans
<|
or_iff_right_of_imp: βˆ€ {a b : Prop}, (a β†’ b) β†’ (a ∨ b ↔ b)
or_iff_right_of_imp
<|
Not.elim: βˆ€ {a : Prop} {Ξ± : Sort ?u.7884}, Β¬a β†’ a β†’ Ξ±
Not.elim
<|
ne_of_gt: βˆ€ {a b : β„•}, b < a β†’ a β‰  b
ne_of_gt
H: 2 ≀ m
H
#align nat.dvd_prime_two_le
Nat.dvd_prime_two_le: βˆ€ {p m : β„•}, Prime p β†’ 2 ≀ m β†’ (m ∣ p ↔ m = p)
Nat.dvd_prime_two_le
theorem
prime_dvd_prime_iff_eq: βˆ€ {p q : β„•}, Prime p β†’ Prime q β†’ (p ∣ q ↔ p = q)
prime_dvd_prime_iff_eq
{p q :
β„•: Type
β„•
} (
pp: Prime p
pp
: p.
Prime: β„• β†’ Prop
Prime
) (
qp: Prime q
qp
: q.
Prime: β„• β†’ Prop
Prime
) : p ∣ q ↔ p = q :=
dvd_prime_two_le: βˆ€ {p m : β„•}, Prime p β†’ 2 ≀ m β†’ (m ∣ p ↔ m = p)
dvd_prime_two_le
qp: Prime q
qp
(
Prime.two_le: βˆ€ {p : β„•}, Prime p β†’ 2 ≀ p
Prime.two_le
pp: Prime p
pp
) #align nat.prime_dvd_prime_iff_eq
Nat.prime_dvd_prime_iff_eq: βˆ€ {p q : β„•}, Prime p β†’ Prime q β†’ (p ∣ q ↔ p = q)
Nat.prime_dvd_prime_iff_eq
theorem
Prime.not_dvd_one: βˆ€ {p : β„•}, Prime p β†’ Β¬p ∣ 1
Prime.not_dvd_one
{p :
β„•: Type
β„•
} (
pp: Prime p
pp
:
Prime: β„• β†’ Prop
Prime
p) : ¬p ∣
1: ?m.7960
1
:=
Irreducible.not_dvd_one: βˆ€ {Ξ± : Type ?u.7978} [inst : CommMonoid Ξ±] {p : Ξ±}, Irreducible p β†’ Β¬p ∣ 1
Irreducible.not_dvd_one
pp: Prime p
pp
#align nat.prime.not_dvd_one
Nat.Prime.not_dvd_one: βˆ€ {p : β„•}, Prime p β†’ Β¬p ∣ 1
Nat.Prime.not_dvd_one
theorem
not_prime_mul: βˆ€ {a b : β„•}, 1 < a β†’ 1 < b β†’ Β¬Prime (a * b)
not_prime_mul
{a b :
β„•: Type
β„•
} (
a1: 1 < a
a1
:
1: ?m.8054
1
< a) (
b1: 1 < b
b1
:
1: ?m.8091
1
< b) : Β¬
Prime: β„• β†’ Prop
Prime
(a * b) := fun
h: ?m.8173
h
=>
ne_of_lt: βˆ€ {a b : β„•}, a < b β†’ a β‰  b
ne_of_lt
(
Nat.mul_lt_mul_of_pos_left: βˆ€ {n m k : β„•}, n < m β†’ k > 0 β†’ k * n < k * m
Nat.mul_lt_mul_of_pos_left
b1: 1 < b
b1
(
lt_of_succ_lt: βˆ€ {n m : β„•}, succ n < m β†’ n < m
lt_of_succ_lt
a1: 1 < a
a1
)) <|

Goals accomplished! πŸ™
a, b: β„•

a1: 1 < a

b1: 1 < b

h: Prime (a * b)


a * 1 = a * b

Goals accomplished! πŸ™
#align nat.not_prime_mul
Nat.not_prime_mul: βˆ€ {a b : β„•}, 1 < a β†’ 1 < b β†’ Β¬Prime (a * b)
Nat.not_prime_mul
theorem
not_prime_mul': βˆ€ {a b n : β„•}, a * b = n β†’ 1 < a β†’ 1 < b β†’ Β¬Prime n
not_prime_mul'
{a b n :
β„•: Type
β„•
} (
h: a * b = n
h
: a * b = n) (
h₁: 1 < a
h₁
:
1: ?m.8759
1
< a) (
hβ‚‚: 1 < b
hβ‚‚
:
1: ?m.8796
1
< b) : Β¬
Prime: β„• β†’ Prop
Prime
n :=

Goals accomplished! πŸ™
a, b, n: β„•

h: a * b = n

h₁: 1 < a

hβ‚‚: 1 < b


a, b, n: β„•

h: a * b = n

h₁: 1 < a

hβ‚‚: 1 < b


a, b, n: β„•

h: a * b = n

h₁: 1 < a

hβ‚‚: 1 < b


Β¬Prime (a * b)
a, b, n: β„•

h: a * b = n

h₁: 1 < a

hβ‚‚: 1 < b


Β¬Prime (a * b)
a, b, n: β„•

h: a * b = n

h₁: 1 < a

hβ‚‚: 1 < b



Goals accomplished! πŸ™
#align nat.not_prime_mul'
Nat.not_prime_mul': βˆ€ {a b n : β„•}, a * b = n β†’ 1 < a β†’ 1 < b β†’ Β¬Prime n
Nat.not_prime_mul'
theorem
prime_mul_iff: βˆ€ {a b : β„•}, Prime (a * b) ↔ Prime a ∧ b = 1 ∨ Prime b ∧ a = 1
prime_mul_iff
{a b :
β„•: Type
β„•
} :
Nat.Prime: β„• β†’ Prop
Nat.Prime
(a * b) ↔ a.
Prime: β„• β†’ Prop
Prime
∧ b =
1: ?m.8927
1
∨ b.
Prime: β„• β†’ Prop
Prime
∧ a =
1: ?m.8954
1
:=

Goals accomplished! πŸ™
a, b: β„•



Goals accomplished! πŸ™
#align nat.prime_mul_iff
Nat.prime_mul_iff: βˆ€ {a b : β„•}, Prime (a * b) ↔ Prime a ∧ b = 1 ∨ Prime b ∧ a = 1
Nat.prime_mul_iff
theorem
Prime.dvd_iff_eq: βˆ€ {p a : β„•}, Prime p β†’ a β‰  1 β†’ (a ∣ p ↔ p = a)
Prime.dvd_iff_eq
{p a :
β„•: Type
β„•
} (
hp: Prime p
hp
: p.
Prime: β„• β†’ Prop
Prime
) (
a1: a β‰  1
a1
: a β‰ 
1: ?m.9169
1
) : a ∣ p ↔ p = a :=

Goals accomplished! πŸ™
p, a: β„•

hp: Prime p

a1: a β‰  1


a ∣ p ↔ p = a
p, a: β„•

hp: Prime p

a1: a β‰  1


a ∣ p ↔ p = a

Goals accomplished! πŸ™
p, a: β„•

hp: Prime p

a1: a β‰  1


p = a β†’ a ∣ p
p: β„•

hp: Prime p

a1: p β‰  1


p ∣ p
p, a: β„•

hp: Prime p

a1: a β‰  1


p = a β†’ a ∣ p

Goals accomplished! πŸ™
p, a: β„•

hp: Prime p

a1: a β‰  1


a ∣ p β†’ p = a
p, a: β„•

hp: Prime p

a1: a β‰  1


a ∣ p ↔ p = a
a: β„•

a1: a β‰  1

j: β„•

hp: Prime (a * j)


intro
a * j = a
p, a: β„•

hp: Prime p

a1: a β‰  1


a ∣ p ↔ p = a
a: β„•

a1: a β‰  1

left✝: Prime a

hp: Prime (a * 1)


intro.inl.intro
a * 1 = a
j: β„•

left✝: Prime j

a1: 1 β‰  1

hp: Prime (1 * j)


intro.inr.intro
1 * j = 1
p, a: β„•

hp: Prime p

a1: a β‰  1


a ∣ p ↔ p = a
a: β„•

a1: a β‰  1

left✝: Prime a

hp: Prime (a * 1)


intro.inl.intro
a * 1 = a
a: β„•

a1: a β‰  1

left✝: Prime a

hp: Prime (a * 1)


intro.inl.intro
a * 1 = a
j: β„•

left✝: Prime j

a1: 1 β‰  1

hp: Prime (1 * j)


intro.inr.intro
1 * j = 1

Goals accomplished! πŸ™
p, a: β„•

hp: Prime p

a1: a β‰  1


a ∣ p ↔ p = a
j: β„•

left✝: Prime j

a1: 1 β‰  1

hp: Prime (1 * j)


intro.inr.intro
1 * j = 1
j: β„•

left✝: Prime j

a1: 1 β‰  1

hp: Prime (1 * j)


intro.inr.intro
1 * j = 1

Goals accomplished! πŸ™
#align nat.prime.dvd_iff_eq
Nat.Prime.dvd_iff_eq: βˆ€ {p a : β„•}, Prime p β†’ a β‰  1 β†’ (a ∣ p ↔ p = a)
Nat.Prime.dvd_iff_eq
section MinFac theorem
minFac_lemma: βˆ€ (n k : β„•), Β¬n < k * k β†’ sqrt n - k < sqrt n + 2 - k
minFac_lemma
(n k :
β„•: Type
β„•
) (
h: Β¬n < k * k
h
: Β¬n < k * k) :
sqrt: β„• β†’ β„•
sqrt
n - k <
sqrt: β„• β†’ β„•
sqrt
n +
2: ?m.9582
2
- k := (
tsub_lt_tsub_iff_right: βˆ€ {Ξ± : Type ?u.9709} [inst : CanonicallyLinearOrderedAddMonoid Ξ±] [inst_1 : Sub Ξ±] [inst_2 : OrderedSub Ξ±] {a b c : Ξ±} [inst_3 : ContravariantClass Ξ± Ξ± (fun x x_1 => x + x_1) fun x x_1 => x ≀ x_1], c ≀ a β†’ (a - c < b - c ↔ a < b)
tsub_lt_tsub_iff_right
<|
le_sqrt: βˆ€ {m n : β„•}, m ≀ sqrt n ↔ m * m ≀ n
le_sqrt
.
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
<|
le_of_not_gt: βˆ€ {Ξ± : Type ?u.9729} [inst : LinearOrder Ξ±] {a b : Ξ±}, Β¬a > b β†’ a ≀ b
le_of_not_gt
h: Β¬n < k * k
h
).
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
<|
Nat.lt_add_of_pos_right: βˆ€ {n k : β„•}, 0 < k β†’ n < n + k
Nat.lt_add_of_pos_right
(

Goals accomplished! πŸ™
n, k: β„•

h: Β¬n < k * k


0 < 2

Goals accomplished! πŸ™
) #align nat.min_fac_lemma
Nat.minFac_lemma: βˆ€ (n k : β„•), Β¬n < k * k β†’ sqrt n - k < sqrt n + 2 - k
Nat.minFac_lemma
/-- If `n < k * k`, then `minFacAux n k = n`, if `k | n`, then `minFacAux n k = k`. Otherwise, `minFacAux n k = minFacAux n (k+2)` using well-founded recursion. If `n` is odd and `1 < n`, then then `minFacAux n 3` is the smallest prime factor of `n`. -/ def
minFacAux: β„• β†’ β„• β†’ β„•
minFacAux
(n :
β„•: Type
β„•
) :
β„•: Type
β„•
β†’
β„•: Type
β„•
|
k: ?m.10013
k
=> if
h: ?m.10085
h
: n <
k: ?m.10013
k
*
k: ?m.10013
k
then n else if
k: ?m.10013
k
∣ n then
k: ?m.10013
k
else have :=
minFac_lemma: βˆ€ (n k : β„•), Β¬n < k * k β†’ sqrt n - k < sqrt n + 2 - k
minFac_lemma
n
k: ?m.10013
k
h: ?m.10090
h
minFacAux: β„• β†’ β„• β†’ β„•
minFacAux
n (
k: ?m.10013
k
+
2: ?m.10117
2
) termination_by _ n k =>
sqrt: β„• β†’ β„•
sqrt
n +
2: ?m.10250
2
-
k: ?Ξ±
k
#align nat.min_fac_aux
Nat.minFacAux: β„• β†’ β„• β†’ β„•
Nat.minFacAux
/-- Returns the smallest prime factor of `n β‰  1`. -/ def
minFac: β„• β†’ β„•
minFac
(n :
β„•: Type
β„•
) :
β„•: Type
β„•
:= if
2: ?m.30036
2
∣ n then
2: ?m.30063
2
else
minFacAux: β„• β†’ β„• β†’ β„•
minFacAux
n
3: ?m.30073
3
#align nat.min_fac
Nat.minFac: β„• β†’ β„•
Nat.minFac
@[simp] theorem
minFac_zero: minFac 0 = 2
minFac_zero
:
minFac: β„• β†’ β„•
minFac
0: ?m.30110
0
=
2: ?m.30121
2
:=
rfl: βˆ€ {Ξ± : Sort ?u.30139} {a : Ξ±}, a = a
rfl
#align nat.min_fac_zero
Nat.minFac_zero: minFac 0 = 2
Nat.minFac_zero
@[simp] theorem
minFac_one: minFac 1 = 1
minFac_one
:
minFac: β„• β†’ β„•
minFac
1: ?m.30159
1
=
1: ?m.30170
1
:=
rfl: βˆ€ {Ξ± : Sort ?u.30187} {a : Ξ±}, a = a
rfl
#align nat.min_fac_one
Nat.minFac_one: minFac 1 = 1
Nat.minFac_one
theorem
minFac_eq: βˆ€ (n : β„•), minFac n = if 2 ∣ n then 2 else minFacAux n 3
minFac_eq
(n :
β„•: Type
β„•
) :
minFac: β„• β†’ β„•
minFac
n = if
2: ?m.30227
2
∣ n then
2: ?m.30243
2
else
minFacAux: β„• β†’ β„• β†’ β„•
minFacAux
n
3: ?m.30253
3
:=
rfl: βˆ€ {Ξ± : Sort ?u.30279} {a : Ξ±}, a = a
rfl
#align nat.min_fac_eq
Nat.minFac_eq: βˆ€ (n : β„•), minFac n = if 2 ∣ n then 2 else minFacAux n 3
Nat.minFac_eq
private def
minFacProp: β„• β†’ β„• β†’ Prop
minFacProp
(n k :
β„•: Type
β„•
) :=
2: ?m.30419
2
≀ k ∧ k ∣ n ∧ βˆ€
m: ?m.30455
m
,
2: ?m.30461
2
≀
m: ?m.30455
m
β†’
m: ?m.30455
m
∣ n β†’ k ≀
m: ?m.30455
m
theorem
minFacAux_has_prop: βˆ€ {n : β„•}, 2 ≀ n β†’ βˆ€ (k i : β„•), k = 2 * i + 3 β†’ (βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ k ≀ m) β†’ Nat.minFacProp n (minFacAux n k)
minFacAux_has_prop
{n :
β„•: Type
β„•
} (
n2: 2 ≀ n
n2
:
2: ?m.30580
2
≀ n) : βˆ€
k: ?m.30612
k
i: ?m.30615
i
,
k: ?m.30612
k
=
2: ?m.30627
2
*
i: ?m.30615
i
+
3: ?m.30637
3
β†’ (βˆ€
m: ?m.30705
m
,
2: ?m.30711
2
≀
m: ?m.30705
m
β†’
m: ?m.30705
m
∣ n β†’
k: ?m.30612
k
≀
m: ?m.30705
m
) β†’
minFacProp: β„• β†’ β„• β†’ Prop
minFacProp
n (
minFacAux: β„• β†’ β„• β†’ β„•
minFacAux
n
k: ?m.30612
k
) |
k: ?m.31052
k
=> fun
i: ?m.31055
i
e: ?m.31058
e
a: ?m.31061
a
=>

Goals accomplished! πŸ™
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m


Nat.minFacProp n (minFacAux n x✝)
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m


Nat.minFacProp n (minFacAux n x✝)
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m


Nat.minFacProp n (if h : n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝); minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m


Nat.minFacProp n (if h : n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝); minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m


Nat.minFacProp n (minFacAux n x✝)
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: n < k * k


pos
Nat.minFacProp n (if h : n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝); minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k


neg
Nat.minFacProp n (if h : n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝); minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m


Nat.minFacProp n (if h : n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝); minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: n < k * k


pos
Nat.minFacProp n (if h : n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝); minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k


neg
Nat.minFacProp n (if h : n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝); minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m


Nat.minFacProp n (if h : n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝); minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k


neg
Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m


Nat.minFacProp n (minFacAux n x✝)
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: n < k * k


pos
Nat.minFacProp n n
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: n < k * k


pos
Nat.minFacProp n n
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k


neg
Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: n < k * k

pp: Prime n


pos
Nat.minFacProp n n
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: n < k * k


pos
Nat.minFacProp n n

Goals accomplished! πŸ™
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m


Nat.minFacProp n (minFacAux n x✝)
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k


neg
Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))

Goals accomplished! πŸ™
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k


n: β„•

n2: 2 ≀ n

i: β„•

k:= 2 * i + 3: β„•

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ 2 * i + 3 ≀ m

h: Β¬n < k * k


n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k



Goals accomplished! πŸ™
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m


Nat.minFacProp n (minFacAux n x✝)
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k

k2: 2 ≀ k

dk: k ∣ n


pos
Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k

k2: 2 ≀ k

dk: ¬k ∣ n


neg
Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k

k2: 2 ≀ k


neg
Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k

k2: 2 ≀ k

dk: k ∣ n


pos
Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k

k2: 2 ≀ k

dk: ¬k ∣ n


neg
Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k

k2: 2 ≀ k


neg
Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k

k2: 2 ≀ k

dk: k ∣ n


pos
Nat.minFacProp n x✝
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m


Nat.minFacProp n (minFacAux n x✝)
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k

k2: 2 ≀ k

dk: k ∣ n


pos
Nat.minFacProp n x✝
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k

k2: 2 ≀ k

dk: k ∣ n


pos
Nat.minFacProp n x✝
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k

k2: 2 ≀ k

dk: ¬k ∣ n


neg
Nat.minFacProp n (minFacAux n (x✝ + 2))

Goals accomplished! πŸ™
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m


Nat.minFacProp n (minFacAux n x✝)
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k

k2: 2 ≀ k

dk: ¬k ∣ n


neg
Nat.minFacProp n (minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k

k2: 2 ≀ k

dk: ¬k ∣ n


neg
Nat.minFacProp n (minFacAux n (x✝ + 2))
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k

k2: 2 ≀ k

dk: ¬k ∣ n


neg
Nat.minFacProp n (minFacAux n (x✝ + 2))

Goals accomplished! πŸ™
n: β„•

n2: 2 ≀ n

x✝: β„•

k:= x✝: β„•

i: β„•

e: x✝ = 2 * i + 3

a: βˆ€ (m : β„•), 2 ≀ m β†’ m ∣ n β†’ x✝ ≀ m

h: Β¬n < k * k

k2: 2 ≀ k

dk: ¬k ∣ n

this: sqrt n - k < sqrt n + 2 - k


k + 2 = 2 * (i + 1) + 3

Goals accomplished! πŸ™