Metamath Proof Explorer

Theorem genpnnp

Description: The result of an operation on positive reals is different from the set of positive fractions. (Contributed by NM, 29-Feb-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypotheses genp.1 
|- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )
genp.2 
|- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )
genpnnp.3 
|- ( z e. Q. -> ( x  ( z G x )
genpnnp.4 
|- ( x G y ) = ( y G x )
Assertion genpnnp 
|- ( ( A e. P. /\ B e. P. ) -> -. ( A F B ) = Q. )

Proof

Step Hyp Ref Expression
1 genp.1 
 |-  F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )
2 genp.2 
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )
3 genpnnp.3 
 |-  ( z e. Q. -> ( x  ( z G x )
4 genpnnp.4 
 |-  ( x G y ) = ( y G x )
5 prpssnq 
 |-  ( A e. P. -> A C. Q. )
6 pssnel 
 |-  ( A C. Q. -> E. w ( w e. Q. /\ -. w e. A ) )
7 5 6 syl 
 |-  ( A e. P. -> E. w ( w e. Q. /\ -. w e. A ) )
8 prpssnq 
 |-  ( B e. P. -> B C. Q. )
9 pssnel 
 |-  ( B C. Q. -> E. v ( v e. Q. /\ -. v e. B ) )
10 8 9 syl 
 |-  ( B e. P. -> E. v ( v e. Q. /\ -. v e. B ) )
11 7 10 anim12i 
 |-  ( ( A e. P. /\ B e. P. ) -> ( E. w ( w e. Q. /\ -. w e. A ) /\ E. v ( v e. Q. /\ -. v e. B ) ) )
12 exdistrv 
 |-  ( E. w E. v ( ( w e. Q. /\ -. w e. A ) /\ ( v e. Q. /\ -. v e. B ) ) <-> ( E. w ( w e. Q. /\ -. w e. A ) /\ E. v ( v e. Q. /\ -. v e. B ) ) )
13 11 12 sylibr 
 |-  ( ( A e. P. /\ B e. P. ) -> E. w E. v ( ( w e. Q. /\ -. w e. A ) /\ ( v e. Q. /\ -. v e. B ) ) )
14 prub 
 |-  ( ( ( A e. P. /\ f e. A ) /\ w e. Q. ) -> ( -. w e. A -> f
15 prub 
 |-  ( ( ( B e. P. /\ g e. B ) /\ v e. Q. ) -> ( -. v e. B -> g
16 14 15 im2anan9 
 |-  ( ( ( ( A e. P. /\ f e. A ) /\ w e. Q. ) /\ ( ( B e. P. /\ g e. B ) /\ v e. Q. ) ) -> ( ( -. w e. A /\ -. v e. B ) -> ( f
17 elprnq 
 |-  ( ( A e. P. /\ f e. A ) -> f e. Q. )
18 17 anim1i 
 |-  ( ( ( A e. P. /\ f e. A ) /\ w e. Q. ) -> ( f e. Q. /\ w e. Q. ) )
19 elprnq 
 |-  ( ( B e. P. /\ g e. B ) -> g e. Q. )
20 19 anim1i 
 |-  ( ( ( B e. P. /\ g e. B ) /\ v e. Q. ) -> ( g e. Q. /\ v e. Q. ) )
21 ltsonq 
 |-
22 so2nr 
 |-  ( (  -. ( f
23 21 22 mpan 
 |-  ( ( f e. Q. /\ w e. Q. ) -> -. ( f
24 23 ad2antrr 
 |-  ( ( ( ( f e. Q. /\ w e. Q. ) /\ ( g e. Q. /\ v e. Q. ) ) /\ ( w G v ) = ( f G g ) ) -> -. ( f
25 simpr 
 |-  ( ( g e. Q. /\ v e. Q. ) -> v e. Q. )
26 simpl 
 |-  ( ( f e. Q. /\ w e. Q. ) -> f e. Q. )
27 25 26 anim12i 
 |-  ( ( ( g e. Q. /\ v e. Q. ) /\ ( f e. Q. /\ w e. Q. ) ) -> ( v e. Q. /\ f e. Q. ) )
28 27 ancoms 
 |-  ( ( ( f e. Q. /\ w e. Q. ) /\ ( g e. Q. /\ v e. Q. ) ) -> ( v e. Q. /\ f e. Q. ) )
29 vex 
 |-  w e. _V
30 vex 
 |-  v e. _V
31 vex 
 |-  f e. _V
32 vex 
 |-  g e. _V
33 29 30 3 31 4 32 caovord3 
 |-  ( ( ( v e. Q. /\ f e. Q. ) /\ ( w G v ) = ( f G g ) ) -> ( w  g
34 33 anbi2d 
 |-  ( ( ( v e. Q. /\ f e. Q. ) /\ ( w G v ) = ( f G g ) ) -> ( ( f  ( f
35 28 34 sylan 
 |-  ( ( ( ( f e. Q. /\ w e. Q. ) /\ ( g e. Q. /\ v e. Q. ) ) /\ ( w G v ) = ( f G g ) ) -> ( ( f  ( f
36 24 35 mtbid 
 |-  ( ( ( ( f e. Q. /\ w e. Q. ) /\ ( g e. Q. /\ v e. Q. ) ) /\ ( w G v ) = ( f G g ) ) -> -. ( f
37 36 ex 
 |-  ( ( ( f e. Q. /\ w e. Q. ) /\ ( g e. Q. /\ v e. Q. ) ) -> ( ( w G v ) = ( f G g ) -> -. ( f
38 37 con2d 
 |-  ( ( ( f e. Q. /\ w e. Q. ) /\ ( g e. Q. /\ v e. Q. ) ) -> ( ( f  -. ( w G v ) = ( f G g ) ) )
39 18 20 38 syl2an 
 |-  ( ( ( ( A e. P. /\ f e. A ) /\ w e. Q. ) /\ ( ( B e. P. /\ g e. B ) /\ v e. Q. ) ) -> ( ( f  -. ( w G v ) = ( f G g ) ) )
40 16 39 syld 
 |-  ( ( ( ( A e. P. /\ f e. A ) /\ w e. Q. ) /\ ( ( B e. P. /\ g e. B ) /\ v e. Q. ) ) -> ( ( -. w e. A /\ -. v e. B ) -> -. ( w G v ) = ( f G g ) ) )
41 40 an4s 
 |-  ( ( ( ( A e. P. /\ f e. A ) /\ ( B e. P. /\ g e. B ) ) /\ ( w e. Q. /\ v e. Q. ) ) -> ( ( -. w e. A /\ -. v e. B ) -> -. ( w G v ) = ( f G g ) ) )
42 41 ex 
 |-  ( ( ( A e. P. /\ f e. A ) /\ ( B e. P. /\ g e. B ) ) -> ( ( w e. Q. /\ v e. Q. ) -> ( ( -. w e. A /\ -. v e. B ) -> -. ( w G v ) = ( f G g ) ) ) )
43 42 an4s 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( f e. A /\ g e. B ) ) -> ( ( w e. Q. /\ v e. Q. ) -> ( ( -. w e. A /\ -. v e. B ) -> -. ( w G v ) = ( f G g ) ) ) )
44 43 ex 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( f e. A /\ g e. B ) -> ( ( w e. Q. /\ v e. Q. ) -> ( ( -. w e. A /\ -. v e. B ) -> -. ( w G v ) = ( f G g ) ) ) ) )
45 44 com24 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( -. w e. A /\ -. v e. B ) -> ( ( w e. Q. /\ v e. Q. ) -> ( ( f e. A /\ g e. B ) -> -. ( w G v ) = ( f G g ) ) ) ) )
46 45 imp32 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( ( -. w e. A /\ -. v e. B ) /\ ( w e. Q. /\ v e. Q. ) ) ) -> ( ( f e. A /\ g e. B ) -> -. ( w G v ) = ( f G g ) ) )
47 46 ralrimivv 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( ( -. w e. A /\ -. v e. B ) /\ ( w e. Q. /\ v e. Q. ) ) ) -> A. f e. A A. g e. B -. ( w G v ) = ( f G g ) )
48 ralnex2 
 |-  ( A. f e. A A. g e. B -. ( w G v ) = ( f G g ) <-> -. E. f e. A E. g e. B ( w G v ) = ( f G g ) )
49 47 48 sylib 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( ( -. w e. A /\ -. v e. B ) /\ ( w e. Q. /\ v e. Q. ) ) ) -> -. E. f e. A E. g e. B ( w G v ) = ( f G g ) )
50 1 2 genpelv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( w G v ) e. ( A F B ) <-> E. f e. A E. g e. B ( w G v ) = ( f G g ) ) )
51 50 adantr 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( ( -. w e. A /\ -. v e. B ) /\ ( w e. Q. /\ v e. Q. ) ) ) -> ( ( w G v ) e. ( A F B ) <-> E. f e. A E. g e. B ( w G v ) = ( f G g ) ) )
52 49 51 mtbird 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ ( ( -. w e. A /\ -. v e. B ) /\ ( w e. Q. /\ v e. Q. ) ) ) -> -. ( w G v ) e. ( A F B ) )
53 52 expcom 
 |-  ( ( ( -. w e. A /\ -. v e. B ) /\ ( w e. Q. /\ v e. Q. ) ) -> ( ( A e. P. /\ B e. P. ) -> -. ( w G v ) e. ( A F B ) ) )
54 53 ancoms 
 |-  ( ( ( w e. Q. /\ v e. Q. ) /\ ( -. w e. A /\ -. v e. B ) ) -> ( ( A e. P. /\ B e. P. ) -> -. ( w G v ) e. ( A F B ) ) )
55 54 an4s 
 |-  ( ( ( w e. Q. /\ -. w e. A ) /\ ( v e. Q. /\ -. v e. B ) ) -> ( ( A e. P. /\ B e. P. ) -> -. ( w G v ) e. ( A F B ) ) )
56 2 caovcl 
 |-  ( ( w e. Q. /\ v e. Q. ) -> ( w G v ) e. Q. )
57 eleq2 
 |-  ( ( A F B ) = Q. -> ( ( w G v ) e. ( A F B ) <-> ( w G v ) e. Q. ) )
58 57 biimprcd 
 |-  ( ( w G v ) e. Q. -> ( ( A F B ) = Q. -> ( w G v ) e. ( A F B ) ) )
59 58 con3d 
 |-  ( ( w G v ) e. Q. -> ( -. ( w G v ) e. ( A F B ) -> -. ( A F B ) = Q. ) )
60 56 59 syl 
 |-  ( ( w e. Q. /\ v e. Q. ) -> ( -. ( w G v ) e. ( A F B ) -> -. ( A F B ) = Q. ) )
61 60 ad2ant2r 
 |-  ( ( ( w e. Q. /\ -. w e. A ) /\ ( v e. Q. /\ -. v e. B ) ) -> ( -. ( w G v ) e. ( A F B ) -> -. ( A F B ) = Q. ) )
62 55 61 syldc 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( ( w e. Q. /\ -. w e. A ) /\ ( v e. Q. /\ -. v e. B ) ) -> -. ( A F B ) = Q. ) )
63 62 exlimdvv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( E. w E. v ( ( w e. Q. /\ -. w e. A ) /\ ( v e. Q. /\ -. v e. B ) ) -> -. ( A F B ) = Q. ) )
64 13 63 mpd 
 |-  ( ( A e. P. /\ B e. P. ) -> -. ( A F B ) = Q. )