Step | Hyp | Ref
| Expression |
1 | | iftrue 3540 |
. . . . 5
        |
2 | 1 | prodeq2i 11570 |
. . . 4

   
   |
3 | | ssun1 3299 |
. . . . . 6

  |
4 | | fprodsplitdc.2 |
. . . . . 6
     |
5 | 3, 4 | sseqtrrid 3207 |
. . . . 5

  |
6 | 1 | adantl 277 |
. . . . . 6
 
        |
7 | 5 | sselda 3156 |
. . . . . . 7
 
   |
8 | | fprodsplitdc.4 |
. . . . . . 7
 
   |
9 | 7, 8 | syldan 282 |
. . . . . 6
 
   |
10 | 6, 9 | eqeltrd 2254 |
. . . . 5
 
        |
11 | | fprodsplitdc.a |
. . . . 5
  DECID   |
12 | | eldifn 3259 |
. . . . . . 7
  
  |
13 | 12 | iffalsed 3545 |
. . . . . 6
          |
14 | 13 | adantl 277 |
. . . . 5
 

 
   
   |
15 | | fprodsplitdc.3 |
. . . . 5
   |
16 | 5, 10, 11, 14, 15 | fprodssdc 11598 |
. . . 4
               |
17 | 2, 16 | eqtr3id 2224 |
. . 3
 
        |
18 | | iftrue 3540 |
. . . . 5
        |
19 | 18 | prodeq2i 11570 |
. . . 4

   
   |
20 | | ssun2 3300 |
. . . . . 6

  |
21 | 20, 4 | sseqtrrid 3207 |
. . . . 5

  |
22 | 18 | adantl 277 |
. . . . . 6
 
        |
23 | 21 | sselda 3156 |
. . . . . . 7
 
   |
24 | 23, 8 | syldan 282 |
. . . . . 6
 
   |
25 | 22, 24 | eqeltrd 2254 |
. . . . 5
 
        |
26 | | fprodsplitdc.1 |
. . . . . . . . . . . . . 14
     |
27 | | disj 3472 |
. . . . . . . . . . . . . 14
  

  |
28 | 26, 27 | sylib 122 |
. . . . . . . . . . . . 13
 
  |
29 | 28 | ad2antrr 488 |
. . . . . . . . . . . 12
    DECID
 
  |
30 | 29 | r19.21bi 2565 |
. . . . . . . . . . 11
   
 DECID


  |
31 | 30 | olcd 734 |
. . . . . . . . . 10
   
 DECID



   |
32 | | df-dc 835 |
. . . . . . . . . 10
DECID     |
33 | 31, 32 | sylibr 134 |
. . . . . . . . 9
   
 DECID


DECID
  |
34 | | simpr 110 |
. . . . . . . . . . . 12
   
 DECID
 
  |
35 | | simpllr 534 |
. . . . . . . . . . . . . . 15
   
 DECID
 
  |
36 | 4 | eleq2d 2247 |
. . . . . . . . . . . . . . . 16
       |
37 | 36 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
   
 DECID
 

     |
38 | 35, 37 | mpbid 147 |
. . . . . . . . . . . . . 14
   
 DECID
 

   |
39 | | elun 3277 |
. . . . . . . . . . . . . 14
  

   |
40 | 38, 39 | sylib 122 |
. . . . . . . . . . . . 13
   
 DECID
 

   |
41 | 40 | orcomd 729 |
. . . . . . . . . . . 12
   
 DECID
 

   |
42 | 34, 41 | ecased 1349 |
. . . . . . . . . . 11
   
 DECID
 
  |
43 | 42 | orcd 733 |
. . . . . . . . . 10
   
 DECID
 

   |
44 | 43, 32 | sylibr 134 |
. . . . . . . . 9
   
 DECID
 
DECID
  |
45 | | exmiddc 836 |
. . . . . . . . . 10
DECID

   |
46 | 45 | adantl 277 |
. . . . . . . . 9
    DECID
 
   |
47 | 33, 44, 46 | mpjaodan 798 |
. . . . . . . 8
    DECID

DECID
  |
48 | 47 | ex 115 |
. . . . . . 7
 
 DECID
DECID
   |
49 | 48 | ralimdva 2544 |
. . . . . 6
   DECID 
DECID    |
50 | 11, 49 | mpd 13 |
. . . . 5
  DECID   |
51 | | eldifn 3259 |
. . . . . . 7
  
  |
52 | 51 | iffalsed 3545 |
. . . . . 6
          |
53 | 52 | adantl 277 |
. . . . 5
 

 
   
   |
54 | 21, 25, 50, 53, 15 | fprodssdc 11598 |
. . . 4
               |
55 | 19, 54 | eqtr3id 2224 |
. . 3
 
        |
56 | 17, 55 | oveq12d 5893 |
. 2
  
                  |
57 | | 1cnd 7973 |
. . . 4
 
   |
58 | | eleq1w 2238 |
. . . . . . . 8
 
   |
59 | 58 | dcbid 838 |
. . . . . . 7
 DECID
DECID
   |
60 | 59 | cbvralv 2704 |
. . . . . 6
 
DECID
 DECID   |
61 | 11, 60 | sylib 122 |
. . . . 5
  DECID   |
62 | 61 | r19.21bi 2565 |
. . . 4
 

DECID
  |
63 | 8, 57, 62 | ifcldcd 3571 |
. . 3
 
        |
64 | | eleq1w 2238 |
. . . . . . . 8
 
   |
65 | 64 | dcbid 838 |
. . . . . . 7
 DECID
DECID
   |
66 | 65 | cbvralv 2704 |
. . . . . 6
 
DECID
 DECID   |
67 | 50, 66 | sylib 122 |
. . . . 5
  DECID   |
68 | 67 | r19.21bi 2565 |
. . . 4
 

DECID
  |
69 | 8, 57, 68 | ifcldcd 3571 |
. . 3
 
        |
70 | 15, 63, 69 | fprodmul 11599 |
. 2
                              |
71 | 4 | eleq2d 2247 |
. . . . . 6
       |
72 | | elun 3277 |
. . . . . 6
  

   |
73 | 71, 72 | bitrdi 196 |
. . . . 5
  
    |
74 | 73 | biimpa 296 |
. . . 4
 
 
   |
75 | | disjel 3478 |
. . . . . . . . 9
    
  |
76 | 26, 75 | sylan 283 |
. . . . . . . 8
 

  |
77 | 76 | iffalsed 3545 |
. . . . . . 7
 
        |
78 | 6, 77 | oveq12d 5893 |
. . . . . 6
 
                 |
79 | 9 | mulridd 7974 |
. . . . . 6
 
 
   |
80 | 78, 79 | eqtrd 2210 |
. . . . 5
 
               |
81 | 76 | ex 115 |
. . . . . . . . . 10
     |
82 | 81 | con2d 624 |
. . . . . . . . 9
     |
83 | 82 | imp 124 |
. . . . . . . 8
 

  |
84 | 83 | iffalsed 3545 |
. . . . . . 7
 
        |
85 | 84, 22 | oveq12d 5893 |
. . . . . 6
 
                 |
86 | 24 | mulid2d 7976 |
. . . . . 6
 
     |
87 | 85, 86 | eqtrd 2210 |
. . . . 5
 
               |
88 | 80, 87 | jaodan 797 |
. . . 4
 

                |
89 | 74, 88 | syldan 282 |
. . 3
 
               |
90 | 89 | prodeq2dv 11574 |
. 2
              
  |
91 | 56, 70, 90 | 3eqtr2rd 2217 |
1
 
      |