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 ( 𝐵 ∈ ( 0 ..^ 𝐴 ) → ( 𝐴 ∥ 𝐵 ↔ 𝐵 = 0 ) )

Proof

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