Proof of Theorem 0ringnnzr
Step | Hyp | Ref
| Expression |
1 | | 1re 10959 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
2 | 1 | ltnri 11067 |
. . . . . . 7
⊢ ¬ 1
< 1 |
3 | | breq2 5082 |
. . . . . . 7
⊢
((♯‘(Base‘𝑅)) = 1 → (1 <
(♯‘(Base‘𝑅)) ↔ 1 < 1)) |
4 | 2, 3 | mtbiri 326 |
. . . . . 6
⊢
((♯‘(Base‘𝑅)) = 1 → ¬ 1 <
(♯‘(Base‘𝑅))) |
5 | 4 | adantl 481 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧
(♯‘(Base‘𝑅)) = 1) → ¬ 1 <
(♯‘(Base‘𝑅))) |
6 | 5 | intnand 488 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧
(♯‘(Base‘𝑅)) = 1) → ¬ (𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅)))) |
7 | 6 | ex 412 |
. . 3
⊢ (𝑅 ∈ Ring →
((♯‘(Base‘𝑅)) = 1 → ¬ (𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))))) |
8 | | ianor 978 |
. . . . 5
⊢ (¬
(𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))) ↔ (¬ 𝑅 ∈ Ring ∨ ¬ 1 <
(♯‘(Base‘𝑅)))) |
9 | | pm2.21 123 |
. . . . . 6
⊢ (¬
𝑅 ∈ Ring → (𝑅 ∈ Ring →
(♯‘(Base‘𝑅)) = 1)) |
10 | | fvex 6781 |
. . . . . . . . . 10
⊢
(Base‘𝑅)
∈ V |
11 | | hashxrcl 14053 |
. . . . . . . . . 10
⊢
((Base‘𝑅)
∈ V → (♯‘(Base‘𝑅)) ∈
ℝ*) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
⊢
(♯‘(Base‘𝑅)) ∈
ℝ* |
13 | | 1xr 11018 |
. . . . . . . . 9
⊢ 1 ∈
ℝ* |
14 | | xrlenlt 11024 |
. . . . . . . . 9
⊢
(((♯‘(Base‘𝑅)) ∈ ℝ* ∧ 1 ∈
ℝ*) → ((♯‘(Base‘𝑅)) ≤ 1 ↔ ¬ 1 <
(♯‘(Base‘𝑅)))) |
15 | 12, 13, 14 | mp2an 688 |
. . . . . . . 8
⊢
((♯‘(Base‘𝑅)) ≤ 1 ↔ ¬ 1 <
(♯‘(Base‘𝑅))) |
16 | 15 | bicomi 223 |
. . . . . . 7
⊢ (¬ 1
< (♯‘(Base‘𝑅)) ↔ (♯‘(Base‘𝑅)) ≤ 1) |
17 | | simpr 484 |
. . . . . . . . . 10
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) →
(♯‘(Base‘𝑅)) ≤ 1) |
18 | | 1nn0 12232 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ0 |
19 | | hashbnd 14031 |
. . . . . . . . . . . . 13
⊢
(((Base‘𝑅)
∈ V ∧ 1 ∈ ℕ0 ∧
(♯‘(Base‘𝑅)) ≤ 1) → (Base‘𝑅) ∈ Fin) |
20 | 10, 18, 17, 19 | mp3an12i 1463 |
. . . . . . . . . . . 12
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) → (Base‘𝑅) ∈ Fin) |
21 | | hashcl 14052 |
. . . . . . . . . . . . 13
⊢
((Base‘𝑅)
∈ Fin → (♯‘(Base‘𝑅)) ∈
ℕ0) |
22 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ∈ ℕ0) →
(♯‘(Base‘𝑅)) ∈
ℕ0) |
23 | | hasheq0 14059 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((Base‘𝑅)
∈ V → ((♯‘(Base‘𝑅)) = 0 ↔ (Base‘𝑅) = ∅)) |
24 | 10, 23 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘(Base‘𝑅)) ∈ ℕ0 →
((♯‘(Base‘𝑅)) = 0 ↔ (Base‘𝑅) = ∅)) |
25 | 24 | biimpd 228 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘(Base‘𝑅)) ∈ ℕ0 →
((♯‘(Base‘𝑅)) = 0 → (Base‘𝑅) = ∅)) |
26 | 25 | necon3d 2965 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘(Base‘𝑅)) ∈ ℕ0 →
((Base‘𝑅) ≠
∅ → (♯‘(Base‘𝑅)) ≠ 0)) |
27 | 26 | impcom 407 |
. . . . . . . . . . . . . . . 16
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ∈ ℕ0) →
(♯‘(Base‘𝑅)) ≠ 0) |
28 | | elnnne0 12230 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘(Base‘𝑅)) ∈ ℕ ↔
((♯‘(Base‘𝑅)) ∈ ℕ0 ∧
(♯‘(Base‘𝑅)) ≠ 0)) |
29 | 22, 27, 28 | sylanbrc 582 |
. . . . . . . . . . . . . . 15
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ∈ ℕ0) →
(♯‘(Base‘𝑅)) ∈ ℕ) |
30 | 29 | ex 412 |
. . . . . . . . . . . . . 14
⊢
((Base‘𝑅) ≠
∅ → ((♯‘(Base‘𝑅)) ∈ ℕ0 →
(♯‘(Base‘𝑅)) ∈ ℕ)) |
31 | 30 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) →
((♯‘(Base‘𝑅)) ∈ ℕ0 →
(♯‘(Base‘𝑅)) ∈ ℕ)) |
32 | 21, 31 | syl5com 31 |
. . . . . . . . . . . 12
⊢
((Base‘𝑅)
∈ Fin → (((Base‘𝑅) ≠ ∅ ∧
(♯‘(Base‘𝑅)) ≤ 1) →
(♯‘(Base‘𝑅)) ∈ ℕ)) |
33 | 20, 32 | mpcom 38 |
. . . . . . . . . . 11
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) →
(♯‘(Base‘𝑅)) ∈ ℕ) |
34 | | nnle1eq1 11986 |
. . . . . . . . . . 11
⊢
((♯‘(Base‘𝑅)) ∈ ℕ →
((♯‘(Base‘𝑅)) ≤ 1 ↔
(♯‘(Base‘𝑅)) = 1)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . 10
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) →
((♯‘(Base‘𝑅)) ≤ 1 ↔
(♯‘(Base‘𝑅)) = 1)) |
36 | 17, 35 | mpbid 231 |
. . . . . . . . 9
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) →
(♯‘(Base‘𝑅)) = 1) |
37 | 36 | ex 412 |
. . . . . . . 8
⊢
((Base‘𝑅) ≠
∅ → ((♯‘(Base‘𝑅)) ≤ 1 →
(♯‘(Base‘𝑅)) = 1)) |
38 | | ringgrp 19769 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
39 | | eqid 2739 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
40 | 39 | grpbn0 18589 |
. . . . . . . . 9
⊢ (𝑅 ∈ Grp →
(Base‘𝑅) ≠
∅) |
41 | 38, 40 | syl 17 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) ≠
∅) |
42 | 37, 41 | syl11 33 |
. . . . . . 7
⊢
((♯‘(Base‘𝑅)) ≤ 1 → (𝑅 ∈ Ring →
(♯‘(Base‘𝑅)) = 1)) |
43 | 16, 42 | sylbi 216 |
. . . . . 6
⊢ (¬ 1
< (♯‘(Base‘𝑅)) → (𝑅 ∈ Ring →
(♯‘(Base‘𝑅)) = 1)) |
44 | 9, 43 | jaoi 853 |
. . . . 5
⊢ ((¬
𝑅 ∈ Ring ∨ ¬ 1
< (♯‘(Base‘𝑅))) → (𝑅 ∈ Ring →
(♯‘(Base‘𝑅)) = 1)) |
45 | 8, 44 | sylbi 216 |
. . . 4
⊢ (¬
(𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))) → (𝑅 ∈ Ring →
(♯‘(Base‘𝑅)) = 1)) |
46 | 45 | com12 32 |
. . 3
⊢ (𝑅 ∈ Ring → (¬
(𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))) → (♯‘(Base‘𝑅)) = 1)) |
47 | 7, 46 | impbid 211 |
. 2
⊢ (𝑅 ∈ Ring →
((♯‘(Base‘𝑅)) = 1 ↔ ¬ (𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))))) |
48 | 39 | isnzr2hash 20516 |
. . . 4
⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅)))) |
49 | 48 | bicomi 223 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))) ↔ 𝑅 ∈ NzRing) |
50 | 49 | notbii 319 |
. 2
⊢ (¬
(𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))) ↔ ¬ 𝑅 ∈ NzRing) |
51 | 47, 50 | bitrdi 286 |
1
⊢ (𝑅 ∈ Ring →
((♯‘(Base‘𝑅)) = 1 ↔ ¬ 𝑅 ∈ NzRing)) |