Metamath Proof Explorer

Theorem dedekind

Description: The Dedekind cut theorem. This theorem, which may be used to replace ax-pre-sup with appropriate adjustments, states that, if A completely preceeds B , then there is some number separating the two of them. (Contributed by Scott Fenton, 13-Jun-2013)

Ref Expression
Assertion dedekind 
|- ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x < y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ x ( A =/= (/) /\ B =/= (/) )
2 nfv 
 |-  F/ x ( A C_ RR /\ B C_ RR )
3 nfra1 
 |-  F/ x A. x e. A A. y e. B x < y
4 1 2 3 nf3an 
 |-  F/ x ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y )
5 nfv 
 |-  F/ x z e. RR
6 nfra1 
 |-  F/ x A. x e. A -. z < x
7 nfra1 
 |-  F/ x A. x e. RR ( x < z -> E. w e. A x < w )
8 6 7 nfan 
 |-  F/ x ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) )
9 5 8 nfan 
 |-  F/ x ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) )
10 4 9 nfan 
 |-  F/ x ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) )
11 nfv 
 |-  F/ y ( A =/= (/) /\ B =/= (/) )
12 nfv 
 |-  F/ y ( A C_ RR /\ B C_ RR )
13 nfra2w 
 |-  F/ y A. x e. A A. y e. B x < y
14 11 12 13 nf3an 
 |-  F/ y ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y )
15 nfv 
 |-  F/ y ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) )
16 14 15 nfan 
 |-  F/ y ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) )
17 nfv 
 |-  F/ y x e. A
18 simpl2l 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) ) -> A C_ RR )
19 18 sselda 
 |-  ( ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) ) /\ x e. A ) -> x e. RR )
20 simplrl 
 |-  ( ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) ) /\ x e. A ) -> z e. RR )
21 simprrl 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) ) -> A. x e. A -. z < x )
22 21 r19.21bi 
 |-  ( ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) ) /\ x e. A ) -> -. z < x )
23 19 20 22 nltled 
 |-  ( ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) ) /\ x e. A ) -> x <_ z )
24 23 ex 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) ) -> ( x e. A -> x <_ z ) )
25 simprll 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) /\ y e. B ) ) -> z e. RR )
26 simp2r 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> B C_ RR )
27 simpr 
 |-  ( ( ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) /\ y e. B ) -> y e. B )
28 ssel2 
 |-  ( ( B C_ RR /\ y e. B ) -> y e. RR )
29 26 27 28 syl2an 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) /\ y e. B ) ) -> y e. RR )
30 simpl3 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) /\ y e. B ) ) -> A. x e. A A. y e. B x < y )
31 simp2 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> ( A C_ RR /\ B C_ RR ) )
32 rsp 
 |-  ( A. y e. B x < y -> ( y e. B -> x < y ) )
33 32 com12 
 |-  ( y e. B -> ( A. y e. B x < y -> x < y ) )
34 33 adantl 
 |-  ( ( ( ( A C_ RR /\ B C_ RR ) /\ x e. A ) /\ y e. B ) -> ( A. y e. B x < y -> x < y ) )
35 ssel2 
 |-  ( ( A C_ RR /\ x e. A ) -> x e. RR )
36 35 adantlr 
 |-  ( ( ( A C_ RR /\ B C_ RR ) /\ x e. A ) -> x e. RR )
37 simplr 
 |-  ( ( ( A C_ RR /\ B C_ RR ) /\ x e. A ) -> B C_ RR )
38 37 sselda 
 |-  ( ( ( ( A C_ RR /\ B C_ RR ) /\ x e. A ) /\ y e. B ) -> y e. RR )
39 ltnsym 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x < y -> -. y < x ) )
40 36 38 39 syl2an2r 
 |-  ( ( ( ( A C_ RR /\ B C_ RR ) /\ x e. A ) /\ y e. B ) -> ( x < y -> -. y < x ) )
41 34 40 syld 
 |-  ( ( ( ( A C_ RR /\ B C_ RR ) /\ x e. A ) /\ y e. B ) -> ( A. y e. B x < y -> -. y < x ) )
42 41 an32s 
 |-  ( ( ( ( A C_ RR /\ B C_ RR ) /\ y e. B ) /\ x e. A ) -> ( A. y e. B x < y -> -. y < x ) )
43 42 ralimdva 
 |-  ( ( ( A C_ RR /\ B C_ RR ) /\ y e. B ) -> ( A. x e. A A. y e. B x < y -> A. x e. A -. y < x ) )
44 31 27 43 syl2an 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) /\ y e. B ) ) -> ( A. x e. A A. y e. B x < y -> A. x e. A -. y < x ) )
45 30 44 mpd 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) /\ y e. B ) ) -> A. x e. A -. y < x )
46 breq2 
 |-  ( x = w -> ( y < x <-> y < w ) )
47 46 notbid 
 |-  ( x = w -> ( -. y < x <-> -. y < w ) )
48 47 cbvralvw 
 |-  ( A. x e. A -. y < x <-> A. w e. A -. y < w )
49 45 48 sylib 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) /\ y e. B ) ) -> A. w e. A -. y < w )
50 ralnex 
 |-  ( A. w e. A -. y < w <-> -. E. w e. A y < w )
