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

Theorem archrecpr 7516
 Description: Archimedean principle for positive reals (reciprocal version). (Contributed by Jim Kingdon, 25-Nov-2020.)
Assertion
Ref Expression
archrecpr (𝐴P → ∃𝑗N ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑗, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑢}⟩<P 𝐴)
Distinct variable groups:   𝐴,𝑗   𝑗,𝑙,𝑢
Allowed substitution hints:   𝐴(𝑢,𝑙)

Proof of Theorem archrecpr
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 prop 7327 . . . 4 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
2 prml 7329 . . . 4 (⟨(1st𝐴), (2nd𝐴)⟩ ∈ P → ∃𝑥Q 𝑥 ∈ (1st𝐴))
31, 2syl 14 . . 3 (𝐴P → ∃𝑥Q 𝑥 ∈ (1st𝐴))
4 archrecnq 7515 . . . . 5 (𝑥Q → ∃𝑗N (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥)
54ad2antrl 482 . . . 4 ((𝐴P ∧ (𝑥Q𝑥 ∈ (1st𝐴))) → ∃𝑗N (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥)
61ad2antrr 480 . . . . . 6 (((𝐴P ∧ (𝑥Q𝑥 ∈ (1st𝐴))) ∧ 𝑗N) → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
7 simplrr 526 . . . . . 6 (((𝐴P ∧ (𝑥Q𝑥 ∈ (1st𝐴))) ∧ 𝑗N) → 𝑥 ∈ (1st𝐴))
8 prcdnql 7336 . . . . . 6 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑥 ∈ (1st𝐴)) → ((*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥 → (*Q‘[⟨𝑗, 1o⟩] ~Q ) ∈ (1st𝐴)))
96, 7, 8syl2anc 409 . . . . 5 (((𝐴P ∧ (𝑥Q𝑥 ∈ (1st𝐴))) ∧ 𝑗N) → ((*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥 → (*Q‘[⟨𝑗, 1o⟩] ~Q ) ∈ (1st𝐴)))
109reximdva 2538 . . . 4 ((𝐴P ∧ (𝑥Q𝑥 ∈ (1st𝐴))) → (∃𝑗N (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑥 → ∃𝑗N (*Q‘[⟨𝑗, 1o⟩] ~Q ) ∈ (1st𝐴)))
115, 10mpd 13 . . 3 ((𝐴P ∧ (𝑥Q𝑥 ∈ (1st𝐴))) → ∃𝑗N (*Q‘[⟨𝑗, 1o⟩] ~Q ) ∈ (1st𝐴))
123, 11rexlimddv 2558 . 2 (𝐴P → ∃𝑗N (*Q‘[⟨𝑗, 1o⟩] ~Q ) ∈ (1st𝐴))
13 nnnq 7274 . . . . . 6 (𝑗N → [⟨𝑗, 1o⟩] ~QQ)
14 recclnq 7244 . . . . . 6 ([⟨𝑗, 1o⟩] ~QQ → (*Q‘[⟨𝑗, 1o⟩] ~Q ) ∈ Q)
1513, 14syl 14 . . . . 5 (𝑗N → (*Q‘[⟨𝑗, 1o⟩] ~Q ) ∈ Q)
1615adantl 275 . . . 4 ((𝐴P𝑗N) → (*Q‘[⟨𝑗, 1o⟩] ~Q ) ∈ Q)
17 simpl 108 . . . 4 ((𝐴P𝑗N) → 𝐴P)
18 nqprl 7403 . . . 4 (((*Q‘[⟨𝑗, 1o⟩] ~Q ) ∈ Q𝐴P) → ((*Q‘[⟨𝑗, 1o⟩] ~Q ) ∈ (1st𝐴) ↔ ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑗, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑢}⟩<P 𝐴))
1916, 17, 18syl2anc 409 . . 3 ((𝐴P𝑗N) → ((*Q‘[⟨𝑗, 1o⟩] ~Q ) ∈ (1st𝐴) ↔ ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑗, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑢}⟩<P 𝐴))
2019rexbidva 2436 . 2 (𝐴P → (∃𝑗N (*Q‘[⟨𝑗, 1o⟩] ~Q ) ∈ (1st𝐴) ↔ ∃𝑗N ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑗, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑢}⟩<P 𝐴))
2112, 20mpbid 146 1 (𝐴P → ∃𝑗N ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑗, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑢}⟩<P 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∈ wcel 1481  {cab 2126  ∃wrex 2418  ⟨cop 3536   class class class wbr 3938  ‘cfv 5132  1st c1st 6045  2nd c2nd 6046  1oc1o 6315  [cec 6436  Ncnpi 7124   ~Q ceq 7131  Qcnq 7132  *Qcrq 7136
 Copyright terms: Public domain W3C validator