Metamath Proof Explorer

Theorem isarchiofld

Description: Axiom of Archimedes : a characterization of the Archimedean property for ordered fields. (Contributed by Thierry Arnoux, 9-Apr-2018)

Ref Expression
Hypotheses isarchiofld.b ⊢ B = Base W
isarchiofld.h ⊢ H = ℤRHom ⁡ W
isarchiofld.l ⊢ < ˙ = < W
Assertion isarchiofld ⊢ W ∈ oField → W ∈ Archi ↔ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n

Proof

Step Hyp Ref Expression
1 isarchiofld.b ⊢ B = Base W
2 isarchiofld.h ⊢ H = ℤRHom ⁡ W
3 isarchiofld.l ⊢ < ˙ = < W
4 isofld ⊢ W ∈ oField ↔ W ∈ Field ∧ W ∈ oRing
5 4 simprbi ⊢ W ∈ oField → W ∈ oRing
6 orngogrp ⊢ W ∈ oRing → W ∈ oGrp
7 eqid ⊢ 0 W = 0 W
8 eqid ⊢ ⋅ W = ⋅ W
9 1 7 3 8 isarchi3 ⊢ W ∈ oGrp → W ∈ Archi ↔ ∀ y ∈ B ∀ x ∈ B 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y
10 5 6 9 3syl ⊢ W ∈ oField → W ∈ Archi ↔ ∀ y ∈ B ∀ x ∈ B 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y
11 orngring ⊢ W ∈ oRing → W ∈ Ring
12 eqid ⊢ 1 W = 1 W
13 1 12 ringidcl ⊢ W ∈ Ring → 1 W ∈ B
14 5 11 13 3syl ⊢ W ∈ oField → 1 W ∈ B
15 breq2 ⊢ y = 1 W → 0 W < ˙ y ↔ 0 W < ˙ 1 W
16 oveq2 ⊢ y = 1 W → n ⋅ W y = n ⋅ W 1 W
17 16 breq2d ⊢ y = 1 W → x < ˙ n ⋅ W y ↔ x < ˙ n ⋅ W 1 W
18 17 rexbidv ⊢ y = 1 W → ∃ n ∈ ℕ x < ˙ n ⋅ W y ↔ ∃ n ∈ ℕ x < ˙ n ⋅ W 1 W
19 15 18 imbi12d ⊢ y = 1 W → 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y ↔ 0 W < ˙ 1 W → ∃ n ∈ ℕ x < ˙ n ⋅ W 1 W
20 19 ralbidv ⊢ y = 1 W → ∀ x ∈ B 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y ↔ ∀ x ∈ B 0 W < ˙ 1 W → ∃ n ∈ ℕ x < ˙ n ⋅ W 1 W
21 20 rspcv ⊢ 1 W ∈ B → ∀ y ∈ B ∀ x ∈ B 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y → ∀ x ∈ B 0 W < ˙ 1 W → ∃ n ∈ ℕ x < ˙ n ⋅ W 1 W
22 14 21 syl ⊢ W ∈ oField → ∀ y ∈ B ∀ x ∈ B 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y → ∀ x ∈ B 0 W < ˙ 1 W → ∃ n ∈ ℕ x < ˙ n ⋅ W 1 W
23 7 12 3 ofldlt1 ⊢ W ∈ oField → 0 W < ˙ 1 W
24 pm5.5 ⊢ 0 W < ˙ 1 W → 0 W < ˙ 1 W → ∃ n ∈ ℕ x < ˙ n ⋅ W 1 W ↔ ∃ n ∈ ℕ x < ˙ n ⋅ W 1 W
25 23 24 syl ⊢ W ∈ oField → 0 W < ˙ 1 W → ∃ n ∈ ℕ x < ˙ n ⋅ W 1 W ↔ ∃ n ∈ ℕ x < ˙ n ⋅ W 1 W
26 25 ralbidv ⊢ W ∈ oField → ∀ x ∈ B 0 W < ˙ 1 W → ∃ n ∈ ℕ x < ˙ n ⋅ W 1 W ↔ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ n ⋅ W 1 W
27 22 26 sylibd ⊢ W ∈ oField → ∀ y ∈ B ∀ x ∈ B 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y → ∀ x ∈ B ∃ n ∈ ℕ x < ˙ n ⋅ W 1 W
28 5 11 syl ⊢ W ∈ oField → W ∈ Ring
29 nnz ⊢ n ∈ ℕ → n ∈ ℤ
30 2 8 12 zrhmulg ⊢ W ∈ Ring ∧ n ∈ ℤ → H ⁡ n = n ⋅ W 1 W
31 28 29 30 syl2an ⊢ W ∈ oField ∧ n ∈ ℕ → H ⁡ n = n ⋅ W 1 W
32 31 breq2d ⊢ W ∈ oField ∧ n ∈ ℕ → x < ˙ H ⁡ n ↔ x < ˙ n ⋅ W 1 W
33 32 rexbidva ⊢ W ∈ oField → ∃ n ∈ ℕ x < ˙ H ⁡ n ↔ ∃ n ∈ ℕ x < ˙ n ⋅ W 1 W
34 33 ralbidv ⊢ W ∈ oField → ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ↔ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ n ⋅ W 1 W
35 27 34 sylibrd ⊢ W ∈ oField → ∀ y ∈ B ∀ x ∈ B 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y → ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n
36 nfv ⊢ Ⅎ x W ∈ oField
37 nfra1 ⊢ Ⅎ x ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n
38 36 37 nfan ⊢ Ⅎ x W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n
39 nfv ⊢ Ⅎ x y ∈ B
40 38 39 nfan ⊢ Ⅎ x W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B
41 28 ad3antrrr ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → W ∈ Ring
42 simplrr ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → x ∈ B
43 simplrl ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → y ∈ B
44 simpr ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → 0 W < ˙ y
45 simplll ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → W ∈ oField
46 ringgrp ⊢ W ∈ Ring → W ∈ Grp
47 1 7 grpidcl ⊢ W ∈ Grp → 0 W ∈ B
48 41 46 47 3syl ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → 0 W ∈ B
49 3 pltne ⊢ W ∈ oField ∧ 0 W ∈ B ∧ y ∈ B → 0 W < ˙ y → 0 W ≠ y
50 45 48 43 49 syl3anc ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → 0 W < ˙ y → 0 W ≠ y
51 44 50 mpd ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → 0 W ≠ y
52 51 necomd ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → y ≠ 0 W
53 4 simplbi ⊢ W ∈ oField → W ∈ Field
54 isfld ⊢ W ∈ Field ↔ W ∈ DivRing ∧ W ∈ CRing
55 54 simplbi ⊢ W ∈ Field → W ∈ DivRing
56 53 55 syl ⊢ W ∈ oField → W ∈ DivRing
57 eqid ⊢ Unit ⁡ W = Unit ⁡ W
58 1 57 7 drngunit ⊢ W ∈ DivRing → y ∈ Unit ⁡ W ↔ y ∈ B ∧ y ≠ 0 W
59 45 56 58 3syl ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → y ∈ Unit ⁡ W ↔ y ∈ B ∧ y ≠ 0 W
60 43 52 59 mpbir2and ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → y ∈ Unit ⁡ W
61 eqid ⊢ / r ⁡ W = / r ⁡ W
62 1 57 61 dvrcl ⊢ W ∈ Ring ∧ x ∈ B ∧ y ∈ Unit ⁡ W → x / r ⁡ W y ∈ B
63 41 42 60 62 syl3anc ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → x / r ⁡ W y ∈ B
64 breq1 ⊢ x = z → x < ˙ H ⁡ n ↔ z < ˙ H ⁡ n
65 64 rexbidv ⊢ x = z → ∃ n ∈ ℕ x < ˙ H ⁡ n ↔ ∃ n ∈ ℕ z < ˙ H ⁡ n
66 65 cbvralvw ⊢ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ↔ ∀ z ∈ B ∃ n ∈ ℕ z < ˙ H ⁡ n
67 66 bilani ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n → ∀ z ∈ B ∃ n ∈ ℕ z < ˙ H ⁡ n
68 67 ad2antrr ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → ∀ z ∈ B ∃ n ∈ ℕ z < ˙ H ⁡ n
69 breq1 ⊢ z = x / r ⁡ W y → z < ˙ H ⁡ n ↔ x / r ⁡ W y < ˙ H ⁡ n
70 69 rexbidv ⊢ z = x / r ⁡ W y → ∃ n ∈ ℕ z < ˙ H ⁡ n ↔ ∃ n ∈ ℕ x / r ⁡ W y < ˙ H ⁡ n
71 70 rspcv ⊢ x / r ⁡ W y ∈ B → ∀ z ∈ B ∃ n ∈ ℕ z < ˙ H ⁡ n → ∃ n ∈ ℕ x / r ⁡ W y < ˙ H ⁡ n
72 63 68 71 sylc ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → ∃ n ∈ ℕ x / r ⁡ W y < ˙ H ⁡ n
73 eqid ⊢ ⋅ W = ⋅ W
74 simp-4l ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → W ∈ oField
75 74 5 syl ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → W ∈ oRing
76 74 28 syl ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → W ∈ Ring
77 simp-4r ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → y ∈ B ∧ x ∈ B
78 77 simprd ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → x ∈ B
79 77 simpld ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → y ∈ B
80 simpllr ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → 0 W < ˙ y
81 76 46 47 3syl ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → 0 W ∈ B
82 74 81 79 49 syl3anc ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → 0 W < ˙ y → 0 W ≠ y
83 80 82 mpd ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → 0 W ≠ y
84 83 necomd ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → y ≠ 0 W
85 74 56 58 3syl ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → y ∈ Unit ⁡ W ↔ y ∈ B ∧ y ≠ 0 W
86 79 84 85 mpbir2and ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → y ∈ Unit ⁡ W
87 76 78 86 62 syl3anc ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → x / r ⁡ W y ∈ B
88 simplr ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → n ∈ ℕ
89 74 88 31 syl2anc ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → H ⁡ n = n ⋅ W 1 W
90 76 46 syl ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → W ∈ Grp
91 88 29 syl ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → n ∈ ℤ
92 76 13 syl ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → 1 W ∈ B
93 1 8 mulgcl ⊢ W ∈ Grp ∧ n ∈ ℤ ∧ 1 W ∈ B → n ⋅ W 1 W ∈ B
94 90 91 92 93 syl3anc ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → n ⋅ W 1 W ∈ B
95 89 94 eqeltrd ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → H ⁡ n ∈ B
96 74 56 syl ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → W ∈ DivRing
97 simpr ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → x / r ⁡ W y < ˙ H ⁡ n
98 1 73 7 75 87 95 79 3 96 97 80 orngrmullt ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → x / r ⁡ W y ⋅ W y < ˙ H ⁡ n ⋅ W y
99 1 57 61 73 dvrcan1 ⊢ W ∈ Ring ∧ x ∈ B ∧ y ∈ Unit ⁡ W → x / r ⁡ W y ⋅ W y = x
100 76 78 86 99 syl3anc ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → x / r ⁡ W y ⋅ W y = x
101 89 oveq1d ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → H ⁡ n ⋅ W y = n ⋅ W 1 W ⋅ W y
102 1 8 73 mulgass2 ⊢ W ∈ Ring ∧ n ∈ ℤ ∧ 1 W ∈ B ∧ y ∈ B → n ⋅ W 1 W ⋅ W y = n ⋅ W 1 W ⋅ W y
103 76 91 92 79 102 syl13anc ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → n ⋅ W 1 W ⋅ W y = n ⋅ W 1 W ⋅ W y
104 1 73 12 ringlidm ⊢ W ∈ Ring ∧ y ∈ B → 1 W ⋅ W y = y
105 76 79 104 syl2anc ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → 1 W ⋅ W y = y
106 105 oveq2d ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → n ⋅ W 1 W ⋅ W y = n ⋅ W y
107 101 103 106 3eqtrd ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → H ⁡ n ⋅ W y = n ⋅ W y
108 98 100 107 3brtr3d ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → x < ˙ n ⋅ W y
109 108 ex ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ → x / r ⁡ W y < ˙ H ⁡ n → x < ˙ n ⋅ W y
110 109 reximdva ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → ∃ n ∈ ℕ x / r ⁡ W y < ˙ H ⁡ n → ∃ n ∈ ℕ x < ˙ n ⋅ W y
111 110 adantllr ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → ∃ n ∈ ℕ x / r ⁡ W y < ˙ H ⁡ n → ∃ n ∈ ℕ x < ˙ n ⋅ W y
112 72 111 mpd ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y
113 112 ex ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B → 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y
114 113 expr ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B → x ∈ B → 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y
115 40 114 ralrimi ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B → ∀ x ∈ B 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y
116 115 ralrimiva ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n → ∀ y ∈ B ∀ x ∈ B 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y
117 116 ex ⊢ W ∈ oField → ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n → ∀ y ∈ B ∀ x ∈ B 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y
118 35 117 impbid ⊢ W ∈ oField → ∀ y ∈ B ∀ x ∈ B 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y ↔ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n
119 10 118 bitrd ⊢ W ∈ oField → W ∈ Archi ↔ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n