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

Theorem mullocpr 6552
 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 6458 . . . . . . . 8 (A P → ⟨(1stA), (2ndA)⟩ P)
2 prmuloc 6547 . . . . . . . 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 2338 . . . . . . 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 953 . . . . . . . 8 (((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟))
9 simprl 483 . . . . . . . . 9 (((((A P B P) (𝑞 Q 𝑟 Q)) 𝑞 <Q 𝑟) ((𝑑 Q u Q) (𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (𝑑 Q u Q))
10 mulclnq 6360 . . . . . . . . 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 6544 . . . . . . . 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 492 . . . . . . . . 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 6544 . . . . . . . . 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 485 . . . . . . . . . 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 483 . . . . . . . . . 10 ((𝑒 Q ((u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)) (𝑒 ·Q (𝑑 ·Q u)) <Q (𝑑 ·Q 𝑟))) → (u ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q u)))
2120ad2antlr 458 . . . . . . . . 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 491 . . . . . . . . 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 492 . . . . . . . . 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 486 . . . . . . . . . 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 900 . . . . . . . . . . 11 ((𝑑 (1stA) u (2ndA) (u ·Q 𝑞) <Q (𝑑 ·Q 𝑟)) → (𝑑 (1stA) u (2ndA)))
2827ad2antll 460 . . . . . . . . . 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 487 . . . . . . . . . 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 483 . . . . . . . . . 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 6551 . . . . . . . 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 2431 . . . . . . 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 2431 . . . . . 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 1774 . . . 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 2395 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 628   ∧ w3a 884  ∃wex 1378   ∈ wcel 1390  ∀wral 2300  ∃wrex 2301  ⟨cop 3370   class class class wbr 3755  ‘cfv 4845  (class class class)co 5455  1st c1st 5707  2nd c2nd 5708  Qcnq 6264   ·Q cmq 6267
 Copyright terms: Public domain W3C validator