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

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

Proof of Theorem mullocpr
Dummy variables 𝑑 𝑒 𝑡 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prop 6716 . . . . . . . 8 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
2 prmuloc 6807 . . . . . . . 8 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑞 <Q 𝑟) → ∃𝑑Q𝑢Q (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))
31, 2sylan 277 . . . . . . 7 ((𝐴P𝑞 <Q 𝑟) → ∃𝑑Q𝑢Q (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))
4 r2ex 2387 . . . . . . 7 (∃𝑑Q𝑢Q (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)) ↔ ∃𝑑𝑢((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟))))
53, 4sylib 120 . . . . . 6 ((𝐴P𝑞 <Q 𝑟) → ∃𝑑𝑢((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟))))
65adantlr 461 . . . . 5 (((𝐴P𝐵P) ∧ 𝑞 <Q 𝑟) → ∃𝑑𝑢((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟))))
76adantlr 461 . . . 4 ((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) → ∃𝑑𝑢((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟))))
8 simprr3 989 . . . . . . . 8 (((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟))
9 simprl 498 . . . . . . . . 9 (((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (𝑑Q𝑢Q))
10 mulclnq 6617 . . . . . . . . 9 ((𝑑Q𝑢Q) → (𝑑 ·Q 𝑢) ∈ Q)
119, 10syl 14 . . . . . . . 8 (((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (𝑑 ·Q 𝑢) ∈ Q)
12 appdivnq 6804 . . . . . . . 8 (((𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟) ∧ (𝑑 ·Q 𝑢) ∈ Q) → ∃𝑒Q ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))
138, 11, 12syl2anc 403 . . . . . . 7 (((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → ∃𝑒Q ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))
14 simprrr 507 . . . . . . . . 9 ((((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) → (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟))
1511adantr 270 . . . . . . . . 9 ((((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) → (𝑑 ·Q 𝑢) ∈ Q)
16 appdivnq 6804 . . . . . . . . 9 (((𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟) ∧ (𝑑 ·Q 𝑢) ∈ Q) → ∃𝑡Q ((𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑡 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑡 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))
1714, 15, 16syl2anc 403 . . . . . . . 8 ((((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) → ∃𝑡Q ((𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑡 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑡 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))
18 simplll 500 . . . . . . . . . 10 (((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (𝐴P𝐵P))
1918ad2antrr 472 . . . . . . . . 9 (((((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑡Q ∧ ((𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑡 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑡 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) → (𝐴P𝐵P))
20 simprl 498 . . . . . . . . . 10 ((𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟))) → (𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)))
2120ad2antlr 473 . . . . . . . . 9 (((((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑡Q ∧ ((𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑡 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑡 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) → (𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)))
22 simprrl 506 . . . . . . . . 9 (((((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑡Q ∧ ((𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑡 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑡 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) → (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑡 ·Q (𝑑 ·Q 𝑢)))
23 simprrr 507 . . . . . . . . 9 (((((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑡Q ∧ ((𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑡 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑡 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) → (𝑡 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟))
24 simpllr 501 . . . . . . . . . 10 (((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (𝑞Q𝑟Q))
2524ad2antrr 472 . . . . . . . . 9 (((((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑡Q ∧ ((𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑡 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑡 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) → (𝑞Q𝑟Q))
269ad2antrr 472 . . . . . . . . 9 (((((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑡Q ∧ ((𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑡 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑡 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) → (𝑑Q𝑢Q))
27 3simpa 936 . . . . . . . . . . 11 ((𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)) → (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴)))
2827ad2antll 475 . . . . . . . . . 10 (((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴)))
2928ad2antrr 472 . . . . . . . . 9 (((((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑡Q ∧ ((𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑡 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑡 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) → (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴)))
30 simplrl 502 . . . . . . . . . 10 (((((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑡Q ∧ ((𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑡 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑡 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) → 𝑒Q)
31 simprl 498 . . . . . . . . . 10 (((((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑡Q ∧ ((𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑡 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑡 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) → 𝑡Q)
3230, 31jca 300 . . . . . . . . 9 (((((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑡Q ∧ ((𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑡 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑡 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) → (𝑒Q𝑡Q))
3319, 21, 22, 23, 25, 26, 29, 32mullocprlem 6811 . . . . . . . 8 (((((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑡Q ∧ ((𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑡 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑡 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) → (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵))))
3417, 33rexlimddv 2482 . . . . . . 7 ((((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) ∧ (𝑒Q ∧ ((𝑢 ·Q 𝑞) <Q (𝑒 ·Q (𝑑 ·Q 𝑢)) ∧ (𝑒 ·Q (𝑑 ·Q 𝑢)) <Q (𝑑 ·Q 𝑟)))) → (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵))))
3513, 34rexlimddv 2482 . . . . . 6 (((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) ∧ ((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟)))) → (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵))))
3635ex 113 . . . . 5 ((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) → (((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟))) → (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)))))
3736exlimdvv 1819 . . . 4 ((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) → (∃𝑑𝑢((𝑑Q𝑢Q) ∧ (𝑑 ∈ (1st𝐴) ∧ 𝑢 ∈ (2nd𝐴) ∧ (𝑢 ·Q 𝑞) <Q (𝑑 ·Q 𝑟))) → (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)))))
387, 37mpd 13 . . 3 ((((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) ∧ 𝑞 <Q 𝑟) → (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵))))
3938ex 113 . 2 (((𝐴P𝐵P) ∧ (𝑞Q𝑟Q)) → (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)))))
4039ralrimivva 2444 1 ((𝐴P𝐵P) → ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘(𝐴 ·P 𝐵)) ∨ 𝑟 ∈ (2nd ‘(𝐴 ·P 𝐵)))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102   ∨ wo 662   ∧ w3a 920  ∃wex 1422   ∈ wcel 1434  ∀wral 2349  ∃wrex 2350  ⟨cop 3403   class class class wbr 3787  ‘cfv 4926  (class class class)co 5537  1st c1st 5790  2nd c2nd 5791  Qcnq 6521   ·Q cmq 6524
 Copyright terms: Public domain W3C validator