Theorem addltmulALT

Description: A proof readability experiment for addltmul . (Contributed by Stefan Allan, 30-Oct-2010) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	addltmulALT	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 2 < 𝐴 ∧ 2 < 𝐵 ) ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → 2 < 𝐴 )
2		2re	⊢ 2 ∈ ℝ
3	2	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → 2 ∈ ℝ )
4		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → 𝐴 ∈ ℝ )
5		1re	⊢ 1 ∈ ℝ
6	5	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → 1 ∈ ℝ )
7		ltsub1	⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 2 < 𝐴 ↔ ( 2 − 1 ) < ( 𝐴 − 1 ) ) )
8	3 4 6 7	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → ( 2 < 𝐴 ↔ ( 2 − 1 ) < ( 𝐴 − 1 ) ) )
9		2cn	⊢ 2 ∈ ℂ
10		ax-1cn	⊢ 1 ∈ ℂ
11		df-2	⊢ 2 = ( 1 + 1 )
12	11	eqcomi	⊢ ( 1 + 1 ) = 2
13	9 10 10 12	subaddrii	⊢ ( 2 − 1 ) = 1
14	13	breq1i	⊢ ( ( 2 − 1 ) < ( 𝐴 − 1 ) ↔ 1 < ( 𝐴 − 1 ) )
15	14	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → ( ( 2 − 1 ) < ( 𝐴 − 1 ) ↔ 1 < ( 𝐴 − 1 ) ) )
16	8 15	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → ( 2 < 𝐴 ↔ 1 < ( 𝐴 − 1 ) ) )
17	1 16	mpbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) → 1 < ( 𝐴 − 1 ) )
18		simpr	⊢ ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → 2 < 𝐵 )
19	2	a1i	⊢ ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → 2 ∈ ℝ )
20		simpl	⊢ ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → 𝐵 ∈ ℝ )
21	5	a1i	⊢ ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → 1 ∈ ℝ )
22		ltsub1	⊢ ( ( 2 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 2 < 𝐵 ↔ ( 2 − 1 ) < ( 𝐵 − 1 ) ) )
23	19 20 21 22	syl3anc	⊢ ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → ( 2 < 𝐵 ↔ ( 2 − 1 ) < ( 𝐵 − 1 ) ) )
24	13	breq1i	⊢ ( ( 2 − 1 ) < ( 𝐵 − 1 ) ↔ 1 < ( 𝐵 − 1 ) )
25	24	a1i	⊢ ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → ( ( 2 − 1 ) < ( 𝐵 − 1 ) ↔ 1 < ( 𝐵 − 1 ) ) )
26	23 25	bitrd	⊢ ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → ( 2 < 𝐵 ↔ 1 < ( 𝐵 − 1 ) ) )
27	18 26	mpbid	⊢ ( ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) → 1 < ( 𝐵 − 1 ) )
28	17 27	anim12i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 2 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 2 < 𝐵 ) ) → ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) )
29	28	an4s	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 2 < 𝐴 ∧ 2 < 𝐵 ) ) → ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) )
30		peano2rem	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − 1 ) ∈ ℝ )
31		peano2rem	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 − 1 ) ∈ ℝ )
32	30 31	anim12i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 − 1 ) ∈ ℝ ∧ ( 𝐵 − 1 ) ∈ ℝ ) )
33	32	anim1i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) ) → ( ( ( 𝐴 − 1 ) ∈ ℝ ∧ ( 𝐵 − 1 ) ∈ ℝ ) ∧ ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) ) )
34		mulgt1	⊢ ( ( ( ( 𝐴 − 1 ) ∈ ℝ ∧ ( 𝐵 − 1 ) ∈ ℝ ) ∧ ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) ) → 1 < ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) )
35	33 34	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) ) → 1 < ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) )
36	35	ex	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) → 1 < ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) ) )
37	36	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 2 < 𝐴 ∧ 2 < 𝐵 ) ) → ( ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) → 1 < ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) ) )
38		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
39	10	a1i	⊢ ( 𝐴 ∈ ℝ → 1 ∈ ℂ )
40	38 39	jca	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) )
41		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
42	10	a1i	⊢ ( 𝐵 ∈ ℝ → 1 ∈ ℂ )
43	41 42	jca	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 ∈ ℂ ∧ 1 ∈ ℂ ) )
44	40 43	anim12i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 1 ∈ ℂ ) ) )
45		mulsub	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 1 ∈ ℂ ) ) → ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) = ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) )
46	44 45	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) = ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) )
47	46	breq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 < ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) ↔ 1 < ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) ) )
48	47	biimpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 < ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) → 1 < ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) ) )
49	48	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 2 < 𝐴 ∧ 2 < 𝐵 ) ) → ( 1 < ( ( 𝐴 − 1 ) · ( 𝐵 − 1 ) ) → 1 < ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) ) )
50	10	mullidi	⊢ ( 1 · 1 ) = 1
51		eqcom	⊢ ( ( 1 · 1 ) = 1 ↔ 1 = ( 1 · 1 ) )
52	51	biimpi	⊢ ( ( 1 · 1 ) = 1 → 1 = ( 1 · 1 ) )
53	50 52	mp1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 1 = ( 1 · 1 ) )
54	53	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 · 𝐵 ) + 1 ) = ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) )
55		mulrid	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )
56		eqcom	⊢ ( ( 𝐴 · 1 ) = 𝐴 ↔ 𝐴 = ( 𝐴 · 1 ) )
57	56	biimpi	⊢ ( ( 𝐴 · 1 ) = 𝐴 → 𝐴 = ( 𝐴 · 1 ) )
58	55 57	syl	⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( 𝐴 · 1 ) )
59	38 58	syl	⊢ ( 𝐴 ∈ ℝ → 𝐴 = ( 𝐴 · 1 ) )
60	59	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 = ( 𝐴 · 1 ) )
61		mulrid	⊢ ( 𝐵 ∈ ℂ → ( 𝐵 · 1 ) = 𝐵 )
62	41 61	syl	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 · 1 ) = 𝐵 )
63		eqcom	⊢ ( ( 𝐵 · 1 ) = 𝐵 ↔ 𝐵 = ( 𝐵 · 1 ) )
64	63	biimpi	⊢ ( ( 𝐵 · 1 ) = 𝐵 → 𝐵 = ( 𝐵 · 1 ) )
65	62 64	syl	⊢ ( 𝐵 ∈ ℝ → 𝐵 = ( 𝐵 · 1 ) )
66	65	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 = ( 𝐵 · 1 ) )
67	60 66	oveq12d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) = ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) )
68	54 67	oveq12d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 · 𝐵 ) + 1 ) − ( 𝐴 + 𝐵 ) ) = ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) )
69	68	breq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 < ( ( ( 𝐴 · 𝐵 ) + 1 ) − ( 𝐴 + 𝐵 ) ) ↔ 1 < ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) ) )
70		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
71	5	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 1 ∈ ℝ )
72		remulcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
73		readdcl	⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝐴 · 𝐵 ) + 1 ) ∈ ℝ )
74	72 71 73	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 · 𝐵 ) + 1 ) ∈ ℝ )
75		ltaddsub2	⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 𝐴 · 𝐵 ) + 1 ) ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) + 1 ) < ( ( 𝐴 · 𝐵 ) + 1 ) ↔ 1 < ( ( ( 𝐴 · 𝐵 ) + 1 ) − ( 𝐴 + 𝐵 ) ) ) )
76	70 71 74 75	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) + 1 ) < ( ( 𝐴 · 𝐵 ) + 1 ) ↔ 1 < ( ( ( 𝐴 · 𝐵 ) + 1 ) − ( 𝐴 + 𝐵 ) ) ) )
77		ltadd1	⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ ( 𝐴 · 𝐵 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ↔ ( ( 𝐴 + 𝐵 ) + 1 ) < ( ( 𝐴 · 𝐵 ) + 1 ) ) )
78	70 72 71 77	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ↔ ( ( 𝐴 + 𝐵 ) + 1 ) < ( ( 𝐴 · 𝐵 ) + 1 ) ) )
79	78	bicomd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) + 1 ) < ( ( 𝐴 · 𝐵 ) + 1 ) ↔ ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ) )
80	79	biimpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) + 1 ) < ( ( 𝐴 · 𝐵 ) + 1 ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ) )
81	76 80	sylbird	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 < ( ( ( 𝐴 · 𝐵 ) + 1 ) − ( 𝐴 + 𝐵 ) ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ) )
82	69 81	sylbird	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 1 < ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ) )
83	82	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 2 < 𝐴 ∧ 2 < 𝐵 ) ) → ( 1 < ( ( ( 𝐴 · 𝐵 ) + ( 1 · 1 ) ) − ( ( 𝐴 · 1 ) + ( 𝐵 · 1 ) ) ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ) )
84	37 49 83	3syld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 2 < 𝐴 ∧ 2 < 𝐵 ) ) → ( ( 1 < ( 𝐴 − 1 ) ∧ 1 < ( 𝐵 − 1 ) ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) ) )
85	29 84	mpd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 2 < 𝐴 ∧ 2 < 𝐵 ) ) → ( 𝐴 + 𝐵 ) < ( 𝐴 · 𝐵 ) )