Step | Hyp | Ref
| Expression |
1 | | df-3an 967 |
. . 3
  oMnd 
 
 
oMnd       |
2 | | df-3an 967 |
. . . . 5
  oMnd

 
oMnd     |
3 | | 3anass 969 |
. . . . 5
  oMnd

 oMnd      |
4 | 2, 3 | bitr3i 251 |
. . . 4
   oMnd

  oMnd 
    |
5 | 4 | anbi1i 695 |
. . 3
    oMnd

    oMnd

     |
6 | 1, 5 | bitr4i 252 |
. 2
  oMnd 
 
   oMnd

    |
7 | | simplr 754 |
. . 3
    oMnd

 
  |
8 | | oveq1 6202 |
. . . . 5
 
     |
9 | 8 | breq2d 4407 |
. . . 4
  
     |
10 | | oveq1 6202 |
. . . . 5
 
     |
11 | 10 | breq2d 4407 |
. . . 4
  
     |
12 | | oveq1 6202 |
. . . . 5
   
       |
13 | 12 | breq2d 4407 |
. . . 4
    
       |
14 | | oveq1 6202 |
. . . . 5
 
     |
15 | 14 | breq2d 4407 |
. . . 4
  
     |
16 | | omndtos 26308 |
. . . . . . . 8
 oMnd Toset |
17 | | tospos 26259 |
. . . . . . . 8
 Toset   |
18 | 16, 17 | syl 16 |
. . . . . . 7
 oMnd   |
19 | | omndmnd 26307 |
. . . . . . . 8
 oMnd   |
20 | | omndmul.0 |
. . . . . . . . 9
     |
21 | | omndmul2.3 |
. . . . . . . . 9
     |
22 | 20, 21 | mndidcl 15553 |
. . . . . . . 8
   |
23 | 19, 22 | syl 16 |
. . . . . . 7
 oMnd
  |
24 | | omndmul.1 |
. . . . . . . 8
     |
25 | 20, 24 | posref 15235 |
. . . . . . 7
    |
26 | 18, 23, 25 | syl2anc 661 |
. . . . . 6
 oMnd
 |
27 | 26 | ad3antrrr 729 |
. . . . 5
    oMnd

 
 |
28 | | omndmul2.2 |
. . . . . . 7
.g   |
29 | 20, 21, 28 | mulg0 15746 |
. . . . . 6
 
  |
30 | 29 | ad3antlr 730 |
. . . . 5
    oMnd

 
   |
31 | 27, 30 | breqtrrd 4421 |
. . . 4
    oMnd

 
    |
32 | 18 | ad5antr 733 |
. . . . 5
      oMnd     
 
  |
33 | 19 | ad5antr 733 |
. . . . . . 7
      oMnd     
 
  |
34 | 33, 22 | syl 16 |
. . . . . 6
      oMnd     
 
  |
35 | | simplr 754 |
. . . . . . 7
      oMnd     
 
  |
36 | | simp-5r 768 |
. . . . . . 7
      oMnd     
 
  |
37 | 20, 28 | mulgnn0cl 15757 |
. . . . . . 7
 
 
   |
38 | 33, 35, 36, 37 | syl3anc 1219 |
. . . . . 6
      oMnd     
 
    |
39 | | simpr32 1079 |
. . . . . . . . . 10
  oMnd 
    
  |
40 | | 1nn0 10701 |
. . . . . . . . . . 11
 |
41 | 40 | a1i 11 |
. . . . . . . . . 10
  oMnd 
       |
42 | 39, 41 | nn0addcld 10746 |
. . . . . . . . 9
  oMnd 
         |
43 | 42 | 3anassrs 1210 |
. . . . . . . 8
    oMnd


   
    |
44 | 43 | 3anassrs 1210 |
. . . . . . 7
      oMnd     
 
    |
45 | 20, 28 | mulgnn0cl 15757 |
. . . . . . 7
  

       |
46 | 33, 44, 36, 45 | syl3anc 1219 |
. . . . . 6
      oMnd     
 
      |
47 | 34, 38, 46 | 3jca 1168 |
. . . . 5
      oMnd     
 


       |
48 | | simpr 461 |
. . . . . 6
      oMnd     
 
    |
49 | | simp-4l 765 |
. . . . . . . . 9
     oMnd
    oMnd |
50 | 19 | ad4antr 731 |
. . . . . . . . . 10
     oMnd
      |
51 | 50, 22 | syl 16 |
. . . . . . . . 9
     oMnd
      |
52 | | simp-4r 766 |
. . . . . . . . 9
     oMnd
      |
53 | | simpr 461 |
. . . . . . . . . 10
     oMnd
      |
54 | 50, 53, 52, 37 | syl3anc 1219 |
. . . . . . . . 9
     oMnd
    
   |
55 | | simplr 754 |
. . . . . . . . 9
     oMnd
      |
56 | | eqid 2452 |
. . . . . . . . . 10
       |
57 | 20, 24, 56 | omndadd 26309 |
. . . . . . . . 9
  oMnd

                     |
58 | 49, 51, 52, 54, 55, 57 | syl131anc 1232 |
. . . . . . . 8
     oMnd
                      |
59 | 20, 56, 21 | mndlid 15555 |
. . . . . . . . 9
  
             |
60 | 50, 54, 59 | syl2anc 661 |
. . . . . . . 8
     oMnd
               |
61 | 40 | a1i 11 |
. . . . . . . . . 10
     oMnd
      |
62 | 20, 28, 56 | mulgnn0dir 15764 |
. . . . . . . . . 10
  
 
                 |
63 | 50, 61, 53, 52, 62 | syl13anc 1221 |
. . . . . . . . 9
     oMnd
      
              |
64 | | ax-1cn 9446 |
. . . . . . . . . . . . 13
 |
65 | 64 | a1i 11 |
. . . . . . . . . . . 12
   oMnd
      |
66 | | simpr3 996 |
. . . . . . . . . . . . 13
   oMnd
   
  |
67 | 66 | nn0cnd 10744 |
. . . . . . . . . . . 12
   oMnd
   
  |
68 | 65, 67 | addcomd 9677 |
. . . . . . . . . . 11
   oMnd
          |
69 | 68 | 3anassrs 1210 |
. . . . . . . . . 10
     oMnd
          |
70 | 69 | oveq1d 6210 |
. . . . . . . . 9
     oMnd
      
       |
71 | 20, 28 | mulg1 15748 |
. . . . . . . . . . 11
 
   |
72 | 52, 71 | syl 16 |
. . . . . . . . . 10
     oMnd
    
   |
73 | 72 | oveq1d 6210 |
. . . . . . . . 9
     oMnd
                          |
74 | 63, 70, 73 | 3eqtr3rd 2502 |
. . . . . . . 8
     oMnd
                   |
75 | 58, 60, 74 | 3brtr3d 4424 |
. . . . . . 7
     oMnd
    
       |
76 | 75 | adantr 465 |
. . . . . 6
      oMnd     
 
        |
77 | 48, 76 | jca 532 |
. . . . 5
      oMnd     
 

          |
78 | 20, 24 | postr 15237 |
. . . . . 6
  

        
      
       |
79 | 78 | imp 429 |
. . . . 5
            
       
      |
80 | 32, 47, 77, 79 | syl21anc 1218 |
. . . 4
      oMnd     
 
      |
81 | 9, 11, 13, 15, 31, 80 | nn0indd 26228 |
. . 3
     oMnd
    
   |
82 | 7, 81 | mpdan 668 |
. 2
    oMnd

 
    |
83 | 6, 82 | sylbi 195 |
1
  oMnd 
      |