Step | Hyp | Ref
| Expression |
1 | | elq 8333 |
. . . 4
       |
2 | 1 | biimpi 113 |
. . 3
 
     |
3 | 2 | adantl 262 |
. 2
 
       |
4 | | simplll 485 |
. . . . . 6
       
  
  |
5 | | elq 8333 |
. . . . . 6
       |
6 | 4, 5 | sylib 127 |
. . . . 5
       
   
     |
7 | | simplrl 487 |
. . . . . . . . . . . . 13
     
    
 

 
  
  |
8 | 7 | zcnd 8137 |
. . . . . . . . . . . 12
     
    
 

 
  
  |
9 | | simprl 483 |
. . . . . . . . . . . . . . . 16
         |
10 | 9 | ad3antrrr 461 |
. . . . . . . . . . . . . . 15
     
    
 

 
  
  |
11 | 10 | zcnd 8137 |
. . . . . . . . . . . . . 14
     
    
 

 
  
  |
12 | | simprr 484 |
. . . . . . . . . . . . . . . 16
         |
13 | 12 | ad3antrrr 461 |
. . . . . . . . . . . . . . 15
     
    
 

 
  
  |
14 | 13 | nncnd 7709 |
. . . . . . . . . . . . . 14
     
    
 

 
  
  |
15 | | nnap0 7724 |
. . . . . . . . . . . . . . 15
 #   |
16 | 13, 15 | syl 14 |
. . . . . . . . . . . . . 14
     
    
 

 
   #   |
17 | 11, 14, 16 | divclapd 7547 |
. . . . . . . . . . . . 13
     
    
 

 
   

  |
18 | | simplrr 488 |
. . . . . . . . . . . . . 14
     
    
 

 
  
  |
19 | 18 | nncnd 7709 |
. . . . . . . . . . . . 13
     
    
 

 
  
  |
20 | 17, 19 | mulcld 6845 |
. . . . . . . . . . . 12
     
    
 

 
         |
21 | | nnap0 7724 |
. . . . . . . . . . . . . 14
 #   |
22 | 18, 21 | syl 14 |
. . . . . . . . . . . . 13
     
    
 

 
   #   |
23 | 19, 22 | recclapd 7539 |
. . . . . . . . . . . 12
     
    
 

 
    
  |
24 | 19, 22 | recap0d 7540 |
. . . . . . . . . . . 12
     
    
 

 
     #   |
25 | | apmul1 7546 |
. . . . . . . . . . . 12
         
 #    #
        #            |
26 | 8, 20, 23, 24, 25 | syl112anc 1138 |
. . . . . . . . . . 11
     
    
 

 
    #
        #            |
27 | 8, 19, 22 | divrecapd 7550 |
. . . . . . . . . . . . 13
     
    
 

 
   

      |
28 | 27 | eqcomd 2042 |
. . . . . . . . . . . 12
     
    
 

 
   

 
    |
29 | 17, 19, 23 | mulassd 6848 |
. . . . . . . . . . . . 13
     
    
 

 
      
              |
30 | 19, 22 | recidapd 7541 |
. . . . . . . . . . . . . 14
     
    
 

 
   

 
  |
31 | 30 | oveq2d 5471 |
. . . . . . . . . . . . 13
     
    
 

 
                 |
32 | 17 | mulid1d 6842 |
. . . . . . . . . . . . 13
     
    
 

 
           |
33 | 29, 31, 32 | 3eqtrd 2073 |
. . . . . . . . . . . 12
     
    
 

 
      
        |
34 | 28, 33 | breq12d 3768 |
. . . . . . . . . . 11
     
    
 

 
     
  #           #      |
35 | 26, 34 | bitrd 177 |
. . . . . . . . . 10
     
    
 

 
    #
      #      |
36 | 13 | nnzd 8135 |
. . . . . . . . . . . . . . 15
     
    
 

 
  
  |
37 | 7, 36 | zmulcld 8142 |
. . . . . . . . . . . . . 14
     
    
 

 
   

  |
38 | 37 | zcnd 8137 |
. . . . . . . . . . . . 13
     
    
 

 
   

  |
39 | 18 | nnzd 8135 |
. . . . . . . . . . . . . . 15
     
    
 

 
  
  |
40 | 39, 10 | zmulcld 8142 |
. . . . . . . . . . . . . 14
     
    
 

 
   

  |
41 | 40 | zcnd 8137 |
. . . . . . . . . . . . 13
     
    
 

 
   

  |
42 | 14, 16 | recclapd 7539 |
. . . . . . . . . . . . 13
     
    
 

 
    
  |
