Proof of Theorem fldiv4p1lem1div2
Step | Hyp | Ref
| Expression |
1 | | 1le1 8519 |
. . . 4
![1 1](1.gif) |
2 | 1 | a1i 9 |
. . 3
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) |
3 | | oveq1 5876 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![( (](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) ![) )](rp.gif) |
4 | 3 | fveq2d 5515 |
. . . . . 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 9080 |
. . . . . . 7
![4 4](4.gif) |
6 | | 3nn0 9183 |
. . . . . . . 8
![NN0 NN0](_bbn0.gif) |
7 | | 4nn 9071 |
. . . . . . . 8
![NN NN](bbn.gif) |
8 | | divfl0 10282 |
. . . . . . . 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 426 |
. . . . . . 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 145 |
. . . . . 6
![( (](lp.gif) ![|_ |_](lfloor.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![0 0](0.gif) |
11 | 4, 10 | eqtrdi 2226 |
. . . . 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 5884 |
. . . 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 9022 |
. . . 4
![( (](lp.gif) ![1 1](1.gif) ![1 1](1.gif) |
14 | 12, 13 | eqtrdi 2226 |
. . 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 5876 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
16 | | 3m1e2 9028 |
. . . . . 6
![( (](lp.gif) ![1 1](1.gif) ![2 2](2.gif) |
17 | 15, 16 | eqtrdi 2226 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![2 2](2.gif) ![) )](rp.gif) |
18 | 17 | oveq1d 5884 |
. . . 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 9040 |
. . . 4
![( (](lp.gif) ![2 2](2.gif) ![1 1](1.gif) |
20 | 18, 19 | eqtrdi 2226 |
. . 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 4032 |
. 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 9550 |
. . 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 8978 |
. . . . . . 7
![RR RR](bbr.gif) |
24 | 23 | leidi 8432 |
. . . . . 6
![2 2](2.gif) |
25 | 24 | a1i 9 |
. . . . 5
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) |
26 | | oveq1 5876 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![( (](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) ![) )](rp.gif) |
27 | 26 | fveq2d 5515 |
. . . . . . . 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 8970 |
. . . . . . . . . . . 12
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) |
29 | 28 | oveq1i 5879 |
. . . . . . . . . . 11
![( (](lp.gif) ![4 4](4.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![4 4](4.gif) ![)
)](rp.gif) |
30 | | 4cn 8986 |
. . . . . . . . . . . . 13
![CC CC](bbc.gif) |
31 | | ax-1cn 7895 |
. . . . . . . . . . . . 13
![CC CC](bbc.gif) |
32 | | 4ap0 9007 |
. . . . . . . . . . . . 13
# ![0 0](0.gif) |
33 | 30, 31, 30, 32 | divdirapi 8715 |
. . . . . . . . . . . 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 8691 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![4 4](4.gif) ![1 1](1.gif) |
35 | 34 | oveq1i 5879 |
. . . . . . . . . . . 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 2198 |
. . . . . . . . . . 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 2198 |
. . . . . . . . . 10
![( (](lp.gif) ![4 4](4.gif) ![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | 37 | fveq2i 5514 |
. . . . . . . . 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 7947 |
. . . . . . . . . . 11
![RR RR](bbr.gif) |
40 | | 0le1 8428 |
. . . . . . . . . . 11
![1 1](1.gif) |
41 | | 4re 8985 |
. . . . . . . . . . 11
![RR RR](bbr.gif) |
42 | | 4pos 9005 |
. . . . . . . . . . 11
![4 4](4.gif) |
43 | | divge0 8819 |
. . . . . . . . . . 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 427 |
. . . . . . . . . 10
![( (](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) |
45 | | 1lt4 9082 |
. . . . . . . . . . 11
![4 4](4.gif) |
46 | | recgt1 8843 |
. . . . . . . . . . . 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 426 |
. . . . . . . . . . 11
![( (](lp.gif)
![( (](lp.gif) ![4 4](4.gif) ![1 1](1.gif) ![) )](rp.gif) |
48 | 45, 47 | mpbi 145 |
. . . . . . . . . 10
![( (](lp.gif) ![4 4](4.gif) ![1 1](1.gif) |
49 | | 1z 9268 |
. . . . . . . . . . 11
![ZZ ZZ](bbz.gif) |
50 | | znq 9613 |
. . . . . . . . . . . 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 426 |
. . . . . . . . . . 11
![( (](lp.gif) ![4 4](4.gif) ![QQ QQ](bbq.gif) |
52 | | flqbi2 10277 |
. . . . . . . . . . 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 426 |
. . . . . . . . . 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 942 |
. . . . . . . . 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 2198 |
. . . . . . . 8
![( (](lp.gif) ![|_ |_](lfloor.gif) ![`
`](backtick.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) ![1 1](1.gif) |
56 | 27, 55 | eqtrdi 2226 |
. . . . . . 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 5884 |
. . . . . 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 9025 |
. . . . . 6
![( (](lp.gif) ![1 1](1.gif) ![2 2](2.gif) |
59 | 57, 58 | eqtrdi 2226 |
. . . . 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 5876 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
61 | 30, 31, 28 | mvrraddi 8164 |
. . . . . . . 8
![( (](lp.gif) ![1 1](1.gif) ![4 4](4.gif) |
62 | 60, 61 | eqtrdi 2226 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![4 4](4.gif) ![) )](rp.gif) |
63 | 62 | oveq1d 5884 |
. . . . . 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 9068 |
. . . . . 6
![( (](lp.gif) ![2 2](2.gif) ![2 2](2.gif) |
65 | 63, 64 | eqtrdi 2226 |
. . . . 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 4032 |
. . . 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 9523 |
. . . . . 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 9613 |
. . . . . . . . . . . 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 425 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![QQ QQ](bbq.gif) ![) )](rp.gif) |
70 | | flqle 10264 |
. . . . . . . . . . 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 276 |
. . . . . . . . 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 10263 |
. . . . . . . . . . . . 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 9364 |
. . . . . . . . . . . 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 9246 |
. . . . . . . . . . . . 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 8781 |
. . . . . . . . . . . . 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 1177 |
. . . . . . . . . . 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 276 |
. . . . . . . . . 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 8377 |
. . . . . . . . . 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 147 |
. . . . . . . 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 9161 |
. . . . . . . . 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 283 |
. . . . . . . 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 8083 |
. . . . . . . . . . . 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 8083 |
. . . . . . . . . . . 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 8214 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![1 1](1.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
94 | 93 | rehalfcld 9154 |
. . . . . . . . . . . 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 1177 |
. . . . . . . . . 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 276 |
. . . . . . . . 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 8030 |
. . . . . . . . 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 433 |
. . . . . . 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 1015 |
. . . . . 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 121 |
. . . . 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 9045 |
. . . . . 6
![( (](lp.gif) ![1 1](1.gif) ![6 6](6.gif) |
104 | 103 | fveq2i 5514 |
. . . . 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 2272 |
. . . 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 716 |
. . 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 716 |
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) |