Step |
Hyp |
Ref |
Expression |
1 |
|
refld |
⊢ ℝfld ∈ Field |
2 |
|
isfld |
⊢ ( ℝfld ∈ Field ↔ ( ℝfld ∈ DivRing ∧ ℝfld ∈ CRing ) ) |
3 |
2
|
simplbi |
⊢ ( ℝfld ∈ Field → ℝfld ∈ DivRing ) |
4 |
|
drngring |
⊢ ( ℝfld ∈ DivRing → ℝfld ∈ Ring ) |
5 |
1 3 4
|
mp2b |
⊢ ℝfld ∈ Ring |
6 |
|
ringgrp |
⊢ ( ℝfld ∈ Ring → ℝfld ∈ Grp ) |
7 |
5 6
|
ax-mp |
⊢ ℝfld ∈ Grp |
8 |
|
grpmnd |
⊢ ( ℝfld ∈ Grp → ℝfld ∈ Mnd ) |
9 |
7 8
|
ax-mp |
⊢ ℝfld ∈ Mnd |
10 |
|
retos |
⊢ ℝfld ∈ Toset |
11 |
|
simpl |
⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) ) → 𝑎 ∈ ℝ ) |
12 |
|
simpr1 |
⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) ) → 𝑏 ∈ ℝ ) |
13 |
|
simpr2 |
⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) ) → 𝑐 ∈ ℝ ) |
14 |
|
simpr3 |
⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) ) → 𝑎 ≤ 𝑏 ) |
15 |
11 12 13 14
|
leadd1dd |
⊢ ( ( 𝑎 ∈ ℝ ∧ ( 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≤ 𝑏 ) ) → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) |
16 |
15
|
3anassrs |
⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑎 ≤ 𝑏 ) → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) |
17 |
16
|
ex |
⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ 𝑐 ∈ ℝ ) → ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) |
18 |
17
|
3impa |
⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) |
19 |
18
|
rgen3 |
⊢ ∀ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ℝ ∀ 𝑐 ∈ ℝ ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) |
20 |
|
rebase |
⊢ ℝ = ( Base ‘ ℝfld ) |
21 |
|
replusg |
⊢ + = ( +g ‘ ℝfld ) |
22 |
|
rele2 |
⊢ ≤ = ( le ‘ ℝfld ) |
23 |
20 21 22
|
isomnd |
⊢ ( ℝfld ∈ oMnd ↔ ( ℝfld ∈ Mnd ∧ ℝfld ∈ Toset ∧ ∀ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ℝ ∀ 𝑐 ∈ ℝ ( 𝑎 ≤ 𝑏 → ( 𝑎 + 𝑐 ) ≤ ( 𝑏 + 𝑐 ) ) ) ) |
24 |
9 10 19 23
|
mpbir3an |
⊢ ℝfld ∈ oMnd |
25 |
|
isogrp |
⊢ ( ℝfld ∈ oGrp ↔ ( ℝfld ∈ Grp ∧ ℝfld ∈ oMnd ) ) |
26 |
7 24 25
|
mpbir2an |
⊢ ℝfld ∈ oGrp |
27 |
|
mulge0 |
⊢ ( ( ( 𝑎 ∈ ℝ ∧ 0 ≤ 𝑎 ) ∧ ( 𝑏 ∈ ℝ ∧ 0 ≤ 𝑏 ) ) → 0 ≤ ( 𝑎 · 𝑏 ) ) |
28 |
27
|
an4s |
⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏 ) ) → 0 ≤ ( 𝑎 · 𝑏 ) ) |
29 |
28
|
ex |
⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏 ) → 0 ≤ ( 𝑎 · 𝑏 ) ) ) |
30 |
29
|
rgen2 |
⊢ ∀ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ℝ ( ( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏 ) → 0 ≤ ( 𝑎 · 𝑏 ) ) |
31 |
|
re0g |
⊢ 0 = ( 0g ‘ ℝfld ) |
32 |
|
remulr |
⊢ · = ( .r ‘ ℝfld ) |
33 |
20 31 32 22
|
isorng |
⊢ ( ℝfld ∈ oRing ↔ ( ℝfld ∈ Ring ∧ ℝfld ∈ oGrp ∧ ∀ 𝑎 ∈ ℝ ∀ 𝑏 ∈ ℝ ( ( 0 ≤ 𝑎 ∧ 0 ≤ 𝑏 ) → 0 ≤ ( 𝑎 · 𝑏 ) ) ) ) |
34 |
5 26 30 33
|
mpbir3an |
⊢ ℝfld ∈ oRing |
35 |
|
isofld |
⊢ ( ℝfld ∈ oField ↔ ( ℝfld ∈ Field ∧ ℝfld ∈ oRing ) ) |
36 |
1 34 35
|
mpbir2an |
⊢ ℝfld ∈ oField |