Proof of Theorem 0ringnnzr
Step | Hyp | Ref
| Expression |
1 | | 1re 10231 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
2 | 1 | ltnri 10338 |
. . . . . . 7
⊢ ¬ 1
< 1 |
3 | | breq2 4808 |
. . . . . . 7
⊢
((♯‘(Base‘𝑅)) = 1 → (1 <
(♯‘(Base‘𝑅)) ↔ 1 < 1)) |
4 | 2, 3 | mtbiri 316 |
. . . . . 6
⊢
((♯‘(Base‘𝑅)) = 1 → ¬ 1 <
(♯‘(Base‘𝑅))) |
5 | 4 | adantl 473 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧
(♯‘(Base‘𝑅)) = 1) → ¬ 1 <
(♯‘(Base‘𝑅))) |
6 | 5 | intnand 1000 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧
(♯‘(Base‘𝑅)) = 1) → ¬ (𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅)))) |
7 | 6 | ex 449 |
. . 3
⊢ (𝑅 ∈ Ring →
((♯‘(Base‘𝑅)) = 1 → ¬ (𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))))) |
8 | | ianor 510 |
. . . . 5
⊢ (¬
(𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))) ↔ (¬ 𝑅 ∈ Ring ∨ ¬ 1 <
(♯‘(Base‘𝑅)))) |
9 | | pm2.21 120 |
. . . . . 6
⊢ (¬
𝑅 ∈ Ring → (𝑅 ∈ Ring →
(♯‘(Base‘𝑅)) = 1)) |
10 | | fvex 6362 |
. . . . . . . . . 10
⊢
(Base‘𝑅)
∈ V |
11 | | hashxrcl 13340 |
. . . . . . . . . 10
⊢
((Base‘𝑅)
∈ V → (♯‘(Base‘𝑅)) ∈
ℝ*) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
⊢
(♯‘(Base‘𝑅)) ∈
ℝ* |
13 | 1 | rexri 10289 |
. . . . . . . . 9
⊢ 1 ∈
ℝ* |
14 | | xrlenlt 10295 |
. . . . . . . . 9
⊢
(((♯‘(Base‘𝑅)) ∈ ℝ* ∧ 1 ∈
ℝ*) → ((♯‘(Base‘𝑅)) ≤ 1 ↔ ¬ 1 <
(♯‘(Base‘𝑅)))) |
15 | 12, 13, 14 | mp2an 710 |
. . . . . . . 8
⊢
((♯‘(Base‘𝑅)) ≤ 1 ↔ ¬ 1 <
(♯‘(Base‘𝑅))) |
16 | 15 | bicomi 214 |
. . . . . . 7
⊢ (¬ 1
< (♯‘(Base‘𝑅)) ↔ (♯‘(Base‘𝑅)) ≤ 1) |
17 | | simpr 479 |
. . . . . . . . . 10
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) →
(♯‘(Base‘𝑅)) ≤ 1) |
18 | 10 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) → (Base‘𝑅) ∈ V) |
19 | | 1nn0 11500 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ0 |
20 | 19 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) → 1 ∈
ℕ0) |
21 | | hashbnd 13317 |
. . . . . . . . . . . . 13
⊢
(((Base‘𝑅)
∈ V ∧ 1 ∈ ℕ0 ∧
(♯‘(Base‘𝑅)) ≤ 1) → (Base‘𝑅) ∈ Fin) |
22 | 18, 20, 17, 21 | syl3anc 1477 |
. . . . . . . . . . . 12
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) → (Base‘𝑅) ∈ Fin) |
23 | | hashcl 13339 |
. . . . . . . . . . . . 13
⊢
((Base‘𝑅)
∈ Fin → (♯‘(Base‘𝑅)) ∈
ℕ0) |
24 | | simpr 479 |
. . . . . . . . . . . . . . . . 17
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ∈ ℕ0) →
(♯‘(Base‘𝑅)) ∈
ℕ0) |
25 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘(Base‘𝑅)) ∈ ℕ0 →
(Base‘𝑅) ∈
V) |
26 | | hasheq0 13346 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((Base‘𝑅)
∈ V → ((♯‘(Base‘𝑅)) = 0 ↔ (Base‘𝑅) = ∅)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘(Base‘𝑅)) ∈ ℕ0 →
((♯‘(Base‘𝑅)) = 0 ↔ (Base‘𝑅) = ∅)) |
28 | 27 | biimpd 219 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘(Base‘𝑅)) ∈ ℕ0 →
((♯‘(Base‘𝑅)) = 0 → (Base‘𝑅) = ∅)) |
29 | 28 | necon3d 2953 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘(Base‘𝑅)) ∈ ℕ0 →
((Base‘𝑅) ≠
∅ → (♯‘(Base‘𝑅)) ≠ 0)) |
30 | 29 | impcom 445 |
. . . . . . . . . . . . . . . . 17
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ∈ ℕ0) →
(♯‘(Base‘𝑅)) ≠ 0) |
31 | | elnnne0 11498 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘(Base‘𝑅)) ∈ ℕ ↔
((♯‘(Base‘𝑅)) ∈ ℕ0 ∧
(♯‘(Base‘𝑅)) ≠ 0)) |
32 | 24, 30, 31 | sylanbrc 701 |
. . . . . . . . . . . . . . . 16
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ∈ ℕ0) →
(♯‘(Base‘𝑅)) ∈ ℕ) |
33 | 32 | ex 449 |
. . . . . . . . . . . . . . 15
⊢
((Base‘𝑅) ≠
∅ → ((♯‘(Base‘𝑅)) ∈ ℕ0 →
(♯‘(Base‘𝑅)) ∈ ℕ)) |
34 | 33 | adantr 472 |
. . . . . . . . . . . . . 14
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) →
((♯‘(Base‘𝑅)) ∈ ℕ0 →
(♯‘(Base‘𝑅)) ∈ ℕ)) |
35 | 34 | com12 32 |
. . . . . . . . . . . . 13
⊢
((♯‘(Base‘𝑅)) ∈ ℕ0 →
(((Base‘𝑅) ≠
∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) →
(♯‘(Base‘𝑅)) ∈ ℕ)) |
36 | 23, 35 | syl 17 |
. . . . . . . . . . . 12
⊢
((Base‘𝑅)
∈ Fin → (((Base‘𝑅) ≠ ∅ ∧
(♯‘(Base‘𝑅)) ≤ 1) →
(♯‘(Base‘𝑅)) ∈ ℕ)) |
37 | 22, 36 | mpcom 38 |
. . . . . . . . . . 11
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) →
(♯‘(Base‘𝑅)) ∈ ℕ) |
38 | | nnle1eq1 11240 |
. . . . . . . . . . 11
⊢
((♯‘(Base‘𝑅)) ∈ ℕ →
((♯‘(Base‘𝑅)) ≤ 1 ↔
(♯‘(Base‘𝑅)) = 1)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) →
((♯‘(Base‘𝑅)) ≤ 1 ↔
(♯‘(Base‘𝑅)) = 1)) |
40 | 17, 39 | mpbid 222 |
. . . . . . . . 9
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) →
(♯‘(Base‘𝑅)) = 1) |
41 | 40 | ex 449 |
. . . . . . . 8
⊢
((Base‘𝑅) ≠
∅ → ((♯‘(Base‘𝑅)) ≤ 1 →
(♯‘(Base‘𝑅)) = 1)) |
42 | | ringgrp 18752 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
43 | | eqid 2760 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
44 | 43 | grpbn0 17652 |
. . . . . . . . 9
⊢ (𝑅 ∈ Grp →
(Base‘𝑅) ≠
∅) |
45 | 42, 44 | syl 17 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) ≠
∅) |
46 | 41, 45 | syl11 33 |
. . . . . . 7
⊢
((♯‘(Base‘𝑅)) ≤ 1 → (𝑅 ∈ Ring →
(♯‘(Base‘𝑅)) = 1)) |
47 | 16, 46 | sylbi 207 |
. . . . . 6
⊢ (¬ 1
< (♯‘(Base‘𝑅)) → (𝑅 ∈ Ring →
(♯‘(Base‘𝑅)) = 1)) |
48 | 9, 47 | jaoi 393 |
. . . . 5
⊢ ((¬
𝑅 ∈ Ring ∨ ¬ 1
< (♯‘(Base‘𝑅))) → (𝑅 ∈ Ring →
(♯‘(Base‘𝑅)) = 1)) |
49 | 8, 48 | sylbi 207 |
. . . 4
⊢ (¬
(𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))) → (𝑅 ∈ Ring →
(♯‘(Base‘𝑅)) = 1)) |
50 | 49 | com12 32 |
. . 3
⊢ (𝑅 ∈ Ring → (¬
(𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))) → (♯‘(Base‘𝑅)) = 1)) |
51 | 7, 50 | impbid 202 |
. 2
⊢ (𝑅 ∈ Ring →
((♯‘(Base‘𝑅)) = 1 ↔ ¬ (𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))))) |
52 | 43 | isnzr2hash 19466 |
. . . 4
⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅)))) |
53 | 52 | bicomi 214 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))) ↔ 𝑅 ∈ NzRing) |
54 | 53 | notbii 309 |
. 2
⊢ (¬
(𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))) ↔ ¬ 𝑅 ∈ NzRing) |
55 | 51, 54 | syl6bb 276 |
1
⊢ (𝑅 ∈ Ring →
((♯‘(Base‘𝑅)) = 1 ↔ ¬ 𝑅 ∈ NzRing)) |