Step | Hyp | Ref
| Expression |
1 | | pntlem3.r |
. 2
ψ |
2 | | pntlem3.a |
. 2
|
3 | | pntlem3.A |
. 2
|
4 | | eqid 2622 |
. 2
|
5 | | pntlemp.b |
. . . 4
|
6 | | pntlemp.l |
. . . 4
|
7 | | pntlemp.d |
. . . 4
|
8 | | pntlemp.f |
. . . 4
; |
9 | 1, 2, 5, 6, 7, 8 | pntlemd 25283 |
. . 3
|
10 | 9 | simp3d 1075 |
. 2
|
11 | | 0m0e0 11130 |
. . . . 5
|
12 | | simpr 477 |
. . . . . 6
|
13 | 12 | oveq1d 6665 |
. . . . . . . . 9
|
14 | | 3nn 11186 |
. . . . . . . . . 10
|
15 | | 0exp 12895 |
. . . . . . . . . 10
|
16 | 14, 15 | ax-mp 5 |
. . . . . . . . 9
|
17 | 13, 16 | syl6eq 2672 |
. . . . . . . 8
|
18 | 17 | oveq2d 6666 |
. . . . . . 7
|
19 | 10 | rpcnd 11874 |
. . . . . . . . 9
|
20 | 19 | mul01d 10235 |
. . . . . . . 8
|
21 | 20 | ad2antrr 762 |
. . . . . . 7
|
22 | 18, 21 | eqtrd 2656 |
. . . . . 6
|
23 | 12, 22 | oveq12d 6668 |
. . . . 5
|
24 | 11, 23, 12 | 3eqtr4a 2682 |
. . . 4
|
25 | | simplr 792 |
. . . 4
|
26 | 24, 25 | eqeltrd 2701 |
. . 3
|
27 | | oveq1 6657 |
. . . . . . . . . . 11
|
28 | 27 | raleqdv 3144 |
. . . . . . . . . 10
|
29 | 28 | cbvrexv 3172 |
. . . . . . . . 9
|
30 | | simplrr 801 |
. . . . . . . . . . . . . . 15
|
31 | | 0re 10040 |
. . . . . . . . . . . . . . . 16
|
32 | 2 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
33 | 32 | rpred 11872 |
. . . . . . . . . . . . . . . 16
|
34 | | elicc2 12238 |
. . . . . . . . . . . . . . . 16
|
35 | 31, 33, 34 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
36 | 30, 35 | mpbid 222 |
. . . . . . . . . . . . . 14
|
37 | 36 | simp1d 1073 |
. . . . . . . . . . . . 13
|
38 | 10 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
39 | 36 | simp2d 1074 |
. . . . . . . . . . . . . . . . . 18
|
40 | | simplrl 800 |
. . . . . . . . . . . . . . . . . 18
|
41 | 37, 39, 40 | ne0gt0d 10174 |
. . . . . . . . . . . . . . . . 17
|
42 | 37, 41 | elrpd 11869 |
. . . . . . . . . . . . . . . 16
|
43 | | 3z 11410 |
. . . . . . . . . . . . . . . 16
|
44 | | rpexpcl 12879 |
. . . . . . . . . . . . . . . 16
|
45 | 42, 43, 44 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
46 | 38, 45 | rpmulcld 11888 |
. . . . . . . . . . . . . 14
|
47 | 46 | rpred 11872 |
. . . . . . . . . . . . 13
|
48 | 37, 47 | resubcld 10458 |
. . . . . . . . . . . 12
|
49 | 3 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
50 | 5 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
51 | 6 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
52 | | pntlemp.K |
. . . . . . . . . . . . . . 15
|
53 | 52 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
54 | 36 | simp3d 1075 |
. . . . . . . . . . . . . 14
|
55 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
56 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
57 | | simprl 794 |
. . . . . . . . . . . . . . . 16
|
58 | | 1rp 11836 |
. . . . . . . . . . . . . . . 16
|
59 | | rpaddcl 11854 |
. . . . . . . . . . . . . . . 16
|
60 | 57, 58, 59 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
61 | 57 | rpge0d 11876 |
. . . . . . . . . . . . . . . 16
|
62 | | 1re 10039 |
. . . . . . . . . . . . . . . . 17
|
63 | 57 | rpred 11872 |
. . . . . . . . . . . . . . . . 17
|
64 | | addge02 10539 |
. . . . . . . . . . . . . . . . 17
|
65 | 62, 63, 64 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
66 | 61, 65 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
67 | 60, 66 | jca 554 |
. . . . . . . . . . . . . 14
|
68 | 57 | rpxrd 11873 |
. . . . . . . . . . . . . . . 16
|
69 | 63 | lep1d 10955 |
. . . . . . . . . . . . . . . 16
|
70 | | df-ico 12181 |
. . . . . . . . . . . . . . . . 17
|
71 | | xrletr 11989 |
. . . . . . . . . . . . . . . . 17
|
72 | 70, 70, 71 | ixxss1 12193 |
. . . . . . . . . . . . . . . 16
|
73 | 68, 69, 72 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
74 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
75 | | ssralv 3666 |
. . . . . . . . . . . . . . 15
|
76 | 73, 74, 75 | sylc 65 |
. . . . . . . . . . . . . 14
|
77 | 1, 32, 49, 50, 51, 7, 8, 53, 42, 54, 55, 56, 67, 76 | pntlemp 25299 |
. . . . . . . . . . . . 13
|
78 | | rpre 11839 |
. . . . . . . . . . . . . . . . . 18
|
79 | 78 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
80 | 79 | leidd 10594 |
. . . . . . . . . . . . . . . . 17
|
81 | | elicopnf 12269 |
. . . . . . . . . . . . . . . . . 18
|
82 | 79, 81 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
83 | 79, 80, 82 | mpbir2and 957 |
. . . . . . . . . . . . . . . 16
|
84 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
85 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
|
86 | 84, 85 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . 19
|
87 | 86 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
88 | 87 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
|
89 | 88 | rspcv 3305 |
. . . . . . . . . . . . . . . 16
|
90 | 83, 89 | syl 17 |
. . . . . . . . . . . . . . 15
|
91 | 1 | pntrf 25252 |
. . . . . . . . . . . . . . . . . . . . 21
|
92 | 91 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . . . . 20
|
93 | | rerpdivcl 11861 |
. . . . . . . . . . . . . . . . . . . 20
|
94 | 92, 93 | mpancom 703 |
. . . . . . . . . . . . . . . . . . 19
|
95 | 94 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
96 | 95 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
|
97 | 96 | absge0d 14183 |
. . . . . . . . . . . . . . . 16
|
98 | | 0red 10041 |
. . . . . . . . . . . . . . . . 17
|
99 | 96 | abscld 14175 |
. . . . . . . . . . . . . . . . 17
|
100 | 48 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
101 | | letr 10131 |
. . . . . . . . . . . . . . . . 17
|
102 | 98, 99, 100, 101 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
103 | 97, 102 | mpand 711 |
. . . . . . . . . . . . . . 15
|
104 | 90, 103 | syld 47 |
. . . . . . . . . . . . . 14
|
105 | 104 | rexlimdva 3031 |
. . . . . . . . . . . . 13
|
106 | 77, 105 | mpd 15 |
. . . . . . . . . . . 12
|
107 | 46 | rpge0d 11876 |
. . . . . . . . . . . . . 14
|
108 | 37, 47 | subge02d 10619 |
. . . . . . . . . . . . . 14
|
109 | 107, 108 | mpbid 222 |
. . . . . . . . . . . . 13
|
110 | 48, 37, 33, 109, 54 | letrd 10194 |
. . . . . . . . . . . 12
|
111 | | elicc2 12238 |
. . . . . . . . . . . . 13
|
112 | 31, 33, 111 | sylancr 695 |
. . . . . . . . . . . 12
|
113 | 48, 106, 110, 112 | mpbir3and 1245 |
. . . . . . . . . . 11
|
114 | 113, 77 | jca 554 |
. . . . . . . . . 10
|
115 | 114 | rexlimdvaa 3032 |
. . . . . . . . 9
|
116 | 29, 115 | syl5bi 232 |
. . . . . . . 8
|
117 | 116 | anassrs 680 |
. . . . . . 7
|
118 | 117 | expimpd 629 |
. . . . . 6
|
119 | | breq2 4657 |
. . . . . . . 8
|
120 | 119 | rexralbidv 3058 |
. . . . . . 7
|
121 | 120 | elrab 3363 |
. . . . . 6
|
122 | | breq2 4657 |
. . . . . . . . 9
|
123 | 122 | rexralbidv 3058 |
. . . . . . . 8
|
124 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
125 | | id 22 |
. . . . . . . . . . . . . 14
|
126 | 124, 125 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
127 | 126 | fveq2d 6195 |
. . . . . . . . . . . 12
|
128 | 127 | breq1d 4663 |
. . . . . . . . . . 11
|
129 | 128 | cbvralv 3171 |
. . . . . . . . . 10
|
130 | | oveq1 6657 |
. . . . . . . . . . 11
|
131 | 130 | raleqdv 3144 |
. . . . . . . . . 10
|
132 | 129, 131 | syl5bb 272 |
. . . . . . . . 9
|
133 | 132 | cbvrexv 3172 |
. . . . . . . 8
|
134 | 123, 133 | syl6bbr 278 |
. . . . . . 7
|
135 | 134 | elrab 3363 |
. . . . . 6
|
136 | 118, 121,
135 | 3imtr4g 285 |
. . . . 5
|
137 | 136 | imp 445 |
. . . 4
|
138 | 137 | an32s 846 |
. . 3
|
139 | 26, 138 | pm2.61dane 2881 |
. 2
|
140 | 1, 2, 3, 4, 10, 139 | pntlem3 25298 |
1
ψ |