Proof of Theorem dirkerper
Step | Hyp | Ref
| Expression |
1 | | dirkerper.2 |
. . . . . . . . . . . . 13
   |
2 | 1 | eqcomi 2460 |
. . . . . . . . . . . 12
   |
3 | 2 | oveq2i 6301 |
. . . . . . . . . . 11
       |
4 | | 2re 10679 |
. . . . . . . . . . . . . . 15
 |
5 | | pire 23413 |
. . . . . . . . . . . . . . 15
 |
6 | 4, 5 | remulcli 9657 |
. . . . . . . . . . . . . 14
   |
7 | 1, 6 | eqeltri 2525 |
. . . . . . . . . . . . 13
 |
8 | 7 | recni 9655 |
. . . . . . . . . . . 12
 |
9 | 8 | mulid2i 9646 |
. . . . . . . . . . 11
   |
10 | 3, 9 | eqtri 2473 |
. . . . . . . . . 10
     |
11 | 10 | oveq2i 6301 |
. . . . . . . . 9
         |
12 | 11 | eqcomi 2460 |
. . . . . . . 8
         |
13 | 12 | oveq1i 6300 |
. . . . . . 7
                 |
14 | 13 | a1i 11 |
. . . . . 6
        
                  |
15 | | id 22 |
. . . . . . . 8
   |
16 | 15 | ad2antlr 733 |
. . . . . . 7
        
  |
17 | | 2rp 11307 |
. . . . . . . . 9
 |
18 | | pirp 23416 |
. . . . . . . . 9
 |
19 | | rpmulcl 11324 |
. . . . . . . . 9
       |
20 | 17, 18, 19 | mp2an 678 |
. . . . . . . 8
   |
21 | 20 | a1i 11 |
. . . . . . 7
        
    |
22 | | 1z 10967 |
. . . . . . . 8
 |
23 | 22 | a1i 11 |
. . . . . . 7
        
  |
24 | | modcyc 12132 |
. . . . . . 7
   
                 |
25 | 16, 21, 23, 24 | syl3anc 1268 |
. . . . . 6
        
                |
26 | | simpr 463 |
. . . . . 6
        
      |
27 | 14, 25, 26 | 3eqtrd 2489 |
. . . . 5
        
        |
28 | 27 | iftrued 3889 |
. . . 4
        
                                                       |
29 | | iftrue 3887 |
. . . . 5
                                                      |
30 | 29 | adantl 468 |
. . . 4
        
                                                 |
31 | 28, 30 | eqtr4d 2488 |
. . 3
        
                                                                          
           |
32 | | iffalse 3890 |
. . . . 5
                                                         
          |
33 | 32 | adantl 468 |
. . . 4
                                                             
          |
34 | | nncn 10617 |
. . . . . . . . . 10
   |
35 | | halfcn 10829 |
. . . . . . . . . . 11
   |
36 | 35 | a1i 11 |
. . . . . . . . . 10
     |
37 | 34, 36 | addcld 9662 |
. . . . . . . . 9
 
     |
38 | 37 | adantr 467 |
. . . . . . . 8
 
       |
39 | | recn 9629 |
. . . . . . . . 9
   |
40 | 39 | adantl 468 |
. . . . . . . 8
 
   |
41 | 38, 40 | mulcld 9663 |
. . . . . . 7
 
         |
42 | 41 | sincld 14184 |
. . . . . 6
 
             |
43 | 42 | adantr 467 |
. . . . 5
                     |
44 | 6 | recni 9655 |
. . . . . . . 8
   |
45 | 44 | a1i 11 |
. . . . . . 7
 
  
  |
46 | 40 | halfcld 10857 |
. . . . . . . 8
 
     |
47 | 46 | sincld 14184 |
. . . . . . 7
 
         |
48 | 45, 47 | mulcld 9663 |
. . . . . 6
 
             |
49 | 48 | adantr 467 |
. . . . 5
           
         |
50 | | dirkerdenne0 37955 |
. . . . . 6
                   |
51 | 50 | adantll 720 |
. . . . 5
           
         |
52 | 43, 49, 51 | div2negd 10398 |
. . . 4
                        
                     
          |
53 | 13 | a1i 11 |
. . . . . . . . . . 11
   
               |
54 | 20, 22, 24 | mp3an23 1356 |
. . . . . . . . . . 11
                 |
55 | 53, 54 | eqtrd 2485 |
. . . . . . . . . 10
   
         |
56 | 55 | adantr 467 |
. . . . . . . . 9
                   |
57 | | simpr 463 |
. . . . . . . . . 10
      
      |
58 | 57 | neqned 2631 |
. . . . . . . . 9
             |
59 | 56, 58 | eqnetrd 2691 |
. . . . . . . 8
               |
60 | 59 | neneqd 2629 |
. . . . . . 7
      
        |
61 | | iffalse 3890 |
. . . . . . . 8
                                                                   
            |
62 | 1 | oveq2i 6301 |
. . . . . . . . . . 11
       |
63 | 62 | oveq2i 6301 |
. . . . . . . . . 10
                   |
64 | 63 | fveq2i 5868 |
. . . . . . . . 9
                           |
65 | 62 | oveq1i 6300 |
. . . . . . . . . . 11
           |
66 | 65 | fveq2i 5868 |
. . . . . . . . . 10
                   |
67 | 66 | oveq2i 6301 |
. . . . . . . . 9
              
            |
68 | 64, 67 | oveq12i 6302 |
. . . . . . . 8
                                                         |
69 | 61, 68 | syl6eq 2501 |
. . . . . . 7
                                                                     
              |
70 | 60, 69 | syl 17 |
. . . . . 6
           
                            
                                           |
71 | 70 | adantll 720 |
. . . . 5
                                                                       
              |
72 | 44 | a1i 11 |
. . . . . . . . . . . . . 14
     |
73 | 34, 36, 72 | adddird 9668 |
. . . . . . . . . . . . 13
                       |
74 | | ax-1cn 9597 |
. . . . . . . . . . . . . . . 16
 |
75 | | 2cnne0 10824 |
. . . . . . . . . . . . . . . 16
   |
76 | | 2cn 10680 |
. . . . . . . . . . . . . . . . 17
 |
77 | | picn 23414 |
. . . . . . . . . . . . . . . . 17
 |
78 | 76, 77 | mulcli 9648 |
. . . . . . . . . . . . . . . 16
   |
79 | | div32 10290 |
. . . . . . . . . . . . . . . 16
                     |
80 | 74, 75, 78, 79 | mp3an 1364 |
. . . . . . . . . . . . . . 15
             |
81 | | 2ne0 10702 |
. . . . . . . . . . . . . . . . . 18
 |
82 | 78, 76, 81 | divcli 10349 |
. . . . . . . . . . . . . . . . 17
     |
83 | 82 | mulid2i 9646 |
. . . . . . . . . . . . . . . 16
           |
84 | 77, 76, 81 | divcan3i 10353 |
. . . . . . . . . . . . . . . 16
     |
85 | 83, 84 | eqtri 2473 |
. . . . . . . . . . . . . . 15
       |
86 | 80, 85 | eqtri 2473 |
. . . . . . . . . . . . . 14
       |
87 | 86 | oveq2i 6301 |
. . . . . . . . . . . . 13
                   |
88 | 73, 87 | syl6eq 2501 |
. . . . . . . . . . . 12
                 |
89 | 88 | oveq2d 6306 |
. . . . . . . . . . 11
                                 |
90 | 89 | adantr 467 |
. . . . . . . . . 10
 
                                 |
91 | 38, 40, 45 | adddid 9667 |
. . . . . . . . . 10
 
                             |
92 | 34, 72 | mulcld 9663 |
. . . . . . . . . . . 12
 
     |
93 | 92 | adantr 467 |
. . . . . . . . . . 11
 
       |
94 | 77 | a1i 11 |
. . . . . . . . . . 11
 
   |
95 | 41, 93, 94 | addassd 9665 |
. . . . . . . . . 10
 
              
                |
96 | 90, 91, 95 | 3eqtr4d 2495 |
. . . . . . . . 9
 
                           |
97 | 96 | fveq2d 5869 |
. . . . . . . 8
 
                                   |
98 | 41, 93 | addcld 9662 |
. . . . . . . . 9
 
               |
99 | | sinppi 23444 |
. . . . . . . . 9
                                                  |
100 | 98, 99 | syl 17 |
. . . . . . . 8
 
                                      |
101 | | simpl 459 |
. . . . . . . . . . 11
 
   |
102 | 101 | nnzd 11039 |
. . . . . . . . . 10
 
   |
103 | | sinper 23436 |
. . . . . . . . . 10
       
                             |
104 | 41, 102, 103 | syl2anc 667 |
. . . . . . . . 9
 
                             |
105 | 104 | negeqd 9869 |
. . . . . . . 8
 
                               |
106 | 97, 100, 105 | 3eqtrd 2489 |
. . . . . . 7
 
                            |
107 | 44 | a1i 11 |
. . . . . . . . . . . . 13
     |
108 | 76 | a1i 11 |
. . . . . . . . . . . . 13
   |
109 | 81 | a1i 11 |
. . . . . . . . . . . . 13
   |
110 | 39, 107, 108, 109 | divdird 10421 |
. . . . . . . . . . . 12
                 |
111 | 84 | a1i 11 |
. . . . . . . . . . . . 13
       |
112 | 111 | oveq2d 6306 |
. . . . . . . . . . . 12
               |
113 | 110, 112 | eqtrd 2485 |
. . . . . . . . . . 11
             |
114 | 113 | fveq2d 5869 |
. . . . . . . . . 10
                     |
115 | 39 | halfcld 10857 |
. . . . . . . . . . 11
     |
116 | | sinppi 23444 |
. . . . . . . . . . 11
                    |
117 | 115, 116 | syl 17 |
. . . . . . . . . 10
                  |
118 | 114, 117 | eqtrd 2485 |
. . . . . . . . 9
                    |
119 | 118 | oveq2d 6306 |
. . . . . . . 8
   
                        |
120 | 119 | adantl 468 |
. . . . . . 7
 
                            |
121 | 106, 120 | oveq12d 6308 |
. . . . . 6
 
                                             
           |
122 | 121 | adantr 467 |
. . . . 5
                                                     
           |
123 | 115 | sincld 14184 |
. . . . . . . 8
         |
124 | 107, 123 | mulneg2d 10072 |
. . . . . . 7
   
                     |
125 | 124 | oveq2d 6306 |
. . . . . 6
                                        
          |
126 | 125 | ad2antlr 733 |
. . . . 5
                                                
          |
127 | 71, 122, 126 | 3eqtrrd 2490 |
. . . 4
                        
            
                            
             |
128 | 33, 52, 127 | 3eqtr2rd 2492 |
. . 3
                                                                                   
           |
129 | 31, 128 | pm2.61dan 800 |
. 2
 
                                                                           
           |
130 | 7 | a1i 11 |
. . . 4
   |
131 | 15, 130 | readdcld 9670 |
. . 3
     |
132 | | dirkerper.1 |
. . . 4
                                            |
133 | 132 | dirkerval2 37956 |
. . 3
  
         
                                                 |
134 | 131, 133 | sylan2 477 |
. 2
 
                                                          |
135 | 132 | dirkerval2 37956 |
. 2
 
                                                  |
136 | 129, 134,
135 | 3eqtr4d 2495 |
1
 
                     |