| Step | Hyp | Ref | Expression | 
						
							| 1 |  | negscl | ⊢ ( 𝐴  ∈   No   →  (  -us  ‘ 𝐴 )  ∈   No  ) | 
						
							| 2 | 1 | ad2antrr | ⊢ ( ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  ∧  ( abss ‘ 𝐴 )  <s  𝐵 )  →  (  -us  ‘ 𝐴 )  ∈   No  ) | 
						
							| 3 |  | absscl | ⊢ ( (  -us  ‘ 𝐴 )  ∈   No   →  ( abss ‘ (  -us  ‘ 𝐴 ) )  ∈   No  ) | 
						
							| 4 | 1 3 | syl | ⊢ ( 𝐴  ∈   No   →  ( abss ‘ (  -us  ‘ 𝐴 ) )  ∈   No  ) | 
						
							| 5 | 4 | ad2antrr | ⊢ ( ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  ∧  ( abss ‘ 𝐴 )  <s  𝐵 )  →  ( abss ‘ (  -us  ‘ 𝐴 ) )  ∈   No  ) | 
						
							| 6 |  | simplr | ⊢ ( ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  ∧  ( abss ‘ 𝐴 )  <s  𝐵 )  →  𝐵  ∈   No  ) | 
						
							| 7 |  | sleabs | ⊢ ( (  -us  ‘ 𝐴 )  ∈   No   →  (  -us  ‘ 𝐴 )  ≤s  ( abss ‘ (  -us  ‘ 𝐴 ) ) ) | 
						
							| 8 | 1 7 | syl | ⊢ ( 𝐴  ∈   No   →  (  -us  ‘ 𝐴 )  ≤s  ( abss ‘ (  -us  ‘ 𝐴 ) ) ) | 
						
							| 9 | 8 | ad2antrr | ⊢ ( ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  ∧  ( abss ‘ 𝐴 )  <s  𝐵 )  →  (  -us  ‘ 𝐴 )  ≤s  ( abss ‘ (  -us  ‘ 𝐴 ) ) ) | 
						
							| 10 |  | abssneg | ⊢ ( 𝐴  ∈   No   →  ( abss ‘ (  -us  ‘ 𝐴 ) )  =  ( abss ‘ 𝐴 ) ) | 
						
							| 11 | 10 | adantr | ⊢ ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  →  ( abss ‘ (  -us  ‘ 𝐴 ) )  =  ( abss ‘ 𝐴 ) ) | 
						
							| 12 | 11 | breq1d | ⊢ ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  →  ( ( abss ‘ (  -us  ‘ 𝐴 ) )  <s  𝐵  ↔  ( abss ‘ 𝐴 )  <s  𝐵 ) ) | 
						
							| 13 | 12 | biimpar | ⊢ ( ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  ∧  ( abss ‘ 𝐴 )  <s  𝐵 )  →  ( abss ‘ (  -us  ‘ 𝐴 ) )  <s  𝐵 ) | 
						
							| 14 | 2 5 6 9 13 | slelttrd | ⊢ ( ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  ∧  ( abss ‘ 𝐴 )  <s  𝐵 )  →  (  -us  ‘ 𝐴 )  <s  𝐵 ) | 
						
							| 15 |  | simpll | ⊢ ( ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  ∧  ( abss ‘ 𝐴 )  <s  𝐵 )  →  𝐴  ∈   No  ) | 
						
							| 16 |  | absscl | ⊢ ( 𝐴  ∈   No   →  ( abss ‘ 𝐴 )  ∈   No  ) | 
						
							| 17 | 16 | ad2antrr | ⊢ ( ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  ∧  ( abss ‘ 𝐴 )  <s  𝐵 )  →  ( abss ‘ 𝐴 )  ∈   No  ) | 
						
							| 18 |  | sleabs | ⊢ ( 𝐴  ∈   No   →  𝐴  ≤s  ( abss ‘ 𝐴 ) ) | 
						
							| 19 | 18 | ad2antrr | ⊢ ( ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  ∧  ( abss ‘ 𝐴 )  <s  𝐵 )  →  𝐴  ≤s  ( abss ‘ 𝐴 ) ) | 
						
							| 20 |  | simpr | ⊢ ( ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  ∧  ( abss ‘ 𝐴 )  <s  𝐵 )  →  ( abss ‘ 𝐴 )  <s  𝐵 ) | 
						
							| 21 | 15 17 6 19 20 | slelttrd | ⊢ ( ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  ∧  ( abss ‘ 𝐴 )  <s  𝐵 )  →  𝐴  <s  𝐵 ) | 
						
							| 22 | 14 21 | jca | ⊢ ( ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  ∧  ( abss ‘ 𝐴 )  <s  𝐵 )  →  ( (  -us  ‘ 𝐴 )  <s  𝐵  ∧  𝐴  <s  𝐵 ) ) | 
						
							| 23 | 22 | ex | ⊢ ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  →  ( ( abss ‘ 𝐴 )  <s  𝐵  →  ( (  -us  ‘ 𝐴 )  <s  𝐵  ∧  𝐴  <s  𝐵 ) ) ) | 
						
							| 24 |  | abssor | ⊢ ( 𝐴  ∈   No   →  ( ( abss ‘ 𝐴 )  =  𝐴  ∨  ( abss ‘ 𝐴 )  =  (  -us  ‘ 𝐴 ) ) ) | 
						
							| 25 | 24 | adantr | ⊢ ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  →  ( ( abss ‘ 𝐴 )  =  𝐴  ∨  ( abss ‘ 𝐴 )  =  (  -us  ‘ 𝐴 ) ) ) | 
						
							| 26 |  | breq1 | ⊢ ( ( abss ‘ 𝐴 )  =  𝐴  →  ( ( abss ‘ 𝐴 )  <s  𝐵  ↔  𝐴  <s  𝐵 ) ) | 
						
							| 27 | 26 | biimprd | ⊢ ( ( abss ‘ 𝐴 )  =  𝐴  →  ( 𝐴  <s  𝐵  →  ( abss ‘ 𝐴 )  <s  𝐵 ) ) | 
						
							| 28 |  | breq1 | ⊢ ( ( abss ‘ 𝐴 )  =  (  -us  ‘ 𝐴 )  →  ( ( abss ‘ 𝐴 )  <s  𝐵  ↔  (  -us  ‘ 𝐴 )  <s  𝐵 ) ) | 
						
							| 29 | 28 | biimprd | ⊢ ( ( abss ‘ 𝐴 )  =  (  -us  ‘ 𝐴 )  →  ( (  -us  ‘ 𝐴 )  <s  𝐵  →  ( abss ‘ 𝐴 )  <s  𝐵 ) ) | 
						
							| 30 | 27 29 | jaoa | ⊢ ( ( ( abss ‘ 𝐴 )  =  𝐴  ∨  ( abss ‘ 𝐴 )  =  (  -us  ‘ 𝐴 ) )  →  ( ( 𝐴  <s  𝐵  ∧  (  -us  ‘ 𝐴 )  <s  𝐵 )  →  ( abss ‘ 𝐴 )  <s  𝐵 ) ) | 
						
							| 31 | 30 | ancomsd | ⊢ ( ( ( abss ‘ 𝐴 )  =  𝐴  ∨  ( abss ‘ 𝐴 )  =  (  -us  ‘ 𝐴 ) )  →  ( ( (  -us  ‘ 𝐴 )  <s  𝐵  ∧  𝐴  <s  𝐵 )  →  ( abss ‘ 𝐴 )  <s  𝐵 ) ) | 
						
							| 32 | 25 31 | syl | ⊢ ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  →  ( ( (  -us  ‘ 𝐴 )  <s  𝐵  ∧  𝐴  <s  𝐵 )  →  ( abss ‘ 𝐴 )  <s  𝐵 ) ) | 
						
							| 33 | 23 32 | impbid | ⊢ ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  →  ( ( abss ‘ 𝐴 )  <s  𝐵  ↔  ( (  -us  ‘ 𝐴 )  <s  𝐵  ∧  𝐴  <s  𝐵 ) ) ) | 
						
							| 34 | 1 | adantr | ⊢ ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  →  (  -us  ‘ 𝐴 )  ∈   No  ) | 
						
							| 35 |  | simpr | ⊢ ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  →  𝐵  ∈   No  ) | 
						
							| 36 | 34 35 | sltnegd | ⊢ ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  →  ( (  -us  ‘ 𝐴 )  <s  𝐵  ↔  (  -us  ‘ 𝐵 )  <s  (  -us  ‘ (  -us  ‘ 𝐴 ) ) ) ) | 
						
							| 37 |  | negnegs | ⊢ ( 𝐴  ∈   No   →  (  -us  ‘ (  -us  ‘ 𝐴 ) )  =  𝐴 ) | 
						
							| 38 | 37 | adantr | ⊢ ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  →  (  -us  ‘ (  -us  ‘ 𝐴 ) )  =  𝐴 ) | 
						
							| 39 | 38 | breq2d | ⊢ ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  →  ( (  -us  ‘ 𝐵 )  <s  (  -us  ‘ (  -us  ‘ 𝐴 ) )  ↔  (  -us  ‘ 𝐵 )  <s  𝐴 ) ) | 
						
							| 40 | 36 39 | bitrd | ⊢ ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  →  ( (  -us  ‘ 𝐴 )  <s  𝐵  ↔  (  -us  ‘ 𝐵 )  <s  𝐴 ) ) | 
						
							| 41 | 40 | anbi1d | ⊢ ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  →  ( ( (  -us  ‘ 𝐴 )  <s  𝐵  ∧  𝐴  <s  𝐵 )  ↔  ( (  -us  ‘ 𝐵 )  <s  𝐴  ∧  𝐴  <s  𝐵 ) ) ) | 
						
							| 42 | 33 41 | bitrd | ⊢ ( ( 𝐴  ∈   No   ∧  𝐵  ∈   No  )  →  ( ( abss ‘ 𝐴 )  <s  𝐵  ↔  ( (  -us  ‘ 𝐵 )  <s  𝐴  ∧  𝐴  <s  𝐵 ) ) ) |