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

Theorem archsr 6923
 Description: For any signed real, there is an integer that is greater than it. This is also known as the "archimedean property". The expression [⟨(⟨{𝑙 ∣ 𝑙
Assertion
Ref Expression
archsr (𝐴R → ∃𝑥N 𝐴 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
Distinct variable group:   𝐴,𝑙,𝑢,𝑥

Proof of Theorem archsr
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nr 6869 . 2 R = ((P × P) / ~R )
2 breq1 3794 . . 3 ([⟨𝑧, 𝑤⟩] ~R = 𝐴 → ([⟨𝑧, 𝑤⟩] ~R <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R𝐴 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))
32rexbidv 2344 . 2 ([⟨𝑧, 𝑤⟩] ~R = 𝐴 → (∃𝑥N [⟨𝑧, 𝑤⟩] ~R <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ↔ ∃𝑥N 𝐴 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))
4 1pr 6709 . . . . . . 7 1PP
5 addclpr 6692 . . . . . . 7 ((𝑧P ∧ 1PP) → (𝑧 +P 1P) ∈ P)
64, 5mpan2 409 . . . . . 6 (𝑧P → (𝑧 +P 1P) ∈ P)
7 archpr 6798 . . . . . 6 ((𝑧 +P 1P) ∈ P → ∃𝑥N (𝑧 +P 1P)<P ⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩)
86, 7syl 14 . . . . 5 (𝑧P → ∃𝑥N (𝑧 +P 1P)<P ⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩)
98adantr 265 . . . 4 ((𝑧P𝑤P) → ∃𝑥N (𝑧 +P 1P)<P ⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩)
10 nnprlu 6708 . . . . . . . . . 10 (𝑥N → ⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ ∈ P)
1110adantl 266 . . . . . . . . 9 (((𝑧P𝑤P) ∧ 𝑥N) → ⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ ∈ P)
12 addclpr 6692 . . . . . . . . 9 ((⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ ∈ P ∧ 1PP) → (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P) ∈ P)
1311, 4, 12sylancl 398 . . . . . . . 8 (((𝑧P𝑤P) ∧ 𝑥N) → (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P) ∈ P)
14 simplr 490 . . . . . . . 8 (((𝑧P𝑤P) ∧ 𝑥N) → 𝑤P)
15 ltaddpr 6752 . . . . . . . 8 (((⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P) ∈ P𝑤P) → (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P)<P ((⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P) +P 𝑤))
1613, 14, 15syl2anc 397 . . . . . . 7 (((𝑧P𝑤P) ∧ 𝑥N) → (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P)<P ((⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P) +P 𝑤))
17 addcomprg 6733 . . . . . . . 8 ((𝑤P ∧ (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P) ∈ P) → (𝑤 +P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P)) = ((⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P) +P 𝑤))
1814, 13, 17syl2anc 397 . . . . . . 7 (((𝑧P𝑤P) ∧ 𝑥N) → (𝑤 +P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P)) = ((⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P) +P 𝑤))
1916, 18breqtrrd 3817 . . . . . 6 (((𝑧P𝑤P) ∧ 𝑥N) → (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P)<P (𝑤 +P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P)))
20 ltaddpr 6752 . . . . . . . 8 ((⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ ∈ P ∧ 1PP) → ⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩<P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P))
2111, 4, 20sylancl 398 . . . . . . 7 (((𝑧P𝑤P) ∧ 𝑥N) → ⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩<P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P))
22 ltsopr 6751 . . . . . . . . 9 <P Or P
23 ltrelpr 6660 . . . . . . . . 9 <P ⊆ (P × P)
2422, 23sotri 4747 . . . . . . . 8 (((𝑧 +P 1P)<P ⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ ∧ ⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩<P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P)) → (𝑧 +P 1P)<P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P))
2524expcom 113 . . . . . . 7 (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩<P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P) → ((𝑧 +P 1P)<P ⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ → (𝑧 +P 1P)<P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P)))
2621, 25syl 14 . . . . . 6 (((𝑧P𝑤P) ∧ 𝑥N) → ((𝑧 +P 1P)<P ⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ → (𝑧 +P 1P)<P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P)))
2722, 23sotri 4747 . . . . . . 7 (((𝑧 +P 1P)<P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P) ∧ (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P)<P (𝑤 +P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P))) → (𝑧 +P 1P)<P (𝑤 +P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P)))
2827expcom 113 . . . . . 6 ((⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P)<P (𝑤 +P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P)) → ((𝑧 +P 1P)<P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P) → (𝑧 +P 1P)<P (𝑤 +P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P))))
2919, 26, 28sylsyld 56 . . . . 5 (((𝑧P𝑤P) ∧ 𝑥N) → ((𝑧 +P 1P)<P ⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ → (𝑧 +P 1P)<P (𝑤 +P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P))))
3029reximdva 2438 . . . 4 ((𝑧P𝑤P) → (∃𝑥N (𝑧 +P 1P)<P ⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ → ∃𝑥N (𝑧 +P 1P)<P (𝑤 +P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P))))
319, 30mpd 13 . . 3 ((𝑧P𝑤P) → ∃𝑥N (𝑧 +P 1P)<P (𝑤 +P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P)))
32 simpl 106 . . . . 5 (((𝑧P𝑤P) ∧ 𝑥N) → (𝑧P𝑤P))
334a1i 9 . . . . 5 (((𝑧P𝑤P) ∧ 𝑥N) → 1PP)
34 ltsrprg 6889 . . . . 5 (((𝑧P𝑤P) ∧ ((⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P) ∈ P ∧ 1PP)) → ([⟨𝑧, 𝑤⟩] ~R <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ↔ (𝑧 +P 1P)<P (𝑤 +P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P))))
3532, 13, 33, 34syl12anc 1144 . . . 4 (((𝑧P𝑤P) ∧ 𝑥N) → ([⟨𝑧, 𝑤⟩] ~R <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ↔ (𝑧 +P 1P)<P (𝑤 +P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P))))
3635rexbidva 2340 . . 3 ((𝑧P𝑤P) → (∃𝑥N [⟨𝑧, 𝑤⟩] ~R <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ↔ ∃𝑥N (𝑧 +P 1P)<P (𝑤 +P (⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P))))
3731, 36mpbird 160 . 2 ((𝑧P𝑤P) → ∃𝑥N [⟨𝑧, 𝑤⟩] ~R <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
381, 3, 37ecoptocl 6223 1 (𝐴R → ∃𝑥N 𝐴 <R [⟨(⟨{𝑙𝑙 <Q [⟨𝑥, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   = wceq 1259   ∈ wcel 1409  {cab 2042  ∃wrex 2324  ⟨cop 3405   class class class wbr 3791  (class class class)co 5539  1𝑜c1o 6024  [cec 6134  Ncnpi 6427   ~Q ceq 6434
 Copyright terms: Public domain W3C validator