Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isarchiofld Structured version   Visualization version   GIF version

Theorem isarchiofld 30126
 Description: Axiom of Archimedes : a characterization of the Archimedean property for ordered fields. (Contributed by Thierry Arnoux, 9-Apr-2018.)
Hypotheses
Ref Expression
isarchiofld.b 𝐵 = (Base‘𝑊)
isarchiofld.h 𝐻 = (ℤRHom‘𝑊)
isarchiofld.l < = (lt‘𝑊)
Assertion
Ref Expression
isarchiofld (𝑊 ∈ oField → (𝑊 ∈ Archi ↔ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)))
Distinct variable groups:   𝑥,𝑛,𝐵   𝑛,𝑊,𝑥   𝑥,𝐻   < ,𝑛,𝑥
Allowed substitution hint:   𝐻(𝑛)

Proof of Theorem isarchiofld
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isofld 30111 . . . 4 (𝑊 ∈ oField ↔ (𝑊 ∈ Field ∧ 𝑊 ∈ oRing))
21simprbi 483 . . 3 (𝑊 ∈ oField → 𝑊 ∈ oRing)
3 orngogrp 30110 . . 3 (𝑊 ∈ oRing → 𝑊 ∈ oGrp)
4 isarchiofld.b . . . 4 𝐵 = (Base‘𝑊)
5 eqid 2760 . . . 4 (0g𝑊) = (0g𝑊)
6 isarchiofld.l . . . 4 < = (lt‘𝑊)
7 eqid 2760 . . . 4 (.g𝑊) = (.g𝑊)
84, 5, 6, 7isarchi3 30050 . . 3 (𝑊 ∈ oGrp → (𝑊 ∈ Archi ↔ ∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦))))
92, 3, 83syl 18 . 2 (𝑊 ∈ oField → (𝑊 ∈ Archi ↔ ∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦))))
10 orngring 30109 . . . . . . 7 (𝑊 ∈ oRing → 𝑊 ∈ Ring)
11 eqid 2760 . . . . . . . 8 (1r𝑊) = (1r𝑊)
124, 11ringidcl 18768 . . . . . . 7 (𝑊 ∈ Ring → (1r𝑊) ∈ 𝐵)
132, 10, 123syl 18 . . . . . 6 (𝑊 ∈ oField → (1r𝑊) ∈ 𝐵)
14 breq2 4808 . . . . . . . . 9 (𝑦 = (1r𝑊) → ((0g𝑊) < 𝑦 ↔ (0g𝑊) < (1r𝑊)))
15 oveq2 6821 . . . . . . . . . . 11 (𝑦 = (1r𝑊) → (𝑛(.g𝑊)𝑦) = (𝑛(.g𝑊)(1r𝑊)))
1615breq2d 4816 . . . . . . . . . 10 (𝑦 = (1r𝑊) → (𝑥 < (𝑛(.g𝑊)𝑦) ↔ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
1716rexbidv 3190 . . . . . . . . 9 (𝑦 = (1r𝑊) → (∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦) ↔ ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
1814, 17imbi12d 333 . . . . . . . 8 (𝑦 = (1r𝑊) → (((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)) ↔ ((0g𝑊) < (1r𝑊) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊)))))
1918ralbidv 3124 . . . . . . 7 (𝑦 = (1r𝑊) → (∀𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)) ↔ ∀𝑥𝐵 ((0g𝑊) < (1r𝑊) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊)))))
2019rspcv 3445 . . . . . 6 ((1r𝑊) ∈ 𝐵 → (∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)) → ∀𝑥𝐵 ((0g𝑊) < (1r𝑊) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊)))))
2113, 20syl 17 . . . . 5 (𝑊 ∈ oField → (∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)) → ∀𝑥𝐵 ((0g𝑊) < (1r𝑊) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊)))))
225, 11, 6ofldlt1 30122 . . . . . . 7 (𝑊 ∈ oField → (0g𝑊) < (1r𝑊))
23 pm5.5 350 . . . . . . 7 ((0g𝑊) < (1r𝑊) → (((0g𝑊) < (1r𝑊) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))) ↔ ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
2422, 23syl 17 . . . . . 6 (𝑊 ∈ oField → (((0g𝑊) < (1r𝑊) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))) ↔ ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
2524ralbidv 3124 . . . . 5 (𝑊 ∈ oField → (∀𝑥𝐵 ((0g𝑊) < (1r𝑊) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))) ↔ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
2621, 25sylibd 229 . . . 4 (𝑊 ∈ oField → (∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)) → ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
272, 10syl 17 . . . . . . . 8 (𝑊 ∈ oField → 𝑊 ∈ Ring)
28 nnz 11591 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
29 isarchiofld.h . . . . . . . . 9 𝐻 = (ℤRHom‘𝑊)
3029, 7, 11zrhmulg 20060 . . . . . . . 8 ((𝑊 ∈ Ring ∧ 𝑛 ∈ ℤ) → (𝐻𝑛) = (𝑛(.g𝑊)(1r𝑊)))
3127, 28, 30syl2an 495 . . . . . . 7 ((𝑊 ∈ oField ∧ 𝑛 ∈ ℕ) → (𝐻𝑛) = (𝑛(.g𝑊)(1r𝑊)))
3231breq2d 4816 . . . . . 6 ((𝑊 ∈ oField ∧ 𝑛 ∈ ℕ) → (𝑥 < (𝐻𝑛) ↔ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
3332rexbidva 3187 . . . . 5 (𝑊 ∈ oField → (∃𝑛 ∈ ℕ 𝑥 < (𝐻𝑛) ↔ ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
3433ralbidv 3124 . . . 4 (𝑊 ∈ oField → (∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛) ↔ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
3526, 34sylibrd 249 . . 3 (𝑊 ∈ oField → (∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)) → ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)))
36 nfv 1992 . . . . . . . 8 𝑥 𝑊 ∈ oField
37 nfra1 3079 . . . . . . . 8 𝑥𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)
3836, 37nfan 1977 . . . . . . 7 𝑥(𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛))
39 nfv 1992 . . . . . . 7 𝑥 𝑦𝐵
4038, 39nfan 1977 . . . . . 6 𝑥((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ 𝑦𝐵)
4127ad3antrrr 768 . . . . . . . . . . 11 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → 𝑊 ∈ Ring)
42 simplrr 820 . . . . . . . . . . 11 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → 𝑥𝐵)
43 simplrl 819 . . . . . . . . . . . 12 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → 𝑦𝐵)
44 simpr 479 . . . . . . . . . . . . . 14 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → (0g𝑊) < 𝑦)
45 simplll 815 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → 𝑊 ∈ oField)
46 ringgrp 18752 . . . . . . . . . . . . . . . 16 (𝑊 ∈ Ring → 𝑊 ∈ Grp)
474, 5grpidcl 17651 . . . . . . . . . . . . . . . 16 (𝑊 ∈ Grp → (0g𝑊) ∈ 𝐵)
4841, 46, 473syl 18 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → (0g𝑊) ∈ 𝐵)
496pltne 17163 . . . . . . . . . . . . . . 15 ((𝑊 ∈ oField ∧ (0g𝑊) ∈ 𝐵𝑦𝐵) → ((0g𝑊) < 𝑦 → (0g𝑊) ≠ 𝑦))
5045, 48, 43, 49syl3anc 1477 . . . . . . . . . . . . . 14 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → ((0g𝑊) < 𝑦 → (0g𝑊) ≠ 𝑦))
5144, 50mpd 15 . . . . . . . . . . . . 13 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → (0g𝑊) ≠ 𝑦)
5251necomd 2987 . . . . . . . . . . . 12 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → 𝑦 ≠ (0g𝑊))
531simplbi 478 . . . . . . . . . . . . . 14 (𝑊 ∈ oField → 𝑊 ∈ Field)
54 isfld 18958 . . . . . . . . . . . . . . 15 (𝑊 ∈ Field ↔ (𝑊 ∈ DivRing ∧ 𝑊 ∈ CRing))
5554simplbi 478 . . . . . . . . . . . . . 14 (𝑊 ∈ Field → 𝑊 ∈ DivRing)
5653, 55syl 17 . . . . . . . . . . . . 13 (𝑊 ∈ oField → 𝑊 ∈ DivRing)
57 eqid 2760 . . . . . . . . . . . . . 14 (Unit‘𝑊) = (Unit‘𝑊)
584, 57, 5drngunit 18954 . . . . . . . . . . . . 13 (𝑊 ∈ DivRing → (𝑦 ∈ (Unit‘𝑊) ↔ (𝑦𝐵𝑦 ≠ (0g𝑊))))
5945, 56, 583syl 18 . . . . . . . . . . . 12 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → (𝑦 ∈ (Unit‘𝑊) ↔ (𝑦𝐵𝑦 ≠ (0g𝑊))))
6043, 52, 59mpbir2and 995 . . . . . . . . . . 11 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → 𝑦 ∈ (Unit‘𝑊))
61 eqid 2760 . . . . . . . . . . . 12 (/r𝑊) = (/r𝑊)
624, 57, 61dvrcl 18886 . . . . . . . . . . 11 ((𝑊 ∈ Ring ∧ 𝑥𝐵𝑦 ∈ (Unit‘𝑊)) → (𝑥(/r𝑊)𝑦) ∈ 𝐵)
6341, 42, 60, 62syl3anc 1477 . . . . . . . . . 10 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → (𝑥(/r𝑊)𝑦) ∈ 𝐵)
64 simpr 479 . . . . . . . . . . . 12 ((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) → ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛))
65 breq1 4807 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑥 < (𝐻𝑛) ↔ 𝑧 < (𝐻𝑛)))
6665rexbidv 3190 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (∃𝑛 ∈ ℕ 𝑥 < (𝐻𝑛) ↔ ∃𝑛 ∈ ℕ 𝑧 < (𝐻𝑛)))
6766cbvralv 3310 . . . . . . . . . . . 12 (∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛) ↔ ∀𝑧𝐵𝑛 ∈ ℕ 𝑧 < (𝐻𝑛))
6864, 67sylib 208 . . . . . . . . . . 11 ((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) → ∀𝑧𝐵𝑛 ∈ ℕ 𝑧 < (𝐻𝑛))
6968ad2antrr 764 . . . . . . . . . 10 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → ∀𝑧𝐵𝑛 ∈ ℕ 𝑧 < (𝐻𝑛))
70 breq1 4807 . . . . . . . . . . . 12 (𝑧 = (𝑥(/r𝑊)𝑦) → (𝑧 < (𝐻𝑛) ↔ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)))
7170rexbidv 3190 . . . . . . . . . . 11 (𝑧 = (𝑥(/r𝑊)𝑦) → (∃𝑛 ∈ ℕ 𝑧 < (𝐻𝑛) ↔ ∃𝑛 ∈ ℕ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)))
7271rspcv 3445 . . . . . . . . . 10 ((𝑥(/r𝑊)𝑦) ∈ 𝐵 → (∀𝑧𝐵𝑛 ∈ ℕ 𝑧 < (𝐻𝑛) → ∃𝑛 ∈ ℕ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)))
7363, 69, 72sylc 65 . . . . . . . . 9 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → ∃𝑛 ∈ ℕ (𝑥(/r𝑊)𝑦) < (𝐻𝑛))
74 eqid 2760 . . . . . . . . . . . . . 14 (.r𝑊) = (.r𝑊)
75 simp-4l 825 . . . . . . . . . . . . . . 15 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑊 ∈ oField)
7675, 2syl 17 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑊 ∈ oRing)
7775, 27syl 17 . . . . . . . . . . . . . . 15 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑊 ∈ Ring)
78 simp-4r 827 . . . . . . . . . . . . . . . 16 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (𝑦𝐵𝑥𝐵))
7978simprd 482 . . . . . . . . . . . . . . 15 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑥𝐵)
8078simpld 477 . . . . . . . . . . . . . . . 16 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑦𝐵)
81 simpllr 817 . . . . . . . . . . . . . . . . . 18 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (0g𝑊) < 𝑦)
8277, 46, 473syl 18 . . . . . . . . . . . . . . . . . . 19 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (0g𝑊) ∈ 𝐵)
8375, 82, 80, 49syl3anc 1477 . . . . . . . . . . . . . . . . . 18 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → ((0g𝑊) < 𝑦 → (0g𝑊) ≠ 𝑦))
8481, 83mpd 15 . . . . . . . . . . . . . . . . 17 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (0g𝑊) ≠ 𝑦)
8584necomd 2987 . . . . . . . . . . . . . . . 16 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑦 ≠ (0g𝑊))
8675, 56, 583syl 18 . . . . . . . . . . . . . . . 16 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (𝑦 ∈ (Unit‘𝑊) ↔ (𝑦𝐵𝑦 ≠ (0g𝑊))))
8780, 85, 86mpbir2and 995 . . . . . . . . . . . . . . 15 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑦 ∈ (Unit‘𝑊))
8877, 79, 87, 62syl3anc 1477 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (𝑥(/r𝑊)𝑦) ∈ 𝐵)
89 simplr 809 . . . . . . . . . . . . . . . 16 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑛 ∈ ℕ)
9075, 89, 31syl2anc 696 . . . . . . . . . . . . . . 15 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (𝐻𝑛) = (𝑛(.g𝑊)(1r𝑊)))
9177, 46syl 17 . . . . . . . . . . . . . . . 16 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑊 ∈ Grp)
9289, 28syl 17 . . . . . . . . . . . . . . . 16 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑛 ∈ ℤ)
9377, 12syl 17 . . . . . . . . . . . . . . . 16 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (1r𝑊) ∈ 𝐵)
944, 7mulgcl 17760 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ (1r𝑊) ∈ 𝐵) → (𝑛(.g𝑊)(1r𝑊)) ∈ 𝐵)
9591, 92, 93, 94syl3anc 1477 . . . . . . . . . . . . . . 15 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (𝑛(.g𝑊)(1r𝑊)) ∈ 𝐵)
9690, 95eqeltrd 2839 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (𝐻𝑛) ∈ 𝐵)
9775, 56syl 17 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑊 ∈ DivRing)
98 simpr 479 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (𝑥(/r𝑊)𝑦) < (𝐻𝑛))
994, 74, 5, 76, 88, 96, 80, 6, 97, 98, 81orngrmullt 30117 . . . . . . . . . . . . 13 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → ((𝑥(/r𝑊)𝑦)(.r𝑊)𝑦) < ((𝐻𝑛)(.r𝑊)𝑦))
1004, 57, 61, 74dvrcan1 18891 . . . . . . . . . . . . . 14 ((𝑊 ∈ Ring ∧ 𝑥𝐵𝑦 ∈ (Unit‘𝑊)) → ((𝑥(/r𝑊)𝑦)(.r𝑊)𝑦) = 𝑥)
10177, 79, 87, 100syl3anc 1477 . . . . . . . . . . . . 13 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → ((𝑥(/r𝑊)𝑦)(.r𝑊)𝑦) = 𝑥)
10290oveq1d 6828 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → ((𝐻𝑛)(.r𝑊)𝑦) = ((𝑛(.g𝑊)(1r𝑊))(.r𝑊)𝑦))
1034, 7, 74mulgass2 18801 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Ring ∧ (𝑛 ∈ ℤ ∧ (1r𝑊) ∈ 𝐵𝑦𝐵)) → ((𝑛(.g𝑊)(1r𝑊))(.r𝑊)𝑦) = (𝑛(.g𝑊)((1r𝑊)(.r𝑊)𝑦)))
10477, 92, 93, 80, 103syl13anc 1479 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → ((𝑛(.g𝑊)(1r𝑊))(.r𝑊)𝑦) = (𝑛(.g𝑊)((1r𝑊)(.r𝑊)𝑦)))
1054, 74, 11ringlidm 18771 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ Ring ∧ 𝑦𝐵) → ((1r𝑊)(.r𝑊)𝑦) = 𝑦)
10677, 80, 105syl2anc 696 . . . . . . . . . . . . . . 15 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → ((1r𝑊)(.r𝑊)𝑦) = 𝑦)
107106oveq2d 6829 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (𝑛(.g𝑊)((1r𝑊)(.r𝑊)𝑦)) = (𝑛(.g𝑊)𝑦))
108102, 104, 1073eqtrd 2798 . . . . . . . . . . . . 13 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → ((𝐻𝑛)(.r𝑊)𝑦) = (𝑛(.g𝑊)𝑦))
10999, 101, 1083brtr3d 4835 . . . . . . . . . . . 12 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑥 < (𝑛(.g𝑊)𝑦))
110109ex 449 . . . . . . . . . . 11 ((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) → ((𝑥(/r𝑊)𝑦) < (𝐻𝑛) → 𝑥 < (𝑛(.g𝑊)𝑦)))
111110reximdva 3155 . . . . . . . . . 10 (((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → (∃𝑛 ∈ ℕ (𝑥(/r𝑊)𝑦) < (𝐻𝑛) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)))
112111adantllr 757 . . . . . . . . 9 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → (∃𝑛 ∈ ℕ (𝑥(/r𝑊)𝑦) < (𝐻𝑛) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)))
11373, 112mpd 15 . . . . . . . 8 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦))
114113ex 449 . . . . . . 7 (((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) → ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)))
115114expr 644 . . . . . 6 (((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ 𝑦𝐵) → (𝑥𝐵 → ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦))))
11640, 115ralrimi 3095 . . . . 5 (((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ 𝑦𝐵) → ∀𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)))
117116ralrimiva 3104 . . . 4 ((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) → ∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)))
118117ex 449 . . 3 (𝑊 ∈ oField → (∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛) → ∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦))))
11935, 118impbid 202 . 2 (𝑊 ∈ oField → (∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)) ↔ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)))
1209, 119bitrd 268 1 (𝑊 ∈ oField → (𝑊 ∈ Archi ↔ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632   ∈ wcel 2139   ≠ wne 2932  ∀wral 3050  ∃wrex 3051   class class class wbr 4804  ‘cfv 6049  (class class class)co 6813  ℕcn 11212  ℤcz 11569  Basecbs 16059  .rcmulr 16144  0gc0g 16302  ltcplt 17142  Grpcgrp 17623  .gcmg 17741  1rcur 18701  Ringcrg 18747  CRingccrg 18748  Unitcui 18839  /rcdvr 18882  DivRingcdr 18949  Fieldcfield 18950  ℤRHomczrh 20050  oGrpcogrp 30007  Archicarchi 30040  oRingcorng 30104  oFieldcofld 30105 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-addf 10207  ax-mulf 10208 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-tpos 7521  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-oadd 7733  df-er 7911  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-fz 12520  df-seq 12996  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-mulr 16157  df-starv 16158  df-tset 16162  df-ple 16163  df-ds 16166  df-unif 16167  df-0g 16304  df-preset 17129  df-poset 17147  df-plt 17159  df-toset 17235  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-mhm 17536  df-grp 17626  df-minusg 17627  df-sbg 17628  df-mulg 17742  df-subg 17792  df-ghm 17859  df-cmn 18395  df-mgp 18690  df-ur 18702  df-ring 18749  df-cring 18750  df-oppr 18823  df-dvdsr 18841  df-unit 18842  df-invr 18872  df-dvr 18883  df-rnghom 18917  df-drng 18951  df-field 18952  df-subrg 18980  df-cnfld 19949  df-zring 20021  df-zrh 20054  df-omnd 30008  df-ogrp 30009  df-inftm 30041  df-archi 30042  df-orng 30106  df-ofld 30107 This theorem is referenced by:  rearchi  30151
 Copyright terms: Public domain W3C validator