This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem alzdvds

Description: Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion alzdvds ( 𝑁 ∈ ℤ → ( ∀ 𝑥 ∈ ℤ 𝑥 ∥ 𝑁 ↔ 𝑁 = 0 ) )

Proof

Step Hyp Ref Expression
1 nnssz ⊢ ℕ ⊆ ℤ
2 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
3 2 abscld ⊢ ( 𝑁 ∈ ℤ → ( abs ‘ 𝑁 ) ∈ ℝ )
4 arch ⊢ ( ( abs ‘ 𝑁 ) ∈ ℝ → ∃ 𝑥 ∈ ℕ ( abs ‘ 𝑁 ) < 𝑥 )
5 3 4 syl ⊢ ( 𝑁 ∈ ℤ → ∃ 𝑥 ∈ ℕ ( abs ‘ 𝑁 ) < 𝑥 )
6 ssrexv ⊢ ( ℕ ⊆ ℤ → ( ∃ 𝑥 ∈ ℕ ( abs ‘ 𝑁 ) < 𝑥 → ∃ 𝑥 ∈ ℤ ( abs ‘ 𝑁 ) < 𝑥 ) )
7 1 5 6 mpsyl ⊢ ( 𝑁 ∈ ℤ → ∃ 𝑥 ∈ ℤ ( abs ‘ 𝑁 ) < 𝑥 )
8 zre ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ )
9 ltnle ⊢ ( ( ( abs ‘ 𝑁 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ 𝑁 ) < 𝑥 ↔ ¬ 𝑥 ≤ ( abs ‘ 𝑁 ) ) )
10 3 8 9 syl2an ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( ( abs ‘ 𝑁 ) < 𝑥 ↔ ¬ 𝑥 ≤ ( abs ‘ 𝑁 ) ) )
11 10 rexbidva ⊢ ( 𝑁 ∈ ℤ → ( ∃ 𝑥 ∈ ℤ ( abs ‘ 𝑁 ) < 𝑥 ↔ ∃ 𝑥 ∈ ℤ ¬ 𝑥 ≤ ( abs ‘ 𝑁 ) ) )
12 rexnal ⊢ ( ∃ 𝑥 ∈ ℤ ¬ 𝑥 ≤ ( abs ‘ 𝑁 ) ↔ ¬ ∀ 𝑥 ∈ ℤ 𝑥 ≤ ( abs ‘ 𝑁 ) )
13 11 12 bitrdi ⊢ ( 𝑁 ∈ ℤ → ( ∃ 𝑥 ∈ ℤ ( abs ‘ 𝑁 ) < 𝑥 ↔ ¬ ∀ 𝑥 ∈ ℤ 𝑥 ≤ ( abs ‘ 𝑁 ) ) )
14 7 13 mpbid ⊢ ( 𝑁 ∈ ℤ → ¬ ∀ 𝑥 ∈ ℤ 𝑥 ≤ ( abs ‘ 𝑁 ) )
15 14 adantl ⊢ ( ( ∀ 𝑥 ∈ ℤ 𝑥 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ¬ ∀ 𝑥 ∈ ℤ 𝑥 ≤ ( abs ‘ 𝑁 ) )
16 ralim ⊢ ( ∀ 𝑥 ∈ ℤ ( 𝑥 ∥ 𝑁 → 𝑥 ≤ ( abs ‘ 𝑁 ) ) → ( ∀ 𝑥 ∈ ℤ 𝑥 ∥ 𝑁 → ∀ 𝑥 ∈ ℤ 𝑥 ≤ ( abs ‘ 𝑁 ) ) )
17 dvdsleabs ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑥 ∥ 𝑁 → 𝑥 ≤ ( abs ‘ 𝑁 ) ) )
18 17 3expb ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑥 ∥ 𝑁 → 𝑥 ≤ ( abs ‘ 𝑁 ) ) )
19 18 expcom ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑥 ∈ ℤ → ( 𝑥 ∥ 𝑁 → 𝑥 ≤ ( abs ‘ 𝑁 ) ) ) )
20 19 ralrimiv ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ∀ 𝑥 ∈ ℤ ( 𝑥 ∥ 𝑁 → 𝑥 ≤ ( abs ‘ 𝑁 ) ) )
21 16 20 syl11 ⊢ ( ∀ 𝑥 ∈ ℤ 𝑥 ∥ 𝑁 → ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ∀ 𝑥 ∈ ℤ 𝑥 ≤ ( abs ‘ 𝑁 ) ) )
22 21 expdimp ⊢ ( ( ∀ 𝑥 ∈ ℤ 𝑥 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≠ 0 → ∀ 𝑥 ∈ ℤ 𝑥 ≤ ( abs ‘ 𝑁 ) ) )
23 15 22 mtod ⊢ ( ( ∀ 𝑥 ∈ ℤ 𝑥 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ¬ 𝑁 ≠ 0 )
24 nne ⊢ ( ¬ 𝑁 ≠ 0 ↔ 𝑁 = 0 )
25 23 24 sylib ⊢ ( ( ∀ 𝑥 ∈ ℤ 𝑥 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → 𝑁 = 0 )
26 25 expcom ⊢ ( 𝑁 ∈ ℤ → ( ∀ 𝑥 ∈ ℤ 𝑥 ∥ 𝑁 → 𝑁 = 0 ) )
27 dvds0 ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∥ 0 )
28 breq2 ⊢ ( 𝑁 = 0 → ( 𝑥 ∥ 𝑁 ↔ 𝑥 ∥ 0 ) )
29 27 28 imbitrrid ⊢ ( 𝑁 = 0 → ( 𝑥 ∈ ℤ → 𝑥 ∥ 𝑁 ) )
30 29 ralrimiv ⊢ ( 𝑁 = 0 → ∀ 𝑥 ∈ ℤ 𝑥 ∥ 𝑁 )
31 26 30 impbid1 ⊢ ( 𝑁 ∈ ℤ → ( ∀ 𝑥 ∈ ℤ 𝑥 ∥ 𝑁 ↔ 𝑁 = 0 ) )