Proof of Theorem 0ringnnzr
Step | Hyp | Ref
| Expression |
1 | | 1re 9918 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
2 | 1 | ltnri 10025 |
. . . . . . 7
⊢ ¬ 1
< 1 |
3 | | breq2 4587 |
. . . . . . 7
⊢
((#‘(Base‘𝑅)) = 1 → (1 <
(#‘(Base‘𝑅))
↔ 1 < 1)) |
4 | 2, 3 | mtbiri 316 |
. . . . . 6
⊢
((#‘(Base‘𝑅)) = 1 → ¬ 1 <
(#‘(Base‘𝑅))) |
5 | 4 | adantl 481 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧
(#‘(Base‘𝑅)) =
1) → ¬ 1 < (#‘(Base‘𝑅))) |
6 | 5 | intnand 953 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧
(#‘(Base‘𝑅)) =
1) → ¬ (𝑅 ∈
Ring ∧ 1 < (#‘(Base‘𝑅)))) |
7 | 6 | ex 449 |
. . 3
⊢ (𝑅 ∈ Ring →
((#‘(Base‘𝑅)) =
1 → ¬ (𝑅 ∈
Ring ∧ 1 < (#‘(Base‘𝑅))))) |
8 | | ianor 508 |
. . . . 5
⊢ (¬
(𝑅 ∈ Ring ∧ 1 <
(#‘(Base‘𝑅)))
↔ (¬ 𝑅 ∈ Ring
∨ ¬ 1 < (#‘(Base‘𝑅)))) |
9 | | pm2.21 119 |
. . . . . 6
⊢ (¬
𝑅 ∈ Ring → (𝑅 ∈ Ring →
(#‘(Base‘𝑅)) =
1)) |
10 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Base‘𝑅)
∈ V |
11 | | hashxrcl 13010 |
. . . . . . . . . 10
⊢
((Base‘𝑅)
∈ V → (#‘(Base‘𝑅)) ∈
ℝ*) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
⊢
(#‘(Base‘𝑅)) ∈
ℝ* |
13 | 1 | rexri 9976 |
. . . . . . . . 9
⊢ 1 ∈
ℝ* |
14 | | xrlenlt 9982 |
. . . . . . . . 9
⊢
(((#‘(Base‘𝑅)) ∈ ℝ* ∧ 1 ∈
ℝ*) → ((#‘(Base‘𝑅)) ≤ 1 ↔ ¬ 1 <
(#‘(Base‘𝑅)))) |
15 | 12, 13, 14 | mp2an 704 |
. . . . . . . 8
⊢
((#‘(Base‘𝑅)) ≤ 1 ↔ ¬ 1 <
(#‘(Base‘𝑅))) |
16 | 15 | bicomi 213 |
. . . . . . 7
⊢ (¬ 1
< (#‘(Base‘𝑅)) ↔ (#‘(Base‘𝑅)) ≤ 1) |
17 | | ringgrp 18375 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
18 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
19 | 18 | grpbn0 17274 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Grp →
(Base‘𝑅) ≠
∅) |
20 | 17, 19 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) ≠
∅) |
21 | | simpr 476 |
. . . . . . . . . . 11
⊢
(((Base‘𝑅)
≠ ∅ ∧ (#‘(Base‘𝑅)) ≤ 1) → (#‘(Base‘𝑅)) ≤ 1) |
22 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((Base‘𝑅)
≠ ∅ ∧ (#‘(Base‘𝑅)) ≤ 1) → (Base‘𝑅) ∈ V) |
23 | | 1nn0 11185 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℕ0 |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((Base‘𝑅)
≠ ∅ ∧ (#‘(Base‘𝑅)) ≤ 1) → 1 ∈
ℕ0) |
25 | | hashbnd 12985 |
. . . . . . . . . . . . . 14
⊢
(((Base‘𝑅)
∈ V ∧ 1 ∈ ℕ0 ∧ (#‘(Base‘𝑅)) ≤ 1) →
(Base‘𝑅) ∈
Fin) |
26 | 22, 24, 21, 25 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢
(((Base‘𝑅)
≠ ∅ ∧ (#‘(Base‘𝑅)) ≤ 1) → (Base‘𝑅) ∈ Fin) |
27 | | hashcl 13009 |
. . . . . . . . . . . . . 14
⊢
((Base‘𝑅)
∈ Fin → (#‘(Base‘𝑅)) ∈
ℕ0) |
28 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢
(((Base‘𝑅)
≠ ∅ ∧ (#‘(Base‘𝑅)) ∈ ℕ0) →
(#‘(Base‘𝑅))
∈ ℕ0) |
29 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘(Base‘𝑅)) ∈ ℕ0 →
(Base‘𝑅) ∈
V) |
30 | | hasheq0 13015 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((Base‘𝑅)
∈ V → ((#‘(Base‘𝑅)) = 0 ↔ (Base‘𝑅) = ∅)) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘(Base‘𝑅)) ∈ ℕ0 →
((#‘(Base‘𝑅)) =
0 ↔ (Base‘𝑅) =
∅)) |
32 | 31 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘(Base‘𝑅)) ∈ ℕ0 →
((#‘(Base‘𝑅)) =
0 → (Base‘𝑅) =
∅)) |
33 | 32 | necon3d 2803 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘(Base‘𝑅)) ∈ ℕ0 →
((Base‘𝑅) ≠
∅ → (#‘(Base‘𝑅)) ≠ 0)) |
34 | 33 | impcom 445 |
. . . . . . . . . . . . . . . . . 18
⊢
(((Base‘𝑅)
≠ ∅ ∧ (#‘(Base‘𝑅)) ∈ ℕ0) →
(#‘(Base‘𝑅))
≠ 0) |
35 | | elnnne0 11183 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘(Base‘𝑅)) ∈ ℕ ↔
((#‘(Base‘𝑅))
∈ ℕ0 ∧ (#‘(Base‘𝑅)) ≠ 0)) |
36 | 28, 34, 35 | sylanbrc 695 |
. . . . . . . . . . . . . . . . 17
⊢
(((Base‘𝑅)
≠ ∅ ∧ (#‘(Base‘𝑅)) ∈ ℕ0) →
(#‘(Base‘𝑅))
∈ ℕ) |
37 | 36 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢
((Base‘𝑅) ≠
∅ → ((#‘(Base‘𝑅)) ∈ ℕ0 →
(#‘(Base‘𝑅))
∈ ℕ)) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((Base‘𝑅)
≠ ∅ ∧ (#‘(Base‘𝑅)) ≤ 1) →
((#‘(Base‘𝑅))
∈ ℕ0 → (#‘(Base‘𝑅)) ∈ ℕ)) |
39 | 38 | com12 32 |
. . . . . . . . . . . . . 14
⊢
((#‘(Base‘𝑅)) ∈ ℕ0 →
(((Base‘𝑅) ≠
∅ ∧ (#‘(Base‘𝑅)) ≤ 1) → (#‘(Base‘𝑅)) ∈
ℕ)) |
40 | 27, 39 | syl 17 |
. . . . . . . . . . . . 13
⊢
((Base‘𝑅)
∈ Fin → (((Base‘𝑅) ≠ ∅ ∧
(#‘(Base‘𝑅))
≤ 1) → (#‘(Base‘𝑅)) ∈ ℕ)) |
41 | 26, 40 | mpcom 37 |
. . . . . . . . . . . 12
⊢
(((Base‘𝑅)
≠ ∅ ∧ (#‘(Base‘𝑅)) ≤ 1) → (#‘(Base‘𝑅)) ∈
ℕ) |
42 | | nnle1eq1 10925 |
. . . . . . . . . . . 12
⊢
((#‘(Base‘𝑅)) ∈ ℕ →
((#‘(Base‘𝑅))
≤ 1 ↔ (#‘(Base‘𝑅)) = 1)) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . 11
⊢
(((Base‘𝑅)
≠ ∅ ∧ (#‘(Base‘𝑅)) ≤ 1) →
((#‘(Base‘𝑅))
≤ 1 ↔ (#‘(Base‘𝑅)) = 1)) |
44 | 21, 43 | mpbid 221 |
. . . . . . . . . 10
⊢
(((Base‘𝑅)
≠ ∅ ∧ (#‘(Base‘𝑅)) ≤ 1) → (#‘(Base‘𝑅)) = 1) |
45 | 44 | ex 449 |
. . . . . . . . 9
⊢
((Base‘𝑅) ≠
∅ → ((#‘(Base‘𝑅)) ≤ 1 → (#‘(Base‘𝑅)) = 1)) |
46 | 20, 45 | syl 17 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
((#‘(Base‘𝑅))
≤ 1 → (#‘(Base‘𝑅)) = 1)) |
47 | 46 | com12 32 |
. . . . . . 7
⊢
((#‘(Base‘𝑅)) ≤ 1 → (𝑅 ∈ Ring →
(#‘(Base‘𝑅)) =
1)) |
48 | 16, 47 | sylbi 206 |
. . . . . 6
⊢ (¬ 1
< (#‘(Base‘𝑅)) → (𝑅 ∈ Ring →
(#‘(Base‘𝑅)) =
1)) |
49 | 9, 48 | jaoi 393 |
. . . . 5
⊢ ((¬
𝑅 ∈ Ring ∨ ¬ 1
< (#‘(Base‘𝑅))) → (𝑅 ∈ Ring →
(#‘(Base‘𝑅)) =
1)) |
50 | 8, 49 | sylbi 206 |
. . . 4
⊢ (¬
(𝑅 ∈ Ring ∧ 1 <
(#‘(Base‘𝑅)))
→ (𝑅 ∈ Ring
→ (#‘(Base‘𝑅)) = 1)) |
51 | 50 | com12 32 |
. . 3
⊢ (𝑅 ∈ Ring → (¬
(𝑅 ∈ Ring ∧ 1 <
(#‘(Base‘𝑅)))
→ (#‘(Base‘𝑅)) = 1)) |
52 | 7, 51 | impbid 201 |
. 2
⊢ (𝑅 ∈ Ring →
((#‘(Base‘𝑅)) =
1 ↔ ¬ (𝑅 ∈
Ring ∧ 1 < (#‘(Base‘𝑅))))) |
53 | 18 | isnzr2hash 19085 |
. . . 4
⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 <
(#‘(Base‘𝑅)))) |
54 | 53 | bicomi 213 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 1 <
(#‘(Base‘𝑅)))
↔ 𝑅 ∈
NzRing) |
55 | 54 | notbii 309 |
. 2
⊢ (¬
(𝑅 ∈ Ring ∧ 1 <
(#‘(Base‘𝑅)))
↔ ¬ 𝑅 ∈
NzRing) |
56 | 52, 55 | syl6bb 275 |
1
⊢ (𝑅 ∈ Ring →
((#‘(Base‘𝑅)) =
1 ↔ ¬ 𝑅 ∈
NzRing)) |