| Step | Hyp | Ref | Expression | 
						
							| 1 |  | madjusmdet.b |  | 
						
							| 2 |  | madjusmdet.a |  | 
						
							| 3 |  | madjusmdet.d |  | 
						
							| 4 |  | madjusmdet.k |  | 
						
							| 5 |  | madjusmdet.t |  | 
						
							| 6 |  | madjusmdet.z |  | 
						
							| 7 |  | madjusmdet.e |  | 
						
							| 8 |  | madjusmdet.n |  | 
						
							| 9 |  | madjusmdet.r |  | 
						
							| 10 |  | madjusmdet.i |  | 
						
							| 11 |  | madjusmdet.j |  | 
						
							| 12 |  | madjusmdet.m |  | 
						
							| 13 |  | madjusmdetlem2.p |  | 
						
							| 14 |  | madjusmdetlem2.s |  | 
						
							| 15 |  | nnuz |  | 
						
							| 16 | 8 15 | eleqtrdi |  | 
						
							| 17 |  | eluzfz2 |  | 
						
							| 18 | 16 17 | syl |  | 
						
							| 19 |  | eqid |  | 
						
							| 20 |  | eqid |  | 
						
							| 21 |  | eqid |  | 
						
							| 22 | 19 14 20 21 | fzto1st |  | 
						
							| 23 | 18 22 | syl |  | 
						
							| 24 | 20 21 | symgbasf1o |  | 
						
							| 25 | 23 24 | syl |  | 
						
							| 26 | 25 | adantr |  | 
						
							| 27 |  | fznatpl1 |  | 
						
							| 28 | 8 27 | sylan |  | 
						
							| 29 |  | eqeq1 |  | 
						
							| 30 |  | breq1 |  | 
						
							| 31 |  | oveq1 |  | 
						
							| 32 |  | id |  | 
						
							| 33 | 30 31 32 | ifbieq12d |  | 
						
							| 34 | 29 33 | ifbieq2d |  | 
						
							| 35 | 34 | cbvmptv |  | 
						
							| 36 | 14 35 | eqtri |  | 
						
							| 37 |  | simpr |  | 
						
							| 38 |  | 1red |  | 
						
							| 39 |  | fz1ssnn |  | 
						
							| 40 |  | simpr |  | 
						
							| 41 | 39 40 | sselid |  | 
						
							| 42 | 41 | nnrpd |  | 
						
							| 43 | 42 | adantr |  | 
						
							| 44 | 38 43 | ltaddrp2d |  | 
						
							| 45 | 38 44 | gtned |  | 
						
							| 46 | 37 45 | eqnetrd |  | 
						
							| 47 | 46 | neneqd |  | 
						
							| 48 | 47 | iffalsed |  | 
						
							| 49 | 8 | adantr |  | 
						
							| 50 | 41 | nnnn0d |  | 
						
							| 51 | 49 | nnnn0d |  | 
						
							| 52 |  | elfzle2 |  | 
						
							| 53 | 40 52 | syl |  | 
						
							| 54 |  | nn0ltlem1 |  | 
						
							| 55 | 54 | biimpar |  | 
						
							| 56 | 50 51 53 55 | syl21anc |  | 
						
							| 57 |  | nnltp1le |  | 
						
							| 58 | 57 | biimpa |  | 
						
							| 59 | 41 49 56 58 | syl21anc |  | 
						
							| 60 | 59 | adantr |  | 
						
							| 61 | 37 60 | eqbrtrd |  | 
						
							| 62 | 61 | iftrued |  | 
						
							| 63 | 37 | oveq1d |  | 
						
							| 64 | 41 | nncnd |  | 
						
							| 65 |  | 1cnd |  | 
						
							| 66 | 64 65 | pncand |  | 
						
							| 67 | 66 | adantr |  | 
						
							| 68 | 63 67 | eqtrd |  | 
						
							| 69 | 48 62 68 | 3eqtrd |  | 
						
							| 70 | 36 69 28 40 | fvmptd2 |  | 
						
							| 71 |  | f1ocnvfv |  | 
						
							| 72 | 71 | imp |  | 
						
							| 73 | 26 28 70 72 | syl21anc |  | 
						
							| 74 | 73 | fveq2d |  | 
						
							| 75 | 74 | adantr |  | 
						
							| 76 |  | breq1 |  | 
						
							| 77 | 76 31 32 | ifbieq12d |  | 
						
							| 78 | 29 77 | ifbieq2d |  | 
						
							| 79 | 78 | cbvmptv |  | 
						
							| 80 | 13 79 | eqtri |  | 
						
							| 81 | 44 37 | breqtrrd |  | 
						
							| 82 | 38 81 | gtned |  | 
						
							| 83 | 82 | neneqd |  | 
						
							| 84 | 83 | iffalsed |  | 
						
							| 85 | 84 | adantlr |  | 
						
							| 86 |  | simpr |  | 
						
							| 87 | 41 | ad2antrr |  | 
						
							| 88 |  | fz1ssnn |  | 
						
							| 89 | 88 10 | sselid |  | 
						
							| 90 | 89 | ad3antrrr |  | 
						
							| 91 |  | simplr |  | 
						
							| 92 |  | nnltp1le |  | 
						
							| 93 | 92 | biimpa |  | 
						
							| 94 | 87 90 91 93 | syl21anc |  | 
						
							| 95 | 86 94 | eqbrtrd |  | 
						
							| 96 | 95 | iftrued |  | 
						
							| 97 | 68 | adantlr |  | 
						
							| 98 | 85 96 97 | 3eqtrd |  | 
						
							| 99 | 28 | adantr |  | 
						
							| 100 |  | simplr |  | 
						
							| 101 | 80 98 99 100 | fvmptd2 |  | 
						
							| 102 | 75 101 | eqtr2d |  | 
						
							| 103 | 74 | adantr |  | 
						
							| 104 | 84 | adantlr |  | 
						
							| 105 | 41 | ad2antrr |  | 
						
							| 106 | 89 | ad3antrrr |  | 
						
							| 107 |  | simplr |  | 
						
							| 108 |  | simpr |  | 
						
							| 109 | 107 108 | eqbrtrrd |  | 
						
							| 110 | 92 | biimpar |  | 
						
							| 111 | 105 106 109 110 | syl21anc |  | 
						
							| 112 | 111 | stoic1a |  | 
						
							| 113 | 112 | an32s |  | 
						
							| 114 | 113 | iffalsed |  | 
						
							| 115 |  | simpr |  | 
						
							| 116 | 104 114 115 | 3eqtrd |  | 
						
							| 117 | 28 | adantr |  | 
						
							| 118 | 80 116 117 117 | fvmptd2 |  | 
						
							| 119 | 103 118 | eqtr2d |  | 
						
							| 120 | 102 119 | ifeqda |  | 
						
							| 121 |  | f1ocnv |  | 
						
							| 122 | 23 24 121 | 3syl |  | 
						
							| 123 |  | f1ofun |  | 
						
							| 124 | 122 123 | syl |  | 
						
							| 125 |  | fzdif2 |  | 
						
							| 126 | 16 125 | syl |  | 
						
							| 127 |  | difss |  | 
						
							| 128 | 126 127 | eqsstrrdi |  | 
						
							| 129 |  | f1odm |  | 
						
							| 130 | 122 129 | syl |  | 
						
							| 131 | 128 130 | sseqtrrd |  | 
						
							| 132 | 131 | sselda |  | 
						
							| 133 |  | fvco |  | 
						
							| 134 | 124 132 133 | syl2an2r |  | 
						
							| 135 | 120 134 | eqtr4d |  |