Theorem 1re 11204

Description: The number 1 is real. This used to be one of our postulates for complex numbers, but Eric Schmidt discovered that it could be derived from a weaker postulate, ax-1cn 11154, by exploiting properties of the imaginary unit i. (Contributed by Eric Schmidt, 11-Apr-2007.) (Revised by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
1re	⊢ 1 ∈ ℝ

Proof of Theorem 1re

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-1ne0 11165	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11154	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11201	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3026	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 252	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11194	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11201	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3027	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 252	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3186	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3186	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 68	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3186	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3186	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 21	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 23	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7416	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7427	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 418	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2985	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 33	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2978	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 876	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 3026	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 3027	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3603	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1137	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 759	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 3026	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 3027	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3603	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
34	33	3expia 1137	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35	34	ad2ant2l 758	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
36	30, 35	jaod 872	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
37	25, 36	syl5 35	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
38	37	rexlimdvva 3228	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3213	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2791	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 417	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2985	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 3026	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3590	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
46	45	expcom 418	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
47	43, 46	syl6 36	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
48	47	com23 87	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
49	48	adantld 495	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
50		neeq1 3026	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3590	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
52	51	expcom 418	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
53	52	adantrd 496	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
54	53	a1dd 51	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
55	49, 54	pm2.61ine 3047	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3213	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11168	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11181	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 727	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2857	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 248	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3172	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 16	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3164	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 860   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∃wrex 3095  (class class class)co 7408  ℂcc 11094  ℝcr 11095  0cc0 11096  1c1 11097  ici 11098   + caddc 11099   · cmul 11101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-mulcl 11158  ax-mulrcl 11159  ax-i2m1 11164  ax-1ne0 11165  ax-rrecex 11168  ax-cnre 11169

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-iota 6490  df-fv 6542  df-ov 7411

This theorem is referenced by:  1red  11205  pr01ssre  11208  1xr  11264  dedekind  11369  peano2re  11379  mul02lem2  11383  addrid  11386  renegcl  11517  peano2rem  11521  0reALT  11551  0lt1  11732  0le1  11733  relin01  11734  1le1  11838  eqneg  11931  ltp1  12051  ltm1  12053  recgt0  12057  ltmulgt11  12070  lemulge11  12073  reclt1  12106  recgt1  12107  recgt1i  12108  recp1lt1  12109  recreclt  12110  recgt0ii  12117  ledivp1i  12136  ltdivp1i  12137  neg1rr  12200  neg1lt0  12202  cju  12210  indf  12220  indfval  12221  nnssre  12233  nnge1  12260  nngt1ne1  12261  nnle1eq1  12262  nngt0  12263  nnnlt1  12264  nnne0  12266  nnrecre  12274  nnrecgt0  12275  nnsub  12276  1t1e1ALT  12287  2re  12311  3re  12317  4re  12321  5re  12324  6re  12327  7re  12330  8re  12333  9re  12336  0le2OLD  12340  2posOLD  12342  1lt2  12409  1lt3  12412  1lt4  12415  1lt5  12419  1lt6  12424  1lt7  12430  1lt8  12437  1lt9  12445  1ne2  12447  1le2  12448  1le3  12451  halflt1  12457  addltmul  12476  nnunb  12496  elnnnn0c  12545  nn0ge2m1nn  12570  elnnz1  12616  znnnlt1  12617  zltp1le  12640  zleltp1  12641  nn0lt2  12655  recnz  12667  gtndiv  12669  3halfnz  12671  10re  12730  1lt10  12852  1lt10OLD  12853  eluzp1m1  12884  eluzp1p1  12886  eluz2b2  12941  zbtwnre  12966  rebtwnz  12967  1rp  13016  divlt1lt  13083  divle1le  13084  nnledivrp  13126  qbtwnxr  13222  xmulrid  13301  xmulm1  13303  x2times  13321  xrub  13334  elicc01  13489  1elunit  13493  divelunit  13517  lincmb01cmp  13518  unitssre  13522  0nelfz1  13567  fzpreddisj  13597  fznatpl1  13602  fztpval  13610  fraclt1  13831  fracle1  13832  flbi2  13846  fldiv4p1lem1div2  13864  fldiv4lem1div2  13866  fldiv  13889  modid  13925  1mod  13932  m1modnnsub1  13949  modm1p1mod0  13954  seqf1olem1  14073  reexpcl  14110  reexpclz  14114  expge0  14130  expge1  14131  expgt1  14132  bernneq  14261  bernneq2  14262  expnbnd  14264  expnlbnd  14265  expnlbnd2  14266  expmulnbnd  14267  discr1  14271  facwordi  14321  faclbnd3  14324  faclbnd4lem1  14325  faclbnd4lem4  14328  faclbnd6  14331  facavg  14333  hashv01gt1  14377  hashnn0n0nn  14423  hashunsnggt  14426  hash1snb  14452  hashgt12el  14455  hashgt12el2  14456  hashfun  14470  hashge2el2dif  14513  tpf1ofv2  14531  lsw0  14598  f1oun2prg  14950  sgnclre  15135  sgnnbi  15137  sgnpbi  15138  cjexp  15197  re1  15201  im1  15202  rei  15203  imi  15204  01sqrexlem1  15289  01sqrexlem2  15290  01sqrexlem3  15291  01sqrexlem4  15292  01sqrexlem7  15295  resqrex  15297  sqrt1  15318  sqrt2gt1lt2  15321  sqrtm1  15322  abs1  15344  absrdbnd  15389  caubnd2  15405  mulcn2  15643  reccn2  15644  rlimno1  15701  o1fsum  15861  expcnv  15914  geolim  15920  geolim2  15921  georeclim  15922  geomulcvg  15926  geoisumr  15928  geoisum1c  15930  fprodge0  16043  fprodge1  16045  rerisefaccl  16067  refallfaccl  16068  ere  16139  ege2le3  16140  efgt1  16168  resin4p  16190  recos4p  16191  tanhbnd  16213  sinbnd  16232  cosbnd  16233  sinbnd2  16234  cosbnd2  16235  ef01bndlem  16236  sin01bnd  16237  cos01bnd  16238  cos1bnd  16239  cos2bnd  16240  sinltx  16241  sin01gt0  16242  cos01gt0  16243  sin02gt0  16244  sincos1sgn  16245  ene1  16262  rpnnen2lem2  16267  rpnnen2lem3  16268  rpnnen2lem4  16269  rpnnen2lem9  16274  rpnnen2lem12  16277  ruclem6  16287  ruclem11  16292  ruclem12  16293  3dvds  16385  flodddiv4  16469  sadcadd  16512  isprm3  16737  sqnprm  16757  coprm  16766  phibndlem  16825  pythagtriplem3  16874  pcmpt  16948  fldivp1  16953  pockthi  16963  infpn2  16969  basendxnmulrndx  17345  starvndxnbasendx  17353  scandxnbasendx  17365  vscandxnbasendx  17370  ipndxnbasendx  17381  basendxnocndx  17432  slotsbhcdif  17464  lt6abl  19961  srgbinomlem4  20307  0ringnnzr  20605  abvneg  20903  abvtrivd  20909  prmidl0  21443  xrsmcmn  21510  xrsnsgrp  21523  gzrngunitlem  21547  gzrngunit  21548  rge0srg  21553  psgnodpmr  21705  remulg  21722  resubdrg  21723  psdmvr  22297  dscmet  24694  dscopn  24695  nrginvrcnlem  24813  idnghm  24865  tgioo  24918  blcvx  24920  iicmp  25010  iiconn  25011  iirev  25053  iihalf1  25055  iihalf2  25057  elii1  25059  elii2  25060  iimulcl  25061  icopnfcnv  25066  icopnfhmeo  25067  iccpnfhmeo  25069  xrhmeo  25070  xrhmph  25071  evth  25083  xlebnum  25089  htpycc  25104  reparphti  25121  pcoval1  25137  pco1  25139  pcoval2  25140  pcocn  25141  pcohtpylem  25143  pcopt  25146  pcopt2  25147  pcoass  25148  pcorevlem  25150  nmhmcn  25244  ncvs1  25281  ovolunlem1a  25620  vitalilem2  25733  vitalilem4  25735  vitalilem5  25736  vitali  25737  i1f1  25814  itg11  25815  itg2const  25864  dveflem  26103  dvlipcn  26118  dvcvx  26144  ply1remlem  26287  fta1blem  26293  plyn0mulidp  26407  plymulidp  26408  vieta1lem2  26437  aalioulem3  26460  aalioulem5  26462  aaliou3lem2  26469  ulmbdd  26523  iblulm  26532  radcnvlem1  26538  dvradcnv  26546  abelthlem2  26557  abelthlem3  26558  abelthlem5  26560  abelthlem7  26563  abelth  26566  abelth2  26567  reeff1olem  26571  reeff1o  26572  sinhalfpilem  26590  tangtx  26632  sincos4thpi  26640  pige3ALT  26647  coskpi  26650  cos0pilt1  26659  recosf1o  26662  tanregt0  26666  efif1olem3  26671  efif1olem4  26672  loge  26713  logdivlti  26747  logcnlem4  26772  logf1o2  26777  logtayl  26787  logccv  26790  recxpcl  26802  cxplea  26823  cxpcn3lem  26874  cxpaddlelem  26878  loglesqrt  26888  ang180lem2  26937  angpined  26957  acosrecl  27030  atancj  27037  atanlogaddlem  27040  atantan  27050  atans2  27058  ressatans  27061  leibpi  27069  log2le1  27077  birthdaylem3  27080  cxp2lim  27103  cxploglim  27104  cxploglim2  27105  divsqrtsumlem  27106  cvxcl  27111  scvxcvx  27112  jensenlem2  27114  amgmlem  27116  emcllem2  27123  emcllem4  27125  emcllem6  27127  emcllem7  27128  emre  27132  emgt0  27133  harmonicbnd3  27134  harmonicubnd  27136  harmonicbnd4  27137  zetacvg  27141  ftalem1  27199  ftalem2  27200  ftalem5  27203  issqf  27262  cht1  27291  chp1  27293  ppiltx  27303  mumullem2  27306  ppiublem1  27328  ppiub  27330  chtublem  27337  chtub  27338  logfacbnd3  27349  logexprlim  27351  perfectlem2  27356  dchrinv  27387  dchr1re  27389  efexple  27407  bposlem1  27410  bposlem2  27411  bposlem5  27414  bposlem8  27417  lgsdir2lem1  27451  lgsdir2lem5  27455  lgsdir  27458  lgsne0  27461  lgsabs1  27462  lgsdinn0  27471  gausslemma2dlem0i  27490  lgseisen  27505  m1lgs  27514  2lgslem3  27530  addsq2nreurex  27570  2sqreultblem  27574  2sqreunnltblem  27577  chebbnd1lem3  27597  chebbnd1  27598  chtppilimlem1  27599  chtppilimlem2  27600  chtppilim  27601  chpchtlim  27605  vmadivsumb  27609  rplogsumlem2  27611  rpvmasumlem  27613  dchrmusumlema  27619  dchrmusum2  27620  dchrvmasumlem2  27624  dchrvmasumiflem1  27627  dchrisum0flblem1  27634  dchrisum0flblem2  27635  dchrisum0fno1  27637  rpvmasum2  27638  dchrisum0re  27639  dchrisum0lema  27640  dchrisum0lem1b  27641  dchrisum0lem1  27642  dchrisum0lem2a  27643  dchrisum0lem2  27644  logdivsum  27659  mulog2sumlem2  27661  2vmadivsumlem  27666  log2sumbnd  27670  selbergb  27675  selberg2b  27678  chpdifbndlem1  27679  selberg3lem1  27683  selberg3lem2  27684  selberg4lem1  27686  pntrmax  27690  pntrsumo1  27691  selbergsb  27701  pntrlog2bndlem3  27705  pntrlog2bndlem5  27707  pntpbnd1a  27711  pntpbnd2  27713  pntibndlem1  27715  pntibndlem3  27718  pntlemd  27720  pntlemc  27721  pntlemb  27723  pntlemr  27728  pntlemf  27731  pntlemk  27732  pntlemo  27733  pntlem3  27735  pntleml  27737  abvcxp  27741  ostth2lem1  27744  ostth1  27759  ostth2lem2  27760  ostth2lem3  27761  ostth2lem4  27762  ostth2  27763  ostth3  27764  ostth  27765  slotsinbpsd  28672  slotslnbpsd  28673  trgcgrg  28746  brbtwn2  29192  colinearalglem4  29196  ax5seglem2  29216  ax5seglem3  29218  axpaschlem  29227  axpasch  29228  axlowdimlem6  29234  axlowdimlem10  29238  axlowdimlem16  29244  axlowdim1  29246  axlowdim2  29247  axlowdim  29248  axcontlem2  29252  elntg2  29272  lfgrnloop  29412  lfuhgr1v0e  29541  usgrexmpldifpr  29545  usgrexmplef  29546  1loopgrvd2  29790  vdegp1bi  29824  lfgrwlkprop  29972  pthdlem1  30052  pthdlem2  30054  clwlkclwwlkf  30296  upgr4cycl4dv4e  30473  konigsberglem2  30541  konigsberglem3  30542  konigsberglem5  30544  frgrreg  30682  ex-dif  30711  ex-in  30713  ex-pss  30716  ex-res  30729  ex-fl  30735  nv1  30964  smcnlem  30986  ipidsq  30999  nmlno0lem  31082  norm-ii-i  31426  bcs2  31471  norm1  31538  nmopub2tALT  32198  nmfnleub2  32215  nmlnop0iALT  32284  unopbd  32304  nmopadjlem  32378  nmopcoadji  32390  pjnmopi  32437  pjbdlni  32438  hstle1  32515  hstle  32519  hstles  32520  stge1i  32527  stlesi  32530  staddi  32535  stadd3i  32537  strlem1  32539  strlem5  32544  jplem1  32557  cdj1i  32722  addltmulALT  32735  xlt2addrd  33041  sgnmulsgp  33113  dp2lt10  33140  dp2ltsuc  33142  dp2ltc  33143  dplti  33161  dpmul4  33170  cshw1s2  33217  xrsmulgzz  33266  rearchi  33605  xrge0slmod  33607  evl1deg3  33809  constrconj  34076  2sqr3minply  34111  submateqlem1  34138  xrge0iifcnv  34264  xrge0iifcv  34265  xrge0iifiso  34266  xrge0iifhom  34268  zrhre  34350  esumcst  34394  cntnevol  34559  omssubadd  34631  iwrdsplit  34718  dstfrvclim1  34809  coinfliprv  34814  ballotlem2  34820  ballotlem4  34830  ballotlemi1  34834  ballotlemic  34838  signswch  34889  signstf  34894  signsvfn  34910  itgexpif  34934  hgt750lemd  34976  logdivsqrle  34978  hgt750lem  34979  hgt750lem2  34980  hgt750leme  34986  tgoldbachgnn  34987  subfacp1lem1  35566  subfacp1lem5  35571  resconn  35633  iisconn  35639  iillysconn  35640  problem2  36053  problem3  36054  sinccvglem  36059  fz0n  36118  dnibndlem12  36963  knoppcnlem4  36970  knoppndvlem13  36998  cnndvlem1  37011  irrdiff  37853  relowlpssretop  37893  sin2h  38144  cos2h  38145  tan2h  38146  poimirlem7  38161  poimirlem16  38170  poimirlem17  38171  poimirlem19  38173  poimirlem20  38174  poimirlem22  38176  poimirlem23  38177  poimirlem29  38183  poimirlem31  38185  itg2addnclem3  38207  asindmre  38237  dvasin  38238  dvacos  38239  dvreasin  38240  dvreacos  38241  fdc  38279  geomcau  38293  cntotbnd  38330  heiborlem8  38352  bfplem2  38357  bfp  38358  aks4d1p1p7  42726  ine1  42960  re1m1e0m0  43043  sn-00idlem1  43044  sn-00idlem2  43045  remul02  43051  sn-0ne2  43052  reixi  43069  rei4  43070  remullid  43080  ipiiie0  43084  sn-0tie0  43110  sn-nnne0  43119  mulgt0b1d  43131  sn-0lt1  43134  sn-ltp1  43135  reneg1lt0  43139  sn-inelr  43146  rabren3dioph  43429  pellexlem5  43447  pellexlem6  43448  pell1qrgaplem  43487  pell14qrgap  43489  pellqrex  43493  pellfundre  43495  pellfundlb  43498  pellfund14gap  43501  jm2.17a  43574  acongeq  43597  jm2.23  43610  jm3.1lem2  43632  sqrtcval  44254  sqrtcval2  44255  resqrtval  44256  imsqrtval  44257  relexp01min  44326  cvgdvgrat  44910  lhe4.4ex1a  44926  binomcxplemnotnn0  44953  isosctrlem1ALT  45529  supxrgelem  45940  xrlexaddrp  45955  infxr  45969  infleinflem2  45973  sumnnodd  46233  limsup10exlem  46373  limsup10ex  46374  dvnprodlem3  46549  stoweidlem1  46602  stoweidlem18  46619  stoweidlem19  46620  stoweidlem26  46627  stoweidlem34  46635  stoweidlem40  46641  stoweidlem41  46642  stoweidlem59  46660  stoweid  46664  stirlinglem10  46684  stirlinglem11  46685  dirkercncflem1  46704  fourierdlem16  46724  fourierdlem21  46729  fourierdlem22  46730  fourierdlem42  46750  fourierdlem68  46775  fourierdlem83  46790  fourierdlem103  46810  sqwvfourb  46830  fouriersw  46832  etransclem23  46858  salgencntex  46944  ovn0lem  47166  smfmullem3  47394  smfmullem4  47395  nthrucw  47489  cjnpoly  47510  zm1nn  47923  ceilhalf1  47959  m1mod0mod1  47981  muldvdsfacgt  48007  fmtnosqrt  48175  nprmdvdsfacm1lem4  48259  perfectALTVlem2  48371  2exp340mod341  48382  8exp8mod9  48385  nfermltl8rev  48391  nnsum3primesprm  48439  nnsum4primesodd  48445  nnsum4primesoddALTV  48446  nnsum4primeseven  48449  nnsum4primesevenALTV  48450  tgblthelfgott  48464  tgoldbach  48466  usgrexmpl1lem  48670  usgrexmpl2lem  48675  usgrexmpl2nb1  48681  usgrexmpl2nb3  48683  usgrexmpl2nb4  48684  usgrexmpl2nb5  48685  usgrexmpl2trifr  48686  gpg3kgrtriexlem3  48734  pgnbgreunbgrlem2lem1  48763  pgnbgreunbgrlem2lem2  48764  rege1logbrege0  49218  rege1logbzge0  49219  blennnelnn  49236  dignnld  49263  nn0sumshdiglemA  49279  nn0sumshdiglem1  49281  rrx2xpref1o  49378  rrxlines  49393  eenglngeehlnmlem1  49397  eenglngeehlnmlem2  49398  line2ylem  49411  line2x  49414  icccldii  49577  io1ii  49579  sepfsepc  49586