Proof of Theorem fldiv4p1lem1div2
Step | Hyp | Ref
| Expression |
1 | | 1le1 8358 |
. . . 4
![1 1](1.gif) |
2 | 1 | a1i 9 |
. . 3
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) |
3 | | oveq1 5789 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![( (](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) ![) )](rp.gif) |
4 | 3 | fveq2d 5433 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
5 | | 3lt4 8916 |
. . . . . . 7
![4 4](4.gif) |
6 | | 3nn0 9019 |
. . . . . . . 8
![NN0 NN0](_bbn0.gif) |
7 | | 4nn 8907 |
. . . . . . . 8
![NN NN](bbn.gif) |
8 | | divfl0 10100 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
9 | 6, 7, 8 | mp2an 423 |
. . . . . . 7
![( (](lp.gif)
![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) ![0 0](0.gif) ![) )](rp.gif) |
10 | 5, 9 | mpbi 144 |
. . . . . 6
![( (](lp.gif) ![|_ |_](lfloor.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![0 0](0.gif) |
11 | 4, 10 | eqtrdi 2189 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![0 0](0.gif) ![) )](rp.gif) |
12 | 11 | oveq1d 5797 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | | 0p1e1 8858 |
. . . 4
![( (](lp.gif) ![1 1](1.gif) ![1 1](1.gif) |
14 | 12, 13 | eqtrdi 2189 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![1 1](1.gif) ![) )](rp.gif) |
15 | | oveq1 5789 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
16 | | 3m1e2 8864 |
. . . . . 6
![( (](lp.gif) ![1 1](1.gif) ![2 2](2.gif) |
17 | 15, 16 | eqtrdi 2189 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) |
18 | 17 | oveq1d 5797 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
19 | | 2div2e1 8876 |
. . . 4
![( (](lp.gif) ![2 2](2.gif) ![1 1](1.gif) |
20 | 18, 19 | eqtrdi 2189 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![1 1](1.gif) ![) )](rp.gif) |
21 | 2, 14, 20 | 3brtr4d 3968 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) |
22 | | uzp1 9383 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![5 5](5.gif)
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
23 | | 2re 8814 |
. . . . . . 7
![RR RR](bbr.gif) |
24 | 23 | leidi 8271 |
. . . . . 6
![2 2](2.gif) |
25 | 24 | a1i 9 |
. . . . 5
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) |
26 | | oveq1 5789 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![( (](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) ![) )](rp.gif) |
27 | 26 | fveq2d 5433 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
28 | | df-5 8806 |
. . . . . . . . . . . 12
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) |
29 | 28 | oveq1i 5792 |
. . . . . . . . . . 11
![( (](lp.gif) ![4 4](4.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![4 4](4.gif) ![)
)](rp.gif) |
30 | | 4cn 8822 |
. . . . . . . . . . . . 13
![CC CC](bbc.gif) |
31 | | ax-1cn 7737 |
. . . . . . . . . . . . 13
![CC CC](bbc.gif) |
32 | | 4ap0 8843 |
. . . . . . . . . . . . 13
# ![0 0](0.gif) |
33 | 30, 31, 30, 32 | divdirapi 8553 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![4 4](4.gif) ![( (](lp.gif) ![( (](lp.gif) ![4
4](4.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![) )](rp.gif) |
34 | 30, 32 | dividapi 8529 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![4 4](4.gif) ![1 1](1.gif) |
35 | 34 | oveq1i 5792 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![) )](rp.gif) |
36 | 33, 35 | eqtri 2161 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![4 4](4.gif) ![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | 29, 36 | eqtri 2161 |
. . . . . . . . . 10
![( (](lp.gif) ![4 4](4.gif) ![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | 37 | fveq2i 5432 |
. . . . . . . . 9
![( (](lp.gif) ![|_ |_](lfloor.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
39 | | 1re 7789 |
. . . . . . . . . . 11
![RR RR](bbr.gif) |
40 | | 0le1 8267 |
. . . . . . . . . . 11
![1 1](1.gif) |
41 | | 4re 8821 |
. . . . . . . . . . 11
![RR RR](bbr.gif) |
42 | | 4pos 8841 |
. . . . . . . . . . 11
![4 4](4.gif) |
43 | | divge0 8655 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif)
![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![) )](rp.gif) |
44 | 39, 40, 41, 42, 43 | mp4an 424 |
. . . . . . . . . 10
![( (](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) |
45 | | 1lt4 8918 |
. . . . . . . . . . 11
![4 4](4.gif) |
46 | | recgt1 8679 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![(
(](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
47 | 41, 42, 46 | mp2an 423 |
. . . . . . . . . . 11
![( (](lp.gif)
![( (](lp.gif) ![4 4](4.gif) ![1 1](1.gif) ![) )](rp.gif) |
48 | 45, 47 | mpbi 144 |
. . . . . . . . . 10
![( (](lp.gif) ![4 4](4.gif) ![1 1](1.gif) |
49 | | 1z 9104 |
. . . . . . . . . . 11
![ZZ ZZ](bbz.gif) |
50 | | znq 9443 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![( (](lp.gif) ![4 4](4.gif) ![QQ QQ](bbq.gif) ![) )](rp.gif) |
51 | 49, 7, 50 | mp2an 423 |
. . . . . . . . . . 11
![( (](lp.gif) ![4 4](4.gif) ![QQ QQ](bbq.gif) |
52 | | flqbi2 10095 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![QQ QQ](bbq.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![4 4](4.gif)
![( (](lp.gif) ![4 4](4.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
53 | 49, 51, 52 | mp2an 423 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![4
4](4.gif) ![( (](lp.gif) ![4 4](4.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
54 | 44, 48, 53 | mpbir2an 927 |
. . . . . . . . 9
![( (](lp.gif) ![|_ |_](lfloor.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) ![) )](rp.gif) ![1 1](1.gif) |
55 | 38, 54 | eqtri 2161 |
. . . . . . . 8
![( (](lp.gif) ![|_ |_](lfloor.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![1 1](1.gif) |
56 | 27, 55 | eqtrdi 2189 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) |
57 | 56 | oveq1d 5797 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
58 | | 1p1e2 8861 |
. . . . . 6
![( (](lp.gif) ![1 1](1.gif) ![2 2](2.gif) |
59 | 57, 58 | eqtrdi 2189 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) |
60 | | oveq1 5789 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
61 | 30, 31, 28 | mvrraddi 8003 |
. . . . . . . 8
![( (](lp.gif) ![1 1](1.gif) ![4 4](4.gif) |
62 | 60, 61 | eqtrdi 2189 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![4 4](4.gif) ![) )](rp.gif) |
63 | 62 | oveq1d 5797 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
64 | | 4d2e2 8904 |
. . . . . 6
![( (](lp.gif) ![2 2](2.gif) ![2 2](2.gif) |
65 | 63, 64 | eqtrdi 2189 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![2 2](2.gif) ![) )](rp.gif) |
66 | 25, 59, 65 | 3brtr4d 3968 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) |
67 | | eluz2 9356 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![6 6](6.gif) ![( (](lp.gif) ![N N](_cn.gif) ![) )](rp.gif) ![) )](rp.gif) |
68 | | znq 9443 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![NN NN](bbn.gif) ![( (](lp.gif) ![4 4](4.gif) ![QQ QQ](bbq.gif) ![) )](rp.gif) |
69 | 7, 68 | mpan2 422 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![QQ QQ](bbq.gif) ![) )](rp.gif) |
70 | | flqle 10082 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![(
(](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) ![) )](rp.gif) |
71 | 69, 70 | syl 14 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![(
(](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) ![) )](rp.gif) |
72 | 71 | adantr 274 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![(
(](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![) )](rp.gif) |
73 | 69 | flqcld 10081 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
74 | 73 | zred 9197 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
75 | | zre 9082 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
76 | | id 19 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
77 | 41 | a1i 9 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
78 | 32 | a1i 9 |
. . . . . . . . . . . . . 14
![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) |
79 | 76, 77, 78 | redivclapd 8618 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
80 | 75, 79 | syl 14 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
81 | 39 | a1i 9 |
. . . . . . . . . . . 12
![( (](lp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
82 | 74, 80, 81 | 3jca 1162 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![( (](lp.gif) ![4 4](4.gif) ![RR RR](bbr.gif) ![) )](rp.gif) ![) )](rp.gif) |
83 | 82 | adantr 274 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![(
(](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif)
![4 4](4.gif) ![)
)](rp.gif) ![( (](lp.gif) ![4 4](4.gif)
![RR RR](bbr.gif) ![) )](rp.gif) ![)
)](rp.gif) |
84 | | leadd1 8216 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![( (](lp.gif) ![4 4](4.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![( (](lp.gif) ![4
4](4.gif)
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![(
(](lp.gif) ![4 4](4.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
85 | 83, 84 | syl 14 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![(
(](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif)
![4 4](4.gif) ![)
)](rp.gif) ![( (](lp.gif) ![4 4](4.gif)
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![(
(](lp.gif) ![4 4](4.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
86 | 72, 85 | mpbid 146 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![(
(](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif)
![4 4](4.gif) ![)
)](rp.gif) ![1 1](1.gif)
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
87 | | div4p1lem1div2 8997 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![(
(](lp.gif) ![( (](lp.gif) ![4
4](4.gif) ![1 1](1.gif)
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
88 | 75, 87 | sylan 281 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![(
(](lp.gif) ![( (](lp.gif) ![4
4](4.gif) ![1 1](1.gif)
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
89 | | peano2re 7922 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
90 | 74, 89 | syl 14 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
91 | | peano2re 7922 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![( (](lp.gif) ![(
(](lp.gif) ![4 4](4.gif) ![1 1](1.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
92 | 80, 91 | syl 14 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![4 4](4.gif) ![1 1](1.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
93 | | peano2rem 8053 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
94 | 93 | rehalfcld 8990 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
95 | 75, 94 | syl 14 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
96 | 90, 92, 95 | 3jca 1162 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif)
![4 4](4.gif) ![)
)](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![4
4](4.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![) )](rp.gif) ![) )](rp.gif) |
97 | 96 | adantr 274 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![4
4](4.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![) )](rp.gif) ![) )](rp.gif) |
98 | | letr 7871 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif)
![4 4](4.gif) ![)
)](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![4
4](4.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![(
(](lp.gif) ![( (](lp.gif) ![4
4](4.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![1 1](1.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
99 | 97, 98 | syl 14 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![(
(](lp.gif) ![( (](lp.gif) ![4
4](4.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![1 1](1.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
100 | 86, 88, 99 | mp2and 430 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![N N](_cn.gif) ![(
(](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif)
![4 4](4.gif) ![)
)](rp.gif) ![1 1](1.gif)
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
101 | 100 | 3adant1 1000 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![N N](_cn.gif) ![( (](lp.gif) ![(
(](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1
1](1.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) |
102 | 67, 101 | sylbi 120 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![6 6](6.gif)
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
103 | | 5p1e6 8881 |
. . . . . 6
![( (](lp.gif) ![1 1](1.gif) ![6 6](6.gif) |
104 | 103 | fveq2i 5432 |
. . . . 5
![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![ZZ>=
ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![6 6](6.gif) ![) )](rp.gif) |
105 | 102, 104 | eleq2s 2235 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
106 | 66, 105 | jaoi 706 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif)
![4 4](4.gif) ![)
)](rp.gif) ![1 1](1.gif)
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
107 | 22, 106 | syl 14 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![5 5](5.gif)
![( (](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
108 | 21, 107 | jaoi 706 |
1
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![ZZ>= ZZ>=](_bbzge.gif) ![` `](backtick.gif) ![5
5](5.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![|_ |_](lfloor.gif) ![` `](backtick.gif) ![( (](lp.gif)
![4 4](4.gif) ![)
)](rp.gif) ![1 1](1.gif)
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |