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 \in oField \to 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 \in oField \to F \in Field$
6		isfld	$⊢ F \in Field \leftrightarrow (F \in DivRing \land F \in CRing)$
7	6	simplbi	$⊢ F \in Field \to F \in DivRing$
8		drngring	$⊢ F \in DivRing \to F \in Ring$
9	5 7 8	3syl	$⊢ F \in oField \to F \in Ring$
10		eqid	$⊢ {Base}_{F} = {Base}_{F}$
11	10 2	ringidcl	$⊢ F \in Ring \to 1_{F} \in {Base}_{F}$
12		eqid	$⊢ \cdot_{F} = \cdot_{F}$
13		eqid	$⊢ 0_{F} = 0_{F}$
14		eqid	$⊢ \{y \in ℕ \| y \cdot_{F} 1_{F} = 0_{F}\} = \{y \in ℕ \| y \cdot_{F} 1_{F} = 0_{F}\}$
15	10 12 13 1 14	odval	$⊢ 1_{F} \in {Base}_{F} \to od (F) (1_{F}) = if (\{y \in ℕ \| y \cdot_{F} 1_{F} = 0_{F}\} = \emptyset, 0, sup (\{y \in ℕ \| y \cdot_{F} 1_{F} = 0_{F}\} ℝ <))$
16	9 11 15	3syl	$⊢ F \in oField \to od (F) (1_{F}) = if (\{y \in ℕ \| y \cdot_{F} 1_{F} = 0_{F}\} = \emptyset, 0, sup (\{y \in ℕ \| y \cdot_{F} 1_{F} = 0_{F}\} ℝ <))$
17		oveq1	$⊢ n = 1 \to n \cdot_{F} 1_{F} = 1 \cdot_{F} 1_{F}$
18	17	breq2d	$⊢ n = 1 \to (0_{F} <_{F} (n \cdot_{F} 1_{F}) \leftrightarrow 0_{F} <_{F} (1 \cdot_{F} 1_{F}))$
19	18	imbi2d	$⊢ n = 1 \to ((F \in oField \to 0_{F} <_{F} (n \cdot_{F} 1_{F})) \leftrightarrow (F \in oField \to 0_{F} <_{F} (1 \cdot_{F} 1_{F})))$
20		oveq1	$⊢ n = m \to n \cdot_{F} 1_{F} = m \cdot_{F} 1_{F}$
21	20	breq2d	$⊢ n = m \to (0_{F} <_{F} (n \cdot_{F} 1_{F}) \leftrightarrow 0_{F} <_{F} (m \cdot_{F} 1_{F}))$
22	21	imbi2d	$⊢ n = m \to ((F \in oField \to 0_{F} <_{F} (n \cdot_{F} 1_{F})) \leftrightarrow (F \in oField \to 0_{F} <_{F} (m \cdot_{F} 1_{F})))$
23		oveq1	$⊢ n = m + 1 \to n \cdot_{F} 1_{F} = (m + 1) \cdot_{F} 1_{F}$
24	23	breq2d	$⊢ n = m + 1 \to (0_{F} <_{F} (n \cdot_{F} 1_{F}) \leftrightarrow 0_{F} <_{F} ((m + 1) \cdot_{F} 1_{F}))$
25	24	imbi2d	$⊢ n = m + 1 \to ((F \in oField \to 0_{F} <_{F} (n \cdot_{F} 1_{F})) \leftrightarrow (F \in oField \to 0_{F} <_{F} ((m + 1) \cdot_{F} 1_{F})))$
26		oveq1	$⊢ n = y \to n \cdot_{F} 1_{F} = y \cdot_{F} 1_{F}$
27	26	breq2d	$⊢ n = y \to (0_{F} <_{F} (n \cdot_{F} 1_{F}) \leftrightarrow 0_{F} <_{F} (y \cdot_{F} 1_{F}))$
28	27	imbi2d	$⊢ n = y \to ((F \in oField \to 0_{F} <_{F} (n \cdot_{F} 1_{F})) \leftrightarrow (F \in oField \to 0_{F} <_{F} (y \cdot_{F} 1_{F})))$
29		eqid	$⊢ <_{F} = <_{F}$
30	13 2 29	ofldlt1	$⊢ F \in oField \to 0_{F} <_{F} 1_{F}$
31	9 11	syl	$⊢ F \in oField \to 1_{F} \in {Base}_{F}$
32	10 12	mulg1	$⊢ 1_{F} \in {Base}_{F} \to 1 \cdot_{F} 1_{F} = 1_{F}$
33	31 32	syl	$⊢ F \in oField \to 1 \cdot_{F} 1_{F} = 1_{F}$
34	30 33	breqtrrd	$⊢ F \in oField \to 0_{F} <_{F} (1 \cdot_{F} 1_{F})$
35		ofldtos	$⊢ F \in oField \to F \in Toset$
36		tospos	$⊢ F \in Toset \to F \in Poset$
37	35 36	syl	$⊢ F \in oField \to F \in Poset$
38	37	ad2antlr	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to F \in Poset$
39		ringgrp	$⊢ F \in Ring \to F \in Grp$
40	9 39	syl	$⊢ F \in oField \to F \in Grp$
41	40	ad2antlr	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to F \in Grp$
42	10 13	grpidcl	$⊢ F \in Grp \to 0_{F} \in {Base}_{F}$
43	41 42	syl	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to 0_{F} \in {Base}_{F}$
44		grpmnd	$⊢ F \in Grp \to F \in Mnd$
45		mndmgm	$⊢ F \in Mnd \to F \in Mgm$
46	44 45	syl	$⊢ F \in Grp \to F \in Mgm$
47	41 46	syl	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to F \in Mgm$
48		simpll	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to m \in ℕ$
49	31	ad2antlr	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to 1_{F} \in {Base}_{F}$
50	10 12	mulgnncl	$⊢ (F \in Mgm \land m \in ℕ \land 1_{F} \in {Base}_{F}) \to m \cdot_{F} 1_{F} \in {Base}_{F}$
51	47 48 49 50	syl3anc	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to m \cdot_{F} 1_{F} \in {Base}_{F}$
52	48	peano2nnd	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to m + 1 \in ℕ$
53	10 12	mulgnncl	$⊢ (F \in Mgm \land m + 1 \in ℕ \land 1_{F} \in {Base}_{F}) \to (m + 1) \cdot_{F} 1_{F} \in {Base}_{F}$
54	47 52 49 53	syl3anc	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to (m + 1) \cdot_{F} 1_{F} \in {Base}_{F}$
55	43 51 54	3jca	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to (0_{F} \in {Base}_{F} \land m \cdot_{F} 1_{F} \in {Base}_{F} \land (m + 1) \cdot_{F} 1_{F} \in {Base}_{F})$
56		simpr	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to 0_{F} <_{F} (m \cdot_{F} 1_{F})$
57		simplr	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to F \in oField$
58		isofld	$⊢ F \in oField \leftrightarrow (F \in Field \land F \in oRing)$
59	58	simprbi	$⊢ F \in oField \to F \in oRing$
60		orngogrp	$⊢ F \in oRing \to F \in oGrp$
61	57 59 60	3syl	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to F \in oGrp$
62	30	ad2antlr	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to 0_{F} <_{F} 1_{F}$
63		eqid	$⊢ +_{F} = +_{F}$
64	10 29 63	ogrpaddlt	$⊢ (F \in oGrp \land (0_{F} \in {Base}_{F} \land 1_{F} \in {Base}_{F} \land m \cdot_{F} 1_{F} \in {Base}_{F}) \land 0_{F} <_{F} 1_{F}) \to (0_{F} +_{F} (m \cdot_{F} 1_{F})) <_{F} (1_{F} +_{F} (m \cdot_{F} 1_{F}))$
65	61 43 49 51 62 64	syl131anc	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to (0_{F} +_{F} (m \cdot_{F} 1_{F})) <_{F} (1_{F} +_{F} (m \cdot_{F} 1_{F}))$
66	10 63 13	grplid	$⊢ (F \in Grp \land m \cdot_{F} 1_{F} \in {Base}_{F}) \to 0_{F} +_{F} (m \cdot_{F} 1_{F}) = m \cdot_{F} 1_{F}$
67	41 51 66	syl2anc	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to 0_{F} +_{F} (m \cdot_{F} 1_{F}) = m \cdot_{F} 1_{F}$
68	67	eqcomd	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to m \cdot_{F} 1_{F} = 0_{F} +_{F} (m \cdot_{F} 1_{F})$
69	10 12 63	mulgnnp1	$⊢ (m \in ℕ \land 1_{F} \in {Base}_{F}) \to (m + 1) \cdot_{F} 1_{F} = (m \cdot_{F} 1_{F}) +_{F} 1_{F}$
70	48 49 69	syl2anc	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to (m + 1) \cdot_{F} 1_{F} = (m \cdot_{F} 1_{F}) +_{F} 1_{F}$
71		ringcmn	$⊢ F \in Ring \to F \in CMnd$
72	57 9 71	3syl	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to F \in CMnd$
73	10 63	cmncom	$⊢ (F \in CMnd \land m \cdot_{F} 1_{F} \in {Base}_{F} \land 1_{F} \in {Base}_{F}) \to (m \cdot_{F} 1_{F}) +_{F} 1_{F} = 1_{F} +_{F} (m \cdot_{F} 1_{F})$
74	72 51 49 73	syl3anc	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to (m \cdot_{F} 1_{F}) +_{F} 1_{F} = 1_{F} +_{F} (m \cdot_{F} 1_{F})$
75	70 74	eqtrd	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to (m + 1) \cdot_{F} 1_{F} = 1_{F} +_{F} (m \cdot_{F} 1_{F})$
76	65 68 75	3brtr4d	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to (m \cdot_{F} 1_{F}) <_{F} ((m + 1) \cdot_{F} 1_{F})$
77	10 29	plttr	$⊢ (F \in Poset \land (0_{F} \in {Base}_{F} \land m \cdot_{F} 1_{F} \in {Base}_{F} \land (m + 1) \cdot_{F} 1_{F} \in {Base}_{F})) \to ((0_{F} <_{F} (m \cdot_{F} 1_{F}) \land (m \cdot_{F} 1_{F}) <_{F} ((m + 1) \cdot_{F} 1_{F})) \to 0_{F} <_{F} ((m + 1) \cdot_{F} 1_{F}))$
78	77	imp	$⊢ ((F \in Poset \land (0_{F} \in {Base}_{F} \land m \cdot_{F} 1_{F} \in {Base}_{F} \land (m + 1) \cdot_{F} 1_{F} \in {Base}_{F})) \land (0_{F} <_{F} (m \cdot_{F} 1_{F}) \land (m \cdot_{F} 1_{F}) <_{F} ((m + 1) \cdot_{F} 1_{F}))) \to 0_{F} <_{F} ((m + 1) \cdot_{F} 1_{F})$
79	38 55 56 76 78	syl22anc	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to 0_{F} <_{F} ((m + 1) \cdot_{F} 1_{F})$
80	79	exp31	$⊢ m \in ℕ \to (F \in oField \to (0_{F} <_{F} (m \cdot_{F} 1_{F}) \to 0_{F} <_{F} ((m + 1) \cdot_{F} 1_{F})))$
81	80	a2d	$⊢ m \in ℕ \to ((F \in oField \to 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to (F \in oField \to 0_{F} <_{F} ((m + 1) \cdot_{F} 1_{F})))$
82	19 22 25 28 34 81	nnind	$⊢ y \in ℕ \to (F \in oField \to 0_{F} <_{F} (y \cdot_{F} 1_{F}))$
83	82	impcom	$⊢ (F \in oField \land y \in ℕ) \to 0_{F} <_{F} (y \cdot_{F} 1_{F})$
84		fvex	$⊢ 0_{F} \in V$
85		ovex	$⊢ y \cdot_{F} 1_{F} \in V$
86	29	pltne	$⊢ (F \in oField \land 0_{F} \in V \land y \cdot_{F} 1_{F} \in V) \to (0_{F} <_{F} (y \cdot_{F} 1_{F}) \to 0_{F} \neq y \cdot_{F} 1_{F})$
87	84 85 86	mp3an23	$⊢ F \in oField \to (0_{F} <_{F} (y \cdot_{F} 1_{F}) \to 0_{F} \neq y \cdot_{F} 1_{F})$
88	87	adantr	$⊢ (F \in oField \land y \in ℕ) \to (0_{F} <_{F} (y \cdot_{F} 1_{F}) \to 0_{F} \neq y \cdot_{F} 1_{F})$
89	83 88	mpd	$⊢ (F \in oField \land y \in ℕ) \to 0_{F} \neq y \cdot_{F} 1_{F}$
90	89	necomd	$⊢ (F \in oField \land y \in ℕ) \to y \cdot_{F} 1_{F} \neq 0_{F}$
91	90	neneqd	$⊢ (F \in oField \land y \in ℕ) \to \neg y \cdot_{F} 1_{F} = 0_{F}$
92	91	ralrimiva	$⊢ F \in oField \to \forall y \in ℕ \neg y \cdot_{F} 1_{F} = 0_{F}$
93		rabeq0	$⊢ \{y \in ℕ \| y \cdot_{F} 1_{F} = 0_{F}\} = \emptyset \leftrightarrow \forall y \in ℕ \neg y \cdot_{F} 1_{F} = 0_{F}$
94	92 93	sylibr	$⊢ F \in oField \to \{y \in ℕ \| y \cdot_{F} 1_{F} = 0_{F}\} = \emptyset$
95	94	iftrued	$⊢ F \in oField \to if (\{y \in ℕ \| y \cdot_{F} 1_{F} = 0_{F}\} = \emptyset, 0, sup (\{y \in ℕ \| y \cdot_{F} 1_{F} = 0_{F}\} ℝ <)) = 0$
96	16 95	eqtrd	$⊢ F \in oField \to od (F) (1_{F}) = 0$
97	4 96	eqtr3id	$⊢ F \in oField \to chr (F) = 0$

Metamath Proof Explorer

Theorem ofldchr

Proof