Metamath Proof Explorer

Theorem alzdvds

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

Ref Expression
Assertion alzdvds ⊢ N ∈ ℤ → ∀ x ∈ ℤ x ∥ N ↔ N = 0

Proof

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