Step |
Hyp |
Ref |
Expression |
1 |
|
elun |
|- ( a e. ( ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) u. ( ZZ>= ` B ) ) <-> ( a e. ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) \/ a e. ( ZZ>= ` B ) ) ) |
2 |
|
ellz1 |
|- ( A e. ZZ -> ( a e. ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) <-> ( a e. ZZ /\ a <_ A ) ) ) |
3 |
2
|
3ad2ant1 |
|- ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( a e. ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) <-> ( a e. ZZ /\ a <_ A ) ) ) |
4 |
|
eluz1 |
|- ( B e. ZZ -> ( a e. ( ZZ>= ` B ) <-> ( a e. ZZ /\ B <_ a ) ) ) |
5 |
4
|
3ad2ant2 |
|- ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( a e. ( ZZ>= ` B ) <-> ( a e. ZZ /\ B <_ a ) ) ) |
6 |
3 5
|
orbi12d |
|- ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( ( a e. ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) \/ a e. ( ZZ>= ` B ) ) <-> ( ( a e. ZZ /\ a <_ A ) \/ ( a e. ZZ /\ B <_ a ) ) ) ) |
7 |
|
zre |
|- ( a e. ZZ -> a e. RR ) |
8 |
7
|
adantl |
|- ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> a e. RR ) |
9 |
|
simpl1 |
|- ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> A e. ZZ ) |
10 |
9
|
zred |
|- ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> A e. RR ) |
11 |
|
lelttric |
|- ( ( a e. RR /\ A e. RR ) -> ( a <_ A \/ A < a ) ) |
12 |
8 10 11
|
syl2anc |
|- ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> ( a <_ A \/ A < a ) ) |
13 |
|
simpll2 |
|- ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> B e. ZZ ) |
14 |
13
|
zred |
|- ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> B e. RR ) |
15 |
|
simpll1 |
|- ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> A e. ZZ ) |
16 |
15
|
peano2zd |
|- ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> ( A + 1 ) e. ZZ ) |
17 |
16
|
zred |
|- ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> ( A + 1 ) e. RR ) |
18 |
7
|
ad2antlr |
|- ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> a e. RR ) |
19 |
|
simpll3 |
|- ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> B <_ ( A + 1 ) ) |
20 |
|
zltp1le |
|- ( ( A e. ZZ /\ a e. ZZ ) -> ( A < a <-> ( A + 1 ) <_ a ) ) |
21 |
20
|
3ad2antl1 |
|- ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> ( A < a <-> ( A + 1 ) <_ a ) ) |
22 |
21
|
biimpa |
|- ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> ( A + 1 ) <_ a ) |
23 |
14 17 18 19 22
|
letrd |
|- ( ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) /\ A < a ) -> B <_ a ) |
24 |
23
|
ex |
|- ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> ( A < a -> B <_ a ) ) |
25 |
24
|
orim2d |
|- ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> ( ( a <_ A \/ A < a ) -> ( a <_ A \/ B <_ a ) ) ) |
26 |
12 25
|
mpd |
|- ( ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) /\ a e. ZZ ) -> ( a <_ A \/ B <_ a ) ) |
27 |
26
|
ex |
|- ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( a e. ZZ -> ( a <_ A \/ B <_ a ) ) ) |
28 |
27
|
pm4.71d |
|- ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( a e. ZZ <-> ( a e. ZZ /\ ( a <_ A \/ B <_ a ) ) ) ) |
29 |
|
andi |
|- ( ( a e. ZZ /\ ( a <_ A \/ B <_ a ) ) <-> ( ( a e. ZZ /\ a <_ A ) \/ ( a e. ZZ /\ B <_ a ) ) ) |
30 |
28 29
|
bitr2di |
|- ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( ( ( a e. ZZ /\ a <_ A ) \/ ( a e. ZZ /\ B <_ a ) ) <-> a e. ZZ ) ) |
31 |
6 30
|
bitrd |
|- ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( ( a e. ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) \/ a e. ( ZZ>= ` B ) ) <-> a e. ZZ ) ) |
32 |
1 31
|
syl5bb |
|- ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( a e. ( ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) u. ( ZZ>= ` B ) ) <-> a e. ZZ ) ) |
33 |
32
|
eqrdv |
|- ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) u. ( ZZ>= ` B ) ) = ZZ ) |