Proof of Theorem 2503prm
Step | Hyp | Ref
| Expression |
1 | | 139prm 15107 |
. 2
;;   |
2 | | 1nn0 10892 |
. . 3
 |
3 | | 8nn 10780 |
. . 3
 |
4 | 2, 3 | decnncl 11071 |
. 2
;  |
5 | | 2503prm.1 |
. . . . 5
;;;    |
6 | | 2nn0 10893 |
. . . . . . . 8
 |
7 | | 5nn0 10896 |
. . . . . . . 8
 |
8 | 6, 7 | deccl 11072 |
. . . . . . 7
;  |
9 | | 0nn0 10891 |
. . . . . . 7
 |
10 | 8, 9 | deccl 11072 |
. . . . . 6
;;   |
11 | | 2p1e3 10740 |
. . . . . 6
   |
12 | | eqid 2453 |
. . . . . 6
;;;   ;;;    |
13 | 10, 6, 11, 12 | decsuc 11081 |
. . . . 5
;;;    ;;;    |
14 | 5, 13 | eqtr4i 2478 |
. . . 4
;;;     |
15 | 14 | oveq1i 6305 |
. . 3
   ;;;      |
16 | | 8nn0 10899 |
. . . . . 6
 |
17 | 2, 16 | deccl 11072 |
. . . . 5
;  |
18 | | 3nn0 10894 |
. . . . . 6
 |
19 | 2, 18 | deccl 11072 |
. . . . 5
;  |
20 | | 9nn0 10900 |
. . . . 5
 |
21 | | eqid 2453 |
. . . . 5
;;  ;;   |
22 | | 6nn0 10897 |
. . . . . 6
 |
23 | 2, 22 | deccl 11072 |
. . . . 5
;  |
24 | | eqid 2453 |
. . . . . 6
; ;  |
25 | | eqid 2453 |
. . . . . 6
; ;  |
26 | | 7nn0 10898 |
. . . . . . 7
 |
27 | | eqid 2453 |
. . . . . . 7
; ;  |
28 | | 6cn 10698 |
. . . . . . . . 9
 |
29 | | ax-1cn 9602 |
. . . . . . . . 9
 |
30 | | 6p1e7 10745 |
. . . . . . . . 9
   |
31 | 28, 29, 30 | addcomli 9830 |
. . . . . . . 8
   |
32 | 26 | dec0h 11074 |
. . . . . . . 8
;  |
33 | 31, 32 | eqtri 2475 |
. . . . . . 7
  ;  |
34 | 29 | mulid1i 9650 |
. . . . . . . . 9
   |
35 | 29 | addid2i 9826 |
. . . . . . . . 9
   |
36 | 34, 35 | oveq12i 6307 |
. . . . . . . 8
         |
37 | | 1p1e2 10730 |
. . . . . . . 8
   |
38 | 36, 37 | eqtri 2475 |
. . . . . . 7
       |
39 | | 8cn 10702 |
. . . . . . . . . 10
 |
40 | 39 | mulid1i 9650 |
. . . . . . . . 9
   |
41 | 40 | oveq1i 6305 |
. . . . . . . 8
       |
42 | | 8p7e15 11118 |
. . . . . . . 8
  ;  |
43 | 41, 42 | eqtri 2475 |
. . . . . . 7
    ;  |
44 | 2, 16, 9, 26, 27, 33, 2, 7, 2,
38, 43 | decmac 11097 |
. . . . . 6
 ;     ;  |
45 | 22 | dec0h 11074 |
. . . . . . 7
;  |
46 | | 3cn 10691 |
. . . . . . . . . 10
 |
47 | 46 | mulid2i 9651 |
. . . . . . . . 9
   |
48 | 46 | addid2i 9826 |
. . . . . . . . 9
   |
49 | 47, 48 | oveq12i 6307 |
. . . . . . . 8
         |
50 | | 3p3e6 10750 |
. . . . . . . 8
   |
51 | 49, 50 | eqtri 2475 |
. . . . . . 7
       |
52 | | 4nn0 10895 |
. . . . . . . 8
 |
53 | | 8t3e24 11147 |
. . . . . . . 8
  ;  |
54 | | 4cn 10694 |
. . . . . . . . 9
 |
55 | | 6p4e10 10760 |
. . . . . . . . 9
   |
56 | 28, 54, 55 | addcomli 9830 |
. . . . . . . 8
   |
57 | 6, 52, 22, 53, 11, 56 | decaddci2 11104 |
. . . . . . 7
    ;  |
58 | 2, 16, 9, 22, 27, 45, 18, 9, 18, 51, 57 | decmac 11097 |
. . . . . 6
 ;   ;  |
59 | 2, 18, 2, 22, 24, 25, 17, 9, 22, 44, 58 | decma2c 11098 |
. . . . 5
 ; ;  ;  ;;   |
60 | | 9cn 10704 |
. . . . . . . . 9
 |
61 | 60 | mulid2i 9651 |
. . . . . . . 8
   |
62 | 61 | oveq1i 6305 |
. . . . . . 7
       |
63 | | 9p7e16 11125 |
. . . . . . 7
  ;  |
64 | 62, 63 | eqtri 2475 |
. . . . . 6
    ;  |
65 | | 9t8e72 11159 |
. . . . . . 7
  ;  |
66 | 60, 39, 65 | mulcomli 9655 |
. . . . . 6
  ;  |
67 | 20, 2, 16, 27, 6, 26, 64, 66 | decmul1c 11105 |
. . . . 5
;  ;;   |
68 | 17, 19, 20, 21, 6, 23, 59, 67 | decmul2c 11106 |
. . . 4
; ;;   ;;;    |
69 | 10, 6 | deccl 11072 |
. . . . . 6
;;;    |
70 | 69 | nn0cni 10888 |
. . . . 5
;;;    |
71 | 70, 29 | pncan3oi 9896 |
. . . 4
 ;;;     ;;;    |
72 | 68, 71 | eqtr4i 2478 |
. . 3
; ;;    ;;;      |
73 | 15, 72 | eqtr4i 2478 |
. 2
  ; ;;    |
74 | 10, 18 | deccl 11072 |
. . . . . 6
;;;    |
75 | 5, 74 | eqeltri 2527 |
. . . . 5
 |
76 | 75 | nn0cni 10888 |
. . . 4
 |
77 | | npcan 9889 |
. . . 4
 
       |
78 | 76, 29, 77 | mp2an 679 |
. . 3
     |
79 | 78 | eqcomi 2462 |
. 2
     |
80 | | 1nn 10627 |
. 2
 |
81 | | 2nn 10774 |
. 2
 |
82 | 19, 20 | deccl 11072 |
. . . . 5
;;   |
83 | 82 | numexp1 15061 |
. . . 4
;;     ;;   |
84 | 83 | oveq2i 6306 |
. . 3
; ;;      ; ;;    |
85 | 73, 84 | eqtr4i 2478 |
. 2
  ; ;;       |
86 | | 8lt10 10820 |
. . . 4
 |
87 | | 1lt10 10827 |
. . . . 5
 |
88 | 80, 18, 2, 87 | declti 11083 |
. . . 4
;  |
89 | 2, 19, 16, 20, 86, 88 | decltc 11080 |
. . 3
; ;;   |
90 | 89, 83 | breqtrri 4431 |
. 2
; ;;      |
91 | 5 | 2503lem2 15121 |
. 2
           |
92 | 5 | 2503lem3 15122 |
. 2
    ;     |
93 | 1, 4, 73, 79, 4, 80, 81, 85, 90, 91, 92 | pockthi 14863 |
1
 |