Proof of Theorem fldiv4p1lem1div2
Step | Hyp | Ref
| Expression |
1 | | 1le1 8528 |
. . . 4
 |
2 | 1 | a1i 9 |
. . 3
   |
3 | | oveq1 5881 |
. . . . . . 7
       |
4 | 3 | fveq2d 5519 |
. . . . . 6
               |
5 | | 3lt4 9090 |
. . . . . . 7
 |
6 | | 3nn0 9193 |
. . . . . . . 8
 |
7 | | 4nn 9081 |
. . . . . . . 8
 |
8 | | divfl0 10295 |
. . . . . . . 8
 
           |
9 | 6, 7, 8 | mp2an 426 |
. . . . . . 7

        |
10 | 5, 9 | mpbi 145 |
. . . . . 6
       |
11 | 4, 10 | eqtrdi 2226 |
. . . . 5
         |
12 | 11 | oveq1d 5889 |
. . . 4
             |
13 | | 0p1e1 9032 |
. . . 4
   |
14 | 12, 13 | eqtrdi 2226 |
. . 3
           |
15 | | oveq1 5881 |
. . . . . 6
 
     |
16 | | 3m1e2 9038 |
. . . . . 6
   |
17 | 15, 16 | eqtrdi 2226 |
. . . . 5
 
   |
18 | 17 | oveq1d 5889 |
. . . 4
         |
19 | | 2div2e1 9050 |
. . . 4
   |
20 | 18, 19 | eqtrdi 2226 |
. . 3
       |
21 | 2, 14, 20 | 3brtr4d 4035 |
. 2
               |
22 | | uzp1 9560 |
. . 3
    
          |
23 | | 2re 8988 |
. . . . . . 7
 |
24 | 23 | leidi 8441 |
. . . . . 6
 |
25 | 24 | a1i 9 |
. . . . 5
   |
26 | | oveq1 5881 |
. . . . . . . . 9
       |
27 | 26 | fveq2d 5519 |
. . . . . . . 8
               |
28 | | df-5 8980 |
. . . . . . . . . . . 12
   |
29 | 28 | oveq1i 5884 |
. . . . . . . . . . 11
       |
30 | | 4cn 8996 |
. . . . . . . . . . . . 13
 |
31 | | ax-1cn 7903 |
. . . . . . . . . . . . 13
 |
32 | | 4ap0 9017 |
. . . . . . . . . . . . 13
#  |
33 | 30, 31, 30, 32 | divdirapi 8725 |
. . . . . . . . . . . 12
           |
34 | 30, 32 | dividapi 8701 |
. . . . . . . . . . . . 13
   |
35 | 34 | oveq1i 5884 |
. . . . . . . . . . . 12
           |
36 | 33, 35 | eqtri 2198 |
. . . . . . . . . . 11
         |
37 | 29, 36 | eqtri 2198 |
. . . . . . . . . 10
       |
38 | 37 | fveq2i 5518 |
. . . . . . . . 9
               |
39 | | 1re 7955 |
. . . . . . . . . . 11
 |
40 | | 0le1 8437 |
. . . . . . . . . . 11
 |
41 | | 4re 8995 |
. . . . . . . . . . 11
 |
42 | | 4pos 9015 |
. . . . . . . . . . 11
 |
43 | | divge0 8829 |
. . . . . . . . . . 11
  
   
    |
44 | 39, 40, 41, 42, 43 | mp4an 427 |
. . . . . . . . . 10
   |
45 | | 1lt4 9092 |
. . . . . . . . . . 11
 |
46 | | recgt1 8853 |
. . . . . . . . . . . 12
         |
47 | 41, 42, 46 | mp2an 426 |
. . . . . . . . . . 11

    |
48 | 45, 47 | mpbi 145 |
. . . . . . . . . 10
   |
49 | | 1z 9278 |
. . . . . . . . . . 11
 |
50 | | znq 9623 |
. . . . . . . . . . . 12
 
     |
51 | 49, 7, 50 | mp2an 426 |
. . . . . . . . . . 11
   |
52 | | flqbi2 10290 |
. . . . . . . . . . 11
                
      |
53 | 49, 51, 52 | mp2an 426 |
. . . . . . . . . 10
        
        |
54 | 44, 48, 53 | mpbir2an 942 |
. . . . . . . . 9
         |
55 | 38, 54 | eqtri 2198 |
. . . . . . . 8
       |
