Step | Hyp | Ref
| Expression |
1 | | oveq1 5881 |
. . . 4
               |
2 | | 2cnd 8991 |
. . . . . . 7
   |
3 | | zcn 9257 |
. . . . . . 7
   |
4 | 2, 3 | mulcld 7977 |
. . . . . 6
     |
5 | | 1cnd 7972 |
. . . . . 6
   |
6 | | 4cn 8996 |
. . . . . . 7
 |
7 | 6 | a1i 9 |
. . . . . 6
   |
8 | | 4ap0 9017 |
. . . . . . 7
#  |
9 | 8 | a1i 9 |
. . . . . 6
 #   |
10 | 4, 5, 7, 9 | divdirapd 8785 |
. . . . 5
                 |
11 | | 2t2e4 9072 |
. . . . . . . . . 10
   |
12 | 11 | eqcomi 2181 |
. . . . . . . . 9
   |
13 | 12 | a1i 9 |
. . . . . . . 8
     |
14 | 13 | oveq2d 5890 |
. . . . . . 7
             |
15 | | 2ap0 9011 |
. . . . . . . . 9
#  |
16 | 15 | a1i 9 |
. . . . . . . 8
 #   |
17 | 3, 2, 2, 16, 16 | divcanap5d 8773 |
. . . . . . 7
           |
18 | 14, 17 | eqtrd 2210 |
. . . . . 6
         |
19 | 18 | oveq1d 5889 |
. . . . 5
                 |
20 | 10, 19 | eqtrd 2210 |
. . . 4
               |
21 | 1, 20 | sylan9eqr 2232 |
. . 3
 
               |
22 | 21 | fveq2d 5519 |
. 2
 
        
              |
23 | | iftrue 3539 |
. . . . . . . 8
                |
24 | 23 | adantr 276 |
. . . . . . 7
 
   
            |
25 | | 1re 7955 |
. . . . . . . . . 10
 |
26 | | 0le1 8437 |
. . . . . . . . . 10
 |
27 | | 4re 8995 |
. . . . . . . . . 10
 |
28 | | 4pos 9015 |
. . . . . . . . . 10
 |
29 | | divge0 8829 |
. . . . . . . . . 10
  
   
    |
30 | 25, 26, 27, 28, 29 | mp4an 427 |
. . . . . . . . 9
   |
31 | | 1lt4 9092 |
. . . . . . . . . 10
 |
32 | | recgt1 8853 |
. . . . . . . . . . 11
         |
33 | 27, 28, 32 | mp2an 426 |
. . . . . . . . . 10

    |
34 | 31, 33 | mpbi 145 |
. . . . . . . . 9
   |
35 | 30, 34 | pm3.2i 272 |
. . . . . . . 8
       |
36 | | evend2 11893 |
. . . . . . . . . 10
 
     |
37 | 36 | biimpac 298 |
. . . . . . . . 9
 
     |
38 | | 4nn 9081 |
. . . . . . . . . 10
 |
39 | | nnrecq 9644 |
. . . . . . . . . 10
     |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . 9
   |
41 | | flqbi2 10290 |
. . . . . . . . 9
                      
      |
42 | 37, 40, 41 | sylancl 413 |
. . . . . . . 8
 
                       |
43 | 35, 42 | mpbiri 168 |
. . . . . . 7
 
               |
44 | 24, 43 | eqtr4d 2213 |
. . . . . 6
 
   
                    |
45 | 44 | expcom 116 |
. . . . 5
 
                        |
46 | | iffalse 3542 |
. . . . . . . 8
                  |
47 | 46 | adantr 276 |
. . . . . . 7
 
                  |
48 | | odd2np1 11877 |
. . . . . . . . 9
 
        |
49 | | ax-1cn 7903 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
50 | | 2cn 8989 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
51 | 50, 15 | pm3.2i 272 |
. . . . . . . . . . . . . . . . . . . . . 22
 #   |
52 | | divcanap5 8670 |
. . . . . . . . . . . . . . . . . . . . . 22
   #   #             |
53 | 49, 51, 51, 52 | mp3an 1337 |
. . . . . . . . . . . . . . . . . . . . 21
         |
54 | | 2t1e2 9071 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
55 | 54, 11 | oveq12i 5886 |
. . . . . . . . . . . . . . . . . . . . 21
         |
56 | 53, 55 | eqtr3i 2200 |
. . . . . . . . . . . . . . . . . . . 20
     |
57 | 56 | oveq1i 5884 |
. . . . . . . . . . . . . . . . . . 19
             |
58 | 50, 49, 6, 8 | divdirapi 8725 |
. . . . . . . . . . . . . . . . . . 19
           |
59 | | 2p1e3 9051 |
. . . . . . . . . . . . . . . . . . . 20
   |
60 | 59 | oveq1i 5884 |
. . . . . . . . . . . . . . . . . . 19
       |
61 | 57, 58, 60 | 3eqtr2i 2204 |
. . . . . . . . . . . . . . . . . 18
         |
62 | 61 | a1i 9 |
. . . . . . . . . . . . . . . . 17
           |
63 | 62 | oveq2d 5890 |
. . . . . . . . . . . . . . . 16
               |
64 | 63 | fveq2d 5519 |
. . . . . . . . . . . . . . 15
                       |
65 | | 3re 8992 |
. . . . . . . . . . . . . . . . . 18
 |
66 | | 0re 7956 |
. . . . . . . . . . . . . . . . . . 19
 |
67 | | 3pos 9012 |
. . . . . . . . . . . . . . . . . . 19
 |
68 | 66, 65, 67 | ltleii 8059 |
. . . . . . . . . . . . . . . . . 18
 |
69 | | divge0 8829 |
. . . . . . . . . . . . . . . . . 18
  
   
    |
