archiabllem1a

Description: Lemma for archiabl : In case an archimedean group W admits a smallest positive element U , then any positive element X of W can be written as ( n .x. U ) with n e. NN . Since the reciprocal holds for negative elements, W is then isomorphic to ZZ . (Contributed by Thierry Arnoux, 12-Apr-2018)

	Ref	Expression
Hypotheses	archiabllem.b	$⊢ B = {Base}_{W}$
	archiabllem.0	$⊢ \underset{˙}{0} = 0_{W}$
	archiabllem.e	$⊢ \underset{˙}{\leq} = \leq_{W}$
	archiabllem.t	$⊢ \underset{˙}{<} = <_{W}$
	archiabllem.m	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	archiabllem.g	$⊢ φ \to W \in oGrp$
	archiabllem.a	$⊢ φ \to W \in Archi$
	archiabllem1.u	$⊢ φ \to U \in B$
	archiabllem1.p	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} U$
	archiabllem1.s	$⊢ (φ \land x \in B \land \underset{˙}{0} \underset{˙}{<} x) \to U \underset{˙}{\leq} x$
	archiabllem1a.x	$⊢ φ \to X \in B$
	archiabllem1a.c	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} X$
Assertion	archiabllem1a	$⊢ φ \to \exists n \in ℕ X = n \underset{˙}{\cdot} U$

Proof

