Step | Hyp | Ref
| Expression |
1 | | rpssre 11843 |
. . . 4
|
2 | 1 | a1i 11 |
. . 3
|
3 | | 1red 10055 |
. . 3
|
4 | | pntrval.r |
. . . . . . . 8
ψ |
5 | 4 | pntrval 25251 |
. . . . . . 7
ψ |
6 | | rpre 11839 |
. . . . . . . . 9
|
7 | | chpcl 24850 |
. . . . . . . . 9
ψ |
8 | 6, 7 | syl 17 |
. . . . . . . 8
ψ |
9 | 8, 6 | resubcld 10458 |
. . . . . . 7
ψ |
10 | 5, 9 | eqeltrd 2701 |
. . . . . 6
|
11 | | rerpdivcl 11861 |
. . . . . 6
|
12 | 10, 11 | mpancom 703 |
. . . . 5
|
13 | 12 | recnd 10068 |
. . . 4
|
14 | 13 | adantl 482 |
. . 3
|
15 | 5 | oveq1d 6665 |
. . . . . 6
ψ |
16 | 8 | recnd 10068 |
. . . . . . 7
ψ |
17 | | rpcn 11841 |
. . . . . . 7
|
18 | | rpne0 11848 |
. . . . . . 7
|
19 | 16, 17, 17, 18 | divsubdird 10840 |
. . . . . 6
ψ ψ |
20 | 17, 18 | dividd 10799 |
. . . . . . 7
|
21 | 20 | oveq2d 6666 |
. . . . . 6
ψ ψ |
22 | 15, 19, 21 | 3eqtrd 2660 |
. . . . 5
ψ |
23 | 22 | mpteq2ia 4740 |
. . . 4
ψ |
24 | | rerpdivcl 11861 |
. . . . . . 7
ψ
ψ |
25 | 8, 24 | mpancom 703 |
. . . . . 6
ψ |
26 | 25 | adantl 482 |
. . . . 5
ψ |
27 | | 1red 10055 |
. . . . 5
|
28 | | chpo1ub 25169 |
. . . . . 6
ψ |
29 | 28 | a1i 11 |
. . . . 5
ψ |
30 | | ax-1cn 9994 |
. . . . . . 7
|
31 | | o1const 14350 |
. . . . . . 7
|
32 | 1, 30, 31 | mp2an 708 |
. . . . . 6
|
33 | 32 | a1i 11 |
. . . . 5
|
34 | 26, 27, 29, 33 | o1sub2 14356 |
. . . 4
ψ |
35 | 23, 34 | syl5eqel 2705 |
. . 3
|
36 | | chpcl 24850 |
. . . . 5
ψ |
37 | | peano2re 10209 |
. . . . 5
ψ ψ |
38 | 36, 37 | syl 17 |
. . . 4
ψ |
39 | 38 | ad2antrl 764 |
. . 3
ψ |
40 | 22 | 3ad2ant1 1082 |
. . . . . . . 8
ψ |
41 | 40 | fveq2d 6195 |
. . . . . . 7
ψ |
42 | | 1re 10039 |
. . . . . . . . . 10
|
43 | 38 | 3ad2ant2 1083 |
. . . . . . . . . 10
ψ |
44 | | resubcl 10345 |
. . . . . . . . . 10
ψ ψ |
45 | 42, 43, 44 | sylancr 695 |
. . . . . . . . 9
ψ |
46 | | 0red 10041 |
. . . . . . . . 9
|
47 | 25 | 3ad2ant1 1082 |
. . . . . . . . 9
ψ |
48 | | chpge0 24852 |
. . . . . . . . . . . 12
ψ |
49 | 48 | 3ad2ant2 1083 |
. . . . . . . . . . 11
ψ |
50 | 36 | 3ad2ant2 1083 |
. . . . . . . . . . . 12
ψ |
51 | | addge02 10539 |
. . . . . . . . . . . 12
ψ
ψ ψ |
52 | 42, 50, 51 | sylancr 695 |
. . . . . . . . . . 11
ψ ψ |
53 | 49, 52 | mpbid 222 |
. . . . . . . . . 10
ψ |
54 | | suble0 10542 |
. . . . . . . . . . 11
ψ ψ
ψ |
55 | 42, 43, 54 | sylancr 695 |
. . . . . . . . . 10
ψ
ψ |
56 | 53, 55 | mpbird 247 |
. . . . . . . . 9
ψ |
57 | 8 | 3ad2ant1 1082 |
. . . . . . . . . 10
ψ |
58 | 6 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
59 | | chpge0 24852 |
. . . . . . . . . . 11
ψ |
60 | 58, 59 | syl 17 |
. . . . . . . . . 10
ψ |
61 | | rpregt0 11846 |
. . . . . . . . . . 11
|
62 | 61 | 3ad2ant1 1082 |
. . . . . . . . . 10
|
63 | | divge0 10892 |
. . . . . . . . . 10
ψ ψ ψ |
64 | 57, 60, 62, 63 | syl21anc 1325 |
. . . . . . . . 9
ψ |
65 | 45, 46, 47, 56, 64 | letrd 10194 |
. . . . . . . 8
ψ ψ |
66 | | 2re 11090 |
. . . . . . . . . . 11
|
67 | | readdcl 10019 |
. . . . . . . . . . 11
ψ ψ |
68 | 50, 66, 67 | sylancl 694 |
. . . . . . . . . 10
ψ |
69 | | 1red 10055 |
. . . . . . . . . . 11
|
70 | 58 | adantr 481 |
. . . . . . . . . . . . . . 15
|
71 | | 1red 10055 |
. . . . . . . . . . . . . . 15
|
72 | 66 | a1i 11 |
. . . . . . . . . . . . . . 15
|
73 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
74 | | 1lt2 11194 |
. . . . . . . . . . . . . . . 16
|
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . 15
|
76 | 70, 71, 72, 73, 75 | lelttrd 10195 |
. . . . . . . . . . . . . 14
|
77 | | chpeq0 24933 |
. . . . . . . . . . . . . . 15
ψ
|
78 | 70, 77 | syl 17 |
. . . . . . . . . . . . . 14
ψ |
79 | 76, 78 | mpbird 247 |
. . . . . . . . . . . . 13
ψ |
80 | 79 | oveq1d 6665 |
. . . . . . . . . . . 12
ψ |
81 | | simp1 1061 |
. . . . . . . . . . . . . . . 16
|
82 | 81 | rpcnne0d 11881 |
. . . . . . . . . . . . . . 15
|
83 | | div0 10715 |
. . . . . . . . . . . . . . 15
|
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . 14
|
85 | 84, 49 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
ψ |
86 | 85 | adantr 481 |
. . . . . . . . . . . 12
ψ |
87 | 80, 86 | eqbrtrd 4675 |
. . . . . . . . . . 11
ψ ψ |
88 | 47 | adantr 481 |
. . . . . . . . . . . 12
ψ |
89 | 57 | adantr 481 |
. . . . . . . . . . . 12
ψ |
90 | 50 | adantr 481 |
. . . . . . . . . . . 12
ψ |
91 | | 0lt1 10550 |
. . . . . . . . . . . . . . . 16
|
92 | 91 | a1i 11 |
. . . . . . . . . . . . . . 15
|
93 | | lediv2a 10917 |
. . . . . . . . . . . . . . . 16
ψ ψ ψ ψ |
94 | 93 | ex 450 |
. . . . . . . . . . . . . . 15
ψ ψ
ψ ψ |
95 | 69, 92, 62, 57, 60, 94 | syl212anc 1336 |
. . . . . . . . . . . . . 14
ψ ψ |
96 | 95 | imp 445 |
. . . . . . . . . . . . 13
ψ ψ |
97 | 89 | recnd 10068 |
. . . . . . . . . . . . . 14
ψ |
98 | 97 | div1d 10793 |
. . . . . . . . . . . . 13
ψ ψ |
99 | 96, 98 | breqtrd 4679 |
. . . . . . . . . . . 12
ψ ψ |
100 | | simp2 1062 |
. . . . . . . . . . . . . 14
|
101 | | ltle 10126 |
. . . . . . . . . . . . . . . 16
|
102 | 6, 101 | sylan 488 |
. . . . . . . . . . . . . . 15
|
103 | 102 | 3impia 1261 |
. . . . . . . . . . . . . 14
|
104 | | chpwordi 24883 |
. . . . . . . . . . . . . 14
ψ ψ |
105 | 58, 100, 103, 104 | syl3anc 1326 |
. . . . . . . . . . . . 13
ψ ψ |
106 | 105 | adantr 481 |
. . . . . . . . . . . 12
ψ ψ |
107 | 88, 89, 90, 99, 106 | letrd 10194 |
. . . . . . . . . . 11
ψ ψ |
108 | 58, 69, 87, 107 | lecasei 10143 |
. . . . . . . . . 10
ψ ψ |
109 | | 2nn0 11309 |
. . . . . . . . . . 11
|
110 | | nn0addge1 11339 |
. . . . . . . . . . 11
ψ ψ ψ |
111 | 50, 109, 110 | sylancl 694 |
. . . . . . . . . 10
ψ ψ |
112 | 47, 50, 68, 108, 111 | letrd 10194 |
. . . . . . . . 9
ψ ψ |
113 | | df-2 11079 |
. . . . . . . . . . 11
|
114 | 113 | oveq2i 6661 |
. . . . . . . . . 10
ψ ψ |
115 | 50 | recnd 10068 |
. . . . . . . . . . 11
ψ |
116 | 30 | a1i 11 |
. . . . . . . . . . 11
|
117 | 115, 116,
116 | add12d 10262 |
. . . . . . . . . 10
ψ ψ |
118 | 114, 117 | syl5eq 2668 |
. . . . . . . . 9
ψ ψ |
119 | 112, 118 | breqtrd 4679 |
. . . . . . . 8
ψ ψ |
120 | 47, 69, 43 | absdifled 14173 |
. . . . . . . 8
ψ ψ ψ ψ ψ ψ |
121 | 65, 119, 120 | mpbir2and 957 |
. . . . . . 7
ψ
ψ |
122 | 41, 121 | eqbrtrd 4675 |
. . . . . 6
ψ |
123 | 122 | 3expb 1266 |
. . . . 5
ψ |
124 | 123 | adantrlr 759 |
. . . 4
ψ |
125 | 124 | adantll 750 |
. . 3
ψ |
126 | 2, 3, 14, 35, 39, 125 | o1bddrp 14273 |
. 2
|
127 | 126 | trud 1493 |
1
|