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