This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐹 ∈ oField → ( chr ‘ 𝐹 ) = 0 )

Proof

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