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

Theorem mullocpr 6402
Description: Locatedness of multiplication on positive reals. Lemma 12.9 in [BauerTaylor], p. 56 (but where both A and B are positive, not just A). (Contributed by Jim Kingdon, 8-Dec-2019.)
Assertion
Ref Expression
mullocpr ((A P B P) → 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1st ‘(A ·P B)) 𝑟 (2nd ‘(A ·P B)))))
Distinct variable groups:   A,𝑞,𝑟   B,𝑞,𝑟

Proof of Theorem mullocpr
Dummy variables 𝑑 𝑒 𝑡 u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prop 6316 . . . . . . . 8 (A P → ⟨(1stA), (2ndA)⟩ P)
2 prmuloc 6397 . . . . . . . 8 ((⟨(1stA), (2ndA)⟩ P 𝑞 <Q 𝑟) → 𝑑 Q u Q (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))
31, 2sylan 267 . . . . . . 7 ((A P 𝑞 <Q 𝑟) → 𝑑 Q u Q (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))
4 r2ex 2314 . . . . . . 7 (𝑑 Q u Q (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)) ↔ 𝑑u((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟))))
53, 4sylib 127 . . . . . 6 ((A P 𝑞 <Q 𝑟) → 𝑑u((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟))))
65adantlr 446 . . . . 5 (((A P B P) 𝑞 <Q 𝑟) → 𝑑u((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟))))
76adantlr 446 . . . 4 ((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) → 𝑑u((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟))))
8 simprr3 936 . . . . . . . 8 (((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟))
9 simprl 468 . . . . . . . . 9 (((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (𝑑 Q u Q))
10 mulclnq 6222 . . . . . . . . 9 ((𝑑 Q u Q) → (𝑑 ·Q u) Q)
119, 10syl 14 . . . . . . . 8 (((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (𝑑 ·Q u) Q)
12 appdivnq 6394 . . . . . . . 8 (((u ·Q 𝑞) <Q (𝑑 ·Q 𝑟) (𝑑 ·Q u) Q) → 𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))
138, 11, 12syl2anc 391 . . . . . . 7 (((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → 𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))
14 simprrr 477 . . . . . . . . 9 ((((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) (𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) → (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟))
1511adantr 261 . . . . . . . . 9 ((((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) (𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) → (𝑑 ·Q u) Q)
16 appdivnq 6394 . . . . . . . . 9 (((𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟) (𝑑 ·Q u) Q) → 𝑡 Q ((𝑒 ·Q (𝑑 ·Q u)) <Q (𝑡 ·Q (𝑑 ·Q u)) (𝑡 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))
1714, 15, 16syl2anc 391 . . . . . . . 8 ((((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) (𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) → 𝑡 Q ((𝑒 ·Q (𝑑 ·Q u)) <Q (𝑡 ·Q (𝑑 ·Q u)) (𝑡 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))
18 simplll 470 . . . . . . . . . 10 (((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (A P B P))
1918ad2antrr 457 . . . . . . . . 9 (((((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) (𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) (𝑡 Q ((𝑒 ·Q (𝑑 ·Q u)) <Q (𝑡 ·Q (𝑑 ·Q u)) (𝑡 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) → (A P B P))
20 simprl 468 . . . . . . . . . 10 ((𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟))) → (u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)))
2120ad2antlr 459 . . . . . . . . 9 (((((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) (𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) (𝑡 Q ((𝑒 ·Q (𝑑 ·Q u)) <Q (𝑡 ·Q (𝑑 ·Q u)) (𝑡 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) → (u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)))
22 simprrl 476 . . . . . . . . 9 (((((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) (𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) (𝑡 Q ((𝑒 ·Q (𝑑 ·Q u)) <Q (𝑡 ·Q (𝑑 ·Q u)) (𝑡 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) → (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑡 ·Q (𝑑 ·Q u)))
23 simprrr 477 . . . . . . . . 9 (((((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) (𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) (𝑡 Q ((𝑒 ·Q (𝑑 ·Q u)) <Q (𝑡 ·Q (𝑑 ·Q u)) (𝑡 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) → (𝑡 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟))
24 simpllr 471 . . . . . . . . . 10 (((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (𝑞 Q 𝑟 Q))
2524ad2antrr 457 . . . . . . . . 9 (((((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) (𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) (𝑡 Q ((𝑒 ·Q (𝑑 ·Q u)) <Q (𝑡 ·Q (𝑑 ·Q u)) (𝑡 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) → (𝑞 Q 𝑟 Q))
269ad2antrr 457 . . . . . . . . 9 (((((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) (𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) (𝑡 Q ((𝑒 ·Q (𝑑 ·Q u)) <Q (𝑡 ·Q (𝑑 ·Q u)) (𝑡 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) → (𝑑 Q u Q))
27 3simpa 883 . . . . . . . . . . 11 ((𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)) → (𝑑 (1stA) u (2ndA)))
2827ad2antll 461 . . . . . . . . . 10 (((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (𝑑 (1stA) u (2ndA)))
2928ad2antrr 457 . . . . . . . . 9 (((((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) (𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) (𝑡 Q ((𝑒 ·Q (𝑑 ·Q u)) <Q (𝑡 ·Q (𝑑 ·Q u)) (𝑡 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) → (𝑑 (1stA) u (2ndA)))
30 simplrl 472 . . . . . . . . . 10 (((((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) (𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) (𝑡 Q ((𝑒 ·Q (𝑑 ·Q u)) <Q (𝑡 ·Q (𝑑 ·Q u)) (𝑡 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) → 𝑒 Q)
31 simprl 468 . . . . . . . . . 10 (((((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) (𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) (𝑡 Q ((𝑒 ·Q (𝑑 ·Q u)) <Q (𝑡 ·Q (𝑑 ·Q u)) (𝑡 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) → 𝑡 Q)
3230, 31jca 290 . . . . . . . . 9 (((((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) (𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) (𝑡 Q ((𝑒 ·Q (𝑑 ·Q u)) <Q (𝑡 ·Q (𝑑 ·Q u)) (𝑡 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) → (𝑒 Q 𝑡 Q))
3319, 21, 22, 23, 25, 26, 29, 32mullocprlem 6401 . . . . . . . 8 (((((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) (𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) (𝑡 Q ((𝑒 ·Q (𝑑 ·Q u)) <Q (𝑡 ·Q (𝑑 ·Q u)) (𝑡 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) → (𝑞 (1st ‘(A ·P B)) 𝑟 (2nd ‘(A ·P B))))
3417, 33rexlimddv 2407 . . . . . . 7 ((((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) (𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟)))) → (𝑞 (1st ‘(A ·P B)) 𝑟 (2nd ‘(A ·P B))))
3513, 34rexlimddv 2407 . . . . . 6 (((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (𝑞 (1st ‘(A ·P B)) 𝑟 (2nd ‘(A ·P B))))
3635ex 108 . . . . 5 ((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) → (((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟))) → (𝑞 (1st ‘(A ·P B)) 𝑟 (2nd ‘(A ·P B)))))
3736exlimdvv 1751 . . . 4 ((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) → (𝑑u((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟))) → (𝑞 (1st ‘(A ·P B)) 𝑟 (2nd ‘(A ·P B)))))
387, 37mpd 13 . . 3 ((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) → (𝑞 (1st ‘(A ·P B)) 𝑟 (2nd ‘(A ·P B))))
3938ex 108 . 2 (((A P B P) (𝑞 Q 𝑟 Q)) → (𝑞 <Q 𝑟 → (𝑞 (1st ‘(A ·P B)) 𝑟 (2nd ‘(A ·P B)))))
4039ralrimivva 2371 1 ((A P B P) → 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1st ‘(A ·P B)) 𝑟 (2nd ‘(A ·P B)))))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wo 613   w3a 867  wex 1355   wcel 1367  wral 2276  wrex 2277  cop 3343   class class class wbr 3728  cfv 4818  (class class class)co 5425  1st c1st 5677  2nd c2nd 5678  Qcnq 6127   ·Q cmq 6130   <Q cltq 6132  Pcnp 6138   ·P cmp 6141
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-po 3997  df-iso 3998  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-2o 5906  df-oadd 5909  df-omul 5910  df-er 6006  df-ec 6008  df-qs 6012  df-ni 6151  df-pli 6152  df-mi 6153  df-lti 6154  df-plpq 6190  df-mpq 6191  df-enq 6193  df-nqqs 6194  df-plqqs 6195  df-mqqs 6196  df-1nqqs 6197  df-rq 6198  df-ltnqqs 6199  df-enq0 6266  df-nq0 6267  df-0nq0 6268  df-plq0 6269  df-mq0 6270  df-inp 6307  df-imp 6310
This theorem is referenced by:  mulclpr  6403
  Copyright terms: Public domain W3C validator