Proof of Theorem fldiv4p1lem1div2
Step | Hyp | Ref
| Expression |
1 | | 1le1 7563 |
. . . 4
|
2 | 1 | a1i 9 |
. . 3
|
3 | | oveq1 5519 |
. . . . . . 7
|
4 | 3 | fveq2d 5182 |
. . . . . 6
|
5 | | 3lt4 8089 |
. . . . . . 7
|
6 | | 3nn0 8199 |
. . . . . . . 8
|
7 | | 4nn 8079 |
. . . . . . . 8
|
8 | | divfl0 9138 |
. . . . . . . 8
|
9 | 6, 7, 8 | mp2an 402 |
. . . . . . 7
|
10 | 5, 9 | mpbi 133 |
. . . . . 6
|
11 | 4, 10 | syl6eq 2088 |
. . . . 5
|
12 | 11 | oveq1d 5527 |
. . . 4
|
13 | | 0p1e1 8031 |
. . . 4
|
14 | 12, 13 | syl6eq 2088 |
. . 3
|
15 | | oveq1 5519 |
. . . . . 6
|
16 | | 3m1e2 8036 |
. . . . . 6
|
17 | 15, 16 | syl6eq 2088 |
. . . . 5
|
18 | 17 | oveq1d 5527 |
. . . 4
|
19 | | 2div2e1 8042 |
. . . 4
|
20 | 18, 19 | syl6eq 2088 |
. . 3
|
21 | 2, 14, 20 | 3brtr4d 3794 |
. 2
|
22 | | uzp1 8506 |
. . 3
|
23 | | 2re 7985 |
. . . . . . 7
|
24 | 23 | leidi 7477 |
. . . . . 6
|
25 | 24 | a1i 9 |
. . . . 5
|
26 | | oveq1 5519 |
. . . . . . . . 9
|
27 | 26 | fveq2d 5182 |
. . . . . . . 8
|
28 | | df-5 7976 |
. . . . . . . . . . . 12
|
29 | 28 | oveq1i 5522 |
. . . . . . . . . . 11
|
30 | | 4cn 7993 |
. . . . . . . . . . . . 13
|
31 | | ax-1cn 6977 |
. . . . . . . . . . . . 13
|
32 | | 4ap0 8015 |
. . . . . . . . . . . . 13
# |
33 | 30, 31, 30, 32 | divdirapi 7745 |
. . . . . . . . . . . 12
|
34 | 30, 32 | dividapi 7721 |
. . . . . . . . . . . . 13
|
35 | 34 | oveq1i 5522 |
. . . . . . . . . . . 12
|
36 | 33, 35 | eqtri 2060 |
. . . . . . . . . . 11
|
37 | 29, 36 | eqtri 2060 |
. . . . . . . . . 10
|
38 | 37 | fveq2i 5181 |
. . . . . . . . 9
|
39 | | 1re 7026 |
. . . . . . . . . . 11
|
40 | | 0le1 7476 |
. . . . . . . . . . 11
|
41 | | 4re 7992 |
. . . . . . . . . . 11
|
42 | | 4pos 8013 |
. . . . . . . . . . 11
|
43 | | divge0 7839 |
. . . . . . . . . . 11
|
44 | 39, 40, 41, 42, 43 | mp4an 403 |
. . . . . . . . . 10
|
45 | | 1lt4 8091 |
. . . . . . . . . . 11
|
46 | | recgt1 7863 |
. . . . . . . . . . . 12
|
47 | 41, 42, 46 | mp2an 402 |
. . . . . . . . . . 11
|
48 | 45, 47 | mpbi 133 |
. . . . . . . . . 10
|
49 | | 1z 8271 |
. . . . . . . . . . 11
|
50 | | znq 8559 |
. . . . . . . . . . . 12
|
51 | 49, 7, 50 | mp2an 402 |
. . . . . . . . . . 11
|
52 | | flqbi2 9133 |
. . . . . . . . . . 11
|
53 | 49, 51, 52 | mp2an 402 |
. . . . . . . . . 10
|
54 | 44, 48, 53 | mpbir2an 849 |
. . . . . . . . 9
|
55 | 38, 54 | eqtri 2060 |
. . . . . . . 8
|
56 | 27, 55 | syl6eq 2088 |
. . . . . . 7
|
57 | 56 | oveq1d 5527 |
. . . . . 6
|
58 | | 1p1e2 8033 |
. . . . . 6
|
59 | 57, 58 | syl6eq 2088 |
. . . . 5
|
60 | | oveq1 5519 |
. . . . . . . 8
|
61 | 30, 31, 28 | mvrraddi 7228 |
. . . . . . . 8
|
62 | 60, 61 | syl6eq 2088 |
. . . . . . 7
|
63 | 62 | oveq1d 5527 |
. . . . . 6
|
64 | | 4d2e2 8076 |
. . . . . 6
|
65 | 63, 64 | syl6eq 2088 |
. . . . 5
|
66 | 25, 59, 65 | 3brtr4d 3794 |
. . . 4
|
67 | | eluz2 8479 |
. . . . . 6
|
68 | | znq 8559 |
. . . . . . . . . . . 12
|
69 | 7, 68 | mpan2 401 |
. . . . . . . . . . 11
|
70 | | flqle 9120 |
. . . . . . . . . . 11
|
71 | 69, 70 | syl 14 |
. . . . . . . . . 10
|
72 | 71 | adantr 261 |
. . . . . . . . 9
|
73 | 69 | flqcld 9119 |
. . . . . . . . . . . . 13
|
74 | 73 | zred 8360 |
. . . . . . . . . . . 12
|
75 | | zre 8249 |
. . . . . . . . . . . . 13
|
76 | | id 19 |
. . . . . . . . . . . . . 14
|
77 | 41 | a1i 9 |
. . . . . . . . . . . . . 14
|
78 | 32 | a1i 9 |
. . . . . . . . . . . . . 14
# |
79 | 76, 77, 78 | redivclapd 7808 |
. . . . . . . . . . . . 13
|
80 | 75, 79 | syl 14 |
. . . . . . . . . . . 12
|
81 | 39 | a1i 9 |
. . . . . . . . . . . 12
|
82 | 74, 80, 81 | 3jca 1084 |
. . . . . . . . . . 11
|
83 | 82 | adantr 261 |
. . . . . . . . . 10
|
84 | | leadd1 7425 |
. . . . . . . . . 10
|
85 | 83, 84 | syl 14 |
. . . . . . . . 9
|
86 | 72, 85 | mpbid 135 |
. . . . . . . 8
|
87 | | div4p1lem1div2 8177 |
. . . . . . . . 9
|
88 | 75, 87 | sylan 267 |
. . . . . . . 8
|
89 | | peano2re 7149 |
. . . . . . . . . . . 12
|
90 | 74, 89 | syl 14 |
. . . . . . . . . . 11
|
91 | | peano2re 7149 |
. . . . . . . . . . . 12
|
92 | 80, 91 | syl 14 |
. . . . . . . . . . 11
|
93 | | peano2rem 7278 |
. . . . . . . . . . . . 13
|
94 | 93 | rehalfcld 8171 |
. . . . . . . . . . . 12
|
95 | 75, 94 | syl 14 |
. . . . . . . . . . 11
|
96 | 90, 92, 95 | 3jca 1084 |
. . . . . . . . . 10
|
97 | 96 | adantr 261 |
. . . . . . . . 9
|
98 | | letr 7101 |
. . . . . . . . 9
|
99 | 97, 98 | syl 14 |
. . . . . . . 8
|
100 | 86, 88, 99 | mp2and 409 |
. . . . . . 7
|
101 | 100 | 3adant1 922 |
. . . . . 6
|
102 | 67, 101 | sylbi 114 |
. . . . 5
|
103 | | 5p1e6 8047 |
. . . . . 6
|
104 | 103 | fveq2i 5181 |
. . . . 5
|
105 | 102, 104 | eleq2s 2132 |
. . . 4
|
106 | 66, 105 | jaoi 636 |
. . 3
|
107 | 22, 106 | syl 14 |
. 2
|
108 | 21, 107 | jaoi 636 |
1
|