ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addnqprllem GIF version

Theorem addnqprllem 7528
Description: Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
Assertion
Ref Expression
addnqprllem (((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โ†’ (๐‘‹ <Q ๐‘† โ†’ ((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) โˆˆ ๐ฟ))

Proof of Theorem addnqprllem
Dummy variables ๐‘ค ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 110 . . . . 5 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ ๐‘‹ <Q ๐‘†)
2 ltrnqi 7422 . . . . . 6 (๐‘‹ <Q ๐‘† โ†’ (*Qโ€˜๐‘†) <Q (*Qโ€˜๐‘‹))
3 ltrelnq 7366 . . . . . . . . . . . 12 <Q โІ (Q ร— Q)
43brel 4680 . . . . . . . . . . 11 (๐‘‹ <Q ๐‘† โ†’ (๐‘‹ โˆˆ Q โˆง ๐‘† โˆˆ Q))
54adantl 277 . . . . . . . . . 10 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ (๐‘‹ โˆˆ Q โˆง ๐‘† โˆˆ Q))
65simprd 114 . . . . . . . . 9 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ ๐‘† โˆˆ Q)
7 recclnq 7393 . . . . . . . . 9 (๐‘† โˆˆ Q โ†’ (*Qโ€˜๐‘†) โˆˆ Q)
86, 7syl 14 . . . . . . . 8 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ (*Qโ€˜๐‘†) โˆˆ Q)
9 simplr 528 . . . . . . . . 9 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ ๐‘‹ โˆˆ Q)
10 recclnq 7393 . . . . . . . . 9 (๐‘‹ โˆˆ Q โ†’ (*Qโ€˜๐‘‹) โˆˆ Q)
119, 10syl 14 . . . . . . . 8 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ (*Qโ€˜๐‘‹) โˆˆ Q)
12 ltmnqg 7402 . . . . . . . 8 (((*Qโ€˜๐‘†) โˆˆ Q โˆง (*Qโ€˜๐‘‹) โˆˆ Q โˆง ๐‘‹ โˆˆ Q) โ†’ ((*Qโ€˜๐‘†) <Q (*Qโ€˜๐‘‹) โ†” (๐‘‹ ยทQ (*Qโ€˜๐‘†)) <Q (๐‘‹ ยทQ (*Qโ€˜๐‘‹))))
138, 11, 9, 12syl3anc 1238 . . . . . . 7 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ ((*Qโ€˜๐‘†) <Q (*Qโ€˜๐‘‹) โ†” (๐‘‹ ยทQ (*Qโ€˜๐‘†)) <Q (๐‘‹ ยทQ (*Qโ€˜๐‘‹))))
14 ltmnqg 7402 . . . . . . . . 9 ((๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q โˆง ๐‘ค โˆˆ Q) โ†’ (๐‘ฆ <Q ๐‘ง โ†” (๐‘ค ยทQ ๐‘ฆ) <Q (๐‘ค ยทQ ๐‘ง)))
1514adantl 277 . . . . . . . 8 (((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โˆง (๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q โˆง ๐‘ค โˆˆ Q)) โ†’ (๐‘ฆ <Q ๐‘ง โ†” (๐‘ค ยทQ ๐‘ฆ) <Q (๐‘ค ยทQ ๐‘ง)))
16 mulclnq 7377 . . . . . . . . 9 ((๐‘‹ โˆˆ Q โˆง (*Qโ€˜๐‘†) โˆˆ Q) โ†’ (๐‘‹ ยทQ (*Qโ€˜๐‘†)) โˆˆ Q)
179, 8, 16syl2anc 411 . . . . . . . 8 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ (๐‘‹ ยทQ (*Qโ€˜๐‘†)) โˆˆ Q)
18 mulclnq 7377 . . . . . . . . 9 ((๐‘‹ โˆˆ Q โˆง (*Qโ€˜๐‘‹) โˆˆ Q) โ†’ (๐‘‹ ยทQ (*Qโ€˜๐‘‹)) โˆˆ Q)
199, 11, 18syl2anc 411 . . . . . . . 8 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ (๐‘‹ ยทQ (*Qโ€˜๐‘‹)) โˆˆ Q)
20 elprnql 7482 . . . . . . . . 9 ((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โ†’ ๐บ โˆˆ Q)
2120ad2antrr 488 . . . . . . . 8 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ ๐บ โˆˆ Q)
22 mulcomnqg 7384 . . . . . . . . 9 ((๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q) โ†’ (๐‘ฆ ยทQ ๐‘ง) = (๐‘ง ยทQ ๐‘ฆ))
2322adantl 277 . . . . . . . 8 (((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โˆง (๐‘ฆ โˆˆ Q โˆง ๐‘ง โˆˆ Q)) โ†’ (๐‘ฆ ยทQ ๐‘ง) = (๐‘ง ยทQ ๐‘ฆ))
2415, 17, 19, 21, 23caovord2d 6046 . . . . . . 7 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ ((๐‘‹ ยทQ (*Qโ€˜๐‘†)) <Q (๐‘‹ ยทQ (*Qโ€˜๐‘‹)) โ†” ((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) <Q ((๐‘‹ ยทQ (*Qโ€˜๐‘‹)) ยทQ ๐บ)))
2513, 24bitrd 188 . . . . . 6 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ ((*Qโ€˜๐‘†) <Q (*Qโ€˜๐‘‹) โ†” ((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) <Q ((๐‘‹ ยทQ (*Qโ€˜๐‘‹)) ยทQ ๐บ)))
262, 25imbitrid 154 . . . . 5 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ (๐‘‹ <Q ๐‘† โ†’ ((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) <Q ((๐‘‹ ยทQ (*Qโ€˜๐‘‹)) ยทQ ๐บ)))
271, 26mpd 13 . . . 4 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ ((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) <Q ((๐‘‹ ยทQ (*Qโ€˜๐‘‹)) ยทQ ๐บ))
28 recidnq 7394 . . . . . . . 8 (๐‘‹ โˆˆ Q โ†’ (๐‘‹ ยทQ (*Qโ€˜๐‘‹)) = 1Q)
2928oveq1d 5892 . . . . . . 7 (๐‘‹ โˆˆ Q โ†’ ((๐‘‹ ยทQ (*Qโ€˜๐‘‹)) ยทQ ๐บ) = (1Q ยทQ ๐บ))
30 1nq 7367 . . . . . . . . 9 1Q โˆˆ Q
31 mulcomnqg 7384 . . . . . . . . 9 ((1Q โˆˆ Q โˆง ๐บ โˆˆ Q) โ†’ (1Q ยทQ ๐บ) = (๐บ ยทQ 1Q))
3230, 31mpan 424 . . . . . . . 8 (๐บ โˆˆ Q โ†’ (1Q ยทQ ๐บ) = (๐บ ยทQ 1Q))
33 mulidnq 7390 . . . . . . . 8 (๐บ โˆˆ Q โ†’ (๐บ ยทQ 1Q) = ๐บ)
3432, 33eqtrd 2210 . . . . . . 7 (๐บ โˆˆ Q โ†’ (1Q ยทQ ๐บ) = ๐บ)
3529, 34sylan9eqr 2232 . . . . . 6 ((๐บ โˆˆ Q โˆง ๐‘‹ โˆˆ Q) โ†’ ((๐‘‹ ยทQ (*Qโ€˜๐‘‹)) ยทQ ๐บ) = ๐บ)
3635breq2d 4017 . . . . 5 ((๐บ โˆˆ Q โˆง ๐‘‹ โˆˆ Q) โ†’ (((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) <Q ((๐‘‹ ยทQ (*Qโ€˜๐‘‹)) ยทQ ๐บ) โ†” ((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) <Q ๐บ))
3721, 9, 36syl2anc 411 . . . 4 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ (((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) <Q ((๐‘‹ ยทQ (*Qโ€˜๐‘‹)) ยทQ ๐บ) โ†” ((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) <Q ๐บ))
3827, 37mpbid 147 . . 3 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ ((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) <Q ๐บ)
39 prcdnql 7485 . . . 4 ((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โ†’ (((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) <Q ๐บ โ†’ ((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) โˆˆ ๐ฟ))
4039ad2antrr 488 . . 3 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ (((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) <Q ๐บ โ†’ ((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) โˆˆ ๐ฟ))
4138, 40mpd 13 . 2 ((((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โˆง ๐‘‹ <Q ๐‘†) โ†’ ((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) โˆˆ ๐ฟ)
4241ex 115 1 (((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐บ โˆˆ ๐ฟ) โˆง ๐‘‹ โˆˆ Q) โ†’ (๐‘‹ <Q ๐‘† โ†’ ((๐‘‹ ยทQ (*Qโ€˜๐‘†)) ยทQ ๐บ) โˆˆ ๐ฟ))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆง w3a 978   = wceq 1353   โˆˆ wcel 2148  โŸจcop 3597   class class class wbr 4005  โ€˜cfv 5218  (class class class)co 5877  Qcnq 7281  1Qc1q 7282   ยทQ cmq 7284  *Qcrq 7285   <Q cltq 7286  Pcnp 7292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-eprel 4291  df-id 4295  df-iord 4368  df-on 4370  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-ov 5880  df-oprab 5881  df-mpo 5882  df-1st 6143  df-2nd 6144  df-recs 6308  df-irdg 6373  df-1o 6419  df-oadd 6423  df-omul 6424  df-er 6537  df-ec 6539  df-qs 6543  df-ni 7305  df-mi 7307  df-lti 7308  df-mpq 7346  df-enq 7348  df-nqqs 7349  df-mqqs 7351  df-1nqqs 7352  df-rq 7353  df-ltnqqs 7354  df-inp 7467
This theorem is referenced by:  addnqprl  7530
  Copyright terms: Public domain W3C validator