Metamath Proof Explorer

Theorem fzo0dvdseq

Description: Zero is the only one of the first A nonnegative integers that is divisible by A . (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Assertion fzo0dvdseq ⊢ B ∈ 0 ..^ A → A ∥ B ↔ B = 0

Proof

Step Hyp Ref Expression
1 elfzolt2 ⊢ B ∈ 0 ..^ A → B < A
2 elfzoelz ⊢ B ∈ 0 ..^ A → B ∈ ℤ
3 2 zred ⊢ B ∈ 0 ..^ A → B ∈ ℝ
4 elfzoel2 ⊢ B ∈ 0 ..^ A → A ∈ ℤ
5 4 zred ⊢ B ∈ 0 ..^ A → A ∈ ℝ
6 3 5 ltnled ⊢ B ∈ 0 ..^ A → B < A ↔ ¬ A ≤ B
7 1 6 mpbid ⊢ B ∈ 0 ..^ A → ¬ A ≤ B
8 7 adantr ⊢ B ∈ 0 ..^ A ∧ B ≠ 0 → ¬ A ≤ B
9 elfzonn0 ⊢ B ∈ 0 ..^ A → B ∈ ℕ 0
10 9 adantr ⊢ B ∈ 0 ..^ A ∧ B ≠ 0 → B ∈ ℕ 0
11 simpr ⊢ B ∈ 0 ..^ A ∧ B ≠ 0 → B ≠ 0
12 eldifsn ⊢ B ∈ ℕ 0 ∖ 0 ↔ B ∈ ℕ 0 ∧ B ≠ 0
13 10 11 12 sylanbrc ⊢ B ∈ 0 ..^ A ∧ B ≠ 0 → B ∈ ℕ 0 ∖ 0
14 dfn2 ⊢ ℕ = ℕ 0 ∖ 0
15 13 14 eleqtrrdi ⊢ B ∈ 0 ..^ A ∧ B ≠ 0 → B ∈ ℕ
16 dvdsle ⊢ A ∈ ℤ ∧ B ∈ ℕ → A ∥ B → A ≤ B
17 4 15 16 syl2an2r ⊢ B ∈ 0 ..^ A ∧ B ≠ 0 → A ∥ B → A ≤ B
18 8 17 mtod ⊢ B ∈ 0 ..^ A ∧ B ≠ 0 → ¬ A ∥ B
19 18 ex ⊢ B ∈ 0 ..^ A → B ≠ 0 → ¬ A ∥ B
20 19 necon4ad ⊢ B ∈ 0 ..^ A → A ∥ B → B = 0
21 dvds0 ⊢ A ∈ ℤ → A ∥ 0
22 4 21 syl ⊢ B ∈ 0 ..^ A → A ∥ 0
23 breq2 ⊢ B = 0 → A ∥ B ↔ A ∥ 0
24 22 23 syl5ibrcom ⊢ B ∈ 0 ..^ A → B = 0 → A ∥ B
25 20 24 impbid ⊢ B ∈ 0 ..^ A → A ∥ B ↔ B = 0