43 | 14, 16 | recap0d 7540 |
. . . . . . . . . . . . 13
     
    
 

 
     #   |
44 | | apmul1 7546 |
. . . . . . . . . . . . 13
   
     
 #      #     

  #    
     |
45 | 38, 41, 42, 43, 44 | syl112anc 1138 |
. . . . . . . . . . . 12
     
    
 

 
      #     

  #    
     |
46 | 8, 14, 42 | mulassd 6848 |
. . . . . . . . . . . . . 14
     
    
 

 
                 |
47 | 14, 16 | recidapd 7541 |
. . . . . . . . . . . . . . 15
     
    
 

 
   

 
  |
48 | 47 | oveq2d 5471 |
. . . . . . . . . . . . . 14
     
    
 

 
   
         |
49 | 8 | mulid1d 6842 |
. . . . . . . . . . . . . 14
     
    
 

 
   

  |
50 | 46, 48, 49 | 3eqtrd 2073 |
. . . . . . . . . . . . 13
     
    
 

 
           |
51 | 50 | breq1d 3765 |
. . . . . . . . . . . 12
     
    
 

 
      

  #    
  #          |
52 | 45, 51 | bitrd 177 |
. . . . . . . . . . 11
     
    
 

 
      #   #          |
53 | 19, 11, 42 | mulassd 6848 |
. . . . . . . . . . . . 13
     
    
 

 
                 |
54 | 11, 14, 16 | divrecapd 7550 |
. . . . . . . . . . . . . 14
     
    
 

 
   

      |
55 | 54 | oveq2d 5471 |
. . . . . . . . . . . . 13
     
    
 

 
   
     
     |
56 | 19, 17 | mulcomd 6846 |
. . . . . . . . . . . . 13
     
    
 

 
   
         |
57 | 53, 55, 56 | 3eqtr2d 2075 |
. . . . . . . . . . . 12
     
    
 

 
               |
58 | 57 | breq2d 3767 |
. . . . . . . . . . 11
     
    
 

 
    #
     
#  
     |
59 | 52, 58 | bitrd 177 |
. . . . . . . . . 10
     
    
 

 
      #   #        |
60 | | simpr 103 |
. . . . . . . . . . 11
     
    
 

 
  
    |
61 | | simpllr 486 |
. . . . . . . . . . 11
     
    
 

 
  
    |
62 | 60, 61 | breq12d 3768 |
. . . . . . . . . 10
     
    
 

 
   
#   #      |
63 | 35, 59, 62 | 3bitr4d 209 |
. . . . . . . . 9
     
    
 

 
      #   #    |
64 | | zapne 8091 |
. . . . . . . . . 10
   
    
 #          |
65 | 37, 40, 64 | syl2anc 391 |
. . . . . . . . 9
     
    
 

 
      #          |
66 | 63, 65 | bitr3d 179 |
. . . . . . . 8
     
    
 

 
   
#        |
67 | 63 | notbid 591 |
. . . . . . . . . 10
     
    
 

 
      #
  #    |
68 | | apti 7406 |
. . . . . . . . . . 11
   
    

    #      |
69 | 38, 41, 68 | syl2anc 391 |
. . . . . . . . . 10
     
    
 

 
     
    #      |
70 | | qcn 8345 |
. . . . . . . . . . . . 13
   |
71 | 70 | ad2antrr 457 |
. . . . . . . . . . . 12
         |
72 | 71 | ad3antrrr 461 |
. . . . . . . . . . 11
     
    
 

 
  
  |
73 | 61, 17 | eqeltrd 2111 |
. . . . . . . . . . 11
     
    
 

 
  
  |
74 | | apti 7406 |
. . . . . . . . . . 11
 
  #    |
75 | 72, 73, 74 | syl2anc 391 |
. . . . . . . . . 10
     
    
 

 
   
#    |
76 | 67, 69, 75 | 3bitr4d 209 |
. . . . . . . . 9
     
    
 

 
     
     |
77 | 76 | necon3bid 2240 |
. . . . . . . 8
     
    
 

 
           |
78 | 66, 77 | bitrd 177 |
. . . . . . 7
     
    
 

 
   
#    |
79 | 78 | ex 108 |
. . . . . 6
      
 
   
    
 #     |
80 | 79 | rexlimdvva 2434 |
. . . . 5
       
         #     |
81 | 6, 80 | mpd 13 |
. . . 4
       
   
#    |
82 | 81 | ex 108 |
. . 3
         
 #     |
83 | 82 | rexlimdvva 2434 |
. 2
 
       #     |
84 | 3, 83 | mpd 13 |
1
 
  #    |