Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-arch Unicode version

Axiom ax-arch 7739
 Description: Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by theorem axarch 7699. This axiom should not be used directly; instead use arch 8974 (which is the same, but stated in terms of and ). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.)
Assertion
Ref Expression
ax-arch
Distinct variable group:   ,,,

Detailed syntax breakdown of Axiom ax-arch
StepHypRef Expression
1 cA . . 3
2 cr 7619 . . 3
31, 2wcel 1480 . 2
4 vn . . . . 5
54cv 1330 . . . 4
6 cltrr 7624 . . . 4
71, 5, 6wbr 3929 . . 3
8 c1 7621 . . . . . . 7
9 vx . . . . . . . 8
109cv 1330 . . . . . . 7
118, 10wcel 1480 . . . . . 6
12 vy . . . . . . . . . 10
1312cv 1330 . . . . . . . . 9
14 caddc 7623 . . . . . . . . 9
1513, 8, 14co 5774 . . . . . . . 8
1615, 10wcel 1480 . . . . . . 7
1716, 12, 10wral 2416 . . . . . 6
1811, 17wa 103 . . . . 5
1918, 9cab 2125 . . . 4
2019cint 3771 . . 3
217, 4, 20wrex 2417 . 2
223, 21wi 4 1
 Colors of variables: wff set class This axiom is referenced by:  arch  8974
 Copyright terms: Public domain W3C validator