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 )