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 simpr ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n → ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n
65 breq1 ⊢ x = z → x < ˙ H ⁡ n ↔ z < ˙ H ⁡ n
66 65 rexbidv ⊢ x = z → ∃ n ∈ ℕ x < ˙ H ⁡ n ↔ ∃ n ∈ ℕ z < ˙ H ⁡ n
67 66 cbvralvw ⊢ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ↔ ∀ z ∈ B ∃ n ∈ ℕ z < ˙ H ⁡ n
68 64 67 sylib ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n → ∀ z ∈ B ∃ n ∈ ℕ z < ˙ H ⁡ n
69 68 ad2antrr ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → ∀ z ∈ B ∃ n ∈ ℕ z < ˙ H ⁡ n
70 breq1 ⊢ z = x / r ⁡ W y → z < ˙ H ⁡ n ↔ x / r ⁡ W y < ˙ H ⁡ n
71 70 rexbidv ⊢ z = x / r ⁡ W y → ∃ n ∈ ℕ z < ˙ H ⁡ n ↔ ∃ n ∈ ℕ x / r ⁡ W y < ˙ H ⁡ n
72 71 rspcv ⊢ x / r ⁡ W y ∈ B → ∀ z ∈ B ∃ n ∈ ℕ z < ˙ H ⁡ n → ∃ n ∈ ℕ x / r ⁡ W y < ˙ H ⁡ n
73 63 69 72 sylc ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → ∃ n ∈ ℕ x / r ⁡ W y < ˙ H ⁡ n
74 eqid ⊢ ⋅ W = ⋅ W
75 simp-4l ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → W ∈ oField
76 75 5 syl ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → W ∈ oRing
77 75 28 syl ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → W ∈ Ring
78 simp-4r ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → y ∈ B ∧ x ∈ B
79 78 simprd ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → x ∈ B
80 78 simpld ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → y ∈ B
81 simpllr ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → 0 W < ˙ y
82 77 46 47 3syl ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → 0 W ∈ B
83 75 82 80 49 syl3anc ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → 0 W < ˙ y → 0 W ≠ y
84 81 83 mpd ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → 0 W ≠ y
85 84 necomd ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → y ≠ 0 W
86 75 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
87 80 85 86 mpbir2and ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → y ∈ Unit ⁡ W
88 77 79 87 62 syl3anc ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → x / r ⁡ W y ∈ B
89 simplr ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → n ∈ ℕ
90 75 89 31 syl2anc ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → H ⁡ n = n ⋅ W 1 W
91 77 46 syl ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → W ∈ Grp
92 89 29 syl ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → n ∈ ℤ
93 77 13 syl ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → 1 W ∈ B
94 1 8 mulgcl ⊢ W ∈ Grp ∧ n ∈ ℤ ∧ 1 W ∈ B → n ⋅ W 1 W ∈ B
95 91 92 93 94 syl3anc ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → n ⋅ W 1 W ∈ B
96 90 95 eqeltrd ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → H ⁡ n ∈ B
97 75 56 syl ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → W ∈ DivRing
98 simpr ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → x / r ⁡ W y < ˙ H ⁡ n
99 1 74 7 76 88 96 80 3 97 98 81 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
100 1 57 61 74 dvrcan1 ⊢ W ∈ Ring ∧ x ∈ B ∧ y ∈ Unit ⁡ W → x / r ⁡ W y ⋅ W y = x
101 77 79 87 100 syl3anc ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → x / r ⁡ W y ⋅ W y = x
102 90 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
103 1 8 74 mulgass2 ⊢ W ∈ Ring ∧ n ∈ ℤ ∧ 1 W ∈ B ∧ y ∈ B → n ⋅ W 1 W ⋅ W y = n ⋅ W 1 W ⋅ W y
104 77 92 93 80 103 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
105 1 74 12 ringlidm ⊢ W ∈ Ring ∧ y ∈ B → 1 W ⋅ W y = y
106 77 80 105 syl2anc ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → 1 W ⋅ W y = y
107 106 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
108 102 104 107 3eqtrd ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → H ⁡ n ⋅ W y = n ⋅ W y
109 99 101 108 3brtr3d ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ ∧ x / r ⁡ W y < ˙ H ⁡ n → x < ˙ n ⋅ W y
110 109 ex ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y ∧ n ∈ ℕ → x / r ⁡ W y < ˙ H ⁡ n → x < ˙ n ⋅ W y
111 110 reximdva ⊢ W ∈ oField ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → ∃ n ∈ ℕ x / r ⁡ W y < ˙ H ⁡ n → ∃ n ∈ ℕ x < ˙ n ⋅ W y
112 111 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
113 73 112 mpd ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B ∧ 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y
114 113 ex ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B ∧ x ∈ B → 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y
115 114 expr ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B → x ∈ B → 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y
116 40 115 ralrimi ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n ∧ y ∈ B → ∀ x ∈ B 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y
117 116 ralrimiva ⊢ W ∈ oField ∧ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n → ∀ y ∈ B ∀ x ∈ B 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y
118 117 ex ⊢ W ∈ oField → ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n → ∀ y ∈ B ∀ x ∈ B 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y
119 35 118 impbid ⊢ W ∈ oField → ∀ y ∈ B ∀ x ∈ B 0 W < ˙ y → ∃ n ∈ ℕ x < ˙ n ⋅ W y ↔ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n
120 10 119 bitrd ⊢ W ∈ oField → W ∈ Archi ↔ ∀ x ∈ B ∃ n ∈ ℕ x < ˙ H ⁡ n