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

Theorem archrecpr 6819
 Description: Archimedean principle for positive reals (reciprocal version). (Contributed by Jim Kingdon, 25-Nov-2020.)
Assertion
Ref Expression
archrecpr (𝐴P → ∃𝑗N ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑗, 1𝑜⟩] ~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 6630 . . . 4 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
2 prml 6632 . . . 4 (⟨(1st𝐴), (2nd𝐴)⟩ ∈ P → ∃𝑥Q 𝑥 ∈ (1st𝐴))
31, 2syl 14 . . 3 (𝐴P → ∃𝑥Q 𝑥 ∈ (1st𝐴))
4 archrecnq 6818 . . . . 5 (𝑥Q → ∃𝑗N (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) <Q 𝑥)
54ad2antrl 467 . . . 4 ((𝐴P ∧ (𝑥Q𝑥 ∈ (1st𝐴))) → ∃𝑗N (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) <Q 𝑥)
61ad2antrr 465 . . . . . 6 (((𝐴P ∧ (𝑥Q𝑥 ∈ (1st𝐴))) ∧ 𝑗N) → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
7 simplrr 496 . . . . . 6 (((𝐴P ∧ (𝑥Q𝑥 ∈ (1st𝐴))) ∧ 𝑗N) → 𝑥 ∈ (1st𝐴))
8 prcdnql 6639 . . . . . 6 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑥 ∈ (1st𝐴)) → ((*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) <Q 𝑥 → (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) ∈ (1st𝐴)))
96, 7, 8syl2anc 397 . . . . 5 (((𝐴P ∧ (𝑥Q𝑥 ∈ (1st𝐴))) ∧ 𝑗N) → ((*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) <Q 𝑥 → (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) ∈ (1st𝐴)))
109reximdva 2438 . . . 4 ((𝐴P ∧ (𝑥Q𝑥 ∈ (1st𝐴))) → (∃𝑗N (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) <Q 𝑥 → ∃𝑗N (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) ∈ (1st𝐴)))
115, 10mpd 13 . . 3 ((𝐴P ∧ (𝑥Q𝑥 ∈ (1st𝐴))) → ∃𝑗N (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) ∈ (1st𝐴))
123, 11rexlimddv 2454 . 2 (𝐴P → ∃𝑗N (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) ∈ (1st𝐴))
13 nnnq 6577 . . . . . 6 (𝑗N → [⟨𝑗, 1𝑜⟩] ~QQ)
14 recclnq 6547 . . . . . 6 ([⟨𝑗, 1𝑜⟩] ~QQ → (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) ∈ Q)
1513, 14syl 14 . . . . 5 (𝑗N → (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) ∈ Q)
1615adantl 266 . . . 4 ((𝐴P𝑗N) → (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) ∈ Q)
17 simpl 106 . . . 4 ((𝐴P𝑗N) → 𝐴P)
18 nqprl 6706 . . . 4 (((*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) ∈ Q𝐴P) → ((*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) ∈ (1st𝐴) ↔ ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) <Q 𝑢}⟩<P 𝐴))
1916, 17, 18syl2anc 397 . . 3 ((𝐴P𝑗N) → ((*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) ∈ (1st𝐴) ↔ ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) <Q 𝑢}⟩<P 𝐴))
2019rexbidva 2340 . 2 (𝐴P → (∃𝑗N (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) ∈ (1st𝐴) ↔ ∃𝑗N ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) <Q 𝑢}⟩<P 𝐴))
2112, 20mpbid 139 1 (𝐴P → ∃𝑗N ⟨{𝑙𝑙 <Q (*Q‘[⟨𝑗, 1𝑜⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑗, 1𝑜⟩] ~Q ) <Q 𝑢}⟩<P 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   ∈ wcel 1409  {cab 2042  ∃wrex 2324  ⟨cop 3405   class class class wbr 3791  ‘cfv 4929  1st c1st 5792  2nd c2nd 5793  1𝑜c1o 6024  [cec 6134  Ncnpi 6427   ~Q ceq 6434  Qcnq 6435  *Qcrq 6439
 Copyright terms: Public domain W3C validator