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	29 30 31	3syl	$⊢ W \in oGrp \to W \in Poset$
33	20 32	syl	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to W \in Poset$
34	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$
35	1 5	mulgcl	$⊢ (W \in Grp \land m \in ℤ \land U \in B) \to m \underset{˙}{\cdot} U \in B$
36	22 24 16 35	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$
37		eqid	$⊢ -_{W} = -_{W}$
38	1 37	grpsubcl	$⊢ (W \in Grp \land X \in B \land m \underset{˙}{\cdot} U \in B) \to X -_{W} (m \underset{˙}{\cdot} U) \in B$
39	22 34 36 38	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$
40	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 ℤ$
41	1 5	mulgcl	$⊢ (W \in Grp \land m + 1 \in ℤ \land U \in B) \to (m + 1) \underset{˙}{\cdot} U \in B$
42	22 40 16 41	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$
43		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)$
44	1 3 37	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))$
45	20 34 42 36 43 44	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))$
46	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 ℂ$
47		1cnd	$⊢ ((φ \land m \in ℕ_{0}) \land ((m \underset{˙}{\cdot} U) \underset{˙}{<} X \land X \underset{˙}{\leq} ((m + 1) \underset{˙}{\cdot} U))) \to 1 \in ℂ$
48	46 47	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$
49	48	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$
50	1 5 37	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)$
51	22 40 24 16 50	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)$
52	49 51 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$
53	45 52	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$
54	10	3expia	$⊢ (φ \land x \in B) \to (\underset{˙}{0} \underset{˙}{<} x \to U \underset{˙}{\leq} x)$
55	54	ralrimiva	$⊢ φ \to \forall x \in B (\underset{˙}{0} \underset{˙}{<} x \to U \underset{˙}{\leq} x)$
56	55	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)$
57	1 2 37	grpsubid	$⊢ (W \in Grp \land m \underset{˙}{\cdot} U \in B) \to (m \underset{˙}{\cdot} U) -_{W} (m \underset{˙}{\cdot} U) = \underset{˙}{0}$
58	22 36 57	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}$
59		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$
60	1 4 37	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))$
61	20 36 34 36 59 60	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))$
62	58 61	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))$
63		breq2	$⊢ x = X -_{W} (m \underset{˙}{\cdot} U) \to (\underset{˙}{0} \underset{˙}{<} x \leftrightarrow \underset{˙}{0} \underset{˙}{<} (X -_{W} (m \underset{˙}{\cdot} U)))$
64		breq2	$⊢ x = X -_{W} (m \underset{˙}{\cdot} U) \to (U \underset{˙}{\leq} x \leftrightarrow U \underset{˙}{\leq} (X -_{W} (m \underset{˙}{\cdot} U)))$
65	63 64	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))))$
66	65	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))))$
67	39 56 62 66	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))$
68	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)$
69	68	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$
70	33 39 16 53 67 69	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$
71	70	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)$
72	19 27 71	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$
73	1 25 37	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$
74	22 34 36 73	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$
75	47 46	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$
76	75	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$
77	72 74 76	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$
78		oveq1	$⊢ n = m + 1 \to n \underset{˙}{\cdot} U = (m + 1) \underset{˙}{\cdot} U$
79	78	rspceeqv	$⊢ (m + 1 \in ℕ \land X = (m + 1) \underset{˙}{\cdot} U) \to \exists n \in ℕ X = n \underset{˙}{\cdot} U$
80	15 77 79	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$
81	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))$
82	80 81	r19.29a	$⊢ φ \to \exists n \in ℕ X = n \underset{˙}{\cdot} U$

Metamath Proof Explorer

Theorem archiabllem1a

Proof