Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
archiabllem.0 ⊢ 0 = ( 0g ‘ 𝑊 )
archiabllem.e ⊢ ≤ = ( le ‘ 𝑊 )
archiabllem.t ⊢ < = ( lt ‘ 𝑊 )
archiabllem.m ⊢ · = ( .g ‘ 𝑊 )
archiabllem.g ⊢ ( 𝜑 → 𝑊 ∈ oGrp )
archiabllem.a ⊢ ( 𝜑 → 𝑊 ∈ Archi )
archiabllem1.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
archiabllem1.p ⊢ ( 𝜑 → 0 < 𝑈 )
archiabllem1.s ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥 ) → 𝑈 ≤ 𝑥 )
archiabllem1a.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
archiabllem1a.c ⊢ ( 𝜑 → 0 < 𝑋 )
Assertion archiabllem1a ( 𝜑 → ∃ 𝑛 ∈ ℕ 𝑋 = ( 𝑛 · 𝑈 ) )

Proof

Step Hyp Ref Expression
1 archiabllem.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 archiabllem.0 ⊢ 0 = ( 0g ‘ 𝑊 )
3 archiabllem.e ⊢ ≤ = ( le ‘ 𝑊 )
4 archiabllem.t ⊢ < = ( lt ‘ 𝑊 )
5 archiabllem.m ⊢ · = ( .g ‘ 𝑊 )
6 archiabllem.g ⊢ ( 𝜑 → 𝑊 ∈ oGrp )
7 archiabllem.a ⊢ ( 𝜑 → 𝑊 ∈ Archi )
8 archiabllem1.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
9 archiabllem1.p ⊢ ( 𝜑 → 0 < 𝑈 )
10 archiabllem1.s ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 0 < 𝑥 ) → 𝑈 ≤ 𝑥 )
11 archiabllem1a.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
12 archiabllem1a.c ⊢ ( 𝜑 → 0 < 𝑋 )
13 simplr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑚 ∈ ℕ0 )
14 nn0p1nn ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℕ )
15 13 14 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 𝑚 + 1 ) ∈ ℕ )
16 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑈 ∈ 𝐵 )
17 1 5 mulg1 ⊢ ( 𝑈 ∈ 𝐵 → ( 1 · 𝑈 ) = 𝑈 )
18 16 17 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 1 · 𝑈 ) = 𝑈 )
19 18 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 1 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = ( 𝑈 ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
20 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑊 ∈ oGrp )
21 ogrpgrp ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ Grp )
22 20 21 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑊 ∈ Grp )
23 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 1 ∈ ℤ )
24 13 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑚 ∈ ℤ )
25 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
26 1 5 25 mulgdir ⊢ ( ( 𝑊 ∈ Grp ∧ ( 1 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑈 ∈ 𝐵 ) ) → ( ( 1 + 𝑚 ) · 𝑈 ) = ( ( 1 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
27 22 23 24 16 26 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 1 + 𝑚 ) · 𝑈 ) = ( ( 1 · 𝑈 ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
28 isogrp ⊢ ( 𝑊 ∈ oGrp ↔ ( 𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd ) )
29 28 simprbi ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ oMnd )
30 omndtos ⊢ ( 𝑊 ∈ oMnd → 𝑊 ∈ Toset )
31 tospos ⊢ ( 𝑊 ∈ Toset → 𝑊 ∈ Poset )
32 29 30 31 3syl ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ Poset )
33 20 32 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑊 ∈ Poset )
34 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑋 ∈ 𝐵 )
35 1 5 mulgcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑈 ∈ 𝐵 ) → ( 𝑚 · 𝑈 ) ∈ 𝐵 )
36 22 24 16 35 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 𝑚 · 𝑈 ) ∈ 𝐵 )
37 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
38 1 37 grpsubcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑚 · 𝑈 ) ∈ 𝐵 ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ∈ 𝐵 )
39 22 34 36 38 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ∈ 𝐵 )
40 24 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 𝑚 + 1 ) ∈ ℤ )
41 1 5 mulgcl ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑚 + 1 ) ∈ ℤ ∧ 𝑈 ∈ 𝐵 ) → ( ( 𝑚 + 1 ) · 𝑈 ) ∈ 𝐵 )
42 22 40 16 41 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 𝑚 + 1 ) · 𝑈 ) ∈ 𝐵 )
43 simprr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) )
44 1 3 37 ogrpsub ⊢ ( ( 𝑊 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑚 + 1 ) · 𝑈 ) ∈ 𝐵 ∧ ( 𝑚 · 𝑈 ) ∈ 𝐵 ) ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ≤ ( ( ( 𝑚 + 1 ) · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
45 20 34 42 36 43 44 syl131anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ≤ ( ( ( 𝑚 + 1 ) · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
46 13 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑚 ∈ ℂ )
47 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 1 ∈ ℂ )
48 46 47 pncan2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 𝑚 + 1 ) − 𝑚 ) = 1 )
49 48 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( ( 𝑚 + 1 ) − 𝑚 ) · 𝑈 ) = ( 1 · 𝑈 ) )
50 1 5 37 mulgsubdir ⊢ ( ( 𝑊 ∈ Grp ∧ ( ( 𝑚 + 1 ) ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑈 ∈ 𝐵 ) ) → ( ( ( 𝑚 + 1 ) − 𝑚 ) · 𝑈 ) = ( ( ( 𝑚 + 1 ) · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
51 22 40 24 16 50 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( ( 𝑚 + 1 ) − 𝑚 ) · 𝑈 ) = ( ( ( 𝑚 + 1 ) · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
52 49 51 18 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( ( 𝑚 + 1 ) · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 𝑈 )
53 45 52 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ≤ 𝑈 )
54 10 3expia ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 < 𝑥 → 𝑈 ≤ 𝑥 ) )
55 54 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 0 < 𝑥 → 𝑈 ≤ 𝑥 ) )
56 55 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ∀ 𝑥 ∈ 𝐵 ( 0 < 𝑥 → 𝑈 ≤ 𝑥 ) )
57 1 2 37 grpsubid ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑚 · 𝑈 ) ∈ 𝐵 ) → ( ( 𝑚 · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 0 )
58 22 36 57 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 𝑚 · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 0 )
59 simprl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 𝑚 · 𝑈 ) < 𝑋 )
60 1 4 37 ogrpsublt ⊢ ( ( 𝑊 ∈ oGrp ∧ ( ( 𝑚 · 𝑈 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑚 · 𝑈 ) ∈ 𝐵 ) ∧ ( 𝑚 · 𝑈 ) < 𝑋 ) → ( ( 𝑚 · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) < ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
61 20 36 34 36 59 60 syl131anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 𝑚 · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) < ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
62 58 61 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 0 < ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
63 breq2 ⊢ ( 𝑥 = ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) → ( 0 < 𝑥 ↔ 0 < ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ) )
64 breq2 ⊢ ( 𝑥 = ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) → ( 𝑈 ≤ 𝑥 ↔ 𝑈 ≤ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ) )
65 63 64 imbi12d ⊢ ( 𝑥 = ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) → ( ( 0 < 𝑥 → 𝑈 ≤ 𝑥 ) ↔ ( 0 < ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) → 𝑈 ≤ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ) ) )
66 65 rspcv ⊢ ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( 0 < 𝑥 → 𝑈 ≤ 𝑥 ) → ( 0 < ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) → 𝑈 ≤ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ) ) )
67 39 56 62 66 syl3c ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑈 ≤ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
68 1 3 posasymb ⊢ ( ( 𝑊 ∈ Poset ∧ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) → ( ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ≤ 𝑈 ∧ 𝑈 ≤ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ) ↔ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 𝑈 ) )
69 68 biimpa ⊢ ( ( ( 𝑊 ∈ Poset ∧ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) ∧ ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ≤ 𝑈 ∧ 𝑈 ≤ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ) ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 𝑈 )
70 33 39 16 53 67 69 syl32anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 𝑈 )
71 70 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = ( 𝑈 ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
72 19 27 71 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = ( ( 1 + 𝑚 ) · 𝑈 ) )
73 1 25 37 grpnpcan ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑚 · 𝑈 ) ∈ 𝐵 ) → ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 𝑋 )
74 22 34 36 73 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 𝑋 )
75 47 46 addcomd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 1 + 𝑚 ) = ( 𝑚 + 1 ) )
76 75 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 1 + 𝑚 ) · 𝑈 ) = ( ( 𝑚 + 1 ) · 𝑈 ) )
77 72 74 76 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑋 = ( ( 𝑚 + 1 ) · 𝑈 ) )
78 oveq1 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑛 · 𝑈 ) = ( ( 𝑚 + 1 ) · 𝑈 ) )
79 78 rspceeqv ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ ∧ 𝑋 = ( ( 𝑚 + 1 ) · 𝑈 ) ) → ∃ 𝑛 ∈ ℕ 𝑋 = ( 𝑛 · 𝑈 ) )
80 15 77 79 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ∃ 𝑛 ∈ ℕ 𝑋 = ( 𝑛 · 𝑈 ) )
81 1 2 4 3 5 6 7 8 11 9 12 archirng ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ0 ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) )
82 80 81 r19.29a ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ 𝑋 = ( 𝑛 · 𝑈 ) )