Proof 01. 1 ⊢ x ∈ ℝ, hypo. 02. 2 ⊢ y ∈ ℝ, hypo. 03. ⊢ 0 ≤ x ∨ ¬0 ≤ x, lem. 04. 4 ⊢ 0 ≤ x, hypo. 05. 1, 4 ⊢ abs x = x, rabs_eql 1 4. 06. ⊢ 0 ≤ y ∨ ¬0 ≤ y, lem. 07. 7 ⊢ 0 ≤ y, hypo. 08. 2, 7 ⊢ abs y = y, rabs_eql 2 7. 09. 1, 2, 4, 7 ⊢ 0 ≤ x⋅y, rle_compat_mul 1 2 4 7. 10. 1, 2 ⊢ x⋅y ∈ ℝ, rmul_closed 1 2. 11. 1, 2, 4, 7 ⊢ abs (x⋅y) = x⋅y, rabs_eql 10 9. 12. 1, 2, 4, 7 ⊢ abs (x⋅y) = (abs x)⋅y, eq_subst_rev 5 11, P t ↔ abs (x⋅y) = t⋅y. 13. 1, 2, 4, 7 ⊢ abs (x⋅y) = (abs x)⋅(abs y), eq_subst_rev 8 12, P t ↔ abs (x⋅y) = (abs x)⋅t. 14. 14 ⊢ ¬0 ≤ y, hypo. 15. 2, 14 ⊢ abs y = -y, rabs_eqr 2 14. 16. ⊢ 0 ∈ ℝ, calc. 17. 2, 14 ⊢ y ≤ 0, rle_neg 16 2 14. 18. 1, 2, 4, 14 ⊢ x⋅y ≤ 0, rmul_nn_np 1 2 4 17. 19. 1, 2, 4, 14 ⊢ abs (x⋅y) = -(x⋅y), rabs_non_positive 10 18. 20. 1, 2 ⊢ -(x⋅y) = x⋅(-y), rmul_compatr_neg 1 2. 21. 1, 2, 4, 14 ⊢ abs (x⋅y) = x⋅(-y), eq_trans 19 20. 22. 1, 2, 4, 14 ⊢ abs (x⋅y) = (abs x)⋅(-y), eq_subst_rev 5 21, P t ↔ abs (x⋅y) = t⋅(-y). 23. 1, 2, 4, 14 ⊢ abs (x⋅y) = (abs x)⋅(abs y), eq_subst_rev 15 22, P t ↔ abs (x⋅y) = (abs x)⋅t. 24. 1, 2, 4 ⊢ abs (x⋅y) = (abs x)⋅(abs y), disj_elim 6 13 23. 25. 25 ⊢ ¬0 ≤ x, hypo. 26. 1, 25 ⊢ x ≤ 0, rle_neg 16 1 25. 27. 1, 25 ⊢ abs x = -x, rabs_non_positive 1 26. 28. ⊢ 0 ≤ y ∨ ¬0 ≤ y, lem. 29. 29 ⊢ 0 ≤ y, hypo. 30. 2, 29 ⊢ abs y = y, rabs_eql 2 29. 31. 1, 2, 25, 29 ⊢ x⋅y ≤ 0, rmul_np_nn 1 2 26 29. 32. 1, 2, 25, 29 ⊢ abs (x⋅y) = -(x⋅y), rabs_non_positive 10 31. 33. 1, 2 ⊢ -(x⋅y) = (-x)⋅y, rmul_compatl_neg 1 2. 34. 1, 2, 25, 29 ⊢ abs (x⋅y) = (-x)⋅y, eq_trans 32 33. 35. 1, 2, 25, 29 ⊢ abs (x⋅y) = (abs x)⋅y, eq_subst_rev 27 34, P t ↔ abs (x⋅y) = t⋅y. 36. 1, 2, 25, 29 ⊢ abs (x⋅y) = (abs x)⋅(abs y), eq_subst_rev 30 35, P t ↔ abs (x⋅y) = (abs x)⋅t. 37. 37 ⊢ ¬0 ≤ y, hypo. 38. 2, 37 ⊢ abs y = -y, rabs_eqr 2 37. 39. 2, 37 ⊢ y ≤ 0, rle_neg 16 2 37. 40. 1, 2, 25, 37 ⊢ 0 ≤ x⋅y, rmul_np_np 1 2 26 39. 41. 1, 2, 25, 37 ⊢ abs (x⋅y) = x⋅y, rabs_eql 10 40. 42. 1, 2 ⊢ (-x)⋅(-y) = x⋅y, rmul_cancel_neg 1 2. 43. 1, 2 ⊢ x⋅y = (-x)⋅(-y), eq_symm 42. 44. 1, 2, 25, 37 ⊢ abs (x⋅y) = (-x)⋅(-y), eq_trans 41 43. 45. 1, 2, 25, 37 ⊢ abs (x⋅y) = (abs x)⋅(-y), eq_subst_rev 27 44, P t ↔ abs (x⋅y) = t⋅(-y). 46. 1, 2, 25, 37 ⊢ abs (x⋅y) = (abs x)⋅(abs y), eq_subst_rev 38 45, P t ↔ abs (x⋅y) = (abs x)⋅t. 47. 1, 2, 25 ⊢ abs (x⋅y) = (abs x)⋅(abs y), disj_elim 28 36 46. 48. 1, 2 ⊢ abs (x⋅y) = (abs x)⋅(abs y), disj_elim 3 24 47. rabs_dist_mul. ⊢ x ∈ ℝ → y ∈ ℝ → abs (x⋅y) = (abs x)⋅(abs y), subj_intro_ii 48.
Dependencies
The given proof depends on 20 axioms:
comp, efq, eq_refl, eq_subst, ext, lem, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rle_antisym, rle_compat_add, rle_compat_mul, rle_refl, rle_total, rmul_closed, rmul_comm, rmul_distl_add, rneg_closed.