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

Theorem archrecnq 7522
 Description: Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.)
Assertion
Ref Expression
archrecnq (𝐴Q → ∃𝑗N (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝐴)
Distinct variable group:   𝐴,𝑗

Proof of Theorem archrecnq
StepHypRef Expression
1 recclnq 7251 . . 3 (𝐴Q → (*Q𝐴) ∈ Q)
2 archnqq 7276 . . 3 ((*Q𝐴) ∈ Q → ∃𝑗N (*Q𝐴) <Q [⟨𝑗, 1o⟩] ~Q )
31, 2syl 14 . 2 (𝐴Q → ∃𝑗N (*Q𝐴) <Q [⟨𝑗, 1o⟩] ~Q )
4 nnnq 7281 . . . . 5 (𝑗N → [⟨𝑗, 1o⟩] ~QQ)
5 ltrnqg 7279 . . . . 5 (((*Q𝐴) ∈ Q ∧ [⟨𝑗, 1o⟩] ~QQ) → ((*Q𝐴) <Q [⟨𝑗, 1o⟩] ~Q ↔ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q (*Q‘(*Q𝐴))))
61, 4, 5syl2an 287 . . . 4 ((𝐴Q𝑗N) → ((*Q𝐴) <Q [⟨𝑗, 1o⟩] ~Q ↔ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q (*Q‘(*Q𝐴))))
7 recrecnq 7253 . . . . . 6 (𝐴Q → (*Q‘(*Q𝐴)) = 𝐴)
87breq2d 3950 . . . . 5 (𝐴Q → ((*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q (*Q‘(*Q𝐴)) ↔ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝐴))
98adantr 274 . . . 4 ((𝐴Q𝑗N) → ((*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q (*Q‘(*Q𝐴)) ↔ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝐴))
106, 9bitrd 187 . . 3 ((𝐴Q𝑗N) → ((*Q𝐴) <Q [⟨𝑗, 1o⟩] ~Q ↔ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝐴))
1110rexbidva 2436 . 2 (𝐴Q → (∃𝑗N (*Q𝐴) <Q [⟨𝑗, 1o⟩] ~Q ↔ ∃𝑗N (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝐴))
123, 11mpbid 146 1 (𝐴Q → ∃𝑗N (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∈ wcel 1481  ∃wrex 2418  ⟨cop 3536   class class class wbr 3938  ‘cfv 5134  1oc1o 6317  [cec 6438  Ncnpi 7131   ~Q ceq 7138  Qcnq 7139  *Qcrq 7143
 Copyright terms: Public domain W3C validator