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

Theorem addnqprulem 6370
Description: Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
Assertion
Ref Expression
addnqprulem (((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) → (𝑆 <Q 𝑋 → ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺) 𝑈))

Proof of Theorem addnqprulem
Dummy variables y z w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 103 . . . . 5 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → 𝑆 <Q 𝑋)
2 ltrnqi 6265 . . . . . 6 (𝑆 <Q 𝑋 → (*Q𝑋) <Q (*Q𝑆))
3 simplr 467 . . . . . . . . 9 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → 𝑋 Q)
4 recclnq 6238 . . . . . . . . 9 (𝑋 Q → (*Q𝑋) Q)
53, 4syl 14 . . . . . . . 8 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → (*Q𝑋) Q)
6 ltrelnq 6211 . . . . . . . . . . . 12 <Q ⊆ (Q × Q)
76brel 4308 . . . . . . . . . . 11 (𝑆 <Q 𝑋 → (𝑆 Q 𝑋 Q))
87adantl 262 . . . . . . . . . 10 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → (𝑆 Q 𝑋 Q))
98simpld 105 . . . . . . . . 9 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → 𝑆 Q)
10 recclnq 6238 . . . . . . . . 9 (𝑆 Q → (*Q𝑆) Q)
119, 10syl 14 . . . . . . . 8 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → (*Q𝑆) Q)
12 ltmnqg 6247 . . . . . . . 8 (((*Q𝑋) Q (*Q𝑆) Q 𝑋 Q) → ((*Q𝑋) <Q (*Q𝑆) ↔ (𝑋 ·Q (*Q𝑋)) <Q (𝑋 ·Q (*Q𝑆))))
135, 11, 3, 12syl3anc 1116 . . . . . . 7 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → ((*Q𝑋) <Q (*Q𝑆) ↔ (𝑋 ·Q (*Q𝑋)) <Q (𝑋 ·Q (*Q𝑆))))
14 ltmnqg 6247 . . . . . . . . 9 ((y Q z Q w Q) → (y <Q z ↔ (w ·Q y) <Q (w ·Q z)))
1514adantl 262 . . . . . . . 8 (((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) (y Q z Q w Q)) → (y <Q z ↔ (w ·Q y) <Q (w ·Q z)))
16 mulclnq 6222 . . . . . . . . 9 ((𝑋 Q (*Q𝑋) Q) → (𝑋 ·Q (*Q𝑋)) Q)
173, 5, 16syl2anc 391 . . . . . . . 8 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → (𝑋 ·Q (*Q𝑋)) Q)
18 mulclnq 6222 . . . . . . . . 9 ((𝑋 Q (*Q𝑆) Q) → (𝑋 ·Q (*Q𝑆)) Q)
193, 11, 18syl2anc 391 . . . . . . . 8 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → (𝑋 ·Q (*Q𝑆)) Q)
20 elprnqu 6323 . . . . . . . . 9 ((⟨𝐿, 𝑈 P 𝐺 𝑈) → 𝐺 Q)
2120ad2antrr 457 . . . . . . . 8 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → 𝐺 Q)
22 mulcomnqg 6229 . . . . . . . . 9 ((y Q z Q) → (y ·Q z) = (z ·Q y))
2322adantl 262 . . . . . . . 8 (((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) (y Q z Q)) → (y ·Q z) = (z ·Q y))
2415, 17, 19, 21, 23caovord2d 5582 . . . . . . 7 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → ((𝑋 ·Q (*Q𝑋)) <Q (𝑋 ·Q (*Q𝑆)) ↔ ((𝑋 ·Q (*Q𝑋)) ·Q 𝐺) <Q ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺)))
2513, 24bitrd 177 . . . . . 6 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → ((*Q𝑋) <Q (*Q𝑆) ↔ ((𝑋 ·Q (*Q𝑋)) ·Q 𝐺) <Q ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺)))
262, 25syl5ib 143 . . . . 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 6239 . . . . . . . 8 (𝑋 Q → (𝑋 ·Q (*Q𝑋)) = 1Q)
2928oveq1d 5440 . . . . . . 7 (𝑋 Q → ((𝑋 ·Q (*Q𝑋)) ·Q 𝐺) = (1Q ·Q 𝐺))
30 1nq 6212 . . . . . . . . 9 1Q Q
31 mulcomnqg 6229 . . . . . . . . 9 ((1Q Q 𝐺 Q) → (1Q ·Q 𝐺) = (𝐺 ·Q 1Q))
3230, 31mpan 400 . . . . . . . 8 (𝐺 Q → (1Q ·Q 𝐺) = (𝐺 ·Q 1Q))
33 mulidnq 6235 . . . . . . . 8 (𝐺 Q → (𝐺 ·Q 1Q) = 𝐺)
3432, 33eqtrd 2046 . . . . . . 7 (𝐺 Q → (1Q ·Q 𝐺) = 𝐺)
3529, 34sylan9eqr 2068 . . . . . 6 ((𝐺 Q 𝑋 Q) → ((𝑋 ·Q (*Q𝑋)) ·Q 𝐺) = 𝐺)
3635breq1d 3738 . . . . 5 ((𝐺 Q 𝑋 Q) → (((𝑋 ·Q (*Q𝑋)) ·Q 𝐺) <Q ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺) ↔ 𝐺 <Q ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺)))
3721, 3, 36syl2anc 391 . . . 4 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → (((𝑋 ·Q (*Q𝑋)) ·Q 𝐺) <Q ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺) ↔ 𝐺 <Q ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺)))
3827, 37mpbid 135 . . 3 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → 𝐺 <Q ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺))
39 prcunqu 6326 . . . 4 ((⟨𝐿, 𝑈 P 𝐺 𝑈) → (𝐺 <Q ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺) → ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺) 𝑈))
4039ad2antrr 457 . . 3 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → (𝐺 <Q ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺) → ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺) 𝑈))
4138, 40mpd 13 . 2 ((((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) 𝑆 <Q 𝑋) → ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺) 𝑈)
4241ex 108 1 (((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) → (𝑆 <Q 𝑋 → ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺) 𝑈))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   w3a 867   = wceq 1224   wcel 1367  cop 3343   class class class wbr 3728  cfv 4818  (class class class)co 5425  Qcnq 6127  1Qc1q 6128   ·Q cmq 6130  *Qcrq 6131   <Q cltq 6132  Pcnp 6138
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 529  ax-in2 530  ax-io 614  ax-5 1310  ax-7 1311  ax-gen 1312  ax-ie1 1356  ax-ie2 1357  ax-8 1369  ax-10 1370  ax-11 1371  ax-i12 1372  ax-bnd 1373  ax-4 1374  ax-13 1378  ax-14 1379  ax-17 1393  ax-i9 1397  ax-ial 1401  ax-i5r 1402  ax-ext 1996  ax-coll 3836  ax-sep 3839  ax-nul 3847  ax-pow 3891  ax-pr 3908  ax-un 4109  ax-setind 4193  ax-iinf 4227
This theorem depends on definitions:  df-bi 110  df-dc 727  df-3or 868  df-3an 869  df-tru 1227  df-fal 1230  df-nf 1324  df-sb 1620  df-eu 1877  df-mo 1878  df-clab 2001  df-cleq 2007  df-clel 2010  df-nfc 2141  df-ne 2180  df-ral 2281  df-rex 2282  df-reu 2283  df-rab 2285  df-v 2529  df-sbc 2734  df-csb 2822  df-dif 2889  df-un 2891  df-in 2893  df-ss 2900  df-nul 3194  df-pw 3326  df-sn 3346  df-pr 3347  df-op 3349  df-uni 3545  df-int 3580  df-iun 3623  df-br 3729  df-opab 3783  df-mpt 3784  df-tr 3819  df-eprel 3990  df-id 3994  df-iord 4042  df-on 4044  df-suc 4047  df-iom 4230  df-xp 4267  df-rel 4268  df-cnv 4269  df-co 4270  df-dm 4271  df-rn 4272  df-res 4273  df-ima 4274  df-iota 4783  df-fun 4820  df-fn 4821  df-f 4822  df-f1 4823  df-fo 4824  df-f1o 4825  df-fv 4826  df-ov 5428  df-oprab 5429  df-mpt2 5430  df-1st 5679  df-2nd 5680  df-recs 5831  df-irdg 5867  df-1o 5905  df-oadd 5909  df-omul 5910  df-er 6006  df-ec 6008  df-qs 6012  df-ni 6151  df-mi 6153  df-lti 6154  df-mpq 6191  df-enq 6193  df-nqqs 6194  df-mqqs 6196  df-1nqqs 6197  df-rq 6198  df-ltnqqs 6199  df-inp 6307
This theorem is referenced by:  addnqpru  6372
  Copyright terms: Public domain W3C validator