Metamath Proof Explorer

Theorem ofldchr

Description: The characteristic of an ordered field is zero. (Contributed by Thierry Arnoux, 21-Jan-2018) (Proof shortened by AV, 6-Oct-2020)

Ref Expression
Assertion ofldchr ⊢ F ∈ oField → chr ⁡ F = 0

Proof

Step Hyp Ref Expression
1 eqid ⊢ od ⁡ F = od ⁡ F
2 eqid ⊢ 1 F = 1 F
3 eqid ⊢ chr ⁡ F = chr ⁡ F
4 1 2 3 chrval ⊢ od ⁡ F ⁡ 1 F = chr ⁡ F
5 ofldfld ⊢ F ∈ oField → F ∈ Field
6 isfld ⊢ F ∈ Field ↔ F ∈ DivRing ∧ F ∈ CRing
7 6 simplbi ⊢ F ∈ Field → F ∈ DivRing
8 drngring ⊢ F ∈ DivRing → F ∈ Ring
9 5 7 8 3syl ⊢ F ∈ oField → F ∈ Ring
10 eqid ⊢ Base F = Base F
11 10 2 ringidcl ⊢ F ∈ Ring → 1 F ∈ Base F
12 eqid ⊢ ⋅ F = ⋅ F
13 eqid ⊢ 0 F = 0 F
14 eqid ⊢ y ∈ ℕ | y ⋅ F 1 F = 0 F = y ∈ ℕ | y ⋅ F 1 F = 0 F
15 10 12 13 1 14 odval ⊢ 1 F ∈ Base F → od ⁡ F ⁡ 1 F = if y ∈ ℕ | y ⋅ F 1 F = 0 F = ∅ 0 sup y ∈ ℕ | y ⋅ F 1 F = 0 F ℝ <
16 9 11 15 3syl ⊢ F ∈ oField → od ⁡ F ⁡ 1 F = if y ∈ ℕ | y ⋅ F 1 F = 0 F = ∅ 0 sup y ∈ ℕ | y ⋅ F 1 F = 0 F ℝ <
17 oveq1 ⊢ n = 1 → n ⋅ F 1 F = 1 ⋅ F 1 F
18 17 breq2d ⊢ n = 1 → 0 F < F n ⋅ F 1 F ↔ 0 F < F 1 ⋅ F 1 F
19 18 imbi2d ⊢ n = 1 → F ∈ oField → 0 F < F n ⋅ F 1 F ↔ F ∈ oField → 0 F < F 1 ⋅ F 1 F
20 oveq1 ⊢ n = m → n ⋅ F 1 F = m ⋅ F 1 F
21 20 breq2d ⊢ n = m → 0 F < F n ⋅ F 1 F ↔ 0 F < F m ⋅ F 1 F
22 21 imbi2d ⊢ n = m → F ∈ oField → 0 F < F n ⋅ F 1 F ↔ F ∈ oField → 0 F < F m ⋅ F 1 F
23 oveq1 ⊢ n = m + 1 → n ⋅ F 1 F = m + 1 ⋅ F 1 F
24 23 breq2d ⊢ n = m + 1 → 0 F < F n ⋅ F 1 F ↔ 0 F < F m + 1 ⋅ F 1 F
25 24 imbi2d ⊢ n = m + 1 → F ∈ oField → 0 F < F n ⋅ F 1 F ↔ F ∈ oField → 0 F < F m + 1 ⋅ F 1 F
26 oveq1 ⊢ n = y → n ⋅ F 1 F = y ⋅ F 1 F
27 26 breq2d ⊢ n = y → 0 F < F n ⋅ F 1 F ↔ 0 F < F y ⋅ F 1 F
28 27 imbi2d ⊢ n = y → F ∈ oField → 0 F < F n ⋅ F 1 F ↔ F ∈ oField → 0 F < F y ⋅ F 1 F
29 eqid ⊢ < F = < F
30 13 2 29 ofldlt1 ⊢ F ∈ oField → 0 F < F 1 F
31 9 11 syl ⊢ F ∈ oField → 1 F ∈ Base F
32 10 12 mulg1 ⊢ 1 F ∈ Base F → 1 ⋅ F 1 F = 1 F
33 31 32 syl ⊢ F ∈ oField → 1 ⋅ F 1 F = 1 F
34 30 33 breqtrrd ⊢ F ∈ oField → 0 F < F 1 ⋅ F 1 F
35 ofldtos ⊢ F ∈ oField → F ∈ Toset
36 tospos ⊢ F ∈ Toset → F ∈ Poset
37 35 36 syl ⊢ F ∈ oField → F ∈ Poset
38 37 ad2antlr ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → F ∈ Poset
39 9 ringgrpd ⊢ F ∈ oField → F ∈ Grp
40 39 ad2antlr ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → F ∈ Grp
41 10 13 grpidcl ⊢ F ∈ Grp → 0 F ∈ Base F
42 40 41 syl ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → 0 F ∈ Base F
43 40 grpmgmd ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → F ∈ Mgm
44 simpll ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → m ∈ ℕ
45 31 ad2antlr ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → 1 F ∈ Base F
46 10 12 mulgnncl ⊢ F ∈ Mgm ∧ m ∈ ℕ ∧ 1 F ∈ Base F → m ⋅ F 1 F ∈ Base F
47 43 44 45 46 syl3anc ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → m ⋅ F 1 F ∈ Base F
48 44 peano2nnd ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → m + 1 ∈ ℕ
49 10 12 mulgnncl ⊢ F ∈ Mgm ∧ m + 1 ∈ ℕ ∧ 1 F ∈ Base F → m + 1 ⋅ F 1 F ∈ Base F
50 43 48 45 49 syl3anc ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → m + 1 ⋅ F 1 F ∈ Base F
51 42 47 50 3jca ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → 0 F ∈ Base F ∧ m ⋅ F 1 F ∈ Base F ∧ m + 1 ⋅ F 1 F ∈ Base F
52 simpr ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → 0 F < F m ⋅ F 1 F
53 simplr ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → F ∈ oField
54 isofld ⊢ F ∈ oField ↔ F ∈ Field ∧ F ∈ oRing
55 54 simprbi ⊢ F ∈ oField → F ∈ oRing
56 orngogrp ⊢ F ∈ oRing → F ∈ oGrp
57 53 55 56 3syl ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → F ∈ oGrp
58 30 ad2antlr ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → 0 F < F 1 F
59 eqid ⊢ + F = + F
60 10 29 59 ogrpaddlt ⊢ F ∈ oGrp ∧ 0 F ∈ Base F ∧ 1 F ∈ Base F ∧ m ⋅ F 1 F ∈ Base F ∧ 0 F < F 1 F → 0 F + F m ⋅ F 1 F < F 1 F + F m ⋅ F 1 F
61 57 42 45 47 58 60 syl131anc ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → 0 F + F m ⋅ F 1 F < F 1 F + F m ⋅ F 1 F
62 10 59 13 40 47 grplidd ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → 0 F + F m ⋅ F 1 F = m ⋅ F 1 F
63 62 eqcomd ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → m ⋅ F 1 F = 0 F + F m ⋅ F 1 F
64 10 12 59 mulgnnp1 ⊢ m ∈ ℕ ∧ 1 F ∈ Base F → m + 1 ⋅ F 1 F = m ⋅ F 1 F + F 1 F
65 44 45 64 syl2anc ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → m + 1 ⋅ F 1 F = m ⋅ F 1 F + F 1 F
66 ringcmn ⊢ F ∈ Ring → F ∈ CMnd
67 53 9 66 3syl ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → F ∈ CMnd
68 10 59 cmncom ⊢ F ∈ CMnd ∧ m ⋅ F 1 F ∈ Base F ∧ 1 F ∈ Base F → m ⋅ F 1 F + F 1 F = 1 F + F m ⋅ F 1 F
69 67 47 45 68 syl3anc ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → m ⋅ F 1 F + F 1 F = 1 F + F m ⋅ F 1 F
70 65 69 eqtrd ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → m + 1 ⋅ F 1 F = 1 F + F m ⋅ F 1 F
71 61 63 70 3brtr4d ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → m ⋅ F 1 F < F m + 1 ⋅ F 1 F
72 10 29 plttr ⊢ F ∈ Poset ∧ 0 F ∈ Base F ∧ m ⋅ F 1 F ∈ Base F ∧ m + 1 ⋅ F 1 F ∈ Base F → 0 F < F m ⋅ F 1 F ∧ m ⋅ F 1 F < F m + 1 ⋅ F 1 F → 0 F < F m + 1 ⋅ F 1 F
73 72 imp ⊢ F ∈ Poset ∧ 0 F ∈ Base F ∧ m ⋅ F 1 F ∈ Base F ∧ m + 1 ⋅ F 1 F ∈ Base F ∧ 0 F < F m ⋅ F 1 F ∧ m ⋅ F 1 F < F m + 1 ⋅ F 1 F → 0 F < F m + 1 ⋅ F 1 F
74 38 51 52 71 73 syl22anc ⊢ m ∈ ℕ ∧ F ∈ oField ∧ 0 F < F m ⋅ F 1 F → 0 F < F m + 1 ⋅ F 1 F
75 74 exp31 ⊢ m ∈ ℕ → F ∈ oField → 0 F < F m ⋅ F 1 F → 0 F < F m + 1 ⋅ F 1 F
76 75 a2d ⊢ m ∈ ℕ → F ∈ oField → 0 F < F m ⋅ F 1 F → F ∈ oField → 0 F < F m + 1 ⋅ F 1 F
77 19 22 25 28 34 76 nnind ⊢ y ∈ ℕ → F ∈ oField → 0 F < F y ⋅ F 1 F
78 77 impcom ⊢ F ∈ oField ∧ y ∈ ℕ → 0 F < F y ⋅ F 1 F
79 fvex ⊢ 0 F ∈ V
80 ovex ⊢ y ⋅ F 1 F ∈ V
81 29 pltne ⊢ F ∈ oField ∧ 0 F ∈ V ∧ y ⋅ F 1 F ∈ V → 0 F < F y ⋅ F 1 F → 0 F ≠ y ⋅ F 1 F
82 79 80 81 mp3an23 ⊢ F ∈ oField → 0 F < F y ⋅ F 1 F → 0 F ≠ y ⋅ F 1 F
83 82 adantr ⊢ F ∈ oField ∧ y ∈ ℕ → 0 F < F y ⋅ F 1 F → 0 F ≠ y ⋅ F 1 F
84 78 83 mpd ⊢ F ∈ oField ∧ y ∈ ℕ → 0 F ≠ y ⋅ F 1 F
85 84 necomd ⊢ F ∈ oField ∧ y ∈ ℕ → y ⋅ F 1 F ≠ 0 F
86 85 neneqd ⊢ F ∈ oField ∧ y ∈ ℕ → ¬ y ⋅ F 1 F = 0 F
87 86 ralrimiva ⊢ F ∈ oField → ∀ y ∈ ℕ ¬ y ⋅ F 1 F = 0 F
88 rabeq0 ⊢ y ∈ ℕ | y ⋅ F 1 F = 0 F = ∅ ↔ ∀ y ∈ ℕ ¬ y ⋅ F 1 F = 0 F
89 87 88 sylibr ⊢ F ∈ oField → y ∈ ℕ | y ⋅ F 1 F = 0 F = ∅
90 89 iftrued ⊢ F ∈ oField → if y ∈ ℕ | y ⋅ F 1 F = 0 F = ∅ 0 sup y ∈ ℕ | y ⋅ F 1 F = 0 F ℝ < = 0
91 16 90 eqtrd ⊢ F ∈ oField → od ⁡ F ⁡ 1 F = 0
92 4 91 eqtr3id ⊢ F ∈ oField → chr ⁡ F = 0