Metamath Proof Explorer

Theorem mulgt1

Description: The product of two numbers greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005)

Ref Expression
Assertion mulgt1 ⊢A∈ℝ∧B∈ℝ∧1<A∧1<B→1<A⁢B

Proof

Step Hyp Ref Expression
1 simpl ⊢1<A∧1<B→1<A
2 1 a1i ⊢A∈ℝ∧B∈ℝ→1<A∧1<B→1<A
3 0lt1 ⊢0<1
4 0re ⊢0∈ℝ
5 1re ⊢1∈ℝ
6 lttr ⊢0∈ℝ∧1∈ℝ∧A∈ℝ→0<1∧1<A→0<A
7 4 5 6 mp3an12 ⊢A∈ℝ→0<1∧1<A→0<A
8 3 7 mpani ⊢A∈ℝ→1<A→0<A
9 8 adantr ⊢A∈ℝ∧B∈ℝ→1<A→0<A
10 ltmul2 ⊢1∈ℝ∧B∈ℝ∧A∈ℝ∧0<A→1<B↔A⋅1<A⁢B
11 10 biimpd ⊢1∈ℝ∧B∈ℝ∧A∈ℝ∧0<A→1<B→A⋅1<A⁢B
12 5 11 mp3an1 ⊢B∈ℝ∧A∈ℝ∧0<A→1<B→A⋅1<A⁢B
13 12 exp32 ⊢B∈ℝ→A∈ℝ→0<A→1<B→A⋅1<A⁢B
14 13 impcom ⊢A∈ℝ∧B∈ℝ→0<A→1<B→A⋅1<A⁢B
15 9 14 syld ⊢A∈ℝ∧B∈ℝ→1<A→1<B→A⋅1<A⁢B
16 15 impd ⊢A∈ℝ∧B∈ℝ→1<A∧1<B→A⋅1<A⁢B
17 ax-1rid ⊢A∈ℝ→A⋅1=A
18 17 adantr ⊢A∈ℝ∧B∈ℝ→A⋅1=A
19 18 breq1d ⊢A∈ℝ∧B∈ℝ→A⋅1<A⁢B↔A<A⁢B
20 16 19 sylibd ⊢A∈ℝ∧B∈ℝ→1<A∧1<B→A<A⁢B
21 2 20 jcad ⊢A∈ℝ∧B∈ℝ→1<A∧1<B→1<A∧A<A⁢B
22 remulcl ⊢A∈ℝ∧B∈ℝ→A⁢B∈ℝ
23 lttr ⊢1∈ℝ∧A∈ℝ∧A⁢B∈ℝ→1<A∧A<A⁢B→1<A⁢B
24 5 23 mp3an1 ⊢A∈ℝ∧A⁢B∈ℝ→1<A∧A<A⁢B→1<A⁢B
25 22 24 syldan ⊢A∈ℝ∧B∈ℝ→1<A∧A<A⁢B→1<A⁢B
26 21 25 syld ⊢A∈ℝ∧B∈ℝ→1<A∧1<B→1<A⁢B
27 26 imp ⊢A∈ℝ∧B∈ℝ∧1<A∧1<B→1<A⁢B