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

Metamath Proof Explorer

Theorem fzp1disj

Description: ( M ... ( N + 1 ) ) is the disjoint union of ( M ... N ) with { ( N + 1 ) } . (Contributed by Mario Carneiro, 7-Mar-2014)

Ref Expression
Assertion fzp1disj 
|- ( ( M ... N ) i^i { ( N + 1 ) } ) = (/)

Proof

Step Hyp Ref Expression
1 elfzle2 
 |-  ( ( N + 1 ) e. ( M ... N ) -> ( N + 1 ) <_ N )
2 elfzel2 
 |-  ( ( N + 1 ) e. ( M ... N ) -> N e. ZZ )
3 2 zred 
 |-  ( ( N + 1 ) e. ( M ... N ) -> N e. RR )
4 ltp1 
 |-  ( N e. RR -> N < ( N + 1 ) )
5 peano2re 
 |-  ( N e. RR -> ( N + 1 ) e. RR )
6 ltnle 
 |-  ( ( N e. RR /\ ( N + 1 ) e. RR ) -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) )
7 5 6 mpdan 
 |-  ( N e. RR -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) )
8 4 7 mpbid 
 |-  ( N e. RR -> -. ( N + 1 ) <_ N )
9 3 8 syl 
 |-  ( ( N + 1 ) e. ( M ... N ) -> -. ( N + 1 ) <_ N )
10 1 9 pm2.65i 
 |-  -. ( N + 1 ) e. ( M ... N )
11 disjsn 
 |-  ( ( ( M ... N ) i^i { ( N + 1 ) } ) = (/) <-> -. ( N + 1 ) e. ( M ... N ) )
12 10 11 mpbir 
 |-  ( ( M ... N ) i^i { ( N + 1 ) } ) = (/)