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 ) )