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

Theorem isarchiofld 30818
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 30803 . . . 4 (𝑊 ∈ oField ↔ (𝑊 ∈ Field ∧ 𝑊 ∈ oRing))
21simprbi 497 . . 3 (𝑊 ∈ oField → 𝑊 ∈ oRing)
3 orngogrp 30802 . . 3 (𝑊 ∈ oRing → 𝑊 ∈ oGrp)
4 isarchiofld.b . . . 4 𝐵 = (Base‘𝑊)
5 eqid 2821 . . . 4 (0g𝑊) = (0g𝑊)
6 isarchiofld.l . . . 4 < = (lt‘𝑊)
7 eqid 2821 . . . 4 (.g𝑊) = (.g𝑊)
84, 5, 6, 7isarchi3 30744 . . 3 (𝑊 ∈ oGrp → (𝑊 ∈ Archi ↔ ∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦))))
92, 3, 83syl 18 . 2 (𝑊 ∈ oField → (𝑊 ∈ Archi ↔ ∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦))))
10 orngring 30801 . . . . . . 7 (𝑊 ∈ oRing → 𝑊 ∈ Ring)
11 eqid 2821 . . . . . . . 8 (1r𝑊) = (1r𝑊)
124, 11ringidcl 19249 . . . . . . 7 (𝑊 ∈ Ring → (1r𝑊) ∈ 𝐵)
132, 10, 123syl 18 . . . . . 6 (𝑊 ∈ oField → (1r𝑊) ∈ 𝐵)
14 breq2 5062 . . . . . . . . 9 (𝑦 = (1r𝑊) → ((0g𝑊) < 𝑦 ↔ (0g𝑊) < (1r𝑊)))
15 oveq2 7153 . . . . . . . . . . 11 (𝑦 = (1r𝑊) → (𝑛(.g𝑊)𝑦) = (𝑛(.g𝑊)(1r𝑊)))
1615breq2d 5070 . . . . . . . . . 10 (𝑦 = (1r𝑊) → (𝑥 < (𝑛(.g𝑊)𝑦) ↔ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
1716rexbidv 3297 . . . . . . . . 9 (𝑦 = (1r𝑊) → (∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦) ↔ ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
1814, 17imbi12d 346 . . . . . . . 8 (𝑦 = (1r𝑊) → (((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)) ↔ ((0g𝑊) < (1r𝑊) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊)))))
1918ralbidv 3197 . . . . . . 7 (𝑦 = (1r𝑊) → (∀𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)) ↔ ∀𝑥𝐵 ((0g𝑊) < (1r𝑊) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊)))))
2019rspcv 3617 . . . . . 6 ((1r𝑊) ∈ 𝐵 → (∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)) → ∀𝑥𝐵 ((0g𝑊) < (1r𝑊) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊)))))
2113, 20syl 17 . . . . 5 (𝑊 ∈ oField → (∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)) → ∀𝑥𝐵 ((0g𝑊) < (1r𝑊) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊)))))
225, 11, 6ofldlt1 30814 . . . . . . 7 (𝑊 ∈ oField → (0g𝑊) < (1r𝑊))
23 pm5.5 363 . . . . . . 7 ((0g𝑊) < (1r𝑊) → (((0g𝑊) < (1r𝑊) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))) ↔ ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
2422, 23syl 17 . . . . . 6 (𝑊 ∈ oField → (((0g𝑊) < (1r𝑊) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))) ↔ ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
2524ralbidv 3197 . . . . 5 (𝑊 ∈ oField → (∀𝑥𝐵 ((0g𝑊) < (1r𝑊) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))) ↔ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
2621, 25sylibd 240 . . . 4 (𝑊 ∈ oField → (∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)) → ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
272, 10syl 17 . . . . . . . 8 (𝑊 ∈ oField → 𝑊 ∈ Ring)
28 nnz 11993 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
29 isarchiofld.h . . . . . . . . 9 𝐻 = (ℤRHom‘𝑊)
3029, 7, 11zrhmulg 20587 . . . . . . . 8 ((𝑊 ∈ Ring ∧ 𝑛 ∈ ℤ) → (𝐻𝑛) = (𝑛(.g𝑊)(1r𝑊)))
3127, 28, 30syl2an 595 . . . . . . 7 ((𝑊 ∈ oField ∧ 𝑛 ∈ ℕ) → (𝐻𝑛) = (𝑛(.g𝑊)(1r𝑊)))
3231breq2d 5070 . . . . . 6 ((𝑊 ∈ oField ∧ 𝑛 ∈ ℕ) → (𝑥 < (𝐻𝑛) ↔ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
3332rexbidva 3296 . . . . 5 (𝑊 ∈ oField → (∃𝑛 ∈ ℕ 𝑥 < (𝐻𝑛) ↔ ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
3433ralbidv 3197 . . . 4 (𝑊 ∈ oField → (∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛) ↔ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)(1r𝑊))))
3526, 34sylibrd 260 . . 3 (𝑊 ∈ oField → (∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)) → ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)))
36 nfv 1906 . . . . . . . 8 𝑥 𝑊 ∈ oField
37 nfra1 3219 . . . . . . . 8 𝑥𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)
3836, 37nfan 1891 . . . . . . 7 𝑥(𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛))
39 nfv 1906 . . . . . . 7 𝑥 𝑦𝐵
4038, 39nfan 1891 . . . . . 6 𝑥((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ 𝑦𝐵)
4127ad3antrrr 726 . . . . . . . . . . 11 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → 𝑊 ∈ Ring)
42 simplrr 774 . . . . . . . . . . 11 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → 𝑥𝐵)
43 simplrl 773 . . . . . . . . . . . 12 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → 𝑦𝐵)
44 simpr 485 . . . . . . . . . . . . . 14 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → (0g𝑊) < 𝑦)
45 simplll 771 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → 𝑊 ∈ oField)
46 ringgrp 19233 . . . . . . . . . . . . . . . 16 (𝑊 ∈ Ring → 𝑊 ∈ Grp)
474, 5grpidcl 18071 . . . . . . . . . . . . . . . 16 (𝑊 ∈ Grp → (0g𝑊) ∈ 𝐵)
4841, 46, 473syl 18 . . . . . . . . . . . . . . 15 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → (0g𝑊) ∈ 𝐵)
496pltne 17562 . . . . . . . . . . . . . . 15 ((𝑊 ∈ oField ∧ (0g𝑊) ∈ 𝐵𝑦𝐵) → ((0g𝑊) < 𝑦 → (0g𝑊) ≠ 𝑦))
5045, 48, 43, 49syl3anc 1363 . . . . . . . . . . . . . 14 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → ((0g𝑊) < 𝑦 → (0g𝑊) ≠ 𝑦))
5144, 50mpd 15 . . . . . . . . . . . . 13 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → (0g𝑊) ≠ 𝑦)
5251necomd 3071 . . . . . . . . . . . 12 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → 𝑦 ≠ (0g𝑊))
531simplbi 498 . . . . . . . . . . . . . 14 (𝑊 ∈ oField → 𝑊 ∈ Field)
54 isfld 19442 . . . . . . . . . . . . . . 15 (𝑊 ∈ Field ↔ (𝑊 ∈ DivRing ∧ 𝑊 ∈ CRing))
5554simplbi 498 . . . . . . . . . . . . . 14 (𝑊 ∈ Field → 𝑊 ∈ DivRing)
5653, 55syl 17 . . . . . . . . . . . . 13 (𝑊 ∈ oField → 𝑊 ∈ DivRing)
57 eqid 2821 . . . . . . . . . . . . . 14 (Unit‘𝑊) = (Unit‘𝑊)
584, 57, 5drngunit 19438 . . . . . . . . . . . . 13 (𝑊 ∈ DivRing → (𝑦 ∈ (Unit‘𝑊) ↔ (𝑦𝐵𝑦 ≠ (0g𝑊))))
5945, 56, 583syl 18 . . . . . . . . . . . 12 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → (𝑦 ∈ (Unit‘𝑊) ↔ (𝑦𝐵𝑦 ≠ (0g𝑊))))
6043, 52, 59mpbir2and 709 . . . . . . . . . . 11 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → 𝑦 ∈ (Unit‘𝑊))
61 eqid 2821 . . . . . . . . . . . 12 (/r𝑊) = (/r𝑊)
624, 57, 61dvrcl 19367 . . . . . . . . . . 11 ((𝑊 ∈ Ring ∧ 𝑥𝐵𝑦 ∈ (Unit‘𝑊)) → (𝑥(/r𝑊)𝑦) ∈ 𝐵)
6341, 42, 60, 62syl3anc 1363 . . . . . . . . . 10 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → (𝑥(/r𝑊)𝑦) ∈ 𝐵)
64 simpr 485 . . . . . . . . . . . 12 ((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) → ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛))
65 breq1 5061 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑥 < (𝐻𝑛) ↔ 𝑧 < (𝐻𝑛)))
6665rexbidv 3297 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (∃𝑛 ∈ ℕ 𝑥 < (𝐻𝑛) ↔ ∃𝑛 ∈ ℕ 𝑧 < (𝐻𝑛)))
6766cbvralvw 3450 . . . . . . . . . . . 12 (∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛) ↔ ∀𝑧𝐵𝑛 ∈ ℕ 𝑧 < (𝐻𝑛))
6864, 67sylib 219 . . . . . . . . . . 11 ((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) → ∀𝑧𝐵𝑛 ∈ ℕ 𝑧 < (𝐻𝑛))
6968ad2antrr 722 . . . . . . . . . 10 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → ∀𝑧𝐵𝑛 ∈ ℕ 𝑧 < (𝐻𝑛))
70 breq1 5061 . . . . . . . . . . . 12 (𝑧 = (𝑥(/r𝑊)𝑦) → (𝑧 < (𝐻𝑛) ↔ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)))
7170rexbidv 3297 . . . . . . . . . . 11 (𝑧 = (𝑥(/r𝑊)𝑦) → (∃𝑛 ∈ ℕ 𝑧 < (𝐻𝑛) ↔ ∃𝑛 ∈ ℕ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)))
7271rspcv 3617 . . . . . . . . . 10 ((𝑥(/r𝑊)𝑦) ∈ 𝐵 → (∀𝑧𝐵𝑛 ∈ ℕ 𝑧 < (𝐻𝑛) → ∃𝑛 ∈ ℕ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)))
7363, 69, 72sylc 65 . . . . . . . . 9 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → ∃𝑛 ∈ ℕ (𝑥(/r𝑊)𝑦) < (𝐻𝑛))
74 eqid 2821 . . . . . . . . . . . . . 14 (.r𝑊) = (.r𝑊)
75 simp-4l 779 . . . . . . . . . . . . . . 15 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑊 ∈ oField)
7675, 2syl 17 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑊 ∈ oRing)
7775, 27syl 17 . . . . . . . . . . . . . . 15 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑊 ∈ Ring)
78 simp-4r 780 . . . . . . . . . . . . . . . 16 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (𝑦𝐵𝑥𝐵))
7978simprd 496 . . . . . . . . . . . . . . 15 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑥𝐵)
8078simpld 495 . . . . . . . . . . . . . . . 16 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑦𝐵)
81 simpllr 772 . . . . . . . . . . . . . . . . . 18 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (0g𝑊) < 𝑦)
8277, 46, 473syl 18 . . . . . . . . . . . . . . . . . . 19 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (0g𝑊) ∈ 𝐵)
8375, 82, 80, 49syl3anc 1363 . . . . . . . . . . . . . . . . . 18 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → ((0g𝑊) < 𝑦 → (0g𝑊) ≠ 𝑦))
8481, 83mpd 15 . . . . . . . . . . . . . . . . 17 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (0g𝑊) ≠ 𝑦)
8584necomd 3071 . . . . . . . . . . . . . . . 16 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑦 ≠ (0g𝑊))
8675, 56, 583syl 18 . . . . . . . . . . . . . . . 16 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (𝑦 ∈ (Unit‘𝑊) ↔ (𝑦𝐵𝑦 ≠ (0g𝑊))))
8780, 85, 86mpbir2and 709 . . . . . . . . . . . . . . 15 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑦 ∈ (Unit‘𝑊))
8877, 79, 87, 62syl3anc 1363 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (𝑥(/r𝑊)𝑦) ∈ 𝐵)
89 simplr 765 . . . . . . . . . . . . . . . 16 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑛 ∈ ℕ)
9075, 89, 31syl2anc 584 . . . . . . . . . . . . . . 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 18185 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ (1r𝑊) ∈ 𝐵) → (𝑛(.g𝑊)(1r𝑊)) ∈ 𝐵)
9591, 92, 93, 94syl3anc 1363 . . . . . . . . . . . . . . 15 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (𝑛(.g𝑊)(1r𝑊)) ∈ 𝐵)
9690, 95eqeltrd 2913 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (𝐻𝑛) ∈ 𝐵)
9775, 56syl 17 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑊 ∈ DivRing)
98 simpr 485 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (𝑥(/r𝑊)𝑦) < (𝐻𝑛))
994, 74, 5, 76, 88, 96, 80, 6, 97, 98, 81orngrmullt 30809 . . . . . . . . . . . . 13 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → ((𝑥(/r𝑊)𝑦)(.r𝑊)𝑦) < ((𝐻𝑛)(.r𝑊)𝑦))
1004, 57, 61, 74dvrcan1 19372 . . . . . . . . . . . . . 14 ((𝑊 ∈ Ring ∧ 𝑥𝐵𝑦 ∈ (Unit‘𝑊)) → ((𝑥(/r𝑊)𝑦)(.r𝑊)𝑦) = 𝑥)
10177, 79, 87, 100syl3anc 1363 . . . . . . . . . . . . 13 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → ((𝑥(/r𝑊)𝑦)(.r𝑊)𝑦) = 𝑥)
10290oveq1d 7160 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → ((𝐻𝑛)(.r𝑊)𝑦) = ((𝑛(.g𝑊)(1r𝑊))(.r𝑊)𝑦))
1034, 7, 74mulgass2 19282 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Ring ∧ (𝑛 ∈ ℤ ∧ (1r𝑊) ∈ 𝐵𝑦𝐵)) → ((𝑛(.g𝑊)(1r𝑊))(.r𝑊)𝑦) = (𝑛(.g𝑊)((1r𝑊)(.r𝑊)𝑦)))
10477, 92, 93, 80, 103syl13anc 1364 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → ((𝑛(.g𝑊)(1r𝑊))(.r𝑊)𝑦) = (𝑛(.g𝑊)((1r𝑊)(.r𝑊)𝑦)))
1054, 74, 11ringlidm 19252 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ Ring ∧ 𝑦𝐵) → ((1r𝑊)(.r𝑊)𝑦) = 𝑦)
10677, 80, 105syl2anc 584 . . . . . . . . . . . . . . 15 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → ((1r𝑊)(.r𝑊)𝑦) = 𝑦)
107106oveq2d 7161 . . . . . . . . . . . . . 14 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → (𝑛(.g𝑊)((1r𝑊)(.r𝑊)𝑦)) = (𝑛(.g𝑊)𝑦))
108102, 104, 1073eqtrd 2860 . . . . . . . . . . . . 13 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → ((𝐻𝑛)(.r𝑊)𝑦) = (𝑛(.g𝑊)𝑦))
10999, 101, 1083brtr3d 5089 . . . . . . . . . . . 12 (((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) ∧ (𝑥(/r𝑊)𝑦) < (𝐻𝑛)) → 𝑥 < (𝑛(.g𝑊)𝑦))
110109ex 413 . . . . . . . . . . 11 ((((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) ∧ 𝑛 ∈ ℕ) → ((𝑥(/r𝑊)𝑦) < (𝐻𝑛) → 𝑥 < (𝑛(.g𝑊)𝑦)))
111110reximdva 3274 . . . . . . . . . 10 (((𝑊 ∈ oField ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → (∃𝑛 ∈ ℕ (𝑥(/r𝑊)𝑦) < (𝐻𝑛) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)))
112111adantllr 715 . . . . . . . . 9 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → (∃𝑛 ∈ ℕ (𝑥(/r𝑊)𝑦) < (𝐻𝑛) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)))
11373, 112mpd 15 . . . . . . . 8 ((((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) ∧ (0g𝑊) < 𝑦) → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦))
114113ex 413 . . . . . . 7 (((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ (𝑦𝐵𝑥𝐵)) → ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)))
115114expr 457 . . . . . 6 (((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ 𝑦𝐵) → (𝑥𝐵 → ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦))))
11640, 115ralrimi 3216 . . . . 5 (((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) ∧ 𝑦𝐵) → ∀𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)))
117116ralrimiva 3182 . . . 4 ((𝑊 ∈ oField ∧ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)) → ∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)))
118117ex 413 . . 3 (𝑊 ∈ oField → (∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛) → ∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦))))
11935, 118impbid 213 . 2 (𝑊 ∈ oField → (∀𝑦𝐵𝑥𝐵 ((0g𝑊) < 𝑦 → ∃𝑛 ∈ ℕ 𝑥 < (𝑛(.g𝑊)𝑦)) ↔ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)))
1209, 119bitrd 280 1 (𝑊 ∈ oField → (𝑊 ∈ Archi ↔ ∀𝑥𝐵𝑛 ∈ ℕ 𝑥 < (𝐻𝑛)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wne 3016  wral 3138  wrex 3139   class class class wbr 5058  cfv 6349  (class class class)co 7145  cn 11627  cz 11970  Basecbs 16473  .rcmulr 16556  0gc0g 16703  ltcplt 17541  Grpcgrp 18043  .gcmg 18164  1rcur 19182  Ringcrg 19228  CRingccrg 19229  Unitcui 19320  /rcdvr 19363  DivRingcdr 19433  Fieldcfield 19434  ℤRHomczrh 20577  oGrpcogrp 30627  Archicarchi 30734  oRingcorng 30796  oFieldcofld 30797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-addf 10605  ax-mulf 10606
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-int 4870  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7569  df-1st 7680  df-2nd 7681  df-tpos 7883  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-oadd 8097  df-er 8279  df-map 8398  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-2 11689  df-3 11690  df-4 11691  df-5 11692  df-6 11693  df-7 11694  df-8 11695  df-9 11696  df-n0 11887  df-z 11971  df-dec 12088  df-uz 12233  df-fz 12883  df-seq 13360  df-struct 16475  df-ndx 16476  df-slot 16477  df-base 16479  df-sets 16480  df-ress 16481  df-plusg 16568  df-mulr 16569  df-starv 16570  df-tset 16574  df-ple 16575  df-ds 16577  df-unif 16578  df-0g 16705  df-proset 17528  df-poset 17546  df-plt 17558  df-toset 17634  df-mgm 17842  df-sgrp 17891  df-mnd 17902  df-mhm 17946  df-grp 18046  df-minusg 18047  df-sbg 18048  df-mulg 18165  df-subg 18216  df-ghm 18296  df-cmn 18839  df-mgp 19171  df-ur 19183  df-ring 19230  df-cring 19231  df-oppr 19304  df-dvdsr 19322  df-unit 19323  df-invr 19353  df-dvr 19364  df-rnghom 19398  df-drng 19435  df-field 19436  df-subrg 19464  df-cnfld 20476  df-zring 20548  df-zrh 20581  df-omnd 30628  df-ogrp 30629  df-inftm 30735  df-archi 30736  df-orng 30798  df-ofld 30799
This theorem is referenced by:  rearchi  30843
  Copyright terms: Public domain W3C validator