Theorem xlt2add 11481

Description: Extended real version of lt2add 10062. Note that ltleadd 10060, which has weaker assumptions, is not true for the extended reals (since 01 fails). (Contributed by Mario Carneiro, 23-Aug-2015.)

Assertion

Ref	Expression
xlt2add

Proof of Theorem xlt2add

Step	Hyp	Ref	Expression
1		xaddcl 11465	. . . . . . . 8
2	1	3ad2ant1 1017	. . . . . . 7
3	2	adantr 465	. . . . . 6
4		simp1l 1020	. . . . . . . 8
5		simp2r 1023	. . . . . . . 8
6		xaddcl 11465	. . . . . . . 8
7	4, 5, 6	syl2anc 661	. . . . . . 7
8	7	adantr 465	. . . . . 6
9		xaddcl 11465	. . . . . . . 8
10	9	3ad2ant2 1018	. . . . . . 7
11	10	adantr 465	. . . . . 6
12		simp3r 1025	. . . . . . . 8
13	12	adantr 465	. . . . . . 7
14		simp1r 1021	. . . . . . . . 9
15	14	adantr 465	. . . . . . . 8
16	5	adantr 465	. . . . . . . 8
17		simprl 756	. . . . . . . 8
18		xltadd2 11478	. . . . . . . 8
19	15, 16, 17, 18	syl3anc 1228	. . . . . . 7
20	13, 19	mpbid 210	. . . . . 6
21		simp3l 1024	. . . . . . . 8
22	21	adantr 465	. . . . . . 7
23	4	adantr 465	. . . . . . . 8
24		simp2l 1022	. . . . . . . . 9
25	24	adantr 465	. . . . . . . 8
26		simprr 757	. . . . . . . 8
27		xltadd1 11477	. . . . . . . 8
28	23, 25, 26, 27	syl3anc 1228	. . . . . . 7
29	22, 28	mpbid 210	. . . . . 6
30	3, 8, 11, 20, 29	xrlttrd 11391	. . . . 5
31	30	anassrs 648	. . . 4
32		pnfxr 11350	. . . . . . . . . . . 12
33	32	a1i 11	. . . . . . . . . . 11
34		pnfge 11368	. . . . . . . . . . . 12
35	24, 34	syl 16	. . . . . . . . . . 11
36	4, 24, 33, 21, 35	xrltletrd 11393	. . . . . . . . . 10
37		nltpnft 11396	. . . . . . . . . . . 12
38	37	necon2abid 2711	. . . . . . . . . . 11
39	4, 38	syl 16	. . . . . . . . . 10
40	36, 39	mpbid 210	. . . . . . . . 9
41		pnfge 11368	. . . . . . . . . . . 12
42	5, 41	syl 16	. . . . . . . . . . 11
43	14, 5, 33, 12, 42	xrltletrd 11393	. . . . . . . . . 10
44		nltpnft 11396	. . . . . . . . . . . 12
45	44	necon2abid 2711	. . . . . . . . . . 11
46	14, 45	syl 16	. . . . . . . . . 10
47	43, 46	mpbid 210	. . . . . . . . 9
48		xaddnepnf 11463	. . . . . . . . 9
49	4, 40, 14, 47, 48	syl22anc 1229	. . . . . . . 8
50		nltpnft 11396	. . . . . . . . . 10
51	50	necon2abid 2711	. . . . . . . . 9
52	2, 51	syl 16	. . . . . . . 8
53	49, 52	mpbird 232	. . . . . . 7
54	53	adantr 465	. . . . . 6
55		oveq2 6304	. . . . . . 7
56		mnfxr 11352	. . . . . . . . . . 11
57	56	a1i 11	. . . . . . . . . 10
58		mnfle 11371	. . . . . . . . . . 11
59	4, 58	syl 16	. . . . . . . . . 10
60	57, 4, 24, 59, 21	xrlelttrd 11392	. . . . . . . . 9
61		ngtmnft 11397	. . . . . . . . . . 11
62	61	necon2abid 2711	. . . . . . . . . 10
63	24, 62	syl 16	. . . . . . . . 9
64	60, 63	mpbid 210	. . . . . . . 8
65		xaddpnf1 11454	. . . . . . . 8
66	24, 64, 65	syl2anc 661	. . . . . . 7
67	55, 66	sylan9eqr 2520	. . . . . 6
68	54, 67	breqtrrd 4478	. . . . 5
69	68	adantlr 714	. . . 4
70		mnfle 11371	. . . . . . . . . . 11
71	14, 70	syl 16	. . . . . . . . . 10
72	57, 14, 5, 71, 12	xrlelttrd 11392	. . . . . . . . 9
73		ngtmnft 11397	. . . . . . . . . . 11
74	73	necon2abid 2711	. . . . . . . . . 10
75	5, 74	syl 16	. . . . . . . . 9
76	72, 75	mpbid 210	. . . . . . . 8
77	76	a1d 25	. . . . . . 7
78	77	necon4bd 2679	. . . . . 6
79	78	imp 429	. . . . 5
80	79	adantlr 714	. . . 4
81		elxr 11354	. . . . . 6
82	5, 81	sylib 196	. . . . 5
83	82	adantr 465	. . . 4
84	31, 69, 80, 83	mpjao3dan 1295	. . 3
85	40	a1d 25	. . . . 5
86	85	necon4bd 2679	. . . 4
87	86	imp 429	. . 3
88		oveq1 6303	. . . . 5
89		xaddmnf2 11457	. . . . . 6
90	14, 47, 89	syl2anc 661	. . . . 5
91	88, 90	sylan9eqr 2520	. . . 4
92		xaddnemnf 11462	. . . . . . 7
93	24, 64, 5, 76, 92	syl22anc 1229	. . . . . 6
94		ngtmnft 11397	. . . . . . . 8
95	94	necon2abid 2711	. . . . . . 7
96	10, 95	syl 16	. . . . . 6
97	93, 96	mpbird 232	. . . . 5
98	97	adantr 465	. . . 4
99	91, 98	eqbrtrd 4472	. . 3
100		elxr 11354	. . . 4
101	4, 100	sylib 196	. . 3
102	84, 87, 99, 101	mpjao3dan 1295	. 2
103	102	3expia 1198	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  \/w3o 972  /\w3a 973  =wceq 1395  e.wcel 1818  =/=wne 2652   class class class wbr 4452  (class class class)co 6296  cr 9512  cpnf 9646  cmnf 9647  cxr 9648  clt 9649  cle 9650  cxad 11345

This theorem is referenced by:  bldisj  20901  iscau3  21717  xrofsup  27582  xrge0addgt0  27681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-cnex 9569  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-po 4805  df-so 4806  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-1st 6800  df-2nd 6801  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831  df-xneg 11347  df-xadd 11348