Proof of Theorem fmtno4nprmfac193
Step | Hyp | Ref
| Expression |
1 | | 1nn0 11308 |
. . . . 5
|
2 | | 9nn0 11316 |
. . . . 5
|
3 | 1, 2 | deccl 11512 |
. . . 4
; |
4 | | 3nn 11186 |
. . . 4
|
5 | 3, 4 | decnncl 11518 |
. . 3
;; |
6 | | 3nn0 11310 |
. . . . 5
|
7 | 6, 6 | deccl 11512 |
. . . 4
; |
8 | 7, 2 | deccl 11512 |
. . 3
;; |
9 | | 1nn 11031 |
. . . . 5
|
10 | 1, 9 | decnncl 11518 |
. . . 4
; |
11 | 10 | decnncl2 11525 |
. . 3
;; |
12 | | 6nn0 11313 |
. . . . . . 7
|
13 | | 5nn0 11312 |
. . . . . . 7
|
14 | 12, 13 | deccl 11512 |
. . . . . 6
; |
15 | | 4nn0 11311 |
. . . . . 6
|
16 | 14, 15 | deccl 11512 |
. . . . 5
;; |
17 | | 2nn0 11309 |
. . . . 5
|
18 | 16, 17 | deccl 11512 |
. . . 4
;;; |
19 | | 7nn0 11314 |
. . . 4
|
20 | 1, 1 | deccl 11512 |
. . . 4
; |
21 | | 0nn0 11307 |
. . . 4
|
22 | 3, 6 | deccl 11512 |
. . . . 5
;; |
23 | | eqid 2622 |
. . . . 5
;; ;; |
24 | 1, 19 | deccl 11512 |
. . . . . 6
; |
25 | 24, 6 | deccl 11512 |
. . . . 5
;; |
26 | | eqid 2622 |
. . . . . 6
; ; |
27 | | eqid 2622 |
. . . . . 6
;; ;; |
28 | | 8nn0 11315 |
. . . . . . 7
|
29 | 13, 28 | deccl 11512 |
. . . . . 6
; |
30 | 13, 19 | deccl 11512 |
. . . . . . 7
; |
31 | | eqid 2622 |
. . . . . . . 8
;; ;; |
32 | | eqid 2622 |
. . . . . . . . 9
; ; |
33 | | 3cn 11095 |
. . . . . . . . . . . 12
|
34 | 33 | mulid2i 10043 |
. . . . . . . . . . 11
|
35 | 34 | oveq1i 6660 |
. . . . . . . . . 10
|
36 | | 3p2e5 11160 |
. . . . . . . . . 10
|
37 | 35, 36 | eqtri 2644 |
. . . . . . . . 9
|
38 | | 9t3e27 11664 |
. . . . . . . . 9
; |
39 | 6, 1, 2, 32, 19, 17, 37, 38 | decmul1c 11587 |
. . . . . . . 8
; ; |
40 | | 3t3e9 11180 |
. . . . . . . 8
|
41 | 6, 3, 6, 31, 2, 39, 40 | decmul1 11585 |
. . . . . . 7
;; ;; |
42 | | eqid 2622 |
. . . . . . . 8
; ; |
43 | | eqid 2622 |
. . . . . . . 8
; ; |
44 | | 5cn 11100 |
. . . . . . . . . . 11
|
45 | | ax-1cn 9994 |
. . . . . . . . . . 11
|
46 | | 5p1e6 11155 |
. . . . . . . . . . 11
|
47 | 44, 45, 46 | addcomli 10228 |
. . . . . . . . . 10
|
48 | 47 | oveq1i 6660 |
. . . . . . . . 9
|
49 | | 6p1e7 11156 |
. . . . . . . . 9
|
50 | 48, 49 | eqtri 2644 |
. . . . . . . 8
|
51 | | 8cn 11106 |
. . . . . . . . 9
|
52 | | 7cn 11104 |
. . . . . . . . 9
|
53 | | 8p7e15 11617 |
. . . . . . . . 9
; |
54 | 51, 52, 53 | addcomli 10228 |
. . . . . . . 8
; |
55 | 1, 19, 13, 28, 42, 43, 50, 13, 54 | decaddc 11572 |
. . . . . . 7
; ; ; |
56 | | 4p1e5 11154 |
. . . . . . . 8
|
57 | | eqid 2622 |
. . . . . . . . 9
; ; |
58 | | 7p7e14 11609 |
. . . . . . . . 9
; |
59 | 13, 19, 19, 57, 46, 15, 58 | decaddci 11580 |
. . . . . . . 8
; ; |
60 | 12, 15, 56, 59 | decsuc 11535 |
. . . . . . 7
; ; |
61 | | 9p5e14 11623 |
. . . . . . 7
; |
62 | 30, 2, 19, 13, 41, 55, 60, 15, 61 | decaddc 11572 |
. . . . . 6
;; ; ; ;; |
63 | | 7p1e8 11157 |
. . . . . . . 8
|
64 | 13, 19, 63, 57 | decsuc 11535 |
. . . . . . 7
; ; |
65 | | 9p3e12 11621 |
. . . . . . 7
; |
66 | 30, 2, 6, 41, 64, 17, 65 | decaddci 11580 |
. . . . . 6
;; ;; |
67 | 6, 6, 24, 6, 26, 27, 22, 17, 29, 62, 66 | decma2c 11568 |
. . . . 5
;; ; ;; ;;; |
68 | | 9cn 11108 |
. . . . . . . . . . 11
|
69 | 68 | mulid2i 10043 |
. . . . . . . . . 10
|
70 | 69 | oveq1i 6660 |
. . . . . . . . 9
|
71 | | 9p8e17 11626 |
. . . . . . . . 9
; |
72 | 70, 71 | eqtri 2644 |
. . . . . . . 8
; |
73 | | 9t9e81 11670 |
. . . . . . . 8
; |
74 | 2, 1, 2, 32, 1, 28, 72, 73 | decmul1c 11587 |
. . . . . . 7
; ;; |
75 | | 1p2e3 11152 |
. . . . . . 7
|
76 | 24, 1, 17, 74, 75 | decaddi 11579 |
. . . . . 6
; ;; |
77 | 68, 33, 38 | mulcomli 10047 |
. . . . . 6
; |
78 | 2, 3, 6, 31, 19, 17, 76, 77 | decmul1c 11587 |
. . . . 5
;; ;;; |
79 | 22, 7, 2, 23, 19, 25, 67, 78 | decmul2c 11589 |
. . . 4
;; ;; ;;;; |
80 | | eqid 2622 |
. . . 4
;; ;; |
81 | | eqid 2622 |
. . . . 5
;;; ;;; |
82 | | eqid 2622 |
. . . . 5
; ; |
83 | | eqid 2622 |
. . . . . 6
;; ;; |
84 | 14, 15, 56, 83 | decsuc 11535 |
. . . . 5
;; ;; |
85 | | 2p1e3 11151 |
. . . . 5
|
86 | 16, 17, 1, 1, 81, 82, 84, 85 | decadd 11570 |
. . . 4
;;; ; ;;; |
87 | 52 | addid1i 10223 |
. . . 4
|
88 | 18, 19, 20, 21, 79, 80, 86, 87 | decadd 11570 |
. . 3
;; ;; ;; ;;;; |
89 | | 10pos 11515 |
. . . 4
; |
90 | | 9nn 11192 |
. . . . 5
|
91 | | 1lt9 11229 |
. . . . 5
|
92 | 1, 1, 90, 91 | declt 11530 |
. . . 4
; ; |
93 | 20, 3, 21, 6, 89, 92 | decltc 11532 |
. . 3
;; ;; |
94 | 5, 8, 11, 88, 93 | ndvdsi 15136 |
. 2
;; ;;;; |
95 | | fmtno4 41464 |
. . 3
FermatNo ;;;; |
96 | 95 | breq2i 4661 |
. 2
;; FermatNo
;; ;;;; |
97 | 94, 96 | mtbir 313 |
1
;; FermatNo |