Step | Hyp | Ref
| Expression |
1 | | ssdif0 3942 |
. . . 4
|
2 | | simpr 477 |
. . . . . 6
SubRingℂfld
|
3 | | simplr 792 |
. . . . . 6
SubRingℂfld
|
4 | 2, 3 | eqssd 3620 |
. . . . 5
SubRingℂfld
|
5 | 4 | orcd 407 |
. . . 4
SubRingℂfld
|
6 | 1, 5 | sylan2br 493 |
. . 3
SubRingℂfld
|
7 | | n0 3931 |
. . . 4
|
8 | | simpll 790 |
. . . . . . . . . 10
SubRingℂfld
SubRingℂfld |
9 | | cnfldbas 19750 |
. . . . . . . . . . 11
ℂfld |
10 | 9 | subrgss 18781 |
. . . . . . . . . 10
SubRingℂfld
|
11 | 8, 10 | syl 17 |
. . . . . . . . 9
SubRingℂfld
|
12 | | replim 13856 |
. . . . . . . . . . . . 13
|
13 | 12 | ad2antll 765 |
. . . . . . . . . . . 12
SubRingℂfld
|
14 | | simpll 790 |
. . . . . . . . . . . . 13
SubRingℂfld
SubRingℂfld |
15 | | simplr 792 |
. . . . . . . . . . . . . 14
SubRingℂfld
|
16 | | recl 13850 |
. . . . . . . . . . . . . . 15
|
17 | 16 | ad2antll 765 |
. . . . . . . . . . . . . 14
SubRingℂfld
|
18 | 15, 17 | sseldd 3604 |
. . . . . . . . . . . . 13
SubRingℂfld
|
19 | | ax-icn 9995 |
. . . . . . . . . . . . . . . . . . 19
|
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
SubRingℂfld
|
21 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . 22
|
22 | 21 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
SubRingℂfld
|
23 | 11, 22 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . 20
SubRingℂfld
|
24 | | imcl 13851 |
. . . . . . . . . . . . . . . . . . . 20
|
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
SubRingℂfld
|
26 | 25 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
SubRingℂfld
|
27 | | eldifn 3733 |
. . . . . . . . . . . . . . . . . . . 20
|
28 | 27 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
SubRingℂfld
|
29 | | reim0b 13859 |
. . . . . . . . . . . . . . . . . . . . 21
|
30 | 29 | necon3bbid 2831 |
. . . . . . . . . . . . . . . . . . . 20
|
31 | 23, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
SubRingℂfld
|
32 | 28, 31 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
SubRingℂfld
|
33 | 20, 26, 32 | divcan4d 10807 |
. . . . . . . . . . . . . . . . 17
SubRingℂfld
|
34 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . . 19
|
35 | 19, 26, 34 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
SubRingℂfld
|
36 | 35, 26, 32 | divrecd 10804 |
. . . . . . . . . . . . . . . . 17
SubRingℂfld
|
37 | 33, 36 | eqtr3d 2658 |
. . . . . . . . . . . . . . . 16
SubRingℂfld
|
38 | 23 | recld 13934 |
. . . . . . . . . . . . . . . . . . . . 21
SubRingℂfld
|
39 | 38 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
SubRingℂfld
|
40 | 23, 39 | negsubd 10398 |
. . . . . . . . . . . . . . . . . . 19
SubRingℂfld
|
41 | | replim 13856 |
. . . . . . . . . . . . . . . . . . . . 21
|
42 | 23, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
SubRingℂfld
|
43 | 42 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
SubRingℂfld
|
44 | 39, 35 | pncan2d 10394 |
. . . . . . . . . . . . . . . . . . 19
SubRingℂfld
|
45 | 40, 43, 44 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . 18
SubRingℂfld
|
46 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . 20
SubRingℂfld
|
47 | 38 | renegcld 10457 |
. . . . . . . . . . . . . . . . . . . 20
SubRingℂfld
|
48 | 46, 47 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . 19
SubRingℂfld
|
49 | | cnfldadd 19751 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld |
50 | 49 | subrgacl 18791 |
. . . . . . . . . . . . . . . . . . 19
SubRingℂfld
|
51 | 8, 22, 48, 50 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
SubRingℂfld
|
52 | 45, 51 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . 17
SubRingℂfld
|
53 | 25, 32 | rereccld 10852 |
. . . . . . . . . . . . . . . . . 18
SubRingℂfld
|
54 | 46, 53 | sseldd 3604 |
. . . . . . . . . . . . . . . . 17
SubRingℂfld
|
55 | | cnfldmul 19752 |
. . . . . . . . . . . . . . . . . 18
ℂfld |
56 | 55 | subrgmcl 18792 |
. . . . . . . . . . . . . . . . 17
SubRingℂfld
|
57 | 8, 52, 54, 56 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
SubRingℂfld
|
58 | 37, 57 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
SubRingℂfld
|
59 | 58 | adantrr 753 |
. . . . . . . . . . . . . 14
SubRingℂfld
|
60 | | imcl 13851 |
. . . . . . . . . . . . . . . 16
|
61 | 60 | ad2antll 765 |
. . . . . . . . . . . . . . 15
SubRingℂfld
|
62 | 15, 61 | sseldd 3604 |
. . . . . . . . . . . . . 14
SubRingℂfld
|
63 | 55 | subrgmcl 18792 |
. . . . . . . . . . . . . 14
SubRingℂfld
|
64 | 14, 59, 62, 63 | syl3anc 1326 |
. . . . . . . . . . . . 13
SubRingℂfld
|
65 | 49 | subrgacl 18791 |
. . . . . . . . . . . . 13
SubRingℂfld
|
66 | 14, 18, 64, 65 | syl3anc 1326 |
. . . . . . . . . . . 12
SubRingℂfld
|
67 | 13, 66 | eqeltrd 2701 |
. . . . . . . . . . 11
SubRingℂfld
|
68 | 67 | expr 643 |
. . . . . . . . . 10
SubRingℂfld
|
69 | 68 | ssrdv 3609 |
. . . . . . . . 9
SubRingℂfld
|
70 | 11, 69 | eqssd 3620 |
. . . . . . . 8
SubRingℂfld
|
71 | 70 | olcd 408 |
. . . . . . 7
SubRingℂfld
|
72 | 71 | ex 450 |
. . . . . 6
SubRingℂfld
|
73 | 72 | exlimdv 1861 |
. . . . 5
SubRingℂfld
|
74 | 73 | imp 445 |
. . . 4
SubRingℂfld
|
75 | 7, 74 | sylan2b 492 |
. . 3
SubRingℂfld
|
76 | 6, 75 | pm2.61dane 2881 |
. 2
SubRingℂfld
|
77 | | elprg 4196 |
. . 3
SubRingℂfld
|
78 | 77 | adantr 481 |
. 2
SubRingℂfld
|
79 | 76, 78 | mpbird 247 |
1
SubRingℂfld
|