Description: Decimal multiplication galore! (Contributed by Thierry Arnoux, 26-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | hgt750lem2 | ⊢ ( 3 · ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) < ( 7 . _ 3 _ 4 8 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1nn0 | ⊢ 1 ∈ ℕ0 | |
| 2 | 0re | ⊢ 0 ∈ ℝ | |
| 3 | 7re | ⊢ 7 ∈ ℝ | |
| 4 | 9re | ⊢ 9 ∈ ℝ | |
| 5 | 5re | ⊢ 5 ∈ ℝ | |
| 6 | 5 5 | pm3.2i | ⊢ ( 5 ∈ ℝ ∧ 5 ∈ ℝ ) |
| 7 | dp2cl | ⊢ ( ( 5 ∈ ℝ ∧ 5 ∈ ℝ ) → _ 5 5 ∈ ℝ ) | |
| 8 | 6 7 | ax-mp | ⊢ _ 5 5 ∈ ℝ |
| 9 | 4 8 | pm3.2i | ⊢ ( 9 ∈ ℝ ∧ _ 5 5 ∈ ℝ ) |
| 10 | dp2cl | ⊢ ( ( 9 ∈ ℝ ∧ _ 5 5 ∈ ℝ ) → _ 9 _ 5 5 ∈ ℝ ) | |
| 11 | 9 10 | ax-mp | ⊢ _ 9 _ 5 5 ∈ ℝ |
| 12 | 4 11 | pm3.2i | ⊢ ( 9 ∈ ℝ ∧ _ 9 _ 5 5 ∈ ℝ ) |
| 13 | dp2cl | ⊢ ( ( 9 ∈ ℝ ∧ _ 9 _ 5 5 ∈ ℝ ) → _ 9 _ 9 _ 5 5 ∈ ℝ ) | |
| 14 | 12 13 | ax-mp | ⊢ _ 9 _ 9 _ 5 5 ∈ ℝ |
| 15 | 3 14 | pm3.2i | ⊢ ( 7 ∈ ℝ ∧ _ 9 _ 9 _ 5 5 ∈ ℝ ) |
| 16 | dp2cl | ⊢ ( ( 7 ∈ ℝ ∧ _ 9 _ 9 _ 5 5 ∈ ℝ ) → _ 7 _ 9 _ 9 _ 5 5 ∈ ℝ ) | |
| 17 | 15 16 | ax-mp | ⊢ _ 7 _ 9 _ 9 _ 5 5 ∈ ℝ |
| 18 | 2 17 | pm3.2i | ⊢ ( 0 ∈ ℝ ∧ _ 7 _ 9 _ 9 _ 5 5 ∈ ℝ ) |
| 19 | dp2cl | ⊢ ( ( 0 ∈ ℝ ∧ _ 7 _ 9 _ 9 _ 5 5 ∈ ℝ ) → _ 0 _ 7 _ 9 _ 9 _ 5 5 ∈ ℝ ) | |
| 20 | 18 19 | ax-mp | ⊢ _ 0 _ 7 _ 9 _ 9 _ 5 5 ∈ ℝ |
| 21 | dpcl | ⊢ ( ( 1 ∈ ℕ0 ∧ _ 0 _ 7 _ 9 _ 9 _ 5 5 ∈ ℝ ) → ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ∈ ℝ ) | |
| 22 | 1 20 21 | mp2an | ⊢ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ∈ ℝ |
| 23 | 22 | resqcli | ⊢ ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) ∈ ℝ |
| 24 | 4nn0 | ⊢ 4 ∈ ℕ0 | |
| 25 | 4nn | ⊢ 4 ∈ ℕ | |
| 26 | nnrp | ⊢ ( 4 ∈ ℕ → 4 ∈ ℝ+ ) | |
| 27 | 25 26 | ax-mp | ⊢ 4 ∈ ℝ+ |
| 28 | 1 27 | rpdp2cl | ⊢ _ 1 4 ∈ ℝ+ |
| 29 | 24 28 | rpdp2cl | ⊢ _ 4 _ 1 4 ∈ ℝ+ |
| 30 | 1 29 | rpdpcl | ⊢ ( 1 . _ 4 _ 1 4 ) ∈ ℝ+ |
| 31 | rpre | ⊢ ( ( 1 . _ 4 _ 1 4 ) ∈ ℝ+ → ( 1 . _ 4 _ 1 4 ) ∈ ℝ ) | |
| 32 | 30 31 | ax-mp | ⊢ ( 1 . _ 4 _ 1 4 ) ∈ ℝ |
| 33 | 23 32 | remulcli | ⊢ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) ∈ ℝ |
| 34 | 6re | ⊢ 6 ∈ ℝ | |
| 35 | 1re | ⊢ 1 ∈ ℝ | |
| 36 | 5 35 | pm3.2i | ⊢ ( 5 ∈ ℝ ∧ 1 ∈ ℝ ) |
| 37 | dp2cl | ⊢ ( ( 5 ∈ ℝ ∧ 1 ∈ ℝ ) → _ 5 1 ∈ ℝ ) | |
| 38 | 36 37 | ax-mp | ⊢ _ 5 1 ∈ ℝ |
| 39 | 34 38 | pm3.2i | ⊢ ( 6 ∈ ℝ ∧ _ 5 1 ∈ ℝ ) |
| 40 | dp2cl | ⊢ ( ( 6 ∈ ℝ ∧ _ 5 1 ∈ ℝ ) → _ 6 _ 5 1 ∈ ℝ ) | |
| 41 | 39 40 | ax-mp | ⊢ _ 6 _ 5 1 ∈ ℝ |
| 42 | dpcl | ⊢ ( ( 1 ∈ ℕ0 ∧ _ 6 _ 5 1 ∈ ℝ ) → ( 1 . _ 6 _ 5 1 ) ∈ ℝ ) | |
| 43 | 1 41 42 | mp2an | ⊢ ( 1 . _ 6 _ 5 1 ) ∈ ℝ |
| 44 | 33 43 | pm3.2i | ⊢ ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) ∈ ℝ ∧ ( 1 . _ 6 _ 5 1 ) ∈ ℝ ) |
| 45 | 22 | sqge0i | ⊢ 0 ≤ ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) |
| 46 | rpgt0 | ⊢ ( ( 1 . _ 4 _ 1 4 ) ∈ ℝ+ → 0 < ( 1 . _ 4 _ 1 4 ) ) | |
| 47 | 30 46 | ax-mp | ⊢ 0 < ( 1 . _ 4 _ 1 4 ) |
| 48 | 2 32 47 | ltleii | ⊢ 0 ≤ ( 1 . _ 4 _ 1 4 ) |
| 49 | 23 32 | mulge0i | ⊢ ( ( 0 ≤ ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) ∧ 0 ≤ ( 1 . _ 4 _ 1 4 ) ) → 0 ≤ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) ) |
| 50 | 45 48 49 | mp2an | ⊢ 0 ≤ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) |
| 51 | 0nn0 | ⊢ 0 ∈ ℕ0 | |
| 52 | 7nn0 | ⊢ 7 ∈ ℕ0 | |
| 53 | 9nn0 | ⊢ 9 ∈ ℕ0 | |
| 54 | 5nn0 | ⊢ 5 ∈ ℕ0 | |
| 55 | 5nn | ⊢ 5 ∈ ℕ | |
| 56 | nnrp | ⊢ ( 5 ∈ ℕ → 5 ∈ ℝ+ ) | |
| 57 | 55 56 | ax-mp | ⊢ 5 ∈ ℝ+ |
| 58 | 54 57 | rpdp2cl | ⊢ _ 5 5 ∈ ℝ+ |
| 59 | 53 58 | rpdp2cl | ⊢ _ 9 _ 5 5 ∈ ℝ+ |
| 60 | 53 59 | rpdp2cl | ⊢ _ 9 _ 9 _ 5 5 ∈ ℝ+ |
| 61 | 52 60 | rpdp2cl | ⊢ _ 7 _ 9 _ 9 _ 5 5 ∈ ℝ+ |
| 62 | 51 61 | rpdp2cl | ⊢ _ 0 _ 7 _ 9 _ 9 _ 5 5 ∈ ℝ+ |
| 63 | 8nn | ⊢ 8 ∈ ℕ | |
| 64 | 63 | rpdp2cl2 | ⊢ _ 8 0 ∈ ℝ+ |
| 65 | 51 64 | rpdp2cl | ⊢ _ 0 _ 8 0 ∈ ℝ+ |
| 66 | 9lt10 | ⊢ 9 < ; 1 0 | |
| 67 | 5lt10 | ⊢ 5 < ; 1 0 | |
| 68 | 54 57 67 67 | dp2lt10 | ⊢ _ 5 5 < ; 1 0 |
| 69 | 53 58 66 68 | dp2lt10 | ⊢ _ 9 _ 5 5 < ; 1 0 |
| 70 | 53 59 66 69 | dp2lt10 | ⊢ _ 9 _ 9 _ 5 5 < ; 1 0 |
| 71 | 7p1e8 | ⊢ ( 7 + 1 ) = 8 | |
| 72 | 52 60 70 71 | dp2ltsuc | ⊢ _ 7 _ 9 _ 9 _ 5 5 < 8 |
| 73 | 8nn0 | ⊢ 8 ∈ ℕ0 | |
| 74 | 73 | dp20u | ⊢ _ 8 0 = 8 |
| 75 | 72 74 | breqtrri | ⊢ _ 7 _ 9 _ 9 _ 5 5 < _ 8 0 |
| 76 | 51 61 64 75 | dp2lt | ⊢ _ 0 _ 7 _ 9 _ 9 _ 5 5 < _ 0 _ 8 0 |
| 77 | 1 62 65 76 | dplt | ⊢ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) < ( 1 . _ 0 _ 8 0 ) |
| 78 | 1 62 | rpdpcl | ⊢ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ∈ ℝ+ |
| 79 | rpge0 | ⊢ ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ∈ ℝ+ → 0 ≤ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ) | |
| 80 | 78 79 | ax-mp | ⊢ 0 ≤ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) |
| 81 | 1 65 | rpdpcl | ⊢ ( 1 . _ 0 _ 8 0 ) ∈ ℝ+ |
| 82 | rpge0 | ⊢ ( ( 1 . _ 0 _ 8 0 ) ∈ ℝ+ → 0 ≤ ( 1 . _ 0 _ 8 0 ) ) | |
| 83 | 81 82 | ax-mp | ⊢ 0 ≤ ( 1 . _ 0 _ 8 0 ) |
| 84 | 8re | ⊢ 8 ∈ ℝ | |
| 85 | 84 2 | pm3.2i | ⊢ ( 8 ∈ ℝ ∧ 0 ∈ ℝ ) |
| 86 | dp2cl | ⊢ ( ( 8 ∈ ℝ ∧ 0 ∈ ℝ ) → _ 8 0 ∈ ℝ ) | |
| 87 | 85 86 | ax-mp | ⊢ _ 8 0 ∈ ℝ |
| 88 | 2 87 | pm3.2i | ⊢ ( 0 ∈ ℝ ∧ _ 8 0 ∈ ℝ ) |
| 89 | dp2cl | ⊢ ( ( 0 ∈ ℝ ∧ _ 8 0 ∈ ℝ ) → _ 0 _ 8 0 ∈ ℝ ) | |
| 90 | 88 89 | ax-mp | ⊢ _ 0 _ 8 0 ∈ ℝ |
| 91 | dpcl | ⊢ ( ( 1 ∈ ℕ0 ∧ _ 0 _ 8 0 ∈ ℝ ) → ( 1 . _ 0 _ 8 0 ) ∈ ℝ ) | |
| 92 | 1 90 91 | mp2an | ⊢ ( 1 . _ 0 _ 8 0 ) ∈ ℝ |
| 93 | 22 92 | lt2sqi | ⊢ ( ( 0 ≤ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ∧ 0 ≤ ( 1 . _ 0 _ 8 0 ) ) → ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) < ( 1 . _ 0 _ 8 0 ) ↔ ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) < ( ( 1 . _ 0 _ 8 0 ) ↑ 2 ) ) ) |
| 94 | 80 83 93 | mp2an | ⊢ ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) < ( 1 . _ 0 _ 8 0 ) ↔ ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) < ( ( 1 . _ 0 _ 8 0 ) ↑ 2 ) ) |
| 95 | 77 94 | mpbi | ⊢ ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) < ( ( 1 . _ 0 _ 8 0 ) ↑ 2 ) |
| 96 | 92 | recni | ⊢ ( 1 . _ 0 _ 8 0 ) ∈ ℂ |
| 97 | 96 | sqvali | ⊢ ( ( 1 . _ 0 _ 8 0 ) ↑ 2 ) = ( ( 1 . _ 0 _ 8 0 ) · ( 1 . _ 0 _ 8 0 ) ) |
| 98 | 6nn0 | ⊢ 6 ∈ ℕ0 | |
| 99 | 1 98 | deccl | ⊢ ; 1 6 ∈ ℕ0 |
| 100 | 98 24 | deccl | ⊢ ; 6 4 ∈ ℕ0 |
| 101 | 4lt10 | ⊢ 4 < ; 1 0 | |
| 102 | 10pos | ⊢ 0 < ; 1 0 | |
| 103 | 99 51 | deccl | ⊢ ; ; 1 6 0 ∈ ℕ0 |
| 104 | eqid | ⊢ ; ; ; 1 6 0 0 = ; ; ; 1 6 0 0 | |
| 105 | eqid | ⊢ ; 6 4 = ; 6 4 | |
| 106 | eqid | ⊢ ; ; 1 6 0 = ; ; 1 6 0 | |
| 107 | 98 | dec0h | ⊢ 6 = ; 0 6 |
| 108 | 99 | nn0cni | ⊢ ; 1 6 ∈ ℂ |
| 109 | 108 | addridi | ⊢ ( ; 1 6 + 0 ) = ; 1 6 |
| 110 | 6cn | ⊢ 6 ∈ ℂ | |
| 111 | 110 | addlidi | ⊢ ( 0 + 6 ) = 6 |
| 112 | 99 51 51 98 106 107 109 111 | decadd | ⊢ ( ; ; 1 6 0 + 6 ) = ; ; 1 6 6 |
| 113 | 4cn | ⊢ 4 ∈ ℂ | |
| 114 | 113 | addlidi | ⊢ ( 0 + 4 ) = 4 |
| 115 | 103 51 98 24 104 105 112 114 | decadd | ⊢ ( ; ; ; 1 6 0 0 + ; 6 4 ) = ; ; ; 1 6 6 4 |
| 116 | 1t1e1 | ⊢ ( 1 · 1 ) = 1 | |
| 117 | 1 | dp0u | ⊢ ( 1 . 0 ) = 1 |
| 118 | 117 117 | oveq12i | ⊢ ( ( 1 . 0 ) · ( 1 . 0 ) ) = ( 1 · 1 ) |
| 119 | 51 | dp20u | ⊢ _ 0 0 = 0 |
| 120 | 119 | oveq2i | ⊢ ( 1 . _ 0 0 ) = ( 1 . 0 ) |
| 121 | 120 117 | eqtri | ⊢ ( 1 . _ 0 0 ) = 1 |
| 122 | 116 118 121 | 3eqtr4i | ⊢ ( ( 1 . 0 ) · ( 1 . 0 ) ) = ( 1 . _ 0 0 ) |
| 123 | 8t8e64 | ⊢ ( 8 · 8 ) = ; 6 4 | |
| 124 | 73 | dp0u | ⊢ ( 8 . 0 ) = 8 |
| 125 | 124 124 | oveq12i | ⊢ ( ( 8 . 0 ) · ( 8 . 0 ) ) = ( 8 · 8 ) |
| 126 | 119 | oveq2i | ⊢ ( ; 6 4 . _ 0 0 ) = ( ; 6 4 . 0 ) |
| 127 | 100 | dp0u | ⊢ ( ; 6 4 . 0 ) = ; 6 4 |
| 128 | 126 127 | eqtri | ⊢ ( ; 6 4 . _ 0 0 ) = ; 6 4 |
| 129 | 123 125 128 | 3eqtr4i | ⊢ ( ( 8 . 0 ) · ( 8 . 0 ) ) = ( ; 6 4 . _ 0 0 ) |
| 130 | 10nn0 | ⊢ ; 1 0 ∈ ℕ0 | |
| 131 | 130 51 | deccl | ⊢ ; ; 1 0 0 ∈ ℕ0 |
| 132 | eqid | ⊢ ; ; ; 1 0 0 1 = ; ; ; 1 0 0 1 | |
| 133 | eqid | ⊢ ; ; 1 6 6 = ; ; 1 6 6 | |
| 134 | eqid | ⊢ ; ; 1 0 0 = ; ; 1 0 0 | |
| 135 | eqid | ⊢ ; 1 6 = ; 1 6 | |
| 136 | dec10p | ⊢ ( ; 1 0 + 1 ) = ; 1 1 | |
| 137 | 130 51 1 98 134 135 136 111 | decadd | ⊢ ( ; ; 1 0 0 + ; 1 6 ) = ; ; 1 1 6 |
| 138 | ax-1cn | ⊢ 1 ∈ ℂ | |
| 139 | 138 110 | addcomi | ⊢ ( 1 + 6 ) = ( 6 + 1 ) |
| 140 | 6p1e7 | ⊢ ( 6 + 1 ) = 7 | |
| 141 | 139 140 | eqtri | ⊢ ( 1 + 6 ) = 7 |
| 142 | 131 1 99 98 132 133 137 141 | decadd | ⊢ ( ; ; ; 1 0 0 1 + ; ; 1 6 6 ) = ; ; ; 1 1 6 7 |
| 143 | eqid | ⊢ ; 1 7 = ; 1 7 | |
| 144 | 141 | oveq1i | ⊢ ( ( 1 + 6 ) + 1 ) = ( 7 + 1 ) |
| 145 | 144 71 | eqtri | ⊢ ( ( 1 + 6 ) + 1 ) = 8 |
| 146 | 7p4e11 | ⊢ ( 7 + 4 ) = ; 1 1 | |
| 147 | 1 52 98 24 143 105 145 1 146 | decaddc | ⊢ ( ; 1 7 + ; 6 4 ) = ; 8 1 |
| 148 | 119 | oveq2i | ⊢ ( ; 1 6 . _ 0 0 ) = ( ; 1 6 . 0 ) |
| 149 | 99 | dp0u | ⊢ ( ; 1 6 . 0 ) = ; 1 6 |
| 150 | 148 149 | eqtri | ⊢ ( ; 1 6 . _ 0 0 ) = ; 1 6 |
| 151 | 121 150 | oveq12i | ⊢ ( ( 1 . _ 0 0 ) + ( ; 1 6 . _ 0 0 ) ) = ( 1 + ; 1 6 ) |
| 152 | 1 | dec0h | ⊢ 1 = ; 0 1 |
| 153 | 138 | addlidi | ⊢ ( 0 + 1 ) = 1 |
| 154 | 51 1 1 98 152 135 153 141 | decadd | ⊢ ( 1 + ; 1 6 ) = ; 1 7 |
| 155 | 151 154 | eqtri | ⊢ ( ( 1 . _ 0 0 ) + ( ; 1 6 . _ 0 0 ) ) = ; 1 7 |
| 156 | 155 128 | oveq12i | ⊢ ( ( ( 1 . _ 0 0 ) + ( ; 1 6 . _ 0 0 ) ) + ( ; 6 4 . _ 0 0 ) ) = ( ; 1 7 + ; 6 4 ) |
| 157 | 117 124 | oveq12i | ⊢ ( ( 1 . 0 ) + ( 8 . 0 ) ) = ( 1 + 8 ) |
| 158 | 8cn | ⊢ 8 ∈ ℂ | |
| 159 | 138 158 | addcomi | ⊢ ( 1 + 8 ) = ( 8 + 1 ) |
| 160 | 8p1e9 | ⊢ ( 8 + 1 ) = 9 | |
| 161 | 157 159 160 | 3eqtri | ⊢ ( ( 1 . 0 ) + ( 8 . 0 ) ) = 9 |
| 162 | 161 161 | oveq12i | ⊢ ( ( ( 1 . 0 ) + ( 8 . 0 ) ) · ( ( 1 . 0 ) + ( 8 . 0 ) ) ) = ( 9 · 9 ) |
| 163 | 9t9e81 | ⊢ ( 9 · 9 ) = ; 8 1 | |
| 164 | 162 163 | eqtri | ⊢ ( ( ( 1 . 0 ) + ( 8 . 0 ) ) · ( ( 1 . 0 ) + ( 8 . 0 ) ) ) = ; 8 1 |
| 165 | 147 156 164 | 3eqtr4ri | ⊢ ( ( ( 1 . 0 ) + ( 8 . 0 ) ) · ( ( 1 . 0 ) + ( 8 . 0 ) ) ) = ( ( ( 1 . _ 0 0 ) + ( ; 1 6 . _ 0 0 ) ) + ( ; 6 4 . _ 0 0 ) ) |
| 166 | 1 51 73 51 1 73 51 51 51 51 1 99 51 51 100 51 51 1 98 98 24 1 1 98 52 101 102 102 115 122 129 142 165 | dpmul4 | ⊢ ( ( 1 . _ 0 _ 8 0 ) · ( 1 . _ 0 _ 8 0 ) ) < ( 1 . _ 1 _ 6 7 ) |
| 167 | 97 166 | eqbrtri | ⊢ ( ( 1 . _ 0 _ 8 0 ) ↑ 2 ) < ( 1 . _ 1 _ 6 7 ) |
| 168 | 92 | resqcli | ⊢ ( ( 1 . _ 0 _ 8 0 ) ↑ 2 ) ∈ ℝ |
| 169 | 34 3 | pm3.2i | ⊢ ( 6 ∈ ℝ ∧ 7 ∈ ℝ ) |
| 170 | dp2cl | ⊢ ( ( 6 ∈ ℝ ∧ 7 ∈ ℝ ) → _ 6 7 ∈ ℝ ) | |
| 171 | 169 170 | ax-mp | ⊢ _ 6 7 ∈ ℝ |
| 172 | 35 171 | pm3.2i | ⊢ ( 1 ∈ ℝ ∧ _ 6 7 ∈ ℝ ) |
| 173 | dp2cl | ⊢ ( ( 1 ∈ ℝ ∧ _ 6 7 ∈ ℝ ) → _ 1 _ 6 7 ∈ ℝ ) | |
| 174 | 172 173 | ax-mp | ⊢ _ 1 _ 6 7 ∈ ℝ |
| 175 | dpcl | ⊢ ( ( 1 ∈ ℕ0 ∧ _ 1 _ 6 7 ∈ ℝ ) → ( 1 . _ 1 _ 6 7 ) ∈ ℝ ) | |
| 176 | 1 174 175 | mp2an | ⊢ ( 1 . _ 1 _ 6 7 ) ∈ ℝ |
| 177 | 23 168 176 | lttri | ⊢ ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) < ( ( 1 . _ 0 _ 8 0 ) ↑ 2 ) ∧ ( ( 1 . _ 0 _ 8 0 ) ↑ 2 ) < ( 1 . _ 1 _ 6 7 ) ) → ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) < ( 1 . _ 1 _ 6 7 ) ) |
| 178 | 95 167 177 | mp2an | ⊢ ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) < ( 1 . _ 1 _ 6 7 ) |
| 179 | 23 176 32 47 | ltmul1ii | ⊢ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) < ( 1 . _ 1 _ 6 7 ) ↔ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) < ( ( 1 . _ 1 _ 6 7 ) · ( 1 . _ 4 _ 1 4 ) ) ) |
| 180 | 178 179 | mpbi | ⊢ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) < ( ( 1 . _ 1 _ 6 7 ) · ( 1 . _ 4 _ 1 4 ) ) |
| 181 | 2nn0 | ⊢ 2 ∈ ℕ0 | |
| 182 | 3nn0 | ⊢ 3 ∈ ℕ0 | |
| 183 | 1lt10 | ⊢ 1 < ; 1 0 | |
| 184 | 3lt10 | ⊢ 3 < ; 1 0 | |
| 185 | 8lt10 | ⊢ 8 < ; 1 0 | |
| 186 | 130 53 | deccl | ⊢ ; ; 1 0 9 ∈ ℕ0 |
| 187 | eqid | ⊢ ; ; ; 1 0 9 2 = ; ; ; 1 0 9 2 | |
| 188 | 53 | dec0h | ⊢ 9 = ; 0 9 |
| 189 | 186 | nn0cni | ⊢ ; ; 1 0 9 ∈ ℂ |
| 190 | 189 | addridi | ⊢ ( ; ; 1 0 9 + 0 ) = ; ; 1 0 9 |
| 191 | dec10p | ⊢ ( ; 1 0 + 0 ) = ; 1 0 | |
| 192 | 138 | addridi | ⊢ ( 1 + 0 ) = 1 |
| 193 | 1 51 51 1 191 152 192 153 | decadd | ⊢ ( ( ; 1 0 + 0 ) + 1 ) = ; 1 1 |
| 194 | 9p1e10 | ⊢ ( 9 + 1 ) = ; 1 0 | |
| 195 | 130 53 51 1 190 152 193 51 194 | decaddc | ⊢ ( ( ; ; 1 0 9 + 0 ) + 1 ) = ; ; 1 1 0 |
| 196 | 9cn | ⊢ 9 ∈ ℂ | |
| 197 | 2cn | ⊢ 2 ∈ ℂ | |
| 198 | 196 197 | addcomi | ⊢ ( 9 + 2 ) = ( 2 + 9 ) |
| 199 | 9p2e11 | ⊢ ( 9 + 2 ) = ; 1 1 | |
| 200 | 198 199 | eqtr3i | ⊢ ( 2 + 9 ) = ; 1 1 |
| 201 | 186 181 51 53 187 188 195 1 200 | decaddc | ⊢ ( ; ; ; 1 0 9 2 + 9 ) = ; ; ; 1 1 0 1 |
| 202 | 113 138 | mulcomi | ⊢ ( 4 · 1 ) = ( 1 · 4 ) |
| 203 | 113 | mulridi | ⊢ ( 4 · 1 ) = 4 |
| 204 | 202 203 | eqtr3i | ⊢ ( 1 · 4 ) = 4 |
| 205 | 24 | dec0h | ⊢ 4 = ; 0 4 |
| 206 | 203 202 205 | 3eqtr3i | ⊢ ( 1 · 4 ) = ; 0 4 |
| 207 | 138 113 | addcli | ⊢ ( 1 + 4 ) ∈ ℂ |
| 208 | 207 | addridi | ⊢ ( ( 1 + 4 ) + 0 ) = ( 1 + 4 ) |
| 209 | 113 138 | addcomi | ⊢ ( 4 + 1 ) = ( 1 + 4 ) |
| 210 | 4p1e5 | ⊢ ( 4 + 1 ) = 5 | |
| 211 | 208 209 210 | 3eqtr2i | ⊢ ( ( 1 + 4 ) + 0 ) = 5 |
| 212 | 54 | dec0h | ⊢ 5 = ; 0 5 |
| 213 | 211 212 | eqtri | ⊢ ( ( 1 + 4 ) + 0 ) = ; 0 5 |
| 214 | 1 1 1 24 51 51 54 24 116 204 116 206 213 192 | dpmul | ⊢ ( ( 1 . 1 ) · ( 1 . 4 ) ) = ( 1 . _ 5 4 ) |
| 215 | 110 | mulridi | ⊢ ( 6 · 1 ) = 6 |
| 216 | 6t4e24 | ⊢ ( 6 · 4 ) = ; 2 4 | |
| 217 | 7cn | ⊢ 7 ∈ ℂ | |
| 218 | 217 | mulridi | ⊢ ( 7 · 1 ) = 7 |
| 219 | 7t4e28 | ⊢ ( 7 · 4 ) = ; 2 8 | |
| 220 | 181 24 | deccl | ⊢ ; 2 4 ∈ ℕ0 |
| 221 | 220 | nn0cni | ⊢ ; 2 4 ∈ ℂ |
| 222 | 221 217 | addcomi | ⊢ ( ; 2 4 + 7 ) = ( 7 + ; 2 4 ) |
| 223 | eqid | ⊢ ; 2 4 = ; 2 4 | |
| 224 | 2p1e3 | ⊢ ( 2 + 1 ) = 3 | |
| 225 | 217 113 146 | addcomli | ⊢ ( 4 + 7 ) = ; 1 1 |
| 226 | 181 24 52 223 224 1 225 | decaddci | ⊢ ( ; 2 4 + 7 ) = ; 3 1 |
| 227 | 222 226 | eqtr3i | ⊢ ( 7 + ; 2 4 ) = ; 3 1 |
| 228 | 227 | oveq1i | ⊢ ( ( 7 + ; 2 4 ) + 2 ) = ( ; 3 1 + 2 ) |
| 229 | eqid | ⊢ ; 3 1 = ; 3 1 | |
| 230 | 197 138 224 | addcomli | ⊢ ( 1 + 2 ) = 3 |
| 231 | 182 1 181 229 230 | decaddi | ⊢ ( ; 3 1 + 2 ) = ; 3 3 |
| 232 | 228 231 | eqtri | ⊢ ( ( 7 + ; 2 4 ) + 2 ) = ; 3 3 |
| 233 | 6p3e9 | ⊢ ( 6 + 3 ) = 9 | |
| 234 | 98 52 1 24 181 182 182 73 215 216 218 219 232 233 | dpmul | ⊢ ( ( 6 . 7 ) · ( 1 . 4 ) ) = ( 9 . _ 3 8 ) |
| 235 | 1 54 | deccl | ⊢ ; 1 5 ∈ ℕ0 |
| 236 | 235 24 | deccl | ⊢ ; ; 1 5 4 ∈ ℕ0 |
| 237 | 51 1 | deccl | ⊢ ; 0 1 ∈ ℕ0 |
| 238 | 237 1 | deccl | ⊢ ; ; 0 1 1 ∈ ℕ0 |
| 239 | eqid | ⊢ ; ; ; 1 5 4 1 = ; ; ; 1 5 4 1 | |
| 240 | 152 | deceq1i | ⊢ ; 1 1 = ; ; 0 1 1 |
| 241 | 240 | deceq1i | ⊢ ; ; 1 1 0 = ; ; ; 0 1 1 0 |
| 242 | eqid | ⊢ ; ; 1 5 4 = ; ; 1 5 4 | |
| 243 | eqid | ⊢ ; ; 0 1 1 = ; ; 0 1 1 | |
| 244 | 152 | oveq2i | ⊢ ( ; 1 5 + 1 ) = ( ; 1 5 + ; 0 1 ) |
| 245 | eqid | ⊢ ; 1 5 = ; 1 5 | |
| 246 | 5p1e6 | ⊢ ( 5 + 1 ) = 6 | |
| 247 | 1 54 1 245 246 | decaddi | ⊢ ( ; 1 5 + 1 ) = ; 1 6 |
| 248 | 244 247 | eqtr3i | ⊢ ( ; 1 5 + ; 0 1 ) = ; 1 6 |
| 249 | 235 24 237 1 242 243 248 210 | decadd | ⊢ ( ; ; 1 5 4 + ; ; 0 1 1 ) = ; ; 1 6 5 |
| 250 | 236 1 238 51 239 241 249 192 | decadd | ⊢ ( ; ; ; 1 5 4 1 + ; ; 1 1 0 ) = ; ; ; 1 6 5 1 |
| 251 | 7t2e14 | ⊢ ( 7 · 2 ) = ; 1 4 | |
| 252 | 8t7e56 | ⊢ ( 8 · 7 ) = ; 5 6 | |
| 253 | 158 217 252 | mulcomli | ⊢ ( 7 · 8 ) = ; 5 6 |
| 254 | 8t2e16 | ⊢ ( 8 · 2 ) = ; 1 6 | |
| 255 | eqid | ⊢ ; 5 6 = ; 5 6 | |
| 256 | 5cn | ⊢ 5 ∈ ℂ | |
| 257 | 256 138 246 | addcomli | ⊢ ( 1 + 5 ) = 6 |
| 258 | 257 | oveq1i | ⊢ ( ( 1 + 5 ) + 1 ) = ( 6 + 1 ) |
| 259 | 258 140 | eqtri | ⊢ ( ( 1 + 5 ) + 1 ) = 7 |
| 260 | 6p6e12 | ⊢ ( 6 + 6 ) = ; 1 2 | |
| 261 | 1 98 54 98 135 255 259 181 260 | decaddc | ⊢ ( ; 1 6 + ; 5 6 ) = ; 7 2 |
| 262 | 261 | oveq1i | ⊢ ( ( ; 1 6 + ; 5 6 ) + 6 ) = ( ; 7 2 + 6 ) |
| 263 | eqid | ⊢ ; 7 2 = ; 7 2 | |
| 264 | 6p2e8 | ⊢ ( 6 + 2 ) = 8 | |
| 265 | 110 197 264 | addcomli | ⊢ ( 2 + 6 ) = 8 |
| 266 | 52 181 98 263 265 | decaddi | ⊢ ( ; 7 2 + 6 ) = ; 7 8 |
| 267 | 262 266 | eqtri | ⊢ ( ( ; 1 6 + ; 5 6 ) + 6 ) = ; 7 8 |
| 268 | eqid | ⊢ ; 1 4 = ; 1 4 | |
| 269 | 1p1e2 | ⊢ ( 1 + 1 ) = 2 | |
| 270 | 1 24 52 268 269 1 225 | decaddci | ⊢ ( ; 1 4 + 7 ) = ; 2 1 |
| 271 | 52 73 181 73 98 52 73 24 251 253 254 123 267 270 | dpmul | ⊢ ( ( 7 . 8 ) · ( 2 . 8 ) ) = ( ; 2 1 . _ 8 4 ) |
| 272 | eqid | ⊢ ; 1 1 = ; 1 1 | |
| 273 | eqid | ⊢ ; 6 7 = ; 6 7 | |
| 274 | 217 138 71 | addcomli | ⊢ ( 1 + 7 ) = 8 |
| 275 | 1 1 98 52 272 273 141 274 | decadd | ⊢ ( ; 1 1 + ; 6 7 ) = ; 7 8 |
| 276 | 1 1 98 52 52 73 275 | dpadd | ⊢ ( ( 1 . 1 ) + ( 6 . 7 ) ) = ( 7 . 8 ) |
| 277 | 4p4e8 | ⊢ ( 4 + 4 ) = 8 | |
| 278 | 1 24 1 24 268 268 269 277 | decadd | ⊢ ( ; 1 4 + ; 1 4 ) = ; 2 8 |
| 279 | 1 24 1 24 181 73 278 | dpadd | ⊢ ( ( 1 . 4 ) + ( 1 . 4 ) ) = ( 2 . 8 ) |
| 280 | 276 279 | oveq12i | ⊢ ( ( ( 1 . 1 ) + ( 6 . 7 ) ) · ( ( 1 . 4 ) + ( 1 . 4 ) ) ) = ( ( 7 . 8 ) · ( 2 . 8 ) ) |
| 281 | 1 181 | deccl | ⊢ ; 1 2 ∈ ℕ0 |
| 282 | eqid | ⊢ ; ; 1 0 9 = ; ; 1 0 9 | |
| 283 | 130 | nn0cni | ⊢ ; 1 0 ∈ ℂ |
| 284 | 283 138 136 | addcomli | ⊢ ( 1 + ; 1 0 ) = ; 1 1 |
| 285 | 1 1 269 284 | decsuc | ⊢ ( ( 1 + ; 1 0 ) + 1 ) = ; 1 2 |
| 286 | 9p5e14 | ⊢ ( 9 + 5 ) = ; 1 4 | |
| 287 | 196 256 286 | addcomli | ⊢ ( 5 + 9 ) = ; 1 4 |
| 288 | 1 54 130 53 245 282 285 24 287 | decaddc | ⊢ ( ; 1 5 + ; ; 1 0 9 ) = ; ; 1 2 4 |
| 289 | 4p2e6 | ⊢ ( 4 + 2 ) = 6 | |
| 290 | 235 24 186 181 242 187 288 289 | decadd | ⊢ ( ; ; 1 5 4 + ; ; ; 1 0 9 2 ) = ; ; ; 1 2 4 6 |
| 291 | 1 54 24 130 53 281 181 24 98 290 | dpadd3 | ⊢ ( ( 1 . _ 5 4 ) + ( ; 1 0 . _ 9 2 ) ) = ( ; 1 2 . _ 4 6 ) |
| 292 | 291 | oveq1i | ⊢ ( ( ( 1 . _ 5 4 ) + ( ; 1 0 . _ 9 2 ) ) + ( 9 . _ 3 8 ) ) = ( ( ; 1 2 . _ 4 6 ) + ( 9 . _ 3 8 ) ) |
| 293 | 181 1 | deccl | ⊢ ; 2 1 ∈ ℕ0 |
| 294 | 281 24 | deccl | ⊢ ; ; 1 2 4 ∈ ℕ0 |
| 295 | 53 182 | deccl | ⊢ ; 9 3 ∈ ℕ0 |
| 296 | eqid | ⊢ ; ; ; 1 2 4 6 = ; ; ; 1 2 4 6 | |
| 297 | eqid | ⊢ ; ; 9 3 8 = ; ; 9 3 8 | |
| 298 | eqid | ⊢ ; ; 1 2 4 = ; ; 1 2 4 | |
| 299 | eqid | ⊢ ; 9 3 = ; 9 3 | |
| 300 | eqid | ⊢ ; 1 2 = ; 1 2 | |
| 301 | 1 181 53 300 269 1 200 | decaddci | ⊢ ( ; 1 2 + 9 ) = ; 2 1 |
| 302 | 4p3e7 | ⊢ ( 4 + 3 ) = 7 | |
| 303 | 281 24 53 182 298 299 301 302 | decadd | ⊢ ( ; ; 1 2 4 + ; 9 3 ) = ; ; 2 1 7 |
| 304 | 293 52 71 303 | decsuc | ⊢ ( ( ; ; 1 2 4 + ; 9 3 ) + 1 ) = ; ; 2 1 8 |
| 305 | 8p6e14 | ⊢ ( 8 + 6 ) = ; 1 4 | |
| 306 | 158 110 305 | addcomli | ⊢ ( 6 + 8 ) = ; 1 4 |
| 307 | 294 98 295 73 296 297 304 24 306 | decaddc | ⊢ ( ; ; ; 1 2 4 6 + ; ; 9 3 8 ) = ; ; ; 2 1 8 4 |
| 308 | 281 24 98 53 182 293 73 73 24 307 | dpadd3 | ⊢ ( ( ; 1 2 . _ 4 6 ) + ( 9 . _ 3 8 ) ) = ( ; 2 1 . _ 8 4 ) |
| 309 | 292 308 | eqtri | ⊢ ( ( ( 1 . _ 5 4 ) + ( ; 1 0 . _ 9 2 ) ) + ( 9 . _ 3 8 ) ) = ( ; 2 1 . _ 8 4 ) |
| 310 | 271 280 309 | 3eqtr4i | ⊢ ( ( ( 1 . 1 ) + ( 6 . 7 ) ) · ( ( 1 . 4 ) + ( 1 . 4 ) ) ) = ( ( ( 1 . _ 5 4 ) + ( ; 1 0 . _ 9 2 ) ) + ( 9 . _ 3 8 ) ) |
| 311 | 1 1 98 52 1 1 54 24 24 24 1 130 53 181 53 182 73 1 1 51 1 1 98 54 1 183 184 185 201 214 234 250 310 | dpmul4 | ⊢ ( ( 1 . _ 1 _ 6 7 ) · ( 1 . _ 4 _ 1 4 ) ) < ( 1 . _ 6 _ 5 1 ) |
| 312 | 176 32 | remulcli | ⊢ ( ( 1 . _ 1 _ 6 7 ) · ( 1 . _ 4 _ 1 4 ) ) ∈ ℝ |
| 313 | 33 312 43 | lttri | ⊢ ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) < ( ( 1 . _ 1 _ 6 7 ) · ( 1 . _ 4 _ 1 4 ) ) ∧ ( ( 1 . _ 1 _ 6 7 ) · ( 1 . _ 4 _ 1 4 ) ) < ( 1 . _ 6 _ 5 1 ) ) → ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) < ( 1 . _ 6 _ 5 1 ) ) |
| 314 | 180 311 313 | mp2an | ⊢ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) < ( 1 . _ 6 _ 5 1 ) |
| 315 | 50 314 | pm3.2i | ⊢ ( 0 ≤ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) ∧ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) < ( 1 . _ 6 _ 5 1 ) ) |
| 316 | 44 315 | pm3.2i | ⊢ ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) ∈ ℝ ∧ ( 1 . _ 6 _ 5 1 ) ∈ ℝ ) ∧ ( 0 ≤ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) ∧ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) < ( 1 . _ 6 _ 5 1 ) ) ) |
| 317 | 4re | ⊢ 4 ∈ ℝ | |
| 318 | 2re | ⊢ 2 ∈ ℝ | |
| 319 | 3re | ⊢ 3 ∈ ℝ | |
| 320 | 34 319 | pm3.2i | ⊢ ( 6 ∈ ℝ ∧ 3 ∈ ℝ ) |
| 321 | dp2cl | ⊢ ( ( 6 ∈ ℝ ∧ 3 ∈ ℝ ) → _ 6 3 ∈ ℝ ) | |
| 322 | 320 321 | ax-mp | ⊢ _ 6 3 ∈ ℝ |
| 323 | 318 322 | pm3.2i | ⊢ ( 2 ∈ ℝ ∧ _ 6 3 ∈ ℝ ) |
| 324 | dp2cl | ⊢ ( ( 2 ∈ ℝ ∧ _ 6 3 ∈ ℝ ) → _ 2 _ 6 3 ∈ ℝ ) | |
| 325 | 323 324 | ax-mp | ⊢ _ 2 _ 6 3 ∈ ℝ |
| 326 | 317 325 | pm3.2i | ⊢ ( 4 ∈ ℝ ∧ _ 2 _ 6 3 ∈ ℝ ) |
| 327 | dp2cl | ⊢ ( ( 4 ∈ ℝ ∧ _ 2 _ 6 3 ∈ ℝ ) → _ 4 _ 2 _ 6 3 ∈ ℝ ) | |
| 328 | 326 327 | ax-mp | ⊢ _ 4 _ 2 _ 6 3 ∈ ℝ |
| 329 | dpcl | ⊢ ( ( 1 ∈ ℕ0 ∧ _ 4 _ 2 _ 6 3 ∈ ℝ ) → ( 1 . _ 4 _ 2 _ 6 3 ) ∈ ℝ ) | |
| 330 | 1 328 329 | mp2an | ⊢ ( 1 . _ 4 _ 2 _ 6 3 ) ∈ ℝ |
| 331 | 84 319 | pm3.2i | ⊢ ( 8 ∈ ℝ ∧ 3 ∈ ℝ ) |
| 332 | dp2cl | ⊢ ( ( 8 ∈ ℝ ∧ 3 ∈ ℝ ) → _ 8 3 ∈ ℝ ) | |
| 333 | 331 332 | ax-mp | ⊢ _ 8 3 ∈ ℝ |
| 334 | 84 333 | pm3.2i | ⊢ ( 8 ∈ ℝ ∧ _ 8 3 ∈ ℝ ) |
| 335 | dp2cl | ⊢ ( ( 8 ∈ ℝ ∧ _ 8 3 ∈ ℝ ) → _ 8 _ 8 3 ∈ ℝ ) | |
| 336 | 334 335 | ax-mp | ⊢ _ 8 _ 8 3 ∈ ℝ |
| 337 | 319 336 | pm3.2i | ⊢ ( 3 ∈ ℝ ∧ _ 8 _ 8 3 ∈ ℝ ) |
| 338 | dp2cl | ⊢ ( ( 3 ∈ ℝ ∧ _ 8 _ 8 3 ∈ ℝ ) → _ 3 _ 8 _ 8 3 ∈ ℝ ) | |
| 339 | 337 338 | ax-mp | ⊢ _ 3 _ 8 _ 8 3 ∈ ℝ |
| 340 | 2 339 | pm3.2i | ⊢ ( 0 ∈ ℝ ∧ _ 3 _ 8 _ 8 3 ∈ ℝ ) |
| 341 | dp2cl | ⊢ ( ( 0 ∈ ℝ ∧ _ 3 _ 8 _ 8 3 ∈ ℝ ) → _ 0 _ 3 _ 8 _ 8 3 ∈ ℝ ) | |
| 342 | 340 341 | ax-mp | ⊢ _ 0 _ 3 _ 8 _ 8 3 ∈ ℝ |
| 343 | dpcl | ⊢ ( ( 1 ∈ ℕ0 ∧ _ 0 _ 3 _ 8 _ 8 3 ∈ ℝ ) → ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ∈ ℝ ) | |
| 344 | 1 342 343 | mp2an | ⊢ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ∈ ℝ |
| 345 | 330 344 | remulcli | ⊢ ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ∈ ℝ |
| 346 | 317 333 | pm3.2i | ⊢ ( 4 ∈ ℝ ∧ _ 8 3 ∈ ℝ ) |
| 347 | dp2cl | ⊢ ( ( 4 ∈ ℝ ∧ _ 8 3 ∈ ℝ ) → _ 4 _ 8 3 ∈ ℝ ) | |
| 348 | 346 347 | ax-mp | ⊢ _ 4 _ 8 3 ∈ ℝ |
| 349 | dpcl | ⊢ ( ( 1 ∈ ℕ0 ∧ _ 4 _ 8 3 ∈ ℝ ) → ( 1 . _ 4 _ 8 3 ) ∈ ℝ ) | |
| 350 | 1 348 349 | mp2an | ⊢ ( 1 . _ 4 _ 8 3 ) ∈ ℝ |
| 351 | 345 350 | pm3.2i | ⊢ ( ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ∈ ℝ ∧ ( 1 . _ 4 _ 8 3 ) ∈ ℝ ) |
| 352 | 3rp | ⊢ 3 ∈ ℝ+ | |
| 353 | 98 352 | rpdp2cl | ⊢ _ 6 3 ∈ ℝ+ |
| 354 | 181 353 | rpdp2cl | ⊢ _ 2 _ 6 3 ∈ ℝ+ |
| 355 | 24 354 | rpdp2cl | ⊢ _ 4 _ 2 _ 6 3 ∈ ℝ+ |
| 356 | 1 355 | rpdpcl | ⊢ ( 1 . _ 4 _ 2 _ 6 3 ) ∈ ℝ+ |
| 357 | rpge0 | ⊢ ( ( 1 . _ 4 _ 2 _ 6 3 ) ∈ ℝ+ → 0 ≤ ( 1 . _ 4 _ 2 _ 6 3 ) ) | |
| 358 | 356 357 | ax-mp | ⊢ 0 ≤ ( 1 . _ 4 _ 2 _ 6 3 ) |
| 359 | 73 352 | rpdp2cl | ⊢ _ 8 3 ∈ ℝ+ |
| 360 | 73 359 | rpdp2cl | ⊢ _ 8 _ 8 3 ∈ ℝ+ |
| 361 | 182 360 | rpdp2cl | ⊢ _ 3 _ 8 _ 8 3 ∈ ℝ+ |
| 362 | 51 361 | rpdp2cl | ⊢ _ 0 _ 3 _ 8 _ 8 3 ∈ ℝ+ |
| 363 | 1 362 | rpdpcl | ⊢ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ∈ ℝ+ |
| 364 | rpge0 | ⊢ ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ∈ ℝ+ → 0 ≤ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) | |
| 365 | 363 364 | ax-mp | ⊢ 0 ≤ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) |
| 366 | 330 344 | mulge0i | ⊢ ( ( 0 ≤ ( 1 . _ 4 _ 2 _ 6 3 ) ∧ 0 ≤ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) → 0 ≤ ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) |
| 367 | 358 365 366 | mp2an | ⊢ 0 ≤ ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) |
| 368 | 318 3 | pm3.2i | ⊢ ( 2 ∈ ℝ ∧ 7 ∈ ℝ ) |
| 369 | dp2cl | ⊢ ( ( 2 ∈ ℝ ∧ 7 ∈ ℝ ) → _ 2 7 ∈ ℝ ) | |
| 370 | 368 369 | ax-mp | ⊢ _ 2 7 ∈ ℝ |
| 371 | 317 370 | pm3.2i | ⊢ ( 4 ∈ ℝ ∧ _ 2 7 ∈ ℝ ) |
| 372 | dp2cl | ⊢ ( ( 4 ∈ ℝ ∧ _ 2 7 ∈ ℝ ) → _ 4 _ 2 7 ∈ ℝ ) | |
| 373 | 371 372 | ax-mp | ⊢ _ 4 _ 2 7 ∈ ℝ |
| 374 | dpcl | ⊢ ( ( 1 ∈ ℕ0 ∧ _ 4 _ 2 7 ∈ ℝ ) → ( 1 . _ 4 _ 2 7 ) ∈ ℝ ) | |
| 375 | 1 373 374 | mp2an | ⊢ ( 1 . _ 4 _ 2 7 ) ∈ ℝ |
| 376 | 330 375 | pm3.2i | ⊢ ( ( 1 . _ 4 _ 2 _ 6 3 ) ∈ ℝ ∧ ( 1 . _ 4 _ 2 7 ) ∈ ℝ ) |
| 377 | 7nn | ⊢ 7 ∈ ℕ | |
| 378 | nnrp | ⊢ ( 7 ∈ ℕ → 7 ∈ ℝ+ ) | |
| 379 | 377 378 | ax-mp | ⊢ 7 ∈ ℝ+ |
| 380 | 181 379 | rpdp2cl | ⊢ _ 2 7 ∈ ℝ+ |
| 381 | 24 380 | rpdp2cl | ⊢ _ 4 _ 2 7 ∈ ℝ+ |
| 382 | 98 352 184 140 | dp2ltsuc | ⊢ _ 6 3 < 7 |
| 383 | 181 353 379 382 | dp2lt | ⊢ _ 2 _ 6 3 < _ 2 7 |
| 384 | 24 354 380 383 | dp2lt | ⊢ _ 4 _ 2 _ 6 3 < _ 4 _ 2 7 |
| 385 | 1 355 381 384 | dplt | ⊢ ( 1 . _ 4 _ 2 _ 6 3 ) < ( 1 . _ 4 _ 2 7 ) |
| 386 | 358 385 | pm3.2i | ⊢ ( 0 ≤ ( 1 . _ 4 _ 2 _ 6 3 ) ∧ ( 1 . _ 4 _ 2 _ 6 3 ) < ( 1 . _ 4 _ 2 7 ) ) |
| 387 | 376 386 | pm3.2i | ⊢ ( ( ( 1 . _ 4 _ 2 _ 6 3 ) ∈ ℝ ∧ ( 1 . _ 4 _ 2 7 ) ∈ ℝ ) ∧ ( 0 ≤ ( 1 . _ 4 _ 2 _ 6 3 ) ∧ ( 1 . _ 4 _ 2 _ 6 3 ) < ( 1 . _ 4 _ 2 7 ) ) ) |
| 388 | 319 4 | pm3.2i | ⊢ ( 3 ∈ ℝ ∧ 9 ∈ ℝ ) |
| 389 | dp2cl | ⊢ ( ( 3 ∈ ℝ ∧ 9 ∈ ℝ ) → _ 3 9 ∈ ℝ ) | |
| 390 | 388 389 | ax-mp | ⊢ _ 3 9 ∈ ℝ |
| 391 | 2 390 | pm3.2i | ⊢ ( 0 ∈ ℝ ∧ _ 3 9 ∈ ℝ ) |
| 392 | dp2cl | ⊢ ( ( 0 ∈ ℝ ∧ _ 3 9 ∈ ℝ ) → _ 0 _ 3 9 ∈ ℝ ) | |
| 393 | 391 392 | ax-mp | ⊢ _ 0 _ 3 9 ∈ ℝ |
| 394 | dpcl | ⊢ ( ( 1 ∈ ℕ0 ∧ _ 0 _ 3 9 ∈ ℝ ) → ( 1 . _ 0 _ 3 9 ) ∈ ℝ ) | |
| 395 | 1 393 394 | mp2an | ⊢ ( 1 . _ 0 _ 3 9 ) ∈ ℝ |
| 396 | 344 395 | pm3.2i | ⊢ ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ∈ ℝ ∧ ( 1 . _ 0 _ 3 9 ) ∈ ℝ ) |
| 397 | 9nn | ⊢ 9 ∈ ℕ | |
| 398 | nnrp | ⊢ ( 9 ∈ ℕ → 9 ∈ ℝ+ ) | |
| 399 | 397 398 | ax-mp | ⊢ 9 ∈ ℝ+ |
| 400 | 182 399 | rpdp2cl | ⊢ _ 3 9 ∈ ℝ+ |
| 401 | 51 400 | rpdp2cl | ⊢ _ 0 _ 3 9 ∈ ℝ+ |
| 402 | 73 352 185 184 | dp2lt10 | ⊢ _ 8 3 < ; 1 0 |
| 403 | 73 359 402 160 | dp2ltsuc | ⊢ _ 8 _ 8 3 < 9 |
| 404 | 182 360 399 403 | dp2lt | ⊢ _ 3 _ 8 _ 8 3 < _ 3 9 |
| 405 | 51 361 400 404 | dp2lt | ⊢ _ 0 _ 3 _ 8 _ 8 3 < _ 0 _ 3 9 |
| 406 | 1 362 401 405 | dplt | ⊢ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) < ( 1 . _ 0 _ 3 9 ) |
| 407 | 365 406 | pm3.2i | ⊢ ( 0 ≤ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ∧ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) < ( 1 . _ 0 _ 3 9 ) ) |
| 408 | 396 407 | pm3.2i | ⊢ ( ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ∈ ℝ ∧ ( 1 . _ 0 _ 3 9 ) ∈ ℝ ) ∧ ( 0 ≤ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ∧ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) < ( 1 . _ 0 _ 3 9 ) ) ) |
| 409 | ltmul12a | ⊢ ( ( ( ( ( 1 . _ 4 _ 2 _ 6 3 ) ∈ ℝ ∧ ( 1 . _ 4 _ 2 7 ) ∈ ℝ ) ∧ ( 0 ≤ ( 1 . _ 4 _ 2 _ 6 3 ) ∧ ( 1 . _ 4 _ 2 _ 6 3 ) < ( 1 . _ 4 _ 2 7 ) ) ) ∧ ( ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ∈ ℝ ∧ ( 1 . _ 0 _ 3 9 ) ∈ ℝ ) ∧ ( 0 ≤ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ∧ ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) < ( 1 . _ 0 _ 3 9 ) ) ) ) → ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( ( 1 . _ 4 _ 2 7 ) · ( 1 . _ 0 _ 3 9 ) ) ) | |
| 410 | 387 408 409 | mp2an | ⊢ ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( ( 1 . _ 4 _ 2 7 ) · ( 1 . _ 0 _ 3 9 ) ) |
| 411 | 6lt10 | ⊢ 6 < ; 1 0 | |
| 412 | 73 1 | deccl | ⊢ ; 8 1 ∈ ℕ0 |
| 413 | eqid | ⊢ ; ; 8 1 6 = ; ; 8 1 6 | |
| 414 | eqid | ⊢ ; 1 0 = ; 1 0 | |
| 415 | eqid | ⊢ ; 8 1 = ; 8 1 | |
| 416 | 73 1 269 415 | decsuc | ⊢ ( ; 8 1 + 1 ) = ; 8 2 |
| 417 | 73 | dec0h | ⊢ 8 = ; 0 8 |
| 418 | 417 | deceq1i | ⊢ ; 8 2 = ; ; 0 8 2 |
| 419 | 416 418 | eqtri | ⊢ ( ; 8 1 + 1 ) = ; ; 0 8 2 |
| 420 | 110 | addridi | ⊢ ( 6 + 0 ) = 6 |
| 421 | 412 98 1 51 413 414 419 420 | decadd | ⊢ ( ; ; 8 1 6 + ; 1 0 ) = ; ; ; 0 8 2 6 |
| 422 | 138 | mul01i | ⊢ ( 1 · 0 ) = 0 |
| 423 | 113 | mul01i | ⊢ ( 4 · 0 ) = 0 |
| 424 | 51 | dec0h | ⊢ 0 = ; 0 0 |
| 425 | 423 424 | eqtri | ⊢ ( 4 · 0 ) = ; 0 0 |
| 426 | 113 | addridi | ⊢ ( 4 + 0 ) = 4 |
| 427 | 426 | oveq1i | ⊢ ( ( 4 + 0 ) + 0 ) = ( 4 + 0 ) |
| 428 | 427 426 205 | 3eqtri | ⊢ ( ( 4 + 0 ) + 0 ) = ; 0 4 |
| 429 | 1 24 1 51 51 51 24 51 116 422 203 425 428 192 | dpmul | ⊢ ( ( 1 . 4 ) · ( 1 . 0 ) ) = ( 1 . _ 4 0 ) |
| 430 | 2t3e6 | ⊢ ( 2 · 3 ) = 6 | |
| 431 | 9t2e18 | ⊢ ( 9 · 2 ) = ; 1 8 | |
| 432 | 196 197 431 | mulcomli | ⊢ ( 2 · 9 ) = ; 1 8 |
| 433 | 7t3e21 | ⊢ ( 7 · 3 ) = ; 2 1 | |
| 434 | 9t7e63 | ⊢ ( 9 · 7 ) = ; 6 3 | |
| 435 | 196 217 434 | mulcomli | ⊢ ( 7 · 9 ) = ; 6 3 |
| 436 | eqid | ⊢ ; 2 1 = ; 2 1 | |
| 437 | eqid | ⊢ ; 1 8 = ; 1 8 | |
| 438 | 159 160 | eqtri | ⊢ ( 1 + 8 ) = 9 |
| 439 | 181 1 1 73 436 437 224 438 | decadd | ⊢ ( ; 2 1 + ; 1 8 ) = ; 3 9 |
| 440 | 439 | oveq1i | ⊢ ( ( ; 2 1 + ; 1 8 ) + 6 ) = ( ; 3 9 + 6 ) |
| 441 | eqid | ⊢ ; 3 9 = ; 3 9 | |
| 442 | 3p1e4 | ⊢ ( 3 + 1 ) = 4 | |
| 443 | 9p6e15 | ⊢ ( 9 + 6 ) = ; 1 5 | |
| 444 | 182 53 98 441 442 54 443 | decaddci | ⊢ ( ; 3 9 + 6 ) = ; 4 5 |
| 445 | 440 444 | eqtri | ⊢ ( ( ; 2 1 + ; 1 8 ) + 6 ) = ; 4 5 |
| 446 | 6p4e10 | ⊢ ( 6 + 4 ) = ; 1 0 | |
| 447 | 181 52 182 53 98 24 54 182 430 432 433 435 445 446 | dpmul | ⊢ ( ( 2 . 7 ) · ( 3 . 9 ) ) = ( ; 1 0 . _ 5 3 ) |
| 448 | 1 24 | deccl | ⊢ ; 1 4 ∈ ℕ0 |
| 449 | 448 51 | deccl | ⊢ ; ; 1 4 0 ∈ ℕ0 |
| 450 | 417 73 | eqeltrri | ⊢ ; 0 8 ∈ ℕ0 |
| 451 | eqid | ⊢ ; ; ; 1 4 0 1 = ; ; ; 1 4 0 1 | |
| 452 | eqid | ⊢ ; ; 0 8 2 = ; ; 0 8 2 | |
| 453 | eqid | ⊢ ; ; 1 4 0 = ; ; 1 4 0 | |
| 454 | 417 158 | eqeltrri | ⊢ ; 0 8 ∈ ℂ |
| 455 | 0cn | ⊢ 0 ∈ ℂ | |
| 456 | 417 | oveq1i | ⊢ ( 8 + 0 ) = ( ; 0 8 + 0 ) |
| 457 | 158 | addridi | ⊢ ( 8 + 0 ) = 8 |
| 458 | 456 457 | eqtr3i | ⊢ ( ; 0 8 + 0 ) = 8 |
| 459 | 454 455 458 | addcomli | ⊢ ( 0 + ; 0 8 ) = 8 |
| 460 | 448 51 450 453 459 | decaddi | ⊢ ( ; ; 1 4 0 + ; 0 8 ) = ; ; 1 4 8 |
| 461 | 449 1 450 181 451 452 460 230 | decadd | ⊢ ( ; ; ; 1 4 0 1 + ; ; 0 8 2 ) = ; ; ; 1 4 8 3 |
| 462 | 4t4e16 | ⊢ ( 4 · 4 ) = ; 1 6 | |
| 463 | 9t4e36 | ⊢ ( 9 · 4 ) = ; 3 6 | |
| 464 | 196 113 463 | mulcomli | ⊢ ( 4 · 9 ) = ; 3 6 |
| 465 | 196 | mulridi | ⊢ ( 9 · 1 ) = 9 |
| 466 | 465 188 | eqtri | ⊢ ( 9 · 1 ) = ; 0 9 |
| 467 | 196 138 466 | mulcomli | ⊢ ( 1 · 9 ) = ; 0 9 |
| 468 | 182 98 | deccl | ⊢ ; 3 6 ∈ ℕ0 |
| 469 | 468 | nn0cni | ⊢ ; 3 6 ∈ ℂ |
| 470 | eqid | ⊢ ; 3 6 = ; 3 6 | |
| 471 | 182 98 24 470 442 51 446 | decaddci | ⊢ ( ; 3 6 + 4 ) = ; 4 0 |
| 472 | 469 113 471 | addcomli | ⊢ ( 4 + ; 3 6 ) = ; 4 0 |
| 473 | 472 | oveq1i | ⊢ ( ( 4 + ; 3 6 ) + 0 ) = ( ; 4 0 + 0 ) |
| 474 | 24 51 | deccl | ⊢ ; 4 0 ∈ ℕ0 |
| 475 | 474 | nn0cni | ⊢ ; 4 0 ∈ ℂ |
| 476 | 475 | addridi | ⊢ ( ; 4 0 + 0 ) = ; 4 0 |
| 477 | 473 476 | eqtri | ⊢ ( ( 4 + ; 3 6 ) + 0 ) = ; 4 0 |
| 478 | 1 98 24 135 269 51 446 | decaddci | ⊢ ( ; 1 6 + 4 ) = ; 2 0 |
| 479 | 24 1 24 53 51 24 51 53 462 464 204 467 477 478 | dpmul | ⊢ ( ( 4 . 1 ) · ( 4 . 9 ) ) = ( ; 2 0 . _ 0 9 ) |
| 480 | eqid | ⊢ ; 2 7 = ; 2 7 | |
| 481 | 230 | oveq1i | ⊢ ( ( 1 + 2 ) + 1 ) = ( 3 + 1 ) |
| 482 | 481 442 | eqtri | ⊢ ( ( 1 + 2 ) + 1 ) = 4 |
| 483 | 1 24 181 52 268 480 482 1 225 | decaddc | ⊢ ( ; 1 4 + ; 2 7 ) = ; 4 1 |
| 484 | 1 24 181 52 24 1 483 | dpadd | ⊢ ( ( 1 . 4 ) + ( 2 . 7 ) ) = ( 4 . 1 ) |
| 485 | 3cn | ⊢ 3 ∈ ℂ | |
| 486 | 485 138 442 | addcomli | ⊢ ( 1 + 3 ) = 4 |
| 487 | 196 | addlidi | ⊢ ( 0 + 9 ) = 9 |
| 488 | 1 51 182 53 414 441 486 487 | decadd | ⊢ ( ; 1 0 + ; 3 9 ) = ; 4 9 |
| 489 | 1 51 182 53 24 53 488 | dpadd | ⊢ ( ( 1 . 0 ) + ( 3 . 9 ) ) = ( 4 . 9 ) |
| 490 | 484 489 | oveq12i | ⊢ ( ( ( 1 . 4 ) + ( 2 . 7 ) ) · ( ( 1 . 0 ) + ( 3 . 9 ) ) ) = ( ( 4 . 1 ) · ( 4 . 9 ) ) |
| 491 | 1 24 73 1 268 415 438 210 | decadd | ⊢ ( ; 1 4 + ; 8 1 ) = ; 9 5 |
| 492 | 448 51 412 98 453 413 491 111 | decadd | ⊢ ( ; ; 1 4 0 + ; ; 8 1 6 ) = ; ; 9 5 6 |
| 493 | 1 24 51 73 1 53 98 54 98 492 | dpadd3 | ⊢ ( ( 1 . _ 4 0 ) + ( 8 . _ 1 6 ) ) = ( 9 . _ 5 6 ) |
| 494 | 493 | oveq1i | ⊢ ( ( ( 1 . _ 4 0 ) + ( 8 . _ 1 6 ) ) + ( ; 1 0 . _ 5 3 ) ) = ( ( 9 . _ 5 6 ) + ( ; 1 0 . _ 5 3 ) ) |
| 495 | 181 51 | deccl | ⊢ ; 2 0 ∈ ℕ0 |
| 496 | 53 54 | deccl | ⊢ ; 9 5 ∈ ℕ0 |
| 497 | 130 54 | deccl | ⊢ ; ; 1 0 5 ∈ ℕ0 |
| 498 | eqid | ⊢ ; ; 9 5 6 = ; ; 9 5 6 | |
| 499 | eqid | ⊢ ; ; ; 1 0 5 3 = ; ; ; 1 0 5 3 | |
| 500 | eqid | ⊢ ; 9 5 = ; 9 5 | |
| 501 | eqid | ⊢ ; ; 1 0 5 = ; ; 1 0 5 | |
| 502 | dec10p | ⊢ ( ; 1 0 + 9 ) = ; 1 9 | |
| 503 | 283 196 502 | addcomli | ⊢ ( 9 + ; 1 0 ) = ; 1 9 |
| 504 | 503 | oveq1i | ⊢ ( ( 9 + ; 1 0 ) + 1 ) = ( ; 1 9 + 1 ) |
| 505 | eqid | ⊢ ; 1 9 = ; 1 9 | |
| 506 | 1 53 1 505 269 51 194 | decaddci | ⊢ ( ; 1 9 + 1 ) = ; 2 0 |
| 507 | 504 506 | eqtri | ⊢ ( ( 9 + ; 1 0 ) + 1 ) = ; 2 0 |
| 508 | 5p5e10 | ⊢ ( 5 + 5 ) = ; 1 0 | |
| 509 | 53 54 130 54 500 501 507 51 508 | decaddc | ⊢ ( ; 9 5 + ; ; 1 0 5 ) = ; ; 2 0 0 |
| 510 | 496 98 497 182 498 499 509 233 | decadd | ⊢ ( ; ; 9 5 6 + ; ; ; 1 0 5 3 ) = ; ; ; 2 0 0 9 |
| 511 | 53 54 98 130 54 495 182 51 53 510 | dpadd3 | ⊢ ( ( 9 . _ 5 6 ) + ( ; 1 0 . _ 5 3 ) ) = ( ; 2 0 . _ 0 9 ) |
| 512 | 494 511 | eqtri | ⊢ ( ( ( 1 . _ 4 0 ) + ( 8 . _ 1 6 ) ) + ( ; 1 0 . _ 5 3 ) ) = ( ; 2 0 . _ 0 9 ) |
| 513 | 479 490 512 | 3eqtr4i | ⊢ ( ( ( 1 . 4 ) + ( 2 . 7 ) ) · ( ( 1 . 0 ) + ( 3 . 9 ) ) ) = ( ( ( 1 . _ 4 0 ) + ( 8 . _ 1 6 ) ) + ( ; 1 0 . _ 5 3 ) ) |
| 514 | 1 24 181 52 1 182 24 51 51 53 1 73 1 98 130 54 182 51 73 181 98 1 24 73 182 411 67 184 421 429 447 461 513 | dpmul4 | ⊢ ( ( 1 . _ 4 _ 2 7 ) · ( 1 . _ 0 _ 3 9 ) ) < ( 1 . _ 4 _ 8 3 ) |
| 515 | 375 395 | remulcli | ⊢ ( ( 1 . _ 4 _ 2 7 ) · ( 1 . _ 0 _ 3 9 ) ) ∈ ℝ |
| 516 | 345 515 350 | lttri | ⊢ ( ( ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( ( 1 . _ 4 _ 2 7 ) · ( 1 . _ 0 _ 3 9 ) ) ∧ ( ( 1 . _ 4 _ 2 7 ) · ( 1 . _ 0 _ 3 9 ) ) < ( 1 . _ 4 _ 8 3 ) ) → ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( 1 . _ 4 _ 8 3 ) ) |
| 517 | 410 514 516 | mp2an | ⊢ ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( 1 . _ 4 _ 8 3 ) |
| 518 | 367 517 | pm3.2i | ⊢ ( 0 ≤ ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ∧ ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( 1 . _ 4 _ 8 3 ) ) |
| 519 | 351 518 | pm3.2i | ⊢ ( ( ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ∈ ℝ ∧ ( 1 . _ 4 _ 8 3 ) ∈ ℝ ) ∧ ( 0 ≤ ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ∧ ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( 1 . _ 4 _ 8 3 ) ) ) |
| 520 | ltmul12a | ⊢ ( ( ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) ∈ ℝ ∧ ( 1 . _ 6 _ 5 1 ) ∈ ℝ ) ∧ ( 0 ≤ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) ∧ ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) < ( 1 . _ 6 _ 5 1 ) ) ) ∧ ( ( ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ∈ ℝ ∧ ( 1 . _ 4 _ 8 3 ) ∈ ℝ ) ∧ ( 0 ≤ ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ∧ ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) < ( 1 . _ 4 _ 8 3 ) ) ) ) → ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) < ( ( 1 . _ 6 _ 5 1 ) · ( 1 . _ 4 _ 8 3 ) ) ) | |
| 521 | 316 519 520 | mp2an | ⊢ ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) < ( ( 1 . _ 6 _ 5 1 ) · ( 1 . _ 4 _ 8 3 ) ) |
| 522 | 24 181 | deccl | ⊢ ; 4 2 ∈ ℕ0 |
| 523 | 495 24 | deccl | ⊢ ; ; 2 0 4 ∈ ℕ0 |
| 524 | eqid | ⊢ ; ; ; 2 0 4 2 = ; ; ; 2 0 4 2 | |
| 525 | eqid | ⊢ ; 4 2 = ; 4 2 | |
| 526 | eqid | ⊢ ; ; 2 0 4 = ; ; 2 0 4 | |
| 527 | 495 24 24 526 277 | decaddi | ⊢ ( ; ; 2 0 4 + 4 ) = ; ; 2 0 8 |
| 528 | 2p2e4 | ⊢ ( 2 + 2 ) = 4 | |
| 529 | 523 181 24 181 524 525 527 528 | decadd | ⊢ ( ; ; ; 2 0 4 2 + ; 4 2 ) = ; ; ; 2 0 8 4 |
| 530 | 446 | oveq1i | ⊢ ( ( 6 + 4 ) + 2 ) = ( ; 1 0 + 2 ) |
| 531 | dec10p | ⊢ ( ; 1 0 + 2 ) = ; 1 2 | |
| 532 | 530 531 | eqtri | ⊢ ( ( 6 + 4 ) + 2 ) = ; 1 2 |
| 533 | 1 98 1 24 181 1 181 24 116 204 215 216 532 269 | dpmul | ⊢ ( ( 1 . 6 ) · ( 1 . 4 ) ) = ( 2 . _ 2 4 ) |
| 534 | 8t5e40 | ⊢ ( 8 · 5 ) = ; 4 0 | |
| 535 | 158 256 534 | mulcomli | ⊢ ( 5 · 8 ) = ; 4 0 |
| 536 | 5t3e15 | ⊢ ( 5 · 3 ) = ; 1 5 | |
| 537 | 158 | mullidi | ⊢ ( 1 · 8 ) = 8 |
| 538 | 485 | mullidi | ⊢ ( 1 · 3 ) = 3 |
| 539 | 182 | dec0h | ⊢ 3 = ; 0 3 |
| 540 | 538 539 | eqtri | ⊢ ( 1 · 3 ) = ; 0 3 |
| 541 | 235 | nn0cni | ⊢ ; 1 5 ∈ ℂ |
| 542 | 8p5e13 | ⊢ ( 8 + 5 ) = ; 1 3 | |
| 543 | 158 256 542 | addcomli | ⊢ ( 5 + 8 ) = ; 1 3 |
| 544 | 1 54 73 245 269 182 543 | decaddci | ⊢ ( ; 1 5 + 8 ) = ; 2 3 |
| 545 | 541 158 544 | addcomli | ⊢ ( 8 + ; 1 5 ) = ; 2 3 |
| 546 | 545 | oveq1i | ⊢ ( ( 8 + ; 1 5 ) + 0 ) = ( ; 2 3 + 0 ) |
| 547 | 181 182 | deccl | ⊢ ; 2 3 ∈ ℕ0 |
| 548 | 547 | nn0cni | ⊢ ; 2 3 ∈ ℂ |
| 549 | 548 | addridi | ⊢ ( ; 2 3 + 0 ) = ; 2 3 |
| 550 | 546 549 | eqtri | ⊢ ( ( 8 + ; 1 5 ) + 0 ) = ; 2 3 |
| 551 | eqid | ⊢ ; 4 0 = ; 4 0 | |
| 552 | 197 | addlidi | ⊢ ( 0 + 2 ) = 2 |
| 553 | 24 51 181 551 552 | decaddi | ⊢ ( ; 4 0 + 2 ) = ; 4 2 |
| 554 | 54 1 73 182 51 181 182 182 535 536 537 540 550 553 | dpmul | ⊢ ( ( 5 . 1 ) · ( 8 . 3 ) ) = ( ; 4 2 . _ 3 3 ) |
| 555 | 181 181 | deccl | ⊢ ; 2 2 ∈ ℕ0 |
| 556 | 555 24 | deccl | ⊢ ; ; 2 2 4 ∈ ℕ0 |
| 557 | eqid | ⊢ ; ; ; 2 2 4 1 = ; ; ; 2 2 4 1 | |
| 558 | eqid | ⊢ ; ; 2 0 8 = ; ; 2 0 8 | |
| 559 | eqid | ⊢ ; ; 2 2 4 = ; ; 2 2 4 | |
| 560 | eqid | ⊢ ; 2 0 = ; 2 0 | |
| 561 | eqid | ⊢ ; 2 2 = ; 2 2 | |
| 562 | 181 181 181 561 528 | decaddi | ⊢ ( ; 2 2 + 2 ) = ; 2 4 |
| 563 | 555 24 181 51 559 560 562 426 | decadd | ⊢ ( ; ; 2 2 4 + ; 2 0 ) = ; ; 2 4 4 |
| 564 | 556 1 495 73 557 558 563 438 | decadd | ⊢ ( ; ; ; 2 2 4 1 + ; ; 2 0 8 ) = ; ; ; 2 4 4 9 |
| 565 | 555 98 | deccl | ⊢ ; ; 2 2 6 ∈ ℕ0 |
| 566 | 522 182 | deccl | ⊢ ; ; 4 2 3 ∈ ℕ0 |
| 567 | eqid | ⊢ ; ; ; 2 2 6 6 = ; ; ; 2 2 6 6 | |
| 568 | eqid | ⊢ ; ; ; 4 2 3 3 = ; ; ; 4 2 3 3 | |
| 569 | eqid | ⊢ ; ; 2 2 6 = ; ; 2 2 6 | |
| 570 | eqid | ⊢ ; ; 4 2 3 = ; ; 4 2 3 | |
| 571 | 113 197 289 | addcomli | ⊢ ( 2 + 4 ) = 6 |
| 572 | 181 181 24 181 561 525 571 528 | decadd | ⊢ ( ; 2 2 + ; 4 2 ) = ; 6 4 |
| 573 | 555 98 522 182 569 570 572 233 | decadd | ⊢ ( ; ; 2 2 6 + ; ; 4 2 3 ) = ; ; 6 4 9 |
| 574 | 565 98 566 182 567 568 573 233 | decadd | ⊢ ( ; ; ; 2 2 6 6 + ; ; ; 4 2 3 3 ) = ; ; ; 6 4 9 9 |
| 575 | 555 98 98 522 182 100 182 53 53 574 | dpadd3 | ⊢ ( ( ; 2 2 . _ 6 6 ) + ( ; 4 2 . _ 3 3 ) ) = ( ; 6 4 . _ 9 9 ) |
| 576 | 495 | nn0cni | ⊢ ; 2 0 ∈ ℂ |
| 577 | 181 51 181 560 552 | decaddi | ⊢ ( ; 2 0 + 2 ) = ; 2 2 |
| 578 | 576 197 577 | addcomli | ⊢ ( 2 + ; 2 0 ) = ; 2 2 |
| 579 | 181 181 495 24 561 526 578 571 | decadd | ⊢ ( ; 2 2 + ; ; 2 0 4 ) = ; ; 2 2 6 |
| 580 | 555 24 523 181 559 524 579 289 | decadd | ⊢ ( ; ; 2 2 4 + ; ; ; 2 0 4 2 ) = ; ; ; 2 2 6 6 |
| 581 | 181 181 24 495 24 555 181 98 98 580 | dpadd3 | ⊢ ( ( 2 . _ 2 4 ) + ( ; 2 0 . _ 4 2 ) ) = ( ; 2 2 . _ 6 6 ) |
| 582 | 581 | oveq1i | ⊢ ( ( ( 2 . _ 2 4 ) + ( ; 2 0 . _ 4 2 ) ) + ( ; 4 2 . _ 3 3 ) ) = ( ( ; 2 2 . _ 6 6 ) + ( ; 4 2 . _ 3 3 ) ) |
| 583 | eqid | ⊢ ; 5 1 = ; 5 1 | |
| 584 | 1 98 54 1 135 583 257 140 | decadd | ⊢ ( ; 1 6 + ; 5 1 ) = ; 6 7 |
| 585 | 1 98 54 1 98 52 584 | dpadd | ⊢ ( ( 1 . 6 ) + ( 5 . 1 ) ) = ( 6 . 7 ) |
| 586 | eqid | ⊢ ; 8 3 = ; 8 3 | |
| 587 | 1 24 73 182 268 586 438 302 | decadd | ⊢ ( ; 1 4 + ; 8 3 ) = ; 9 7 |
| 588 | 1 24 73 182 53 52 587 | dpadd | ⊢ ( ( 1 . 4 ) + ( 8 . 3 ) ) = ( 9 . 7 ) |
| 589 | 585 588 | oveq12i | ⊢ ( ( ( 1 . 6 ) + ( 5 . 1 ) ) · ( ( 1 . 4 ) + ( 8 . 3 ) ) ) = ( ( 6 . 7 ) · ( 9 . 7 ) ) |
| 590 | 9t6e54 | ⊢ ( 9 · 6 ) = ; 5 4 | |
| 591 | 196 110 590 | mulcomli | ⊢ ( 6 · 9 ) = ; 5 4 |
| 592 | 7t6e42 | ⊢ ( 7 · 6 ) = ; 4 2 | |
| 593 | 217 110 592 | mulcomli | ⊢ ( 6 · 7 ) = ; 4 2 |
| 594 | 7t7e49 | ⊢ ( 7 · 7 ) = ; 4 9 | |
| 595 | eqid | ⊢ ; 6 3 = ; 6 3 | |
| 596 | 3p2e5 | ⊢ ( 3 + 2 ) = 5 | |
| 597 | 98 182 24 181 595 525 446 596 | decadd | ⊢ ( ; 6 3 + ; 4 2 ) = ; ; 1 0 5 |
| 598 | 597 | oveq1i | ⊢ ( ( ; 6 3 + ; 4 2 ) + 4 ) = ( ; ; 1 0 5 + 4 ) |
| 599 | 5p4e9 | ⊢ ( 5 + 4 ) = 9 | |
| 600 | 130 54 24 501 599 | decaddi | ⊢ ( ; ; 1 0 5 + 4 ) = ; ; 1 0 9 |
| 601 | 598 600 | eqtri | ⊢ ( ( ; 6 3 + ; 4 2 ) + 4 ) = ; ; 1 0 9 |
| 602 | eqid | ⊢ ; 5 4 = ; 5 4 | |
| 603 | 54 24 1 51 602 414 246 426 | decadd | ⊢ ( ; 5 4 + ; 1 0 ) = ; 6 4 |
| 604 | 98 52 53 52 24 130 53 53 591 593 435 594 601 603 | dpmul | ⊢ ( ( 6 . 7 ) · ( 9 . 7 ) ) = ( ; 6 4 . _ 9 9 ) |
| 605 | 589 604 | eqtri | ⊢ ( ( ( 1 . 6 ) + ( 5 . 1 ) ) · ( ( 1 . 4 ) + ( 8 . 3 ) ) ) = ( ; 6 4 . _ 9 9 ) |
| 606 | 575 582 605 | 3eqtr4ri | ⊢ ( ( ( 1 . 6 ) + ( 5 . 1 ) ) · ( ( 1 . 4 ) + ( 8 . 3 ) ) ) = ( ( ( 2 . _ 2 4 ) + ( ; 2 0 . _ 4 2 ) ) + ( ; 4 2 . _ 3 3 ) ) |
| 607 | 1 98 54 1 1 73 181 24 24 182 181 495 24 181 522 182 182 181 51 73 24 181 24 24 53 101 184 184 529 533 554 564 606 | dpmul4 | ⊢ ( ( 1 . _ 6 _ 5 1 ) · ( 1 . _ 4 _ 8 3 ) ) < ( 2 . _ 4 _ 4 9 ) |
| 608 | 33 345 | remulcli | ⊢ ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ∈ ℝ |
| 609 | 43 350 | remulcli | ⊢ ( ( 1 . _ 6 _ 5 1 ) · ( 1 . _ 4 _ 8 3 ) ) ∈ ℝ |
| 610 | 24 399 | rpdp2cl | ⊢ _ 4 9 ∈ ℝ+ |
| 611 | 24 610 | rpdp2cl | ⊢ _ 4 _ 4 9 ∈ ℝ+ |
| 612 | 181 611 | rpdpcl | ⊢ ( 2 . _ 4 _ 4 9 ) ∈ ℝ+ |
| 613 | rpre | ⊢ ( ( 2 . _ 4 _ 4 9 ) ∈ ℝ+ → ( 2 . _ 4 _ 4 9 ) ∈ ℝ ) | |
| 614 | 612 613 | ax-mp | ⊢ ( 2 . _ 4 _ 4 9 ) ∈ ℝ |
| 615 | 608 609 614 | lttri | ⊢ ( ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) < ( ( 1 . _ 6 _ 5 1 ) · ( 1 . _ 4 _ 8 3 ) ) ∧ ( ( 1 . _ 6 _ 5 1 ) · ( 1 . _ 4 _ 8 3 ) ) < ( 2 . _ 4 _ 4 9 ) ) → ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) < ( 2 . _ 4 _ 4 9 ) ) |
| 616 | 521 607 615 | mp2an | ⊢ ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) < ( 2 . _ 4 _ 4 9 ) |
| 617 | 3pos | ⊢ 0 < 3 | |
| 618 | 608 614 319 | ltmul2i | ⊢ ( 0 < 3 → ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) < ( 2 . _ 4 _ 4 9 ) ↔ ( 3 · ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) < ( 3 · ( 2 . _ 4 _ 4 9 ) ) ) ) |
| 619 | 617 618 | ax-mp | ⊢ ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) < ( 2 . _ 4 _ 4 9 ) ↔ ( 3 · ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) < ( 3 · ( 2 . _ 4 _ 4 9 ) ) ) |
| 620 | 616 619 | mpbi | ⊢ ( 3 · ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) < ( 3 · ( 2 . _ 4 _ 4 9 ) ) |
| 621 | 119 | dp2eq2i | ⊢ _ 0 _ 0 0 = _ 0 0 |
| 622 | 621 119 | eqtri | ⊢ _ 0 _ 0 0 = 0 |
| 623 | 622 | oveq2i | ⊢ ( 3 . _ 0 _ 0 0 ) = ( 3 . 0 ) |
| 624 | 182 | dp0u | ⊢ ( 3 . 0 ) = 3 |
| 625 | 623 624 | eqtr2i | ⊢ 3 = ( 3 . _ 0 _ 0 0 ) |
| 626 | 625 | oveq1i | ⊢ ( 3 · ( 2 . _ 4 _ 4 9 ) ) = ( ( 3 . _ 0 _ 0 0 ) · ( 2 . _ 4 _ 4 9 ) ) |
| 627 | 448 52 | deccl | ⊢ ; ; 1 4 7 ∈ ℕ0 |
| 628 | 627 51 | deccl | ⊢ ; ; ; 1 4 7 0 ∈ ℕ0 |
| 629 | 628 | nn0cni | ⊢ ; ; ; 1 4 7 0 ∈ ℂ |
| 630 | 629 | addridi | ⊢ ( ; ; ; 1 4 7 0 + 0 ) = ; ; ; 1 4 7 0 |
| 631 | 3t2e6 | ⊢ ( 3 · 2 ) = 6 | |
| 632 | 4t3e12 | ⊢ ( 4 · 3 ) = ; 1 2 | |
| 633 | 113 485 632 | mulcomli | ⊢ ( 3 · 4 ) = ; 1 2 |
| 634 | 197 | mul02i | ⊢ ( 0 · 2 ) = 0 |
| 635 | 113 455 425 | mulcomli | ⊢ ( 0 · 4 ) = ; 0 0 |
| 636 | 51 51 1 181 424 300 153 552 | decadd | ⊢ ( 0 + ; 1 2 ) = ; 1 2 |
| 637 | 636 | oveq1i | ⊢ ( ( 0 + ; 1 2 ) + 0 ) = ( ; 1 2 + 0 ) |
| 638 | 281 | nn0cni | ⊢ ; 1 2 ∈ ℂ |
| 639 | 638 | addridi | ⊢ ( ; 1 2 + 0 ) = ; 1 2 |
| 640 | 637 639 | eqtri | ⊢ ( ( 0 + ; 1 2 ) + 0 ) = ; 1 2 |
| 641 | 182 51 181 24 51 1 181 51 631 633 634 635 640 140 | dpmul | ⊢ ( ( 3 . 0 ) · ( 2 . 4 ) ) = ( 7 . _ 2 0 ) |
| 642 | 51 | dp0u | ⊢ ( 0 . 0 ) = 0 |
| 643 | 642 | oveq1i | ⊢ ( ( 0 . 0 ) · ( 4 . 9 ) ) = ( 0 · ( 4 . 9 ) ) |
| 644 | dpcl | ⊢ ( ( 4 ∈ ℕ0 ∧ 9 ∈ ℝ ) → ( 4 . 9 ) ∈ ℝ ) | |
| 645 | 24 4 644 | mp2an | ⊢ ( 4 . 9 ) ∈ ℝ |
| 646 | 645 | recni | ⊢ ( 4 . 9 ) ∈ ℂ |
| 647 | 646 | mul02i | ⊢ ( 0 · ( 4 . 9 ) ) = 0 |
| 648 | 643 647 | eqtri | ⊢ ( ( 0 . 0 ) · ( 4 . 9 ) ) = 0 |
| 649 | 119 | oveq2i | ⊢ ( 0 . _ 0 0 ) = ( 0 . 0 ) |
| 650 | 649 642 | eqtri | ⊢ ( 0 . _ 0 0 ) = 0 |
| 651 | 648 650 | eqtr4i | ⊢ ( ( 0 . 0 ) · ( 4 . 9 ) ) = ( 0 . _ 0 0 ) |
| 652 | 52 181 | deccl | ⊢ ; 7 2 ∈ ℕ0 |
| 653 | 652 51 | deccl | ⊢ ; ; 7 2 0 ∈ ℕ0 |
| 654 | eqid | ⊢ ; ; ; 7 2 0 1 = ; ; ; 7 2 0 1 | |
| 655 | eqid | ⊢ ; ; 1 4 7 = ; ; 1 4 7 | |
| 656 | eqid | ⊢ ; ; 7 2 0 = ; ; 7 2 0 | |
| 657 | 52 181 224 263 | decsuc | ⊢ ( ; 7 2 + 1 ) = ; 7 3 |
| 658 | 652 51 1 24 656 268 657 114 | decadd | ⊢ ( ; ; 7 2 0 + ; 1 4 ) = ; ; 7 3 4 |
| 659 | 653 1 448 52 654 655 658 274 | decadd | ⊢ ( ; ; ; 7 2 0 1 + ; ; 1 4 7 ) = ; ; ; 7 3 4 8 |
| 660 | 642 | oveq2i | ⊢ ( ( 3 . 0 ) + ( 0 . 0 ) ) = ( ( 3 . 0 ) + 0 ) |
| 661 | 624 485 | eqeltri | ⊢ ( 3 . 0 ) ∈ ℂ |
| 662 | 661 | addridi | ⊢ ( ( 3 . 0 ) + 0 ) = ( 3 . 0 ) |
| 663 | 660 662 | eqtri | ⊢ ( ( 3 . 0 ) + ( 0 . 0 ) ) = ( 3 . 0 ) |
| 664 | eqid | ⊢ ; 4 9 = ; 4 9 | |
| 665 | 571 | oveq1i | ⊢ ( ( 2 + 4 ) + 1 ) = ( 6 + 1 ) |
| 666 | 665 140 | eqtri | ⊢ ( ( 2 + 4 ) + 1 ) = 7 |
| 667 | 9p4e13 | ⊢ ( 9 + 4 ) = ; 1 3 | |
| 668 | 196 113 667 | addcomli | ⊢ ( 4 + 9 ) = ; 1 3 |
| 669 | 181 24 24 53 223 664 666 182 668 | decaddc | ⊢ ( ; 2 4 + ; 4 9 ) = ; 7 3 |
| 670 | 181 24 24 53 52 182 669 | dpadd | ⊢ ( ( 2 . 4 ) + ( 4 . 9 ) ) = ( 7 . 3 ) |
| 671 | 663 670 | oveq12i | ⊢ ( ( ( 3 . 0 ) + ( 0 . 0 ) ) · ( ( 2 . 4 ) + ( 4 . 9 ) ) ) = ( ( 3 . 0 ) · ( 7 . 3 ) ) |
| 672 | 217 485 433 | mulcomli | ⊢ ( 3 · 7 ) = ; 2 1 |
| 673 | 3t3e9 | ⊢ ( 3 · 3 ) = 9 | |
| 674 | 217 | mul01i | ⊢ ( 7 · 0 ) = 0 |
| 675 | 217 455 674 | mulcomli | ⊢ ( 0 · 7 ) = 0 |
| 676 | 485 | mul01i | ⊢ ( 3 · 0 ) = 0 |
| 677 | 676 424 | eqtri | ⊢ ( 3 · 0 ) = ; 0 0 |
| 678 | 485 455 677 | mulcomli | ⊢ ( 0 · 3 ) = ; 0 0 |
| 679 | 196 | addridi | ⊢ ( 9 + 0 ) = 9 |
| 680 | 679 | oveq1i | ⊢ ( ( 9 + 0 ) + 0 ) = ( 9 + 0 ) |
| 681 | 680 679 188 | 3eqtri | ⊢ ( ( 9 + 0 ) + 0 ) = ; 0 9 |
| 682 | 196 455 | addcomi | ⊢ ( 9 + 0 ) = ( 0 + 9 ) |
| 683 | 682 | oveq1i | ⊢ ( ( 9 + 0 ) + 0 ) = ( ( 0 + 9 ) + 0 ) |
| 684 | 683 | eqeq1i | ⊢ ( ( ( 9 + 0 ) + 0 ) = ; 0 9 ↔ ( ( 0 + 9 ) + 0 ) = ; 0 9 ) |
| 685 | 681 684 | mpbi | ⊢ ( ( 0 + 9 ) + 0 ) = ; 0 9 |
| 686 | 181 1 51 436 192 | decaddi | ⊢ ( ; 2 1 + 0 ) = ; 2 1 |
| 687 | 182 51 52 182 51 51 53 51 672 673 675 678 685 686 | dpmul | ⊢ ( ( 3 . 0 ) · ( 7 . 3 ) ) = ( ; 2 1 . _ 9 0 ) |
| 688 | 671 687 | eqtri | ⊢ ( ( ( 3 . 0 ) + ( 0 . 0 ) ) · ( ( 2 . 4 ) + ( 4 . 9 ) ) ) = ( ; 2 1 . _ 9 0 ) |
| 689 | 650 | oveq2i | ⊢ ( ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) ) + ( 0 . _ 0 0 ) ) = ( ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) ) + 0 ) |
| 690 | 318 2 | pm3.2i | ⊢ ( 2 ∈ ℝ ∧ 0 ∈ ℝ ) |
| 691 | dp2cl | ⊢ ( ( 2 ∈ ℝ ∧ 0 ∈ ℝ ) → _ 2 0 ∈ ℝ ) | |
| 692 | 690 691 | ax-mp | ⊢ _ 2 0 ∈ ℝ |
| 693 | dpcl | ⊢ ( ( 7 ∈ ℕ0 ∧ _ 2 0 ∈ ℝ ) → ( 7 . _ 2 0 ) ∈ ℝ ) | |
| 694 | 52 692 693 | mp2an | ⊢ ( 7 . _ 2 0 ) ∈ ℝ |
| 695 | 694 | recni | ⊢ ( 7 . _ 2 0 ) ∈ ℂ |
| 696 | 3 2 | pm3.2i | ⊢ ( 7 ∈ ℝ ∧ 0 ∈ ℝ ) |
| 697 | dp2cl | ⊢ ( ( 7 ∈ ℝ ∧ 0 ∈ ℝ ) → _ 7 0 ∈ ℝ ) | |
| 698 | 696 697 | ax-mp | ⊢ _ 7 0 ∈ ℝ |
| 699 | dpcl | ⊢ ( ( ; 1 4 ∈ ℕ0 ∧ _ 7 0 ∈ ℝ ) → ( ; 1 4 . _ 7 0 ) ∈ ℝ ) | |
| 700 | 448 698 699 | mp2an | ⊢ ( ; 1 4 . _ 7 0 ) ∈ ℝ |
| 701 | 700 | recni | ⊢ ( ; 1 4 . _ 7 0 ) ∈ ℂ |
| 702 | 695 701 | addcli | ⊢ ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) ) ∈ ℂ |
| 703 | 702 | addridi | ⊢ ( ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) ) + 0 ) = ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) ) |
| 704 | eqid | ⊢ ; ; ; 1 4 7 0 = ; ; ; 1 4 7 0 | |
| 705 | 448 | nn0cni | ⊢ ; 1 4 ∈ ℂ |
| 706 | 705 217 270 | addcomli | ⊢ ( 7 + ; 1 4 ) = ; 2 1 |
| 707 | 7p2e9 | ⊢ ( 7 + 2 ) = 9 | |
| 708 | 217 197 707 | addcomli | ⊢ ( 2 + 7 ) = 9 |
| 709 | 52 181 448 52 263 655 706 708 | decadd | ⊢ ( ; 7 2 + ; ; 1 4 7 ) = ; ; 2 1 9 |
| 710 | 00id | ⊢ ( 0 + 0 ) = 0 | |
| 711 | 652 51 627 51 656 704 709 710 | decadd | ⊢ ( ; ; 7 2 0 + ; ; ; 1 4 7 0 ) = ; ; ; 2 1 9 0 |
| 712 | 52 181 51 448 52 293 51 53 51 711 | dpadd3 | ⊢ ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) ) = ( ; 2 1 . _ 9 0 ) |
| 713 | 689 703 712 | 3eqtri | ⊢ ( ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) ) + ( 0 . _ 0 0 ) ) = ( ; 2 1 . _ 9 0 ) |
| 714 | 688 713 | eqtr4i | ⊢ ( ( ( 3 . 0 ) + ( 0 . 0 ) ) · ( ( 2 . 4 ) + ( 4 . 9 ) ) ) = ( ( ( 7 . _ 2 0 ) + ( ; 1 4 . _ 7 0 ) ) + ( 0 . _ 0 0 ) ) |
| 715 | 182 51 51 51 181 24 181 51 24 53 52 448 52 51 51 51 51 1 24 52 51 52 182 24 73 102 102 102 630 641 651 659 714 | dpmul4 | ⊢ ( ( 3 . _ 0 _ 0 0 ) · ( 2 . _ 4 _ 4 9 ) ) < ( 7 . _ 3 _ 4 8 ) |
| 716 | 626 715 | eqbrtri | ⊢ ( 3 · ( 2 . _ 4 _ 4 9 ) ) < ( 7 . _ 3 _ 4 8 ) |
| 717 | 319 608 | remulcli | ⊢ ( 3 · ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) ∈ ℝ |
| 718 | 319 614 | remulcli | ⊢ ( 3 · ( 2 . _ 4 _ 4 9 ) ) ∈ ℝ |
| 719 | nnrp | ⊢ ( 8 ∈ ℕ → 8 ∈ ℝ+ ) | |
| 720 | 63 719 | ax-mp | ⊢ 8 ∈ ℝ+ |
| 721 | 24 720 | rpdp2cl | ⊢ _ 4 8 ∈ ℝ+ |
| 722 | 182 721 | rpdp2cl | ⊢ _ 3 _ 4 8 ∈ ℝ+ |
| 723 | 52 722 | rpdpcl | ⊢ ( 7 . _ 3 _ 4 8 ) ∈ ℝ+ |
| 724 | rpre | ⊢ ( ( 7 . _ 3 _ 4 8 ) ∈ ℝ+ → ( 7 . _ 3 _ 4 8 ) ∈ ℝ ) | |
| 725 | 723 724 | ax-mp | ⊢ ( 7 . _ 3 _ 4 8 ) ∈ ℝ |
| 726 | 717 718 725 | lttri | ⊢ ( ( ( 3 · ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) < ( 3 · ( 2 . _ 4 _ 4 9 ) ) ∧ ( 3 · ( 2 . _ 4 _ 4 9 ) ) < ( 7 . _ 3 _ 4 8 ) ) → ( 3 · ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) < ( 7 . _ 3 _ 4 8 ) ) |
| 727 | 620 716 726 | mp2an | ⊢ ( 3 · ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ↑ 2 ) · ( 1 . _ 4 _ 1 4 ) ) · ( ( 1 . _ 4 _ 2 _ 6 3 ) · ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) < ( 7 . _ 3 _ 4 8 ) |