Proof of Theorem oeoa
Step | Hyp | Ref
| Expression |
1 | | oa00 7246 |
. . . . . . . . 9
 
    
    |
2 | 1 | biimpar 492 |
. . . . . . . 8
           |
3 | 2 | oveq2d 6291 |
. . . . . . 7
           
   |
4 | | oveq2 6283 |
. . . . . . . . . 10

  
   |
5 | | oveq2 6283 |
. . . . . . . . . . 11

  
   |
6 | | oe0m0 7208 |
. . . . . . . . . . 11
 
 |
7 | 5, 6 | syl6eq 2501 |
. . . . . . . . . 10

    |
8 | 4, 7 | oveqan12d 6294 |
. . . . . . . . 9
          
    |
9 | | 0elon 5454 |
. . . . . . . . . . 11
 |
10 | | oecl 7225 |
. . . . . . . . . . 11
 
     |
11 | 9, 9, 10 | mp2an 683 |
. . . . . . . . . 10
 
 |
12 | | om1 7229 |
. . . . . . . . . 10
 

   
    |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . 9
 
  
  |
14 | 8, 13 | syl6eq 2501 |
. . . . . . . 8
         
   |
15 | 14 | adantl 472 |
. . . . . . 7
             
   |
16 | 3, 15 | eqtr4d 2488 |
. . . . . 6
                   |
17 | | oacl 7223 |
. . . . . . . . . 10
 
     |
18 | | on0eln0 5456 |
. . . . . . . . . 10
     
     |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
 
 
 
     |
20 | | oe0m1 7209 |
. . . . . . . . . 10
     
       |
21 | 17, 20 | syl 17 |
. . . . . . . . 9
 
 
 
       |
22 | 1 | necon3abid 2659 |
. . . . . . . . 9
 
   

    |
23 | 19, 21, 22 | 3bitr3d 291 |
. . . . . . . 8
 
     
     |
24 | 23 | biimpar 492 |
. . . . . . 7
    
        |
25 | | on0eln0 5456 |
. . . . . . . . . . . 12
 
   |
26 | 25 | adantr 471 |
. . . . . . . . . . 11
 
 
   |
27 | | on0eln0 5456 |
. . . . . . . . . . . 12
 
   |
28 | 27 | adantl 472 |
. . . . . . . . . . 11
 
 
   |
29 | 26, 28 | orbi12d 721 |
. . . . . . . . . 10
 
         |
30 | | neorian 2717 |
. . . . . . . . . 10
  

   |
31 | 29, 30 | syl6bb 269 |
. . . . . . . . 9
 
         |
32 | | oe0m1 7209 |
. . . . . . . . . . . . . . 15
 
     |
33 | 32 | biimpa 491 |
. . . . . . . . . . . . . 14
       |
34 | 33 | oveq1d 6290 |
. . . . . . . . . . . . 13
         
     |
35 | | oecl 7225 |
. . . . . . . . . . . . . . 15
 
     |
36 | 9, 35 | mpan 681 |
. . . . . . . . . . . . . 14
     |
37 | | om0r 7227 |
. . . . . . . . . . . . . 14
 

      |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . 13
       |
39 | 34, 38 | sylan9eq 2505 |
. . . . . . . . . . . 12
   
         |
40 | 39 | an32s 818 |
. . . . . . . . . . 11
             |
41 | | oe0m1 7209 |
. . . . . . . . . . . . . . 15
 
     |
42 | 41 | biimpa 491 |
. . . . . . . . . . . . . 14
       |
43 | 42 | oveq2d 6291 |
. . . . . . . . . . . . 13
               |
44 | | oecl 7225 |
. . . . . . . . . . . . . . 15
 
     |
45 | 9, 44 | mpan 681 |
. . . . . . . . . . . . . 14
     |
46 | | om0 7205 |
. . . . . . . . . . . . . 14
 

   
  |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . 13
       |
48 | 43, 47 | sylan9eqr 2507 |
. . . . . . . . . . . 12
  
          |
49 | 48 | anassrs 658 |
. . . . . . . . . . 11
             |
50 | 40, 49 | jaodan 799 |
. . . . . . . . . 10
      
   
    |
51 | 50 | ex 440 |
. . . . . . . . 9
 
             |
52 | 31, 51 | sylbird 243 |
. . . . . . . 8
 
  

 
 
     |
53 | 52 | imp 435 |
. . . . . . 7
    
          |
54 | 24, 53 | eqtr4d 2488 |
. . . . . 6
    
              |
55 | 16, 54 | pm2.61dan 805 |
. . . . 5
 
 
           |
56 | | oveq1 6282 |
. . . . . 6

    
     |
57 | | oveq1 6282 |
. . . . . . 7

  
   |
58 | | oveq1 6282 |
. . . . . . 7

  
   |
59 | 57, 58 | oveq12d 6293 |
. . . . . 6

              |
60 | 56, 59 | eqeq12d 2466 |
. . . . 5

          
             |
61 | 55, 60 | syl5ibr 229 |
. . . 4

 
              |
62 | 61 | impcom 436 |
. . 3
      
          |
63 | | oveq1 6282 |
. . . . . . . 8
         
         
     |
64 | | oveq1 6282 |
. . . . . . . . 9
                 
   |
65 | | oveq1 6282 |
. . . . . . . . 9
                 
   |
66 | 64, 65 | oveq12d 6293 |
. . . . . . . 8
                                    |
67 | 63, 66 | eqeq12d 2466 |
. . . . . . 7
                                                     |
68 | 67 | imbi2d 322 |
. . . . . 6
                     
       
           
               |
69 | | oveq1 6282 |
. . . . . . . . 9
                 |
70 | 69 | oveq2d 6291 |
. . . . . . . 8
             
               
     |
71 | | oveq2 6283 |
. . . . . . . . 9
             
                 |
72 | 71 | oveq1d 6290 |
. . . . . . . 8
                                  
   
         
    |
73 | 70, 72 | eqeq12d 2466 |
. . . . . . 7
                                                  
                               |
74 | 73 | imbi2d 322 |
. . . . . 6
                                        
       
                
   
         
      |
75 | | eleq1 2517 |
. . . . . . . . . 10
               
   |
76 | | eleq2 2518 |
. . . . . . . . . 10
                   |
77 | 75, 76 | anbi12d 722 |
. . . . . . . . 9
                              |
78 | | eleq1 2517 |
. . . . . . . . . 10
               
   |
79 | | eleq2 2518 |
. . . . . . . . . 10
                   |
80 | 78, 79 | anbi12d 722 |
. . . . . . . . 9
                              |
81 | | 1on 7175 |
. . . . . . . . . 10
 |
82 | | 0lt1o 7192 |
. . . . . . . . . 10
 |
83 | 81, 82 | pm3.2i 461 |
. . . . . . . . 9
   |
84 | 77, 80, 83 | elimhyp 3906 |
. . . . . . . 8
       
         |
85 | 84 | simpli 464 |
. . . . . . 7
        |
86 | 84 | simpri 468 |
. . . . . . 7
        |
87 | 81 | elimel 3910 |
. . . . . . 7
   
  |
88 | 85, 86, 87 | oeoalem 7283 |
. . . . . 6
        
                
   
         
    |
89 | 68, 74, 88 | dedth2h 3900 |
. . . . 5
   
               |
90 | 89 | impr 629 |
. . . 4
    
 
            |
91 | 90 | an32s 818 |
. . 3
      
            |
92 | 62, 91 | oe0lem 7201 |
. 2
  
 
            |
93 | 92 | 3impb 1206 |
1
 
             |