Axiom ax-arch 7932

Description: Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by Theorem axarch 7892.

This axiom should not be used directly; instead use arch 9175 (which is the same, but stated in terms of NN and <). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-arch	|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )

Distinct variable group:   A, n, x, y

Detailed syntax breakdown of Axiom ax-arch

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cr 7812	. . 3 class RR
3	1, 2	wcel 2148	. 2 wff A e. RR
4		vn	. . . . 5 setvar n
5	4	cv 1352	. . . 4 class n
6		cltrr 7817	. . . 4 class <RR
7	1, 5, 6	wbr 4005	. . 3 wff A <RR n
8		c1 7814	. . . . . . 7 class 1
9		vx	. . . . . . . 8 setvar x
10	9	cv 1352	. . . . . . 7 class x
11	8, 10	wcel 2148	. . . . . 6 wff 1 e. x
12		vy	. . . . . . . . . 10 setvar y
13	12	cv 1352	. . . . . . . . 9 class y
14		caddc 7816	. . . . . . . . 9 class +
15	13, 8, 14	co 5877	. . . . . . . 8 class ( y + 1 )
16	15, 10	wcel 2148	. . . . . . 7 wff ( y + 1 ) e. x
17	16, 12, 10	wral 2455	. . . . . 6 wff A. y e. x ( y + 1 ) e. x
18	11, 17	wa 104	. . . . 5 wff ( 1 e. x /\ A. y e. x ( y + 1 ) e. x )
19	18, 9	cab 2163	. . . 4 class { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
20	19	cint 3846	. . 3 class |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }
21	7, 4, 20	wrex 2456	. 2 wff E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n
22	3, 21	wi 4	1 wff ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )

This axiom is referenced by:  arch  9175