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 20 29 30 31 4syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑊 ∈ Poset )
33 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑋 ∈ 𝐵 )
34 1 5 mulgcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑚 ∈ ℤ ∧ 𝑈 ∈ 𝐵 ) → ( 𝑚 · 𝑈 ) ∈ 𝐵 )
35 22 24 16 34 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 𝑚 · 𝑈 ) ∈ 𝐵 )
36 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
37 1 36 grpsubcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑚 · 𝑈 ) ∈ 𝐵 ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ∈ 𝐵 )
38 22 33 35 37 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ∈ 𝐵 )
39 24 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 𝑚 + 1 ) ∈ ℤ )
40 1 5 mulgcl ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑚 + 1 ) ∈ ℤ ∧ 𝑈 ∈ 𝐵 ) → ( ( 𝑚 + 1 ) · 𝑈 ) ∈ 𝐵 )
41 22 39 16 40 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 𝑚 + 1 ) · 𝑈 ) ∈ 𝐵 )
42 simprr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) )
43 1 3 36 ogrpsub ⊢ ( ( 𝑊 ∈ oGrp ∧ ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑚 + 1 ) · 𝑈 ) ∈ 𝐵 ∧ ( 𝑚 · 𝑈 ) ∈ 𝐵 ) ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ≤ ( ( ( 𝑚 + 1 ) · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
44 20 33 41 35 42 43 syl131anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ≤ ( ( ( 𝑚 + 1 ) · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
45 13 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑚 ∈ ℂ )
46 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 1 ∈ ℂ )
47 45 46 pncan2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 𝑚 + 1 ) − 𝑚 ) = 1 )
48 47 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( ( 𝑚 + 1 ) − 𝑚 ) · 𝑈 ) = ( 1 · 𝑈 ) )
49 1 5 36 mulgsubdir ⊢ ( ( 𝑊 ∈ Grp ∧ ( ( 𝑚 + 1 ) ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑈 ∈ 𝐵 ) ) → ( ( ( 𝑚 + 1 ) − 𝑚 ) · 𝑈 ) = ( ( ( 𝑚 + 1 ) · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
50 22 39 24 16 49 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( ( 𝑚 + 1 ) − 𝑚 ) · 𝑈 ) = ( ( ( 𝑚 + 1 ) · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
51 48 50 18 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( ( 𝑚 + 1 ) · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 𝑈 )
52 44 51 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ≤ 𝑈 )
53 10 3expia ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 < 𝑥 → 𝑈 ≤ 𝑥 ) )
54 53 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 0 < 𝑥 → 𝑈 ≤ 𝑥 ) )
55 54 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ∀ 𝑥 ∈ 𝐵 ( 0 < 𝑥 → 𝑈 ≤ 𝑥 ) )
56 1 2 36 grpsubid ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑚 · 𝑈 ) ∈ 𝐵 ) → ( ( 𝑚 · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 0 )
57 22 35 56 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 𝑚 · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 0 )
58 simprl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 𝑚 · 𝑈 ) < 𝑋 )
59 1 4 36 ogrpsublt ⊢ ( ( 𝑊 ∈ oGrp ∧ ( ( 𝑚 · 𝑈 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑚 · 𝑈 ) ∈ 𝐵 ) ∧ ( 𝑚 · 𝑈 ) < 𝑋 ) → ( ( 𝑚 · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) < ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
60 20 35 33 35 58 59 syl131anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 𝑚 · 𝑈 ) ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) < ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
61 57 60 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 0 < ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
62 breq2 ⊢ ( 𝑥 = ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) → ( 0 < 𝑥 ↔ 0 < ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ) )
63 breq2 ⊢ ( 𝑥 = ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) → ( 𝑈 ≤ 𝑥 ↔ 𝑈 ≤ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ) )
64 62 63 imbi12d ⊢ ( 𝑥 = ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) → ( ( 0 < 𝑥 → 𝑈 ≤ 𝑥 ) ↔ ( 0 < ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) → 𝑈 ≤ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ) ) )
65 64 rspcv ⊢ ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( 0 < 𝑥 → 𝑈 ≤ 𝑥 ) → ( 0 < ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) → 𝑈 ≤ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ) ) )
66 38 55 61 65 syl3c ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑈 ≤ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
67 1 3 posasymb ⊢ ( ( 𝑊 ∈ Poset ∧ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) → ( ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ≤ 𝑈 ∧ 𝑈 ≤ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ) ↔ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 𝑈 ) )
68 67 biimpa ⊢ ( ( ( 𝑊 ∈ Poset ∧ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ∈ 𝐵 ∧ 𝑈 ∈ 𝐵 ) ∧ ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ≤ 𝑈 ∧ 𝑈 ≤ ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ) ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 𝑈 )
69 32 38 16 52 66 68 syl32anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 𝑈 )
70 69 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = ( 𝑈 ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) )
71 19 27 70 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = ( ( 1 + 𝑚 ) · 𝑈 ) )
72 1 25 36 grpnpcan ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑚 · 𝑈 ) ∈ 𝐵 ) → ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 𝑋 )
73 22 33 35 72 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 𝑋 ( -g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) ( +g ‘ 𝑊 ) ( 𝑚 · 𝑈 ) ) = 𝑋 )
74 46 45 addcomd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( 1 + 𝑚 ) = ( 𝑚 + 1 ) )
75 74 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ( ( 1 + 𝑚 ) · 𝑈 ) = ( ( 𝑚 + 1 ) · 𝑈 ) )
76 71 73 75 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → 𝑋 = ( ( 𝑚 + 1 ) · 𝑈 ) )
77 oveq1 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑛 · 𝑈 ) = ( ( 𝑚 + 1 ) · 𝑈 ) )
78 77 rspceeqv ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ ∧ 𝑋 = ( ( 𝑚 + 1 ) · 𝑈 ) ) → ∃ 𝑛 ∈ ℕ 𝑋 = ( 𝑛 · 𝑈 ) )
79 15 76 78 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) ) → ∃ 𝑛 ∈ ℕ 𝑋 = ( 𝑛 · 𝑈 ) )
80 1 2 4 3 5 6 7 8 11 9 12 archirng ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ0 ( ( 𝑚 · 𝑈 ) < 𝑋 ∧ 𝑋 ≤ ( ( 𝑚 + 1 ) · 𝑈 ) ) )
81 79 80 r19.29a ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ 𝑋 = ( 𝑛 · 𝑈 ) )