isarchi3

Description: This is the usual definition of the Archimedean property for an ordered group. (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Hypotheses	isarchi3.b	$⊢ B = {Base}_{W}$
	isarchi3.0	$⊢ \underset{˙}{0} = 0_{W}$
	isarchi3.i	$⊢ \underset{˙}{<} = <_{W}$
	isarchi3.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
Assertion	isarchi3	$⊢ W \in oGrp \to (W \in Archi \leftrightarrow \forall x \in B \forall y \in B (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \underset{˙}{<} (n \underset{˙}{\cdot} x)))$

Proof

Step	Hyp	Ref	Expression
1		isarchi3.b	$⊢ B = {Base}_{W}$
2		isarchi3.0	$⊢ \underset{˙}{0} = 0_{W}$
3		isarchi3.i	$⊢ \underset{˙}{<} = <_{W}$
4		isarchi3.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
5		isogrp	$⊢ W \in oGrp \leftrightarrow (W \in Grp \land W \in oMnd)$
6	5	simprbi	$⊢ W \in oGrp \to W \in oMnd$
7		omndtos	$⊢ W \in oMnd \to W \in Toset$
8	6 7	syl	$⊢ W \in oGrp \to W \in Toset$
9		grpmnd	$⊢ W \in Grp \to W \in Mnd$
10	9	adantr	$⊢ (W \in Grp \land W \in oMnd) \to W \in Mnd$
11	5 10	sylbi	$⊢ W \in oGrp \to W \in Mnd$
12		eqid	$⊢ \leq_{W} = \leq_{W}$
13	1 2 4 12 3	isarchi2	$⊢ (W \in Toset \land W \in Mnd) \to (W \in Archi \leftrightarrow \forall x \in B \forall y \in B (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \leq_{W} (n \underset{˙}{\cdot} x)))$
14	8 11 13	syl2anc	$⊢ W \in oGrp \to (W \in Archi \leftrightarrow \forall x \in B \forall y \in B (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \leq_{W} (n \underset{˙}{\cdot} x)))$
15		simpr	$⊢ ((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \to n \in ℕ$
16	15	adantr	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to n \in ℕ$
17	16	peano2nnd	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to n + 1 \in ℕ$
18		simp-4l	$⊢ ((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \to W \in oGrp$
19	18	adantr	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to W \in oGrp$
20		ogrpgrp	$⊢ W \in oGrp \to W \in Grp$
21	1 2	grpidcl	$⊢ W \in Grp \to \underset{˙}{0} \in B$
22	19 20 21	3syl	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to \underset{˙}{0} \in B$
23		simp-4r	$⊢ ((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \to x \in B$
24	23	adantr	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to x \in B$
25	20	ad4antr	$⊢ ((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \to W \in Grp$
26	15	nnzd	$⊢ ((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \to n \in ℤ$
27	1 4	mulgcl	$⊢ (W \in Grp \land n \in ℤ \land x \in B) \to n \underset{˙}{\cdot} x \in B$
28	25 26 23 27	syl3anc	$⊢ ((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \to n \underset{˙}{\cdot} x \in B$
29	28	adantr	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to n \underset{˙}{\cdot} x \in B$
30		simpllr	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to \underset{˙}{0} \underset{˙}{<} x$
31		eqid	$⊢ +_{W} = +_{W}$
32	1 3 31	ogrpaddlt	$⊢ (W \in oGrp \land (\underset{˙}{0} \in B \land x \in B \land n \underset{˙}{\cdot} x \in B) \land \underset{˙}{0} \underset{˙}{<} x) \to (\underset{˙}{0} +_{W} (n \underset{˙}{\cdot} x)) \underset{˙}{<} (x +_{W} (n \underset{˙}{\cdot} x))$
33	19 22 24 29 30 32	syl131anc	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to (\underset{˙}{0} +_{W} (n \underset{˙}{\cdot} x)) \underset{˙}{<} (x +_{W} (n \underset{˙}{\cdot} x))$
34	19 20	syl	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to W \in Grp$
35	1 31 2	grplid	$⊢ (W \in Grp \land n \underset{˙}{\cdot} x \in B) \to \underset{˙}{0} +_{W} (n \underset{˙}{\cdot} x) = n \underset{˙}{\cdot} x$
36	34 29 35	syl2anc	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to \underset{˙}{0} +_{W} (n \underset{˙}{\cdot} x) = n \underset{˙}{\cdot} x$
37		nncn	$⊢ n \in ℕ \to n \in ℂ$
38		ax-1cn	$⊢ 1 \in ℂ$
39		addcom	$⊢ (n \in ℂ \land 1 \in ℂ) \to n + 1 = 1 + n$
40	37 38 39	sylancl	$⊢ n \in ℕ \to n + 1 = 1 + n$
41	40	oveq1d	$⊢ n \in ℕ \to (n + 1) \underset{˙}{\cdot} x = (1 + n) \underset{˙}{\cdot} x$
42	16 41	syl	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to (n + 1) \underset{˙}{\cdot} x = (1 + n) \underset{˙}{\cdot} x$
43		grpsgrp	$⊢ W \in Grp \to W \in Smgrp$
44	19 20 43	3syl	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to W \in Smgrp$
45		1nn	$⊢ 1 \in ℕ$
46	45	a1i	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to 1 \in ℕ$
47	1 4 31	mulgnndir	$⊢ (W \in Smgrp \land (1 \in ℕ \land n \in ℕ \land x \in B)) \to (1 + n) \underset{˙}{\cdot} x = (1 \underset{˙}{\cdot} x) +_{W} (n \underset{˙}{\cdot} x)$
48	44 46 16 24 47	syl13anc	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to (1 + n) \underset{˙}{\cdot} x = (1 \underset{˙}{\cdot} x) +_{W} (n \underset{˙}{\cdot} x)$
49	1 4	mulg1	$⊢ x \in B \to 1 \underset{˙}{\cdot} x = x$
50	24 49	syl	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to 1 \underset{˙}{\cdot} x = x$
51	50	oveq1d	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to (1 \underset{˙}{\cdot} x) +_{W} (n \underset{˙}{\cdot} x) = x +_{W} (n \underset{˙}{\cdot} x)$
52	42 48 51	3eqtrrd	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to x +_{W} (n \underset{˙}{\cdot} x) = (n + 1) \underset{˙}{\cdot} x$
53	33 36 52	3brtr3d	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to (n \underset{˙}{\cdot} x) \underset{˙}{<} ((n + 1) \underset{˙}{\cdot} x)$
54		tospos	$⊢ W \in Toset \to W \in Poset$
55	18 8 54	3syl	$⊢ ((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \to W \in Poset$
56		simpllr	$⊢ ((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \to y \in B$
57	26	peano2zd	$⊢ ((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \to n + 1 \in ℤ$
58	1 4	mulgcl	$⊢ (W \in Grp \land n + 1 \in ℤ \land x \in B) \to (n + 1) \underset{˙}{\cdot} x \in B$
59	25 57 23 58	syl3anc	$⊢ ((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \to (n + 1) \underset{˙}{\cdot} x \in B$
60	1 12 3	plelttr	$⊢ (W \in Poset \land (y \in B \land n \underset{˙}{\cdot} x \in B \land (n + 1) \underset{˙}{\cdot} x \in B)) \to ((y \leq_{W} (n \underset{˙}{\cdot} x) \land (n \underset{˙}{\cdot} x) \underset{˙}{<} ((n + 1) \underset{˙}{\cdot} x)) \to y \underset{˙}{<} ((n + 1) \underset{˙}{\cdot} x))$
61	55 56 28 59 60	syl13anc	$⊢ ((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \to ((y \leq_{W} (n \underset{˙}{\cdot} x) \land (n \underset{˙}{\cdot} x) \underset{˙}{<} ((n + 1) \underset{˙}{\cdot} x)) \to y \underset{˙}{<} ((n + 1) \underset{˙}{\cdot} x))$
62	61	impl	$⊢ ((((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \land (n \underset{˙}{\cdot} x) \underset{˙}{<} ((n + 1) \underset{˙}{\cdot} x)) \to y \underset{˙}{<} ((n + 1) \underset{˙}{\cdot} x)$
63	53 62	mpdan	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to y \underset{˙}{<} ((n + 1) \underset{˙}{\cdot} x)$
64		oveq1	$⊢ m = n + 1 \to m \underset{˙}{\cdot} x = (n + 1) \underset{˙}{\cdot} x$
65	64	breq2d	$⊢ m = n + 1 \to (y \underset{˙}{<} (m \underset{˙}{\cdot} x) \leftrightarrow y \underset{˙}{<} ((n + 1) \underset{˙}{\cdot} x))$
66	65	rspcev	$⊢ (n + 1 \in ℕ \land y \underset{˙}{<} ((n + 1) \underset{˙}{\cdot} x)) \to \exists m \in ℕ y \underset{˙}{<} (m \underset{˙}{\cdot} x)$
67	17 63 66	syl2anc	$⊢ (((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \land y \leq_{W} (n \underset{˙}{\cdot} x)) \to \exists m \in ℕ y \underset{˙}{<} (m \underset{˙}{\cdot} x)$
68	67	r19.29an	$⊢ ((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land \exists n \in ℕ y \leq_{W} (n \underset{˙}{\cdot} x)) \to \exists m \in ℕ y \underset{˙}{<} (m \underset{˙}{\cdot} x)$
69		oveq1	$⊢ m = n \to m \underset{˙}{\cdot} x = n \underset{˙}{\cdot} x$
70	69	breq2d	$⊢ m = n \to (y \underset{˙}{<} (m \underset{˙}{\cdot} x) \leftrightarrow y \underset{˙}{<} (n \underset{˙}{\cdot} x))$
71	70	cbvrexvw	$⊢ \exists m \in ℕ y \underset{˙}{<} (m \underset{˙}{\cdot} x) \leftrightarrow \exists n \in ℕ y \underset{˙}{<} (n \underset{˙}{\cdot} x)$
72	68 71	sylib	$⊢ ((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land \exists n \in ℕ y \leq_{W} (n \underset{˙}{\cdot} x)) \to \exists n \in ℕ y \underset{˙}{<} (n \underset{˙}{\cdot} x)$
73	12 3	pltle	$⊢ (W \in oGrp \land y \in B \land n \underset{˙}{\cdot} x \in B) \to (y \underset{˙}{<} (n \underset{˙}{\cdot} x) \to y \leq_{W} (n \underset{˙}{\cdot} x))$
74	18 56 28 73	syl3anc	$⊢ ((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land n \in ℕ) \to (y \underset{˙}{<} (n \underset{˙}{\cdot} x) \to y \leq_{W} (n \underset{˙}{\cdot} x))$
75	74	reximdva	$⊢ (((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \to (\exists n \in ℕ y \underset{˙}{<} (n \underset{˙}{\cdot} x) \to \exists n \in ℕ y \leq_{W} (n \underset{˙}{\cdot} x))$
76	75	imp	$⊢ ((((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \land \exists n \in ℕ y \underset{˙}{<} (n \underset{˙}{\cdot} x)) \to \exists n \in ℕ y \leq_{W} (n \underset{˙}{\cdot} x)$
77	72 76	impbida	$⊢ (((W \in oGrp \land x \in B) \land y \in B) \land \underset{˙}{0} \underset{˙}{<} x) \to (\exists n \in ℕ y \leq_{W} (n \underset{˙}{\cdot} x) \leftrightarrow \exists n \in ℕ y \underset{˙}{<} (n \underset{˙}{\cdot} x))$
78	77	pm5.74da	$⊢ ((W \in oGrp \land x \in B) \land y \in B) \to ((\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \leq_{W} (n \underset{˙}{\cdot} x)) \leftrightarrow (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \underset{˙}{<} (n \underset{˙}{\cdot} x)))$
79	78	ralbidva	$⊢ (W \in oGrp \land x \in B) \to (\forall y \in B (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \leq_{W} (n \underset{˙}{\cdot} x)) \leftrightarrow \forall y \in B (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \underset{˙}{<} (n \underset{˙}{\cdot} x)))$
80	79	ralbidva	$⊢ W \in oGrp \to (\forall x \in B \forall y \in B (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \leq_{W} (n \underset{˙}{\cdot} x)) \leftrightarrow \forall x \in B \forall y \in B (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \underset{˙}{<} (n \underset{˙}{\cdot} x)))$
81	14 80	bitrd	$⊢ W \in oGrp \to (W \in Archi \leftrightarrow \forall x \in B \forall y \in B (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \underset{˙}{<} (n \underset{˙}{\cdot} x)))$

Metamath Proof Explorer

Theorem isarchi3

Proof