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	9	ringgrpd	$⊢ F \in oField \to F \in Grp$
40	39	ad2antlr	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to F \in Grp$
41	10 13	grpidcl	$⊢ F \in Grp \to 0_{F} \in {Base}_{F}$
42	40 41	syl	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to 0_{F} \in {Base}_{F}$
43	40	grpmgmd	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to F \in Mgm$
44		simpll	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to m \in ℕ$
45	31	ad2antlr	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to 1_{F} \in {Base}_{F}$
46	10 12	mulgnncl	$⊢ (F \in Mgm \land m \in ℕ \land 1_{F} \in {Base}_{F}) \to m \cdot_{F} 1_{F} \in {Base}_{F}$
47	43 44 45 46	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}$
48	44	peano2nnd	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to m + 1 \in ℕ$
49	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}$
50	43 48 45 49	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}$
51	42 47 50	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})$
52		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})$
53		simplr	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to F \in oField$
54		isofld	$⊢ F \in oField \leftrightarrow (F \in Field \land F \in oRing)$
55	54	simprbi	$⊢ F \in oField \to F \in oRing$
56		orngogrp	$⊢ F \in oRing \to F \in oGrp$
57	53 55 56	3syl	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to F \in oGrp$
58	30	ad2antlr	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to 0_{F} <_{F} 1_{F}$
59		eqid	$⊢ +_{F} = +_{F}$
60	10 29 59	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}))$
61	57 42 45 47 58 60	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}))$
62	10 59 13 40 47	grplidd	$⊢ ((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}$
63	62	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})$
64	10 12 59	mulgnnp1	$⊢ (m \in ℕ \land 1_{F} \in {Base}_{F}) \to (m + 1) \cdot_{F} 1_{F} = (m \cdot_{F} 1_{F}) +_{F} 1_{F}$
65	44 45 64	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}$
66		ringcmn	$⊢ F \in Ring \to F \in CMnd$
67	53 9 66	3syl	$⊢ ((m \in ℕ \land F \in oField) \land 0_{F} <_{F} (m \cdot_{F} 1_{F})) \to F \in CMnd$
68	10 59	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})$
69	67 47 45 68	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})$
70	65 69	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})$
71	61 63 70	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})$
72	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}))$
73	72	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})$
74	38 51 52 71 73	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})$
75	74	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})))$
76	75	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})))$
77	19 22 25 28 34 76	nnind	$⊢ y \in ℕ \to (F \in oField \to 0_{F} <_{F} (y \cdot_{F} 1_{F}))$
78	77	impcom	$⊢ (F \in oField \land y \in ℕ) \to 0_{F} <_{F} (y \cdot_{F} 1_{F})$
79		fvex	$⊢ 0_{F} \in V$
80		ovex	$⊢ y \cdot_{F} 1_{F} \in V$
81	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})$
82	79 80 81	mp3an23	$⊢ F \in oField \to (0_{F} <_{F} (y \cdot_{F} 1_{F}) \to 0_{F} \neq y \cdot_{F} 1_{F})$
83	82	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})$
84	78 83	mpd	$⊢ (F \in oField \land y \in ℕ) \to 0_{F} \neq y \cdot_{F} 1_{F}$
85	84	necomd	$⊢ (F \in oField \land y \in ℕ) \to y \cdot_{F} 1_{F} \neq 0_{F}$
86	85	neneqd	$⊢ (F \in oField \land y \in ℕ) \to \neg y \cdot_{F} 1_{F} = 0_{F}$
87	86	ralrimiva	$⊢ F \in oField \to \forall y \in ℕ \neg y \cdot_{F} 1_{F} = 0_{F}$
88		rabeq0	$⊢ \{y \in ℕ \| y \cdot_{F} 1_{F} = 0_{F}\} = \emptyset \leftrightarrow \forall y \in ℕ \neg y \cdot_{F} 1_{F} = 0_{F}$
89	87 88	sylibr	$⊢ F \in oField \to \{y \in ℕ \| y \cdot_{F} 1_{F} = 0_{F}\} = \emptyset$
90	89	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$
91	16 90	eqtrd	$⊢ F \in oField \to od (F) (1_{F}) = 0$
92	4 91	eqtr3id	$⊢ F \in oField \to chr (F) = 0$

Metamath Proof Explorer

Theorem ofldchr

Proof