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

Theorem appdiv0nq 7392
 Description: Approximate division for positive rationals. This can be thought of as a variation of appdivnq 7391 in which 𝐴 is zero, although it can be stated and proved in terms of positive rationals alone, without zero as such. (Contributed by Jim Kingdon, 9-Dec-2019.)
Assertion
Ref Expression
appdiv0nq ((𝐵Q𝐶Q) → ∃𝑚Q (𝑚 ·Q 𝐶) <Q 𝐵)
Distinct variable groups:   𝐵,𝑚   𝐶,𝑚

Proof of Theorem appdiv0nq
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 nsmallnqq 7240 . . 3 (𝐵Q → ∃𝑥Q 𝑥 <Q 𝐵)
21adantr 274 . 2 ((𝐵Q𝐶Q) → ∃𝑥Q 𝑥 <Q 𝐵)
3 appdivnq 7391 . . . . 5 ((𝑥 <Q 𝐵𝐶Q) → ∃𝑚Q (𝑥 <Q (𝑚 ·Q 𝐶) ∧ (𝑚 ·Q 𝐶) <Q 𝐵))
4 simpr 109 . . . . . 6 ((𝑥 <Q (𝑚 ·Q 𝐶) ∧ (𝑚 ·Q 𝐶) <Q 𝐵) → (𝑚 ·Q 𝐶) <Q 𝐵)
54reximi 2530 . . . . 5 (∃𝑚Q (𝑥 <Q (𝑚 ·Q 𝐶) ∧ (𝑚 ·Q 𝐶) <Q 𝐵) → ∃𝑚Q (𝑚 ·Q 𝐶) <Q 𝐵)
63, 5syl 14 . . . 4 ((𝑥 <Q 𝐵𝐶Q) → ∃𝑚Q (𝑚 ·Q 𝐶) <Q 𝐵)
76ancoms 266 . . 3 ((𝐶Q𝑥 <Q 𝐵) → ∃𝑚Q (𝑚 ·Q 𝐶) <Q 𝐵)
87ad2ant2l 500 . 2 (((𝐵Q𝐶Q) ∧ (𝑥Q𝑥 <Q 𝐵)) → ∃𝑚Q (𝑚 ·Q 𝐶) <Q 𝐵)
92, 8rexlimddv 2555 1 ((𝐵Q𝐶Q) → ∃𝑚Q (𝑚 ·Q 𝐶) <Q 𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1481  ∃wrex 2418   class class class wbr 3933  (class class class)co 5778  Qcnq 7108   ·Q cmq 7111
 Copyright terms: Public domain W3C validator