Proof of Theorem 0ringnnzr
Step | Hyp | Ref
| Expression |
1 | | 1re 10363 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
2 | 1 | ltnri 10472 |
. . . . . . 7
⊢ ¬ 1
< 1 |
3 | | breq2 4879 |
. . . . . . 7
⊢
((♯‘(Base‘𝑅)) = 1 → (1 <
(♯‘(Base‘𝑅)) ↔ 1 < 1)) |
4 | 2, 3 | mtbiri 319 |
. . . . . 6
⊢
((♯‘(Base‘𝑅)) = 1 → ¬ 1 <
(♯‘(Base‘𝑅))) |
5 | 4 | adantl 475 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧
(♯‘(Base‘𝑅)) = 1) → ¬ 1 <
(♯‘(Base‘𝑅))) |
6 | 5 | intnand 484 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧
(♯‘(Base‘𝑅)) = 1) → ¬ (𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅)))) |
7 | 6 | ex 403 |
. . 3
⊢ (𝑅 ∈ Ring →
((♯‘(Base‘𝑅)) = 1 → ¬ (𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))))) |
8 | | ianor 1009 |
. . . . 5
⊢ (¬
(𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))) ↔ (¬ 𝑅 ∈ Ring ∨ ¬ 1 <
(♯‘(Base‘𝑅)))) |
9 | | pm2.21 121 |
. . . . . 6
⊢ (¬
𝑅 ∈ Ring → (𝑅 ∈ Ring →
(♯‘(Base‘𝑅)) = 1)) |
10 | | fvex 6450 |
. . . . . . . . . 10
⊢
(Base‘𝑅)
∈ V |
11 | | hashxrcl 13445 |
. . . . . . . . . 10
⊢
((Base‘𝑅)
∈ V → (♯‘(Base‘𝑅)) ∈
ℝ*) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
⊢
(♯‘(Base‘𝑅)) ∈
ℝ* |
13 | | 1xr 10423 |
. . . . . . . . 9
⊢ 1 ∈
ℝ* |
14 | | xrlenlt 10429 |
. . . . . . . . 9
⊢
(((♯‘(Base‘𝑅)) ∈ ℝ* ∧ 1 ∈
ℝ*) → ((♯‘(Base‘𝑅)) ≤ 1 ↔ ¬ 1 <
(♯‘(Base‘𝑅)))) |
15 | 12, 13, 14 | mp2an 683 |
. . . . . . . 8
⊢
((♯‘(Base‘𝑅)) ≤ 1 ↔ ¬ 1 <
(♯‘(Base‘𝑅))) |
16 | 15 | bicomi 216 |
. . . . . . 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 11643 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ0 |
20 | 19 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) → 1 ∈
ℕ0) |
21 | | hashbnd 13423 |
. . . . . . . . . . . . 13
⊢
(((Base‘𝑅)
∈ V ∧ 1 ∈ ℕ0 ∧
(♯‘(Base‘𝑅)) ≤ 1) → (Base‘𝑅) ∈ Fin) |
22 | 18, 20, 17, 21 | syl3anc 1494 |
. . . . . . . . . . . 12
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) → (Base‘𝑅) ∈ Fin) |
23 | | hashcl 13444 |
. . . . . . . . . . . . 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 13451 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((Base‘𝑅)
∈ V → ((♯‘(Base‘𝑅)) = 0 ↔ (Base‘𝑅) = ∅)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘(Base‘𝑅)) ∈ ℕ0 →
((♯‘(Base‘𝑅)) = 0 ↔ (Base‘𝑅) = ∅)) |
28 | 27 | biimpd 221 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘(Base‘𝑅)) ∈ ℕ0 →
((♯‘(Base‘𝑅)) = 0 → (Base‘𝑅) = ∅)) |
29 | 28 | necon3d 3020 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘(Base‘𝑅)) ∈ ℕ0 →
((Base‘𝑅) ≠
∅ → (♯‘(Base‘𝑅)) ≠ 0)) |
30 | 29 | impcom 398 |
. . . . . . . . . . . . . . . . 17
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ∈ ℕ0) →
(♯‘(Base‘𝑅)) ≠ 0) |
31 | | elnnne0 11641 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘(Base‘𝑅)) ∈ ℕ ↔
((♯‘(Base‘𝑅)) ∈ ℕ0 ∧
(♯‘(Base‘𝑅)) ≠ 0)) |
32 | 24, 30, 31 | sylanbrc 578 |
. . . . . . . . . . . . . . . 16
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ∈ ℕ0) →
(♯‘(Base‘𝑅)) ∈ ℕ) |
33 | 32 | ex 403 |
. . . . . . . . . . . . . . 15
⊢
((Base‘𝑅) ≠
∅ → ((♯‘(Base‘𝑅)) ∈ ℕ0 →
(♯‘(Base‘𝑅)) ∈ ℕ)) |
34 | 33 | adantr 474 |
. . . . . . . . . . . . . 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 11389 |
. . . . . . . . . . 11
⊢
((♯‘(Base‘𝑅)) ∈ ℕ →
((♯‘(Base‘𝑅)) ≤ 1 ↔
(♯‘(Base‘𝑅)) = 1)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) →
((♯‘(Base‘𝑅)) ≤ 1 ↔
(♯‘(Base‘𝑅)) = 1)) |
40 | 17, 39 | mpbid 224 |
. . . . . . . . 9
⊢
(((Base‘𝑅)
≠ ∅ ∧ (♯‘(Base‘𝑅)) ≤ 1) →
(♯‘(Base‘𝑅)) = 1) |
41 | 40 | ex 403 |
. . . . . . . 8
⊢
((Base‘𝑅) ≠
∅ → ((♯‘(Base‘𝑅)) ≤ 1 →
(♯‘(Base‘𝑅)) = 1)) |
42 | | ringgrp 18913 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
43 | | eqid 2825 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
44 | 43 | grpbn0 17812 |
. . . . . . . . 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 209 |
. . . . . 6
⊢ (¬ 1
< (♯‘(Base‘𝑅)) → (𝑅 ∈ Ring →
(♯‘(Base‘𝑅)) = 1)) |
48 | 9, 47 | jaoi 888 |
. . . . 5
⊢ ((¬
𝑅 ∈ Ring ∨ ¬ 1
< (♯‘(Base‘𝑅))) → (𝑅 ∈ Ring →
(♯‘(Base‘𝑅)) = 1)) |
49 | 8, 48 | sylbi 209 |
. . . 4
⊢ (¬
(𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))) → (𝑅 ∈ Ring →
(♯‘(Base‘𝑅)) = 1)) |
50 | 49 | com12 32 |
. . 3
⊢ (𝑅 ∈ Ring → (¬
(𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))) → (♯‘(Base‘𝑅)) = 1)) |
51 | 7, 50 | impbid 204 |
. 2
⊢ (𝑅 ∈ Ring →
((♯‘(Base‘𝑅)) = 1 ↔ ¬ (𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))))) |
52 | 43 | isnzr2hash 19632 |
. . . 4
⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅)))) |
53 | 52 | bicomi 216 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))) ↔ 𝑅 ∈ NzRing) |
54 | 53 | notbii 312 |
. 2
⊢ (¬
(𝑅 ∈ Ring ∧ 1 <
(♯‘(Base‘𝑅))) ↔ ¬ 𝑅 ∈ NzRing) |
55 | 51, 54 | syl6bb 279 |
1
⊢ (𝑅 ∈ Ring →
((♯‘(Base‘𝑅)) = 1 ↔ ¬ 𝑅 ∈ NzRing)) |