Theorem fzoun

Description: A half-open integer range as union of two half-open integer ranges. (Contributed by AV, 23-Apr-2022)

	Ref	Expression
Assertion	fzoun	|- ( ( B e. ( ZZ>= ` A ) /\ C e. NN0 ) -> ( A ..^ ( B + C ) ) = ( ( A ..^ B ) u. ( B ..^ ( B + C ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eluzel2	|- ( B e. ( ZZ>= ` A ) -> A e. ZZ )
2	1	adantr	|- ( ( B e. ( ZZ>= ` A ) /\ C e. NN0 ) -> A e. ZZ )
3		eluzelz	|- ( B e. ( ZZ>= ` A ) -> B e. ZZ )
4		nn0z	|- ( C e. NN0 -> C e. ZZ )
5		zaddcl	|- ( ( B e. ZZ /\ C e. ZZ ) -> ( B + C ) e. ZZ )
6	3 4 5	syl2an	|- ( ( B e. ( ZZ>= ` A ) /\ C e. NN0 ) -> ( B + C ) e. ZZ )
7	3	adantr	|- ( ( B e. ( ZZ>= ` A ) /\ C e. NN0 ) -> B e. ZZ )
8		eluzle	|- ( B e. ( ZZ>= ` A ) -> A <_ B )
9	8	adantr	|- ( ( B e. ( ZZ>= ` A ) /\ C e. NN0 ) -> A <_ B )
10		nn0ge0	|- ( C e. NN0 -> 0 <_ C )
11	10	adantl	|- ( ( B e. ( ZZ>= ` A ) /\ C e. NN0 ) -> 0 <_ C )
12		eluzelre	|- ( B e. ( ZZ>= ` A ) -> B e. RR )
13		nn0re	|- ( C e. NN0 -> C e. RR )
14		addge01	|- ( ( B e. RR /\ C e. RR ) -> ( 0 <_ C <-> B <_ ( B + C ) ) )
15	12 13 14	syl2an	|- ( ( B e. ( ZZ>= ` A ) /\ C e. NN0 ) -> ( 0 <_ C <-> B <_ ( B + C ) ) )
16	11 15	mpbid	|- ( ( B e. ( ZZ>= ` A ) /\ C e. NN0 ) -> B <_ ( B + C ) )
17	2 6 7 9 16	elfzd	|- ( ( B e. ( ZZ>= ` A ) /\ C e. NN0 ) -> B e. ( A ... ( B + C ) ) )
18		fzosplit	|- ( B e. ( A ... ( B + C ) ) -> ( A ..^ ( B + C ) ) = ( ( A ..^ B ) u. ( B ..^ ( B + C ) ) ) )
19	17 18	syl	|- ( ( B e. ( ZZ>= ` A ) /\ C e. NN0 ) -> ( A ..^ ( B + C ) ) = ( ( A ..^ B ) u. ( B ..^ ( B + C ) ) ) )