Step | Hyp | Ref
| Expression |
1 | | elq 9621 |
. . . 4

      |
2 | 1 | biimpi 120 |
. . 3
       |
3 | 2 | adantl 277 |
. 2
 
       |
4 | | simplll 533 |
. . . . . 6
     
 
     |
5 | | elq 9621 |
. . . . . 6

      |
6 | 4, 5 | sylib 122 |
. . . . 5
     
 
         |
7 | | simplrl 535 |
. . . . . . . . . . . . 13
     
       
 

    |
8 | 7 | zcnd 9375 |
. . . . . . . . . . . 12
     
       
 

    |
9 | | simprl 529 |
. . . . . . . . . . . . . . . 16
         |
10 | 9 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
     
       
 

    |
11 | 10 | zcnd 9375 |
. . . . . . . . . . . . . 14
     
       
 

    |
12 | | simprr 531 |
. . . . . . . . . . . . . . . 16
      
  |
13 | 12 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
     
       
 

    |
14 | 13 | nncnd 8932 |
. . . . . . . . . . . . . 14
     
       
 

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

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

      |
18 | | simplrr 536 |
. . . . . . . . . . . . . 14
     
       
 

    |
19 | 18 | nncnd 8932 |
. . . . . . . . . . . . 13
     
       
 

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

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

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

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

    #   |
25 | | apmul1 8744 |
. . . . . . . . . . . 12
           #    #         #            |
26 | 8, 20, 23, 24, 25 | syl112anc 1242 |
. . . . . . . . . . 11
     
       
 

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

          |
28 | 27 | eqcomd 2183 |
. . . . . . . . . . . 12
     
       
 

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

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

        |
31 | 30 | oveq2d 5890 |
. . . . . . . . . . . . 13
     
       
 

                |
32 | 17 | mulridd 7973 |
. . . . . . . . . . . . 13
     
       
 

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

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

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

   #    
  #      |
36 | 13 | nnzd 9373 |
. . . . . . . . . . . . . . 15
     
       
 

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

      |
38 | 37 | zcnd 9375 |
. . . . . . . . . . . . 13
     
       
 

      |
39 | 18 | nnzd 9373 |
. . . . . . . . . . . . . . 15
     
       
 

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

      |
41 | 40 | zcnd 9375 |
. . . . . . . . . . . . 13
     
       
 

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

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

    #   |
44 | | apmul1 8744 |
. . . . . . . . . . . . 13
           #      #         #          |
45 | 38, 41, 42, 43, 44 | syl112anc 1242 |
. . . . . . . . . . . 12
     
       
 

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

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

        |
48 | 47 | oveq2d 5890 |
. . . . . . . . . . . . . 14
     
       
 

            |
49 | 8 | mulridd 7973 |
. . . . . . . . . . . . . 14
     
       
 

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

          |
51 | 50 | breq1d 4013 |
. . . . . . . . . . . 12
     
       
 

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

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

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

          |
55 | 54 | oveq2d 5890 |
. . . . . . . . . . . . 13
     
       
 

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

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

              |
58 | 57 | breq2d 4015 |
. . . . . . . . . . 11
     
       
 

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

     #  
#        |
60 | | simpr 110 |
. . . . . . . . . . 11
     
       
 

      |
61 | | simpllr 534 |
. . . . . . . . . . 11
     
       
 

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

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

     #  
#    |
64 | | zapne 9326 |
. . . . . . . . . 10
          #          |
65 | 37, 40, 64 | syl2anc 411 |
. . . . . . . . 9
     
       
 

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

   #
       |
67 | 63 | notbid 667 |
. . . . . . . . . 10
     
       
 

     #  
#    |
68 | | apti 8578 |
. . . . . . . . . . 11
           
  #      |
69 | 38, 41, 68 | syl2anc 411 |
. . . . . . . . . 10
     
       
 

      
  #      |
70 | | qcn 9633 |
. . . . . . . . . . . . 13
   |
71 | 70 | ad2antrr 488 |
. . . . . . . . . . . 12
      
  |
72 | 71 | ad3antrrr 492 |
. . . . . . . . . . 11
     
       
 

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

    |
74 | | apti 8578 |
. . . . . . . . . . 11
 
 
#    |
75 | 72, 73, 74 | syl2anc 411 |
. . . . . . . . . 10
     
       
 

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

      
   |
77 | 76 | necon3bid 2388 |
. . . . . . . 8
     
       
 

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

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