Step	Hyp	Ref	Expression
1		archiabllem.b	$⊢ B = {Base}_{W}$
2		archiabllem.0	$⊢ \underset{˙}{0} = 0_{W}$
3		archiabllem.e	$⊢ \underset{˙}{\leq} = \leq_{W}$
4		archiabllem.t	$⊢ \underset{˙}{<} = <_{W}$
5		archiabllem.m	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		archiabllem.g	$⊢ φ \to W \in oGrp$
7		archiabllem.a	$⊢ φ \to W \in Archi$
8		archiabllem1.u	$⊢ φ \to U \in B$
9		archiabllem1.p	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} U$
10		archiabllem1.s	$⊢ (φ \land x \in B \land \underset{˙}{0} \underset{˙}{<} x) \to U \underset{˙}{\leq} x$
11		archiabllem1a.x	$⊢ φ \to X \in B$
12		archiabllem1a.c	$⊢ φ \to \underset{˙}{0} \underset{˙}{<} X$
13		simplr	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to m \in ℕ_{0}$
14		nn0p1nn	$⊢ m \in ℕ_{0} \to m + 1 \in ℕ$
15	13 14	syl	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to m + 1 \in ℕ$
16	8	ad2antrr	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to U \in B$
17	1 5	mulg1	$⊢ U \in B \to 1 \underset{˙}{\cdot} U = U$
18	16 17	syl	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to 1 \underset{˙}{\cdot} U = U$
19	18	oveq1d	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to (1 \underset{˙}{\cdot} U) +_{W} (m \underset{˙}{\cdot} U) = U +_{W} (m \underset{˙}{\cdot} U)$
20	6	ad2antrr	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to W \in oGrp$
21		ogrpgrp	$⊢ W \in oGrp \to W \in Grp$
22	20 21	syl	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to W \in Grp$
23		1zzd	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to 1 \in ℤ$
24	13	nn0zd	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to m \in ℤ$
25		eqid	$⊢ +_{W} = +_{W}$
26	1 5 25	mulgdir	$⊢ (W \in Grp \land (1 \in ℤ \land m \in ℤ \land U \in B)) \to (1 + m) \underset{˙}{\cdot} U = (1 \underset{˙}{\cdot} U) +_{W} (m \underset{˙}{\cdot} U)$
27	22 23 24 16 26	syl13anc	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to (1 + m) \underset{˙}{\cdot} U = (1 \underset{˙}{\cdot} U) +_{W} (m \underset{˙}{\cdot} U)$
28		isogrp	$⊢ W \in oGrp \leftrightarrow (W \in Grp \land W \in oMnd)$
29	28	simprbi	$⊢ W \in oGrp \to W \in oMnd$
30		omndtos	$⊢ W \in oMnd \to W \in Toset$
31		tospos	$⊢ W \in Toset \to W \in Poset$
32	20 29 30 31	4syl	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to W \in Poset$
33	11	ad2antrr	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to X \in B$
34	1 5	mulgcl	$⊢ (W \in Grp \land m \in ℤ \land U \in B) \to m \underset{˙}{\cdot} U \in B$
35	22 24 16 34	syl3anc	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to m \underset{˙}{\cdot} U \in B$
36		eqid	$⊢ -_{W} = -_{W}$
37	1 36	grpsubcl	$⊢ (W \in Grp \land X \in B \land m \underset{˙}{\cdot} U \in B) \to X -_{W} (m \underset{˙}{\cdot} U) \in B$
38	22 33 35 37	syl3anc	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to X -_{W} (m \underset{˙}{\cdot} U) \in B$
39	24	peano2zd	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to m + 1 \in ℤ$
40	1 5	mulgcl	$⊢ (W \in Grp \land m + 1 \in ℤ \land U \in B) \to (m + 1) \underset{˙}{\cdot} U \in B$
41	22 39 16 40	syl3anc	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to (m + 1) \underset{˙}{\cdot} U \in B$
42		simprr	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U)$
43	1 3 36	ogrpsub	$⊢ (W \in oGrp \land (X \in B \land (m + 1) \underset{˙}{\cdot} U \in B \land m \underset{˙}{\cdot} U \in B) \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U)) \to (X -_{W} (m \underset{˙}{\cdot} U)) \underset{˙}{\leq} (((m + 1) \underset{˙}{\cdot} U) -_{W} (m \underset{˙}{\cdot} U))$
44	20 33 41 35 42 43	syl131anc	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to (X -_{W} (m \underset{˙}{\cdot} U)) \underset{˙}{\leq} (((m + 1) \underset{˙}{\cdot} U) -_{W} (m \underset{˙}{\cdot} U))$
45	13	nn0cnd	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to m \in ℂ$
46		1cnd	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to 1 \in ℂ$
47	45 46	pncan2d	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to m + 1 - m = 1$
48	47	oveq1d	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to (m + 1 - m) \underset{˙}{\cdot} U = 1 \underset{˙}{\cdot} U$
49	1 5 36	mulgsubdir	$⊢ (W \in Grp \land (m + 1 \in ℤ \land m \in ℤ \land U \in B)) \to (m + 1 - m) \underset{˙}{\cdot} U = ((m + 1) \underset{˙}{\cdot} U) -_{W} (m \underset{˙}{\cdot} U)$
50	22 39 24 16 49	syl13anc	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to (m + 1 - m) \underset{˙}{\cdot} U = ((m + 1) \underset{˙}{\cdot} U) -_{W} (m \underset{˙}{\cdot} U)$
51	48 50 18	3eqtr3d	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to ((m + 1) \underset{˙}{\cdot} U) -_{W} (m \underset{˙}{\cdot} U) = U$
52	44 51	breqtrd	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to (X -_{W} (m \underset{˙}{\cdot} U)) \underset{˙}{\leq} U$
53	10	3expia	$⊢ (φ \land x \in B) \to (\underset{˙}{0} \underset{˙}{<} x \to U \underset{˙}{\leq} x)$
54	53	ralrimiva	$⊢ φ \to \forall x \in B (\underset{˙}{0} \underset{˙}{<} x \to U \underset{˙}{\leq} x)$
55	54	ad2antrr	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to \forall x \in B (\underset{˙}{0} \underset{˙}{<} x \to U \underset{˙}{\leq} x)$
56	1 2 36	grpsubid	$⊢ (W \in Grp \land m \underset{˙}{\cdot} U \in B) \to (m \underset{˙}{\cdot} U) -_{W} (m \underset{˙}{\cdot} U) = \underset{˙}{0}$
57	22 35 56	syl2anc	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to (m \underset{˙}{\cdot} U) -_{W} (m \underset{˙}{\cdot} U) = \underset{˙}{0}$
58		simprl	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to (m \underset{˙}{\cdot} U) \underset{˙}{<} X$
59	1 4 36	ogrpsublt	$⊢ (W \in oGrp \land (m \underset{˙}{\cdot} U \in B \land X \in B \land m \underset{˙}{\cdot} U \in B) \land (m \underset{˙}{\cdot} U) \underset{˙}{<} X) \to ((m \underset{˙}{\cdot} U) -_{W} (m \underset{˙}{\cdot} U)) \underset{˙}{<} (X -_{W} (m \underset{˙}{\cdot} U))$
60	20 35 33 35 58 59	syl131anc	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to ((m \underset{˙}{\cdot} U) -_{W} (m \underset{˙}{\cdot} U)) \underset{˙}{<} (X -_{W} (m \underset{˙}{\cdot} U))$
61	57 60	eqbrtrrd	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to \underset{˙}{0} \underset{˙}{<} (X -_{W} (m \underset{˙}{\cdot} U))$
62		breq2	$⊢ x = X -_{W} (m \underset{˙}{\cdot} U) \to (\underset{˙}{0} \underset{˙}{<} x \leftrightarrow \underset{˙}{0} \underset{˙}{<} (X -_{W} (m \underset{˙}{\cdot} U)))$
63		breq2	$⊢ x = X -_{W} (m \underset{˙}{\cdot} U) \to (U \underset{˙}{\leq} x \leftrightarrow U \underset{˙}{\leq} (X -_{W} (m \underset{˙}{\cdot} U)))$
64	62 63	imbi12d	$⊢ x = X -_{W} (m \underset{˙}{\cdot} U) \to ((\underset{˙}{0} \underset{˙}{<} x \to U \underset{˙}{\leq} x) \leftrightarrow (\underset{˙}{0} \underset{˙}{<} (X -_{W} (m \underset{˙}{\cdot} U)) \to U \underset{˙}{\leq} (X -_{W} (m \underset{˙}{\cdot} U))))$
65	64	rspcv	$⊢ X -_{W} (m \underset{˙}{\cdot} U) \in B \to (\forall x \in B (\underset{˙}{0} \underset{˙}{<} x \to U \underset{˙}{\leq} x) \to (\underset{˙}{0} \underset{˙}{<} (X -_{W} (m \underset{˙}{\cdot} U)) \to U \underset{˙}{\leq} (X -_{W} (m \underset{˙}{\cdot} U))))$
66	38 55 61 65	syl3c	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to U \underset{˙}{\leq} (X -_{W} (m \underset{˙}{\cdot} U))$
67	1 3	posasymb	$⊢ (W \in Poset \land X -_{W} (m \underset{˙}{\cdot} U) \in B \land U \in B) \to (((X -_{W} (m \underset{˙}{\cdot} U)) \underset{˙}{\leq} U \land U \underset{˙}{\leq} (X -_{W} (m \underset{˙}{\cdot} U))) \leftrightarrow X -_{W} (m \underset{˙}{\cdot} U) = U)$
68	67	biimpa	$⊢ ((W \in Poset \land X -_{W} (m \underset{˙}{\cdot} U) \in B \land U \in B) \land ((X -_{W} (m \underset{˙}{\cdot} U)) \underset{˙}{\leq} U \land U \underset{˙}{\leq} (X -_{W} (m \underset{˙}{\cdot} U)))) \to X -_{W} (m \underset{˙}{\cdot} U) = U$
69	32 38 16 52 66 68	syl32anc	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to X -_{W} (m \underset{˙}{\cdot} U) = U$
70	69	oveq1d	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to (X -_{W} (m \underset{˙}{\cdot} U)) +_{W} (m \underset{˙}{\cdot} U) = U +_{W} (m \underset{˙}{\cdot} U)$
71	19 27 70	3eqtr4rd	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to (X -_{W} (m \underset{˙}{\cdot} U)) +_{W} (m \underset{˙}{\cdot} U) = (1 + m) \underset{˙}{\cdot} U$
72	1 25 36	grpnpcan	$⊢ (W \in Grp \land X \in B \land m \underset{˙}{\cdot} U \in B) \to (X -_{W} (m \underset{˙}{\cdot} U)) +_{W} (m \underset{˙}{\cdot} U) = X$
73	22 33 35 72	syl3anc	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to (X -_{W} (m \underset{˙}{\cdot} U)) +_{W} (m \underset{˙}{\cdot} U) = X$
74	46 45	addcomd	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to 1 + m = m + 1$
75	74	oveq1d	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to (1 + m) \underset{˙}{\cdot} U = (m + 1) \underset{˙}{\cdot} U$
76	71 73 75	3eqtr3d	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to X = (m + 1) \underset{˙}{\cdot} U$
77		oveq1	$⊢ n = m + 1 \to n \underset{˙}{\cdot} U = (m + 1) \underset{˙}{\cdot} U$
78	77	rspceeqv	$⊢ (m + 1 \in ℕ \land X = (m + 1) \underset{˙}{\cdot} U) \to \exists n \in ℕ X = n \underset{˙}{\cdot} U$
79	15 76 78	syl2anc	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to \exists n \in ℕ X = n \underset{˙}{\cdot} U$
80	1 2 4 3 5 6 7 8 11 9 12	archirng	$⊢ φ \to \exists m \in ℕ_{0} ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))$
81	79 80	r19.29a	$⊢ φ \to \exists n \in ℕ X = n \underset{˙}{\cdot} U$

Metamath Proof Explorer

Theorem archiabllem1a

Proof