51 49 50 sylib 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) /\ y e. B ) ) -> -. E. w e. A y < w )
52 breq1 
 |-  ( x = y -> ( x < z <-> y < z ) )
53 breq1 
 |-  ( x = y -> ( x < w <-> y < w ) )
54 53 rexbidv 
 |-  ( x = y -> ( E. w e. A x < w <-> E. w e. A y < w ) )
55 52 54 imbi12d 
 |-  ( x = y -> ( ( x < z -> E. w e. A x < w ) <-> ( y < z -> E. w e. A y < w ) ) )
56 simplrr 
 |-  ( ( ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) /\ y e. B ) -> A. x e. RR ( x < z -> E. w e. A x < w ) )
57 56 adantl 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) /\ y e. B ) ) -> A. x e. RR ( x < z -> E. w e. A x < w ) )
58 55 57 29 rspcdva 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) /\ y e. B ) ) -> ( y < z -> E. w e. A y < w ) )
59 51 58 mtod 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) /\ y e. B ) ) -> -. y < z )
60 25 29 59 nltled 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) /\ y e. B ) ) -> z <_ y )
61 60 expr 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) ) -> ( y e. B -> z <_ y ) )
62 24 61 anim12d 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) ) -> ( ( x e. A /\ y e. B ) -> ( x <_ z /\ z <_ y ) ) )
63 62 expd 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) ) -> ( x e. A -> ( y e. B -> ( x <_ z /\ z <_ y ) ) ) )
64 16 17 63 ralrimd 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) ) -> ( x e. A -> A. y e. B ( x <_ z /\ z <_ y ) ) )
65 10 64 ralrimi 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) /\ ( z e. RR /\ ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) ) ) -> A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )
66 simp2l 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> A C_ RR )
67 simp1l 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> A =/= (/) )
68 simp1r 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> B =/= (/) )
69 n0 
 |-  ( B =/= (/) <-> E. z z e. B )
70 68 69 sylib 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> E. z z e. B )
71 26 sseld 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> ( z e. B -> z e. RR ) )
72 ralcom 
 |-  ( A. x e. A A. y e. B x < y <-> A. y e. B A. x e. A x < y )
73 breq2 
 |-  ( y = z -> ( x < y <-> x < z ) )
74 73 ralbidv 
 |-  ( y = z -> ( A. x e. A x < y <-> A. x e. A x < z ) )
75 74 rspccv 
 |-  ( A. y e. B A. x e. A x < y -> ( z e. B -> A. x e. A x < z ) )
76 72 75 sylbi 
 |-  ( A. x e. A A. y e. B x < y -> ( z e. B -> A. x e. A x < z ) )
77 76 3ad2ant3 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> ( z e. B -> A. x e. A x < z ) )
78 71 77 jcad 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> ( z e. B -> ( z e. RR /\ A. x e. A x < z ) ) )
79 78 eximdv 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> ( E. z z e. B -> E. z ( z e. RR /\ A. x e. A x < z ) ) )
80 70 79 mpd 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> E. z ( z e. RR /\ A. x e. A x < z ) )
81 df-rex 
 |-  ( E. z e. RR A. x e. A x < z <-> E. z ( z e. RR /\ A. x e. A x < z ) )
82 80 81 sylibr 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> E. z e. RR A. x e. A x < z )
83 axsup 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. z e. RR A. x e. A x < z ) -> E. z e. RR ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) )
84 66 67 82 83 syl3anc 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> E. z e. RR ( A. x e. A -. z < x /\ A. x e. RR ( x < z -> E. w e. A x < w ) ) )
85 65 84 reximddv 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )
86 85 3expib 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( ( ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) ) )
87 1re 
 |-  1 e. RR
88 rzal 
 |-  ( A = (/) -> A. x e. A A. y e. B ( x <_ 1 /\ 1 <_ y ) )
89 breq2 
 |-  ( z = 1 -> ( x <_ z <-> x <_ 1 ) )
90 breq1 
 |-  ( z = 1 -> ( z <_ y <-> 1 <_ y ) )
91 89 90 anbi12d 
 |-  ( z = 1 -> ( ( x <_ z /\ z <_ y ) <-> ( x <_ 1 /\ 1 <_ y ) ) )
92 91 2ralbidv 
 |-  ( z = 1 -> ( A. x e. A A. y e. B ( x <_ z /\ z <_ y ) <-> A. x e. A A. y e. B ( x <_ 1 /\ 1 <_ y ) ) )
93 92 rspcev 
 |-  ( ( 1 e. RR /\ A. x e. A A. y e. B ( x <_ 1 /\ 1 <_ y ) ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )
94 87 88 93 sylancr 
 |-  ( A = (/) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )
95 94 a1d 
 |-  ( A = (/) -> ( ( ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) ) )
96 rzal 
 |-  ( B = (/) -> A. y e. B ( x <_ 1 /\ 1 <_ y ) )
97 96 ralrimivw 
 |-  ( B = (/) -> A. x e. A A. y e. B ( x <_ 1 /\ 1 <_ y ) )
98 87 97 93 sylancr 
 |-  ( B = (/) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )
99 98 a1d 
 |-  ( B = (/) -> ( ( ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) ) )
100 86 95 99 pm2.61iine 
 |-  ( ( ( A C_ RR /\ B C_ RR ) /\ A. x e. A A. y e. B x < y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )
101 100 3impa 
 |-  ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x < y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) )