56 | 27, 55 | eqtrdi 2226 |
. . . . . . 7
         |
57 | 56 | oveq1d 5889 |
. . . . . 6
             |
58 | | 1p1e2 9035 |
. . . . . 6
   |
59 | 57, 58 | eqtrdi 2226 |
. . . . 5
           |
60 | | oveq1 5881 |
. . . . . . . 8
 
     |
61 | 30, 31, 28 | mvrraddi 8173 |
. . . . . . . 8
   |
62 | 60, 61 | eqtrdi 2226 |
. . . . . . 7
 
   |
63 | 62 | oveq1d 5889 |
. . . . . 6
         |
64 | | 4d2e2 9078 |
. . . . . 6
   |
65 | 63, 64 | eqtrdi 2226 |
. . . . 5
       |
66 | 25, 59, 65 | 3brtr4d 4035 |
. . . 4
               |
67 | | eluz2 9533 |
. . . . . 6
         |
68 | | znq 9623 |
. . . . . . . . . . . 12
 
     |
69 | 7, 68 | mpan2 425 |
. . . . . . . . . . 11
     |
70 | | flqle 10277 |
. . . . . . . . . . 11
             |
71 | 69, 70 | syl 14 |
. . . . . . . . . 10
           |
72 | 71 | adantr 276 |
. . . . . . . . 9
             |
73 | 69 | flqcld 10276 |
. . . . . . . . . . . . 13
         |
74 | 73 | zred 9374 |
. . . . . . . . . . . 12
         |
75 | | zre 9256 |
. . . . . . . . . . . . 13
   |
76 | | id 19 |
. . . . . . . . . . . . . 14
   |
77 | 41 | a1i 9 |
. . . . . . . . . . . . . 14
   |
78 | 32 | a1i 9 |
. . . . . . . . . . . . . 14
 #   |
79 | 76, 77, 78 | redivclapd 8791 |
. . . . . . . . . . . . 13
     |
80 | 75, 79 | syl 14 |
. . . . . . . . . . . 12
     |
81 | 39 | a1i 9 |
. . . . . . . . . . . 12
   |
82 | 74, 80, 81 | 3jca 1177 |
. . . . . . . . . . 11
             |
83 | 82 | adantr 276 |
. . . . . . . . . 10
       
   
   |
84 | | leadd1 8386 |
. . . . . . . . . 10
                   
               |
85 | 83, 84 | syl 14 |
. . . . . . . . 9
       
   
               |
86 | 72, 85 | mpbid 147 |
. . . . . . . 8
       
  
      |
87 | | div4p1lem1div2 9171 |
. . . . . . . . 9
      
 
    |
88 | 75, 87 | sylan 283 |
. . . . . . . 8
      
 
    |
89 | | peano2re 8092 |
. . . . . . . . . . . 12
                 |
90 | 74, 89 | syl 14 |
. . . . . . . . . . 11
           |
91 | | peano2re 8092 |
. . . . . . . . . . . 12
         |
92 | 80, 91 | syl 14 |
. . . . . . . . . . 11
       |
93 | | peano2rem 8223 |
. . . . . . . . . . . . 13
 
   |
94 | 93 | rehalfcld 9164 |
. . . . . . . . . . . 12
       |
95 | 75, 94 | syl 14 |
. . . . . . . . . . 11
       |
96 | 90, 92, 95 | 3jca 1177 |
. . . . . . . . . 10
      
              |
97 | 96 | adantr 276 |
. . . . . . . . 9
                       |
98 | | letr 8039 |
. . . . . . . . 9
      
                                                  |
99 | 97, 98 | syl 14 |
. . . . . . . 8
                                         |
100 | 86, 88, 99 | mp2and 433 |
. . . . . . 7
       
  
 
    |
101 | 100 | 3adant1 1015 |
. . . . . 6
 
               |
102 | 67, 101 | sylbi 121 |
. . . . 5
    
              |
103 | | 5p1e6 9055 |
. . . . . 6
   |
104 | 103 | fveq2i 5518 |
. . . . 5
           |
105 | 102, 104 | eleq2s 2272 |
. . . 4
      
              |
106 | 66, 105 | jaoi 716 |
. . 3
             
  
 
    |
107 | 22, 106 | syl 14 |
. 2
    
              |
108 | 21, 107 | jaoi 716 |
1
           
  
 
    |