Proof of Theorem 31prm
Step | Hyp | Ref
| Expression |
1 | | 2z 11409 |
. . 3
|
2 | | 3nn0 11310 |
. . . . 5
|
3 | | 1nn0 11308 |
. . . . 5
|
4 | 2, 3 | deccl 11512 |
. . . 4
; |
5 | 4 | nn0zi 11402 |
. . 3
; |
6 | | 3nn 11186 |
. . . 4
|
7 | | 2nn0 11309 |
. . . 4
|
8 | | 2re 11090 |
. . . . 5
|
9 | | 9re 11107 |
. . . . 5
|
10 | | 2lt9 11228 |
. . . . 5
|
11 | 8, 9, 10 | ltleii 10160 |
. . . 4
|
12 | 6, 3, 7, 11 | declei 11542 |
. . 3
; |
13 | | eluz2 11693 |
. . 3
;
;
; |
14 | 1, 5, 12, 13 | mpbir3an 1244 |
. 2
; |
15 | | elun 3753 |
. . . . . 6
|
16 | | elin 3796 |
. . . . . . . 8
|
17 | | vex 3203 |
. . . . . . . . . . 11
|
18 | 17 | elpr 4198 |
. . . . . . . . . 10
|
19 | | 0nn0 11307 |
. . . . . . . . . . . . 13
|
20 | | 2cn 11091 |
. . . . . . . . . . . . . 14
|
21 | 20 | mul02i 10225 |
. . . . . . . . . . . . 13
|
22 | | 1e0p1 11552 |
. . . . . . . . . . . . 13
|
23 | 2, 19, 21, 22 | dec2dvds 15767 |
. . . . . . . . . . . 12
; |
24 | | breq1 4656 |
. . . . . . . . . . . 12
;
; |
25 | 23, 24 | mtbiri 317 |
. . . . . . . . . . 11
; |
26 | | 3ndvds4 41510 |
. . . . . . . . . . . . 13
|
27 | 2, 3 | 3dvdsdec 15054 |
. . . . . . . . . . . . . 14
; |
28 | | 3p1e4 11153 |
. . . . . . . . . . . . . . 15
|
29 | 28 | breq2i 4661 |
. . . . . . . . . . . . . 14
|
30 | 27, 29 | bitri 264 |
. . . . . . . . . . . . 13
; |
31 | 26, 30 | mtbir 313 |
. . . . . . . . . . . 12
; |
32 | | breq1 4656 |
. . . . . . . . . . . 12
;
; |
33 | 31, 32 | mtbiri 317 |
. . . . . . . . . . 11
; |
34 | 25, 33 | jaoi 394 |
. . . . . . . . . 10
; |
35 | 18, 34 | sylbi 207 |
. . . . . . . . 9
; |
36 | 35 | adantr 481 |
. . . . . . . 8
; |
37 | 16, 36 | sylbi 207 |
. . . . . . 7
; |
38 | | elin 3796 |
. . . . . . . 8
|
39 | 17 | elpr 4198 |
. . . . . . . . . 10
|
40 | | eleq1 2689 |
. . . . . . . . . . . 12
|
41 | | 4nprm 15407 |
. . . . . . . . . . . . 13
|
42 | 41 | pm2.21i 116 |
. . . . . . . . . . . 12
; |
43 | 40, 42 | syl6bi 243 |
. . . . . . . . . . 11
; |
44 | | 1nn 11031 |
. . . . . . . . . . . . . 14
|
45 | | 1lt5 11203 |
. . . . . . . . . . . . . 14
|
46 | 2, 44, 45 | dec5dvds 15768 |
. . . . . . . . . . . . 13
; |
47 | | breq1 4656 |
. . . . . . . . . . . . 13
;
; |
48 | 46, 47 | mtbiri 317 |
. . . . . . . . . . . 12
; |
49 | 48 | a1d 25 |
. . . . . . . . . . 11
; |
50 | 43, 49 | jaoi 394 |
. . . . . . . . . 10
; |
51 | 39, 50 | sylbi 207 |
. . . . . . . . 9
; |
52 | 51 | imp 445 |
. . . . . . . 8
; |
53 | 38, 52 | sylbi 207 |
. . . . . . 7
; |
54 | 37, 53 | jaoi 394 |
. . . . . 6
; |
55 | 15, 54 | sylbi 207 |
. . . . 5
; |
56 | | indir 3875 |
. . . . 5
|
57 | 55, 56 | eleq2s 2719 |
. . . 4
; |
58 | | 5nn0 11312 |
. . . . . . . . 9
|
59 | | 5re 11099 |
. . . . . . . . . 10
|
60 | | 5lt9 11225 |
. . . . . . . . . 10
|
61 | 59, 9, 60 | ltleii 10160 |
. . . . . . . . 9
|
62 | | 2lt3 11195 |
. . . . . . . . 9
|
63 | 7, 2, 58, 3, 61, 62 | decleh 11541 |
. . . . . . . 8
; ; |
64 | | 6nn 11189 |
. . . . . . . . 9
|
65 | | 1lt6 11208 |
. . . . . . . . 9
|
66 | 2, 3, 64, 65 | declt 11530 |
. . . . . . . 8
; ; |
67 | 4 | nn0rei 11303 |
. . . . . . . . . 10
; |
68 | | 0re 10040 |
. . . . . . . . . . . 12
|
69 | | 9pos 11122 |
. . . . . . . . . . . 12
|
70 | 68, 9, 69 | ltleii 10160 |
. . . . . . . . . . 11
|
71 | 6, 3, 19, 70 | declei 11542 |
. . . . . . . . . 10
; |
72 | 67, 71 | pm3.2i 471 |
. . . . . . . . 9
;
; |
73 | | flsqrt5 41509 |
. . . . . . . . . 10
; ; ; ; ; ;
; |
74 | 73 | bicomd 213 |
. . . . . . . . 9
; ; ;
; ; ; ; |
75 | 72, 74 | ax-mp 5 |
. . . . . . . 8
; ; ; ; ; |
76 | 63, 66, 75 | mpbir2an 955 |
. . . . . . 7
; |
77 | 76 | oveq2i 6661 |
. . . . . 6
; |
78 | | 5nn 11188 |
. . . . . . . . . 10
|
79 | 78 | nnzi 11401 |
. . . . . . . . 9
|
80 | | 3z 11410 |
. . . . . . . . 9
|
81 | 1, 79, 80 | 3pm3.2i 1239 |
. . . . . . . 8
|
82 | | 3re 11094 |
. . . . . . . . . 10
|
83 | 8, 82, 62 | ltleii 10160 |
. . . . . . . . 9
|
84 | | 3lt5 11201 |
. . . . . . . . . 10
|
85 | 82, 59, 84 | ltleii 10160 |
. . . . . . . . 9
|
86 | 83, 85 | pm3.2i 471 |
. . . . . . . 8
|
87 | | elfz2 12333 |
. . . . . . . 8
|
88 | 81, 86, 87 | mpbir2an 955 |
. . . . . . 7
|
89 | | fzsplit 12367 |
. . . . . . 7
|
90 | 88, 89 | ax-mp 5 |
. . . . . 6
|
91 | | df-3 11080 |
. . . . . . . . 9
|
92 | 91 | oveq2i 6661 |
. . . . . . . 8
|
93 | | fzpr 12396 |
. . . . . . . . 9
|
94 | 1, 93 | ax-mp 5 |
. . . . . . . 8
|
95 | | 2p1e3 11151 |
. . . . . . . . 9
|
96 | 95 | preq2i 4272 |
. . . . . . . 8
|
97 | 92, 94, 96 | 3eqtri 2648 |
. . . . . . 7
|
98 | 28 | oveq1i 6660 |
. . . . . . . 8
|
99 | | df-5 11082 |
. . . . . . . . 9
|
100 | 99 | oveq2i 6661 |
. . . . . . . 8
|
101 | | 4z 11411 |
. . . . . . . . . 10
|
102 | | fzpr 12396 |
. . . . . . . . . 10
|
103 | 101, 102 | ax-mp 5 |
. . . . . . . . 9
|
104 | | 4p1e5 11154 |
. . . . . . . . . 10
|
105 | 104 | preq2i 4272 |
. . . . . . . . 9
|
106 | 103, 105 | eqtri 2644 |
. . . . . . . 8
|
107 | 98, 100, 106 | 3eqtri 2648 |
. . . . . . 7
|
108 | 97, 107 | uneq12i 3765 |
. . . . . 6
|
109 | 77, 90, 108 | 3eqtri 2648 |
. . . . 5
; |
110 | 109 | ineq1i 3810 |
. . . 4
; |
111 | 57, 110 | eleq2s 2719 |
. . 3
; ; |
112 | 111 | rgen 2922 |
. 2
;
; |
113 | | isprm7 15420 |
. 2
; ;
;
; |
114 | 14, 112, 113 | mpbir2an 955 |
1
; |