Step | Hyp | Ref
| Expression |
1 | | iccssxr 12256 |
. . . 4
|
2 | | xrltso 11974 |
. . . 4
|
3 | | soss 5053 |
. . . 4
|
4 | 1, 2, 3 | mp2 9 |
. . 3
|
5 | | iccssxr 12256 |
. . . . 5
|
6 | | soss 5053 |
. . . . 5
|
7 | 5, 2, 6 | mp2 9 |
. . . 4
|
8 | | sopo 5052 |
. . . 4
|
9 | 7, 8 | ax-mp 5 |
. . 3
|
10 | | iccpnfhmeo.f |
. . . . . 6
|
11 | 10 | iccpnfcnv 22743 |
. . . . 5
|
12 | 11 | simpli 474 |
. . . 4
|
13 | | f1ofo 6144 |
. . . 4
|
14 | 12, 13 | ax-mp 5 |
. . 3
|
15 | | 0re 10040 |
. . . . . . . . . . . . 13
|
16 | | 1re 10039 |
. . . . . . . . . . . . 13
|
17 | 15, 16 | elicc2i 12239 |
. . . . . . . . . . . 12
|
18 | 17 | simp1bi 1076 |
. . . . . . . . . . 11
|
19 | 18 | 3ad2ant1 1082 |
. . . . . . . . . 10
|
20 | 15, 16 | elicc2i 12239 |
. . . . . . . . . . . . 13
|
21 | 20 | simp1bi 1076 |
. . . . . . . . . . . 12
|
22 | 21 | 3ad2ant2 1083 |
. . . . . . . . . . 11
|
23 | | 1red 10055 |
. . . . . . . . . . 11
|
24 | | simp3 1063 |
. . . . . . . . . . 11
|
25 | 20 | simp3bi 1078 |
. . . . . . . . . . . 12
|
26 | 25 | 3ad2ant2 1083 |
. . . . . . . . . . 11
|
27 | 19, 22, 23, 24, 26 | ltletrd 10197 |
. . . . . . . . . 10
|
28 | 19, 27 | gtned 10172 |
. . . . . . . . 9
|
29 | 28 | necomd 2849 |
. . . . . . . 8
|
30 | | ifnefalse 4098 |
. . . . . . . 8
|
31 | 29, 30 | syl 17 |
. . . . . . 7
|
32 | | breq2 4657 |
. . . . . . . 8
|
33 | | breq2 4657 |
. . . . . . . 8
|
34 | | resubcl 10345 |
. . . . . . . . . . . 12
|
35 | 16, 19, 34 | sylancr 695 |
. . . . . . . . . . 11
|
36 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
|
37 | 19 | recnd 10068 |
. . . . . . . . . . . . 13
|
38 | | subeq0 10307 |
. . . . . . . . . . . . . 14
|
39 | 38 | necon3bid 2838 |
. . . . . . . . . . . . 13
|
40 | 36, 37, 39 | sylancr 695 |
. . . . . . . . . . . 12
|
41 | 28, 40 | mpbird 247 |
. . . . . . . . . . 11
|
42 | 19, 35, 41 | redivcld 10853 |
. . . . . . . . . 10
|
43 | | ltpnf 11954 |
. . . . . . . . . 10
|
44 | 42, 43 | syl 17 |
. . . . . . . . 9
|
45 | 44 | adantr 481 |
. . . . . . . 8
|
46 | | simpl3 1066 |
. . . . . . . . . 10
|
47 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
48 | | eqid 2622 |
. . . . . . . . . . . . . 14
ℂfld ℂfld |
49 | 47, 48 | icopnfhmeo 22742 |
. . . . . . . . . . . . 13
ℂfld ↾t ℂfld ↾t
|
50 | 49 | simpli 474 |
. . . . . . . . . . . 12
|
51 | 50 | a1i 11 |
. . . . . . . . . . 11
|
52 | | simp1 1061 |
. . . . . . . . . . . . . . . . . 18
|
53 | | 0xr 10086 |
. . . . . . . . . . . . . . . . . . 19
|
54 | 16 | rexri 10097 |
. . . . . . . . . . . . . . . . . . 19
|
55 | | 0le1 10551 |
. . . . . . . . . . . . . . . . . . 19
|
56 | | snunico 12299 |
. . . . . . . . . . . . . . . . . . 19
|
57 | 53, 54, 55, 56 | mp3an 1424 |
. . . . . . . . . . . . . . . . . 18
|
58 | 52, 57 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . 17
|
59 | | elun 3753 |
. . . . . . . . . . . . . . . . 17
|
60 | 58, 59 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
61 | 60 | ord 392 |
. . . . . . . . . . . . . . 15
|
62 | | elsni 4194 |
. . . . . . . . . . . . . . 15
|
63 | 61, 62 | syl6 35 |
. . . . . . . . . . . . . 14
|
64 | 63 | necon1ad 2811 |
. . . . . . . . . . . . 13
|
65 | 29, 64 | mpd 15 |
. . . . . . . . . . . 12
|
66 | 65 | adantr 481 |
. . . . . . . . . . 11
|
67 | | simp2 1062 |
. . . . . . . . . . . . . . . . 17
|
68 | 67, 57 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . 16
|
69 | | elun 3753 |
. . . . . . . . . . . . . . . 16
|
70 | 68, 69 | sylib 208 |
. . . . . . . . . . . . . . 15
|
71 | 70 | ord 392 |
. . . . . . . . . . . . . 14
|
72 | | elsni 4194 |
. . . . . . . . . . . . . 14
|
73 | 71, 72 | syl6 35 |
. . . . . . . . . . . . 13
|
74 | 73 | con1d 139 |
. . . . . . . . . . . 12
|
75 | 74 | imp 445 |
. . . . . . . . . . 11
|
76 | | isorel 6576 |
. . . . . . . . . . 11
|
77 | 51, 66, 75, 76 | syl12anc 1324 |
. . . . . . . . . 10
|
78 | 46, 77 | mpbid 222 |
. . . . . . . . 9
|
79 | | id 22 |
. . . . . . . . . . . 12
|
80 | | oveq2 6658 |
. . . . . . . . . . . 12
|
81 | 79, 80 | oveq12d 6668 |
. . . . . . . . . . 11
|
82 | | ovex 6678 |
. . . . . . . . . . 11
|
83 | 81, 47, 82 | fvmpt 6282 |
. . . . . . . . . 10
|
84 | 66, 83 | syl 17 |
. . . . . . . . 9
|
85 | | id 22 |
. . . . . . . . . . . 12
|
86 | | oveq2 6658 |
. . . . . . . . . . . 12
|
87 | 85, 86 | oveq12d 6668 |
. . . . . . . . . . 11
|
88 | | ovex 6678 |
. . . . . . . . . . 11
|
89 | 87, 47, 88 | fvmpt 6282 |
. . . . . . . . . 10
|
90 | 75, 89 | syl 17 |
. . . . . . . . 9
|
91 | 78, 84, 90 | 3brtr3d 4684 |
. . . . . . . 8
|
92 | 32, 33, 45, 91 | ifbothda 4123 |
. . . . . . 7
|
93 | 31, 92 | eqbrtrd 4675 |
. . . . . 6
|
94 | 93 | 3expia 1267 |
. . . . 5
|
95 | | eqeq1 2626 |
. . . . . . . 8
|
96 | 95, 81 | ifbieq2d 4111 |
. . . . . . 7
|
97 | | pnfex 10093 |
. . . . . . . 8
|
98 | 97, 82 | ifex 4156 |
. . . . . . 7
|
99 | 96, 10, 98 | fvmpt 6282 |
. . . . . 6
|
100 | | eqeq1 2626 |
. . . . . . . 8
|
101 | 100, 87 | ifbieq2d 4111 |
. . . . . . 7
|
102 | 97, 88 | ifex 4156 |
. . . . . . 7
|
103 | 101, 10, 102 | fvmpt 6282 |
. . . . . 6
|
104 | 99, 103 | breqan12d 4669 |
. . . . 5
|
105 | 94, 104 | sylibrd 249 |
. . . 4
|
106 | 105 | rgen2a 2977 |
. . 3
|
107 | | soisoi 6578 |
. . 3
|
108 | 4, 9, 14, 106, 107 | mp4an 709 |
. 2
|
109 | | letsr 17227 |
. . . . . 6
|
110 | 109 | elexi 3213 |
. . . . 5
|
111 | 110 | inex1 4799 |
. . . 4
|
112 | 110 | inex1 4799 |
. . . 4
|
113 | | leiso 13243 |
. . . . . . . 8
|
114 | 1, 5, 113 | mp2an 708 |
. . . . . . 7
|
115 | 108, 114 | mpbi 220 |
. . . . . 6
|
116 | | isores1 6584 |
. . . . . 6
|
117 | 115, 116 | mpbi 220 |
. . . . 5
|
118 | | isores2 6583 |
. . . . 5
|
119 | 117, 118 | mpbi 220 |
. . . 4
|
120 | | tsrps 17221 |
. . . . . . . 8
|
121 | 109, 120 | ax-mp 5 |
. . . . . . 7
|
122 | | ledm 17224 |
. . . . . . . 8
|
123 | 122 | psssdm 17216 |
. . . . . . 7
|
124 | 121, 1, 123 | mp2an 708 |
. . . . . 6
|
125 | 124 | eqcomi 2631 |
. . . . 5
|
126 | 122 | psssdm 17216 |
. . . . . . 7
|
127 | 121, 5, 126 | mp2an 708 |
. . . . . 6
|
128 | 127 | eqcomi 2631 |
. . . . 5
|
129 | 125, 128 | ordthmeo 21605 |
. . . 4
ordTop
ordTop
|
130 | 111, 112,
119, 129 | mp3an 1424 |
. . 3
ordTop ordTop
|
131 | | dfii5 22688 |
. . . 4
ordTop |
132 | | iccpnfhmeo.k |
. . . . 5
ordTop ↾t |
133 | | ordtresticc 21027 |
. . . . 5
ordTop
↾t ordTop
|
134 | 132, 133 | eqtri 2644 |
. . . 4
ordTop
|
135 | 131, 134 | oveq12i 6662 |
. . 3
ordTop ordTop
|
136 | 130, 135 | eleqtrri 2700 |
. 2
|
137 | 108, 136 | pm3.2i 471 |
1
|