Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltexnq Structured version   Unicode version

Theorem ltexnq 8857
 Description: Ordering on positive fractions in terms of existence of sum. Definition in Proposition 9-2.6 of [Gleason] p. 119. (Contributed by NM, 24-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
Assertion
Ref Expression
ltexnq
Distinct variable groups:   ,   ,

Proof of Theorem ltexnq
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelnq 8808 . . . 4
21brel 4929 . . 3
3 ordpinq 8825 . . . 4
4 elpqn 8807 . . . . . . . . 9
54adantr 453 . . . . . . . 8
6 xp1st 6379 . . . . . . . 8
75, 6syl 16 . . . . . . 7
8 elpqn 8807 . . . . . . . . 9
98adantl 454 . . . . . . . 8
10 xp2nd 6380 . . . . . . . 8
119, 10syl 16 . . . . . . 7
12 mulclpi 8775 . . . . . . 7
137, 11, 12syl2anc 644 . . . . . 6
14 xp1st 6379 . . . . . . . 8
159, 14syl 16 . . . . . . 7
16 xp2nd 6380 . . . . . . . 8
175, 16syl 16 . . . . . . 7
18 mulclpi 8775 . . . . . . 7
1915, 17, 18syl2anc 644 . . . . . 6
20 ltexpi 8784 . . . . . 6
2113, 19, 20syl2anc 644 . . . . 5
22 relxp 4986 . . . . . . . . . . . 12
234ad2antrr 708 . . . . . . . . . . . 12
24 1st2nd 6396 . . . . . . . . . . . 12
2522, 23, 24sylancr 646 . . . . . . . . . . 11
2625oveq1d 6099 . . . . . . . . . 10
277adantr 453 . . . . . . . . . . 11
2817adantr 453 . . . . . . . . . . 11
29 simpr 449 . . . . . . . . . . 11
30 mulclpi 8775 . . . . . . . . . . . . 13
3117, 11, 30syl2anc 644 . . . . . . . . . . . 12
3231adantr 453 . . . . . . . . . . 11
33 addpipq 8819 . . . . . . . . . . 11
3427, 28, 29, 32, 33syl22anc 1186 . . . . . . . . . 10
3526, 34eqtrd 2470 . . . . . . . . 9
36 oveq2 6092 . . . . . . . . . . . 12
37 distrpi 8780 . . . . . . . . . . . . 13
38 fvex 5745 . . . . . . . . . . . . . . 15
39 fvex 5745 . . . . . . . . . . . . . . 15
40 fvex 5745 . . . . . . . . . . . . . . 15
41 mulcompi 8778 . . . . . . . . . . . . . . 15
42 mulasspi 8779 . . . . . . . . . . . . . . 15
4338, 39, 40, 41, 42caov12 6278 . . . . . . . . . . . . . 14
44 mulcompi 8778 . . . . . . . . . . . . . 14
4543, 44oveq12i 6096 . . . . . . . . . . . . 13
4637, 45eqtr2i 2459 . . . . . . . . . . . 12
47 mulasspi 8779 . . . . . . . . . . . . 13
48 mulcompi 8778 . . . . . . . . . . . . . 14
4948oveq2i 6095 . . . . . . . . . . . . 13
5047, 49eqtri 2458 . . . . . . . . . . . 12
5136, 46, 503eqtr4g 2495 . . . . . . . . . . 11
52 mulasspi 8779 . . . . . . . . . . . . 13
5352eqcomi 2442 . . . . . . . . . . . 12
5453a1i 11 . . . . . . . . . . 11
5551, 54opeq12d 3994 . . . . . . . . . 10
5655eqeq2d 2449 . . . . . . . . 9
5735, 56syl5ibcom 213 . . . . . . . 8
58 fveq2 5731 . . . . . . . . 9
59 adderpq 8838 . . . . . . . . . . 11
60 nqerid 8815 . . . . . . . . . . . . 13
6160ad2antrr 708 . . . . . . . . . . . 12
6261oveq1d 6099 . . . . . . . . . . 11
6359, 62syl5eqr 2484 . . . . . . . . . 10
64 mulclpi 8775 . . . . . . . . . . . . . . . 16
6517, 17, 64syl2anc 644 . . . . . . . . . . . . . . 15
6665adantr 453 . . . . . . . . . . . . . 14
6715adantr 453 . . . . . . . . . . . . . 14
6811adantr 453 . . . . . . . . . . . . . 14
69 mulcanenq 8842 . . . . . . . . . . . . . 14
7066, 67, 68, 69syl3anc 1185 . . . . . . . . . . . . 13
718ad2antlr 709 . . . . . . . . . . . . . 14
72 1st2nd 6396 . . . . . . . . . . . . . 14
7322, 71, 72sylancr 646 . . . . . . . . . . . . 13
7470, 73breqtrrd 4241 . . . . . . . . . . . 12
75 mulclpi 8775 . . . . . . . . . . . . . . 15
7666, 67, 75syl2anc 644 . . . . . . . . . . . . . 14
77 mulclpi 8775 . . . . . . . . . . . . . . 15
7866, 68, 77syl2anc 644 . . . . . . . . . . . . . 14
79 opelxpi 4913 . . . . . . . . . . . . . 14
8076, 78, 79syl2anc 644 . . . . . . . . . . . . 13
81 nqereq 8817 . . . . . . . . . . . . 13
8280, 71, 81syl2anc 644 . . . . . . . . . . . 12
8374, 82mpbid 203 . . . . . . . . . . 11
84 nqerid 8815 . . . . . . . . . . . 12
8584ad2antlr 709 . . . . . . . . . . 11
8683, 85eqtrd 2470 . . . . . . . . . 10
8763, 86eqeq12d 2452 . . . . . . . . 9
8858, 87syl5ib 212 . . . . . . . 8
8957, 88syld 43 . . . . . . 7
90 fvex 5745 . . . . . . . 8
91 oveq2 6092 . . . . . . . . 9
9291eqeq1d 2446 . . . . . . . 8
9390, 92spcev 3045 . . . . . . 7
9489, 93syl6 32 . . . . . 6
9594rexlimdva 2832 . . . . 5
9621, 95sylbid 208 . . . 4
973, 96sylbid 208 . . 3
982, 97mpcom 35 . 2
99 eleq1 2498 . . . . . . 7
10099biimparc 475 . . . . . 6
101 addnqf 8830 . . . . . . . 8
102101fdmi 5599 . . . . . . 7
103 0nnq 8806 . . . . . . 7
104102, 103ndmovrcl 6236 . . . . . 6
105 ltaddnq 8856 . . . . . 6
106100, 104, 1053syl 19 . . . . 5
107 simpr 449 . . . . 5
108106, 107breqtrd 4239 . . . 4
109108ex 425 . . 3
110109exlimdv 1647 . 2
11198, 110impbid2 197 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360  wex 1551   wceq 1653   wcel 1726  wrex 2708  cop 3819   class class class wbr 4215   cxp 4879   wrel 4886  cfv 5457  (class class class)co 6084  c1st 6350  c2nd 6351  cnpi 8724   cpli 8725   cmi 8726   clti 8727   cplpq 8728   ceq 8731  cnq 8732  cerq 8734   cplq 8735   cltq 8738 This theorem is referenced by:  ltbtwnnq  8860  prnmadd  8879  ltexprlem4  8921  ltexprlem7  8924  prlem936  8929 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-1st 6352  df-2nd 6353  df-recs 6636  df-rdg 6671  df-1o 6727  df-oadd 6731  df-omul 6732  df-er 6908  df-ni 8754  df-pli 8755  df-mi 8756  df-lti 8757  df-plpq 8790  df-mpq 8791  df-ltpq 8792  df-enq 8793  df-nq 8794  df-erq 8795  df-plq 8796  df-mq 8797  df-1nq 8798  df-ltnq 8800
 Copyright terms: Public domain W3C validator