Step | Hyp | Ref
| Expression |
1 | | bitsval 15146 |
. . . 4
bits
|
2 | | simp32 1098 |
. . . . . . 7
..^
|
3 | | nn0uz 11722 |
. . . . . . 7
|
4 | 2, 3 | syl6eleq 2711 |
. . . . . 6
..^
|
5 | | simp1r 1086 |
. . . . . . 7
..^
|
6 | 5 | nn0zd 11480 |
. . . . . 6
..^
|
7 | | 2re 11090 |
. . . . . . . . . 10
|
8 | 7 | a1i 11 |
. . . . . . . . 9
..^
|
9 | 8, 2 | reexpcld 13025 |
. . . . . . . 8
..^
|
10 | | simp1l 1085 |
. . . . . . . . 9
..^
|
11 | 10 | zred 11482 |
. . . . . . . 8
..^
|
12 | 8, 5 | reexpcld 13025 |
. . . . . . . 8
..^
|
13 | 9 | recnd 10068 |
. . . . . . . . . 10
..^
|
14 | 13 | mulid2d 10058 |
. . . . . . . . 9
..^
|
15 | | simp33 1099 |
. . . . . . . . . . 11
..^
|
16 | | 2rp 11837 |
. . . . . . . . . . . . . . . 16
|
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . 15
..^
|
18 | 2 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
..^
|
19 | 17, 18 | rpexpcld 13032 |
. . . . . . . . . . . . . 14
..^
|
20 | 11, 19 | rerpdivcld 11903 |
. . . . . . . . . . . . 13
..^
|
21 | | 1red 10055 |
. . . . . . . . . . . . 13
..^
|
22 | 20, 21 | ltnled 10184 |
. . . . . . . . . . . 12
..^
|
23 | | 0p1e1 11132 |
. . . . . . . . . . . . . 14
|
24 | 23 | breq2i 4661 |
. . . . . . . . . . . . 13
|
25 | | elfzole1 12478 |
. . . . . . . . . . . . . . . 16
..^
|
26 | 25 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
..^
|
27 | 11, 19, 26 | divge0d 11912 |
. . . . . . . . . . . . . 14
..^
|
28 | | 0z 11388 |
. . . . . . . . . . . . . . . 16
|
29 | | flbi 12617 |
. . . . . . . . . . . . . . . 16
|
30 | 20, 28, 29 | sylancl 694 |
. . . . . . . . . . . . . . 15
..^
|
31 | | 2z 11409 |
. . . . . . . . . . . . . . . . 17
|
32 | | dvds0 14997 |
. . . . . . . . . . . . . . . . 17
|
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
34 | | id 22 |
. . . . . . . . . . . . . . . 16
|
35 | 33, 34 | syl5breqr 4691 |
. . . . . . . . . . . . . . 15
|
36 | 30, 35 | syl6bir 244 |
. . . . . . . . . . . . . 14
..^
|
37 | 27, 36 | mpand 711 |
. . . . . . . . . . . . 13
..^
|
38 | 24, 37 | syl5bir 233 |
. . . . . . . . . . . 12
..^
|
39 | 22, 38 | sylbird 250 |
. . . . . . . . . . 11
..^
|
40 | 15, 39 | mt3d 140 |
. . . . . . . . . 10
..^
|
41 | 21, 11, 19 | lemuldivd 11921 |
. . . . . . . . . 10
..^
|
42 | 40, 41 | mpbird 247 |
. . . . . . . . 9
..^
|
43 | 14, 42 | eqbrtrrd 4677 |
. . . . . . . 8
..^
|
44 | | elfzolt2 12479 |
. . . . . . . . 9
..^
|
45 | 44 | 3ad2ant2 1083 |
. . . . . . . 8
..^
|
46 | 9, 11, 12, 43, 45 | lelttrd 10195 |
. . . . . . 7
..^
|
47 | | 1lt2 11194 |
. . . . . . . . 9
|
48 | 47 | a1i 11 |
. . . . . . . 8
..^
|
49 | 8, 18, 6, 48 | ltexp2d 13038 |
. . . . . . 7
..^
|
50 | 46, 49 | mpbird 247 |
. . . . . 6
..^
|
51 | | elfzo2 12473 |
. . . . . 6
..^
|
52 | 4, 6, 50, 51 | syl3anbrc 1246 |
. . . . 5
..^
..^ |
53 | 52 | 3expia 1267 |
. . . 4
..^
..^ |
54 | 1, 53 | syl5bi 232 |
. . 3
..^ bits ..^ |
55 | 54 | ssrdv 3609 |
. 2
..^ bits
..^ |
56 | | simpr 477 |
. . . . . . . 8
bits ..^ |
57 | 56 | nnred 11035 |
. . . . . . 7
bits ..^ |
58 | | simpllr 799 |
. . . . . . . 8
bits ..^ |
59 | 58 | nn0red 11352 |
. . . . . . 7
bits ..^ |
60 | | max2 12018 |
. . . . . . 7
|
61 | 57, 59, 60 | syl2anc 693 |
. . . . . 6
bits ..^ |
62 | | simplr 792 |
. . . . . . . . 9
bits ..^ bits
..^ |
63 | | n2dvds1 15104 |
. . . . . . . . . . . 12
|
64 | | 1z 11407 |
. . . . . . . . . . . . 13
|
65 | | dvdsnegb 14999 |
. . . . . . . . . . . . 13
|
66 | 31, 64, 65 | mp2an 708 |
. . . . . . . . . . . 12
|
67 | 63, 66 | mtbi 312 |
. . . . . . . . . . 11
|
68 | | simplll 798 |
. . . . . . . . . . . . . . . 16
bits ..^ |
69 | 68 | zred 11482 |
. . . . . . . . . . . . . . 15
bits ..^ |
70 | | 2nn 11185 |
. . . . . . . . . . . . . . . . 17
|
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . . 16
bits ..^ |
72 | 56 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
73 | 58, 72 | ifcld 4131 |
. . . . . . . . . . . . . . . 16
bits ..^ |
74 | 71, 73 | nnexpcld 13030 |
. . . . . . . . . . . . . . 15
bits ..^ |
75 | 69, 74 | nndivred 11069 |
. . . . . . . . . . . . . 14
bits ..^ |
76 | | 1red 10055 |
. . . . . . . . . . . . . 14
bits ..^ |
77 | 68 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
bits ..^ |
78 | 74 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
bits ..^ |
79 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
80 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . 18
|
81 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
82 | 73 | nn0zd 11480 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
83 | 79, 81, 82 | expne0d 13014 |
. . . . . . . . . . . . . . . 16
bits ..^ |
84 | 77, 78, 83 | divnegd 10814 |
. . . . . . . . . . . . . . 15
bits ..^ |
85 | 73 | nn0red 11352 |
. . . . . . . . . . . . . . . . . 18
bits ..^ |
86 | 74 | nnred 11035 |
. . . . . . . . . . . . . . . . . 18
bits ..^ |
87 | | max1 12016 |
. . . . . . . . . . . . . . . . . . 19
|
88 | 57, 59, 87 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
bits ..^ |
89 | | uzid 11702 |
. . . . . . . . . . . . . . . . . . . . 21
|
90 | 31, 89 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
|
91 | | bernneq3 12992 |
. . . . . . . . . . . . . . . . . . . 20
|
92 | 90, 73, 91 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
bits ..^ |
93 | 85, 86, 92 | ltled 10185 |
. . . . . . . . . . . . . . . . . 18
bits ..^ |
94 | 57, 85, 86, 88, 93 | letrd 10194 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
95 | 78 | mulid1d 10057 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
96 | 94, 95 | breqtrrd 4681 |
. . . . . . . . . . . . . . . 16
bits ..^ |
97 | 74 | nnrpd 11870 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
98 | 57, 76, 97 | ledivmuld 11925 |
. . . . . . . . . . . . . . . 16
bits ..^
|
99 | 96, 98 | mpbird 247 |
. . . . . . . . . . . . . . 15
bits ..^ |
100 | 84, 99 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
bits ..^ |
101 | 75, 76, 100 | lenegcon1d 10609 |
. . . . . . . . . . . . 13
bits ..^ |
102 | 56 | nngt0d 11064 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
103 | 74 | nngt0d 11064 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
104 | 57, 86, 102, 103 | divgt0d 10959 |
. . . . . . . . . . . . . . . 16
bits ..^ |
105 | 104, 84 | breqtrrd 4681 |
. . . . . . . . . . . . . . 15
bits ..^ |
106 | 75 | lt0neg1d 10597 |
. . . . . . . . . . . . . . 15
bits ..^
|
107 | 105, 106 | mpbird 247 |
. . . . . . . . . . . . . 14
bits ..^ |
108 | | ax-1cn 9994 |
. . . . . . . . . . . . . . 15
|
109 | | neg1cn 11124 |
. . . . . . . . . . . . . . 15
|
110 | | 1pneg1e0 11129 |
. . . . . . . . . . . . . . 15
|
111 | 108, 109,
110 | addcomli 10228 |
. . . . . . . . . . . . . 14
|
112 | 107, 111 | syl6breqr 4695 |
. . . . . . . . . . . . 13
bits ..^ |
113 | | neg1z 11413 |
. . . . . . . . . . . . . 14
|
114 | | flbi 12617 |
. . . . . . . . . . . . . 14
|
115 | 75, 113, 114 | sylancl 694 |
. . . . . . . . . . . . 13
bits ..^
|
116 | 101, 112,
115 | mpbir2and 957 |
. . . . . . . . . . . 12
bits ..^
|
117 | 116 | breq2d 4665 |
. . . . . . . . . . 11
bits ..^ |
118 | 67, 117 | mtbiri 317 |
. . . . . . . . . 10
bits ..^
|
119 | | bitsval2 15147 |
. . . . . . . . . . 11
bits
|
120 | 68, 73, 119 | syl2anc 693 |
. . . . . . . . . 10
bits ..^ bits
|
121 | 118, 120 | mpbird 247 |
. . . . . . . . 9
bits ..^ bits |
122 | 62, 121 | sseldd 3604 |
. . . . . . . 8
bits ..^ ..^ |
123 | | elfzolt2 12479 |
. . . . . . . 8
..^
|
124 | 122, 123 | syl 17 |
. . . . . . 7
bits ..^ |
125 | 85, 59 | ltnled 10184 |
. . . . . . 7
bits ..^
|
126 | 124, 125 | mpbid 222 |
. . . . . 6
bits ..^
|
127 | 61, 126 | pm2.65da 600 |
. . . . 5
bits ..^
|
128 | 127 | intnand 962 |
. . . 4
bits ..^
|
129 | | simpll 790 |
. . . . . 6
bits ..^
|
130 | | elznn0nn 11391 |
. . . . . 6
|
131 | 129, 130 | sylib 208 |
. . . . 5
bits ..^
|
132 | 131 | ord 392 |
. . . 4
bits ..^
|
133 | 128, 132 | mt3d 140 |
. . 3
bits ..^
|
134 | | simplr 792 |
. . 3
bits ..^
|
135 | | simpr 477 |
. . 3
bits ..^
bits
..^ |
136 | | eqid 2622 |
. . 3
inf
inf
|
137 | 133, 134,
135, 136 | bitsfzolem 15156 |
. 2
bits ..^
..^ |
138 | 55, 137 | impbida 877 |
1
..^
bits
..^ |