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

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 e. ( 0 ..^ A ) -> ( A || B <-> B = 0 ) )

Proof

Step Hyp Ref Expression
1 elfzolt2 
 |-  ( B e. ( 0 ..^ A ) -> B < A )
2 elfzoelz 
 |-  ( B e. ( 0 ..^ A ) -> B e. ZZ )
3 2 zred 
 |-  ( B e. ( 0 ..^ A ) -> B e. RR )
4 elfzoel2 
 |-  ( B e. ( 0 ..^ A ) -> A e. ZZ )
5 4 zred 
 |-  ( B e. ( 0 ..^ A ) -> A e. RR )
6 3 5 ltnled 
 |-  ( B e. ( 0 ..^ A ) -> ( B < A <-> -. A <_ B ) )
7 1 6 mpbid 
 |-  ( B e. ( 0 ..^ A ) -> -. A <_ B )
8 7 adantr 
 |-  ( ( B e. ( 0 ..^ A ) /\ B =/= 0 ) -> -. A <_ B )
9 elfzonn0 
 |-  ( B e. ( 0 ..^ A ) -> B e. NN0 )
10 9 adantr 
 |-  ( ( B e. ( 0 ..^ A ) /\ B =/= 0 ) -> B e. NN0 )
11 simpr 
 |-  ( ( B e. ( 0 ..^ A ) /\ B =/= 0 ) -> B =/= 0 )
12 eldifsn 
 |-  ( B e. ( NN0 \ { 0 } ) <-> ( B e. NN0 /\ B =/= 0 ) )
13 10 11 12 sylanbrc 
 |-  ( ( B e. ( 0 ..^ A ) /\ B =/= 0 ) -> B e. ( NN0 \ { 0 } ) )
14 dfn2 
 |-  NN = ( NN0 \ { 0 } )
15 13 14 eleqtrrdi 
 |-  ( ( B e. ( 0 ..^ A ) /\ B =/= 0 ) -> B e. NN )
16 dvdsle 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A || B -> A <_ B ) )
17 4 15 16 syl2an2r 
 |-  ( ( B e. ( 0 ..^ A ) /\ B =/= 0 ) -> ( A || B -> A <_ B ) )
18 8 17 mtod 
 |-  ( ( B e. ( 0 ..^ A ) /\ B =/= 0 ) -> -. A || B )
19 18 ex 
 |-  ( B e. ( 0 ..^ A ) -> ( B =/= 0 -> -. A || B ) )
20 19 necon4ad 
 |-  ( B e. ( 0 ..^ A ) -> ( A || B -> B = 0 ) )
21 dvds0 
 |-  ( A e. ZZ -> A || 0 )
22 4 21 syl 
 |-  ( B e. ( 0 ..^ A ) -> A || 0 )
23 breq2 
 |-  ( B = 0 -> ( A || B <-> A || 0 ) )
24 22 23 syl5ibrcom 
 |-  ( B e. ( 0 ..^ A ) -> ( B = 0 -> A || B ) )
25 20 24 impbid 
 |-  ( B e. ( 0 ..^ A ) -> ( A || B <-> B = 0 ) )