70 | 65, 68, 27, 28, 69 | mp4an 427 |
. . . . . . . . . . . . . . . . 17
   |
71 | | 3lt4 9090 |
. . . . . . . . . . . . . . . . . 18
 |
72 | | nnrp 9662 |
. . . . . . . . . . . . . . . . . . . 20
   |
73 | 38, 72 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
 |
74 | | divlt1lt 9723 |
. . . . . . . . . . . . . . . . . . 19
 
       |
75 | 65, 73, 74 | mp2an 426 |
. . . . . . . . . . . . . . . . . 18
  
  |
76 | 71, 75 | mpbir 146 |
. . . . . . . . . . . . . . . . 17
   |
77 | 70, 76 | pm3.2i 272 |
. . . . . . . . . . . . . . . 16
       |
78 | | 3z 9281 |
. . . . . . . . . . . . . . . . . 18
 |
79 | | znq 9623 |
. . . . . . . . . . . . . . . . . 18
 
     |
80 | 78, 38, 79 | mp2an 426 |
. . . . . . . . . . . . . . . . 17
   |
81 | | flqbi2 10290 |
. . . . . . . . . . . . . . . . 17
                
      |
82 | 80, 81 | mpan2 425 |
. . . . . . . . . . . . . . . 16
         
         |
83 | 77, 82 | mpbiri 168 |
. . . . . . . . . . . . . . 15
           |
84 | 64, 83 | eqtrd 2210 |
. . . . . . . . . . . . . 14
               |
85 | 84 | adantr 276 |
. . . . . . . . . . . . 13
          
          |
86 | | oveq1 5881 |
. . . . . . . . . . . . . . . . . 18
               |
87 | 86 | eqcoms 2180 |
. . . . . . . . . . . . . . . . 17
               |
88 | | 2z 9280 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
89 | 88 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . 21
   |
90 | | id 19 |
. . . . . . . . . . . . . . . . . . . . 21
   |
91 | 89, 90 | zmulcld 9380 |
. . . . . . . . . . . . . . . . . . . 20
     |
92 | 91 | zcnd 9375 |
. . . . . . . . . . . . . . . . . . 19
     |
93 | | 1cnd 7972 |
. . . . . . . . . . . . . . . . . . 19
   |
94 | | 2cnd 8991 |
. . . . . . . . . . . . . . . . . . 19
   |
95 | 15 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
 #   |
96 | 92, 93, 94, 95 | divdirapd 8785 |
. . . . . . . . . . . . . . . . . 18
                 |
97 | | zcn 9257 |
. . . . . . . . . . . . . . . . . . . 20
   |
98 | 97, 94, 95 | divcanap3d 8751 |
. . . . . . . . . . . . . . . . . . 19
       |
99 | 98 | oveq1d 5889 |
. . . . . . . . . . . . . . . . . 18
               |
100 | 96, 99 | eqtrd 2210 |
. . . . . . . . . . . . . . . . 17
             |
101 | 87, 100 | sylan9eqr 2232 |
. . . . . . . . . . . . . . . 16
               |
102 | 101 | oveq1d 5889 |
. . . . . . . . . . . . . . 15
                       |
103 | | halfcn 9132 |
. . . . . . . . . . . . . . . . . 18
   |
104 | 103 | a1i 9 |
. . . . . . . . . . . . . . . . 17
     |
105 | 6, 8 | recclapi 8698 |
. . . . . . . . . . . . . . . . . 18
   |
106 | 105 | a1i 9 |
. . . . . . . . . . . . . . . . 17
     |
107 | 97, 104, 106 | addassd 7979 |
. . . . . . . . . . . . . . . 16
                   |
108 | 107 | adantr 276 |
. . . . . . . . . . . . . . 15
                         |
109 | 102, 108 | eqtrd 2210 |
. . . . . . . . . . . . . 14
                       |
110 | 109 | fveq2d 5519 |
. . . . . . . . . . . . 13
                               |
111 | | oveq1 5881 |
. . . . . . . . . . . . . . . . 17
     
         |
112 | 111 | eqcoms 2180 |
. . . . . . . . . . . . . . . 16
     
         |
113 | | pncan1 8333 |
. . . . . . . . . . . . . . . . 17
             |
114 | 92, 113 | syl 14 |
. . . . . . . . . . . . . . . 16
           |
115 | 112, 114 | sylan9eqr 2232 |
. . . . . . . . . . . . . . 15
             |
116 | 115 | oveq1d 5889 |
. . . . . . . . . . . . . 14
                 |
117 | 98 | adantr 276 |
. . . . . . . . . . . . . 14
             |
118 | 116, 117 | eqtrd 2210 |
. . . . . . . . . . . . 13
             |
119 | 85, 110, 118 | 3eqtr4rd 2221 |
. . . . . . . . . . . 12
                       |
120 | 119 | ex 115 |
. . . . . . . . . . 11
                       |
121 | 120 | adantl 277 |
. . . . . . . . . 10
 
                       |
122 | 121 | rexlimdva 2594 |
. . . . . . . . 9
  
                     |
123 | 48, 122 | sylbid 150 |
. . . . . . . 8
 
                 |
124 | 123 | impcom 125 |
. . . . . . 7
 
                 |
125 | 47, 124 | eqtrd 2210 |
. . . . . 6
 
                        |
126 | 125 | expcom 116 |
. . . . 5
 
                        |
127 | | zeo3 11872 |
. . . . 5
 
   |
128 | 45, 126, 127 | mpjaod 718 |
. . . 4
                        |
129 | 128 | eqcomd 2183 |
. . 3
             
          |
130 | 129 | adantr 276 |
. 2
 
                            |
131 | 22, 130 | eqtrd 2210 |
1
 
        
               |