Step | Hyp | Ref
| Expression |
1 | | simp2l 1023 |
. . 3
  
 
 
  |
2 | | elq 9611 |
. . 3

      |
3 | 1, 2 | sylib 122 |
. 2
  
 
  
     |
4 | | simp3l 1025 |
. . 3
  
 
 
  |
5 | | elq 9611 |
. . 3

      |
6 | 4, 5 | sylib 122 |
. 2
  
 
  
     |
7 | | reeanv 2646 |
. . 3
  
 
     
 
          |
8 | | reeanv 2646 |
. . . . 5
  

 
  
 
  
     |
9 | | simp2r 1024 |
. . . . . . . . 9
  
 
    |
10 | | simp3r 1026 |
. . . . . . . . 9
  
 
    |
11 | 9, 10 | jca 306 |
. . . . . . . 8
  
 
  
   |
12 | 11 | ad2antrr 488 |
. . . . . . 7
      
  
     
   |
13 | | simp1 997 |
. . . . . . . 8
  
 
 
  |
14 | | simprl 529 |
. . . . . . . . . . . . . 14
           |
15 | 14 | nncnd 8922 |
. . . . . . . . . . . . 13
           |
16 | 14 | nnap0d 8954 |
. . . . . . . . . . . . 13
         #   |
17 | 15, 16 | div0apd 8733 |
. . . . . . . . . . . 12
             |
18 | | oveq1 5876 |
. . . . . . . . . . . . 13
       |
19 | 18 | eqeq1d 2186 |
. . . . . . . . . . . 12
         |
20 | 17, 19 | syl5ibrcom 157 |
. . . . . . . . . . 11
               |
21 | 20 | necon3d 2391 |
. . . . . . . . . 10
               |
22 | | simprr 531 |
. . . . . . . . . . . . . 14
        
  |
23 | 22 | nncnd 8922 |
. . . . . . . . . . . . 13
        
  |
24 | 22 | nnap0d 8954 |
. . . . . . . . . . . . 13
         #   |
25 | 23, 24 | div0apd 8733 |
. . . . . . . . . . . 12
             |
26 | | oveq1 5876 |
. . . . . . . . . . . . 13
       |
27 | 26 | eqeq1d 2186 |
. . . . . . . . . . . 12
         |
28 | 25, 27 | syl5ibrcom 157 |
. . . . . . . . . . 11
               |
29 | 28 | necon3d 2391 |
. . . . . . . . . 10
               |
30 | | simpll 527 |
. . . . . . . . . . . . . 14
       
 
  
  |
31 | | simplrl 535 |
. . . . . . . . . . . . . . 15
       
 
  
  |
32 | | simplrr 536 |
. . . . . . . . . . . . . . 15
       
 
     |
33 | 31, 32 | zmulcld 9370 |
. . . . . . . . . . . . . 14
       
 
       |
34 | 31 | zcnd 9365 |
. . . . . . . . . . . . . . . 16
       
 
  
  |
35 | 32 | zcnd 9365 |
. . . . . . . . . . . . . . . 16
       
 
     |
36 | | simprrl 539 |
. . . . . . . . . . . . . . . . 17
       
 
     |
37 | | 0zd 9254 |
. . . . . . . . . . . . . . . . . 18
       
 
     |
38 | | zapne 9316 |
. . . . . . . . . . . . . . . . . 18
 
  #    |
39 | 31, 37, 38 | syl2anc 411 |
. . . . . . . . . . . . . . . . 17
       
 
    #    |
40 | 36, 39 | mpbird 167 |
. . . . . . . . . . . . . . . 16
       
 
   #   |
41 | | simprrr 540 |
. . . . . . . . . . . . . . . . 17
       
 
     |
42 | | zapne 9316 |
. . . . . . . . . . . . . . . . . 18
 
  #    |
43 | 32, 37, 42 | syl2anc 411 |
. . . . . . . . . . . . . . . . 17
       
 
    #    |
44 | 41, 43 | mpbird 167 |
. . . . . . . . . . . . . . . 16
       
 
   #   |
45 | 34, 35, 40, 44 | mulap0d 8604 |
. . . . . . . . . . . . . . 15
       
 
     #   |
46 | | zapne 9316 |
. . . . . . . . . . . . . . . 16
   
    #      |
47 | 33, 37, 46 | syl2anc 411 |
. . . . . . . . . . . . . . 15
       
 
      #      |
48 | 45, 47 | mpbid 147 |
. . . . . . . . . . . . . 14
       
 
       |
49 | 14 | adantrr 479 |
. . . . . . . . . . . . . . 15
       
 
     |
50 | 22 | adantrr 479 |
. . . . . . . . . . . . . . 15
       
 
  
  |
51 | 49, 50 | nnmulcld 8957 |
. . . . . . . . . . . . . 14
       
 
       |
52 | | pcdiv 12285 |
. . . . . . . . . . . . . 14
     
              
   
      |
53 | 30, 33, 48, 51, 52 | syl121anc 1243 |
. . . . . . . . . . . . 13
       
 
            
   
      |
54 | | pcmul 12284 |
. . . . . . . . . . . . . . 15
      
            |
55 | 30, 31, 36, 32, 41, 54 | syl122anc 1247 |
. . . . . . . . . . . . . 14
       
 
        
      |
56 | 49 | nnzd 9363 |
. . . . . . . . . . . . . . 15
       
 
     |
57 | 14 | nnne0d 8953 |
. . . . . . . . . . . . . . . 16
           |
58 | 57 | adantrr 479 |
. . . . . . . . . . . . . . 15
       
 
     |
59 | 50 | nnzd 9363 |
. . . . . . . . . . . . . . 15
       
 
  
  |
60 | 22 | nnne0d 8953 |
. . . . . . . . . . . . . . . 16
           |
61 | 60 | adantrr 479 |
. . . . . . . . . . . . . . 15
       
 
     |
62 | | pcmul 12284 |
. . . . . . . . . . . . . . 15
    
 
            |
63 | 30, 56, 58, 59, 61, 62 | syl122anc 1247 |
. . . . . . . . . . . . . 14
       
 
        
      |
64 | 55, 63 | oveq12d 5887 |
. . . . . . . . . . . . 13
       
 
               
             |
65 | | pczcl 12281 |
. . . . . . . . . . . . . . . 16
         |
66 | 30, 31, 36, 65 | syl12anc 1236 |
. . . . . . . . . . . . . . 15
       
 
       |
67 | 66 | nn0cnd 9220 |
. . . . . . . . . . . . . 14
       
 
       |
68 | | pczcl 12281 |
. . . . . . . . . . . . . . . 16
         |
69 | 30, 32, 41, 68 | syl12anc 1236 |
. . . . . . . . . . . . . . 15
       
 
       |
70 | 69 | nn0cnd 9220 |
. . . . . . . . . . . . . 14
       
 
       |
71 | 30, 49 | pccld 12283 |
. . . . . . . . . . . . . . 15
       
 
       |
72 | 71 | nn0cnd 9220 |
. . . . . . . . . . . . . 14
       
 
       |
73 | 30, 50 | pccld 12283 |
. . . . . . . . . . . . . . 15
       
 
       |
74 | 73 | nn0cnd 9220 |
. . . . . . . . . . . . . 14
       
 
       |
75 | 67, 70, 72, 74 | addsub4d 8305 |
. . . . . . . . . . . . 13
       
 
       
   
               
     |
76 | 53, 64, 75 | 3eqtrd 2214 |
. . . . . . . . . . . 12
       
 
                     
     |
77 | 15 | adantrr 479 |
. . . . . . . . . . . . . 14
       
 
     |
78 | 23 | adantrr 479 |
. . . . . . . . . . . . . 14
       
 
  
  |
79 | 16 | adantrr 479 |
. . . . . . . . . . . . . 14
       
 
   #   |
80 | 24 | adantrr 479 |
. . . . . . . . . . . . . 14
       
 
   #   |
81 | 34, 77, 35, 78, 79, 80 | divmuldivapd 8778 |
. . . . . . . . . . . . 13
       
 
                 |
82 | 81 | oveq2d 5885 |
. . . . . . . . . . . 12
       
 
                     |
83 | | pcdiv 12285 |
. . . . . . . . . . . . . 14
   
      
      |
84 | 30, 31, 36, 49, 83 | syl121anc 1243 |
. . . . . . . . . . . . 13
       
 
        
      |
85 | | pcdiv 12285 |
. . . . . . . . . . . . . 14
   
      
      |
86 | 30, 32, 41, 50, 85 | syl121anc 1243 |
. . . . . . . . . . . . 13
       
 
        
      |
87 | 84, 86 | oveq12d 5887 |
. . . . . . . . . . . 12
       
 
               
             |
88 | 76, 82, 87 | 3eqtr4d 2220 |
. . . . . . . . . . 11
       
 
            
          |
89 | 88 | expr 375 |
. . . . . . . . . 10
                                 |
90 | 21, 29, 89 | syl2and 295 |
. . . . . . . . 9
                                     |
91 | | neeq1 2360 |
. . . . . . . . . . 11
   
     |
92 | | neeq1 2360 |
. . . . . . . . . . 11
   
     |
93 | 91, 92 | bi2anan9 606 |
. . . . . . . . . 10
   
     
         |
94 | | oveq12 5878 |
. . . . . . . . . . . 12
   
             |
95 | 94 | oveq2d 5885 |
. . . . . . . . . . 11
   
    
            |
96 | | oveq2 5877 |
. . . . . . . . . . . 12
           |
97 | | oveq2 5877 |
. . . . . . . . . . . 12
           |
98 | 96, 97 | oveqan12d 5888 |
. . . . . . . . . . 11
   
                     |
99 | 95, 98 | eqeq12d 2192 |
. . . . . . . . . 10
   
         
   
                     |
100 | 93, 99 | imbi12d 234 |
. . . . . . . . 9
   
                                               |
101 | 90, 100 | syl5ibrcom 157 |
. . . . . . . 8
            
    

              |
102 | 13, 101 | sylanl1 402 |
. . . . . . 7
      
  
        
    

              |
103 | 12, 102 | mpid 42 |
. . . . . 6
      
  
        
                |
104 | 103 | rexlimdvva 2602 |
. . . . 5
        
 
 
   
                |
105 | 8, 104 | biimtrrid 153 |
. . . 4
        
 
  
       
   
       |
106 | 105 | rexlimdvva 2602 |
. . 3
  
 
            
             |
107 | 7, 106 | biimtrrid 153 |
. 2
  
 
            
             |
108 | 3, 6, 107 | mp2and 433 |
1
  
 
   
   
      |