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 B0..^AABB=0

Proof

Step Hyp Ref Expression
1 elfzolt2 B0..^AB<A
2 elfzoelz B0..^AB
3 2 zred B0..^AB
4 elfzoel2 B0..^AA
5 4 zred B0..^AA
6 3 5 ltnled B0..^AB<A¬AB
7 1 6 mpbid B0..^A¬AB
8 7 adantr B0..^AB0¬AB
9 elfzonn0 B0..^AB0
10 9 adantr B0..^AB0B0
11 simpr B0..^AB0B0
12 eldifsn B00B0B0
13 10 11 12 sylanbrc B0..^AB0B00
14 dfn2 =00
15 13 14 eleqtrrdi B0..^AB0B
16 dvdsle ABABAB
17 4 15 16 syl2an2r B0..^AB0ABAB
18 8 17 mtod B0..^AB0¬AB
19 18 ex B0..^AB0¬AB
20 19 necon4ad B0..^AABB=0
21 dvds0 AA0
22 4 21 syl B0..^AA0
23 breq2 B=0ABA0
24 22 23 syl5ibrcom B0..^AB=0AB
25 20 24 impbid B0..^AABB=0