Theorem 1re 11135

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 11087, 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 11098	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11087	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11132	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 2996	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 250	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11127	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11132	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 2997	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 250	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3154	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3154	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3154	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3154	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 22	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7364	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7375	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 414	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2955	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 32	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2948	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 869	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 2996	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 2997	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3573	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1127	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 753	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 2996	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 2997	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3573	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
34	33	3expia 1127	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35	34	ad2ant2l 752	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
36	30, 35	jaod 865	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
37	25, 36	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
38	37	rexlimdvva 3196	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3181	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2761	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 413	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2955	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 2996	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3560	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
46	45	expcom 414	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
47	43, 46	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
48	47	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
49	48	adantld 491	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
50		neeq1 2996	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3560	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
52	51	expcom 414	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
53	52	adantrd 492	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
54	53	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
55	49, 54	pm2.61ine 3017	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3181	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11101	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11114	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 721	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2827	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 246	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3140	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3132	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 853   = wceq 1547   ∈ wcel 2119   ≠ wne 2934  ∃wrex 3063  (class class class)co 7356  ℂcc 11027  ℝcr 11028  0cc0 11029  1c1 11030  ici 11031   + caddc 11032   · cmul 11034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359

This theorem is referenced by:  1red  11136  pr01ssre  11139  1xr  11195  dedekind  11300  peano2re  11310  mul02lem2  11314  addrid  11317  renegcl  11448  peano2rem  11452  0reALT  11482  0lt1  11663  0le1  11664  relin01  11665  1le1  11769  eqneg  11866  ltp1  11986  ltm1  11988  recgt0  11992  mulgt1OLD  12005  ltmulgt11  12006  lemulge11  12009  reclt1  12042  recgt1  12043  recgt1i  12044  recp1lt1  12045  recreclt  12046  recgt0ii  12053  ledivp1i  12072  ltdivp1i  12073  neg1rr  12136  neg1lt0  12138  cju  12146  indf  12156  indfval  12157  nnssre  12169  nnge1  12196  nngt1ne1  12197  nnle1eq1  12198  nngt0  12199  nnnlt1  12200  nnne0  12202  nnrecre  12210  nnrecgt0  12211  nnsub  12212  1t1e1ALT  12223  2re  12246  3re  12252  4re  12256  5re  12259  6re  12262  7re  12265  8re  12268  9re  12271  0le2  12274  2pos  12275  3pos  12277  4pos  12279  5pos  12281  6pos  12282  7pos  12283  8pos  12284  9pos  12285  1lt2  12338  1lt3  12340  1lt4  12343  1lt5  12347  1lt6  12352  1lt7  12358  1lt8  12365  1lt9  12373  1ne2  12375  1le2  12376  1le3  12379  halflt1  12385  addltmul  12404  nnunb  12424  elnnnn0c  12473  nn0ge2m1nn  12498  elnnz1  12544  znnnlt1  12545  zltp1le  12568  zleltp1  12569  nn0lt2  12583  recnz  12595  gtndiv  12597  3halfnz  12599  10re  12654  1lt10  12774  eluzp1m1  12805  eluzp1p1  12807  eluz2b2  12862  zbtwnre  12887  rebtwnz  12888  1rp  12937  divlt1lt  13004  divle1le  13005  nnledivrp  13047  qbtwnxr  13143  xmulrid  13222  xmulm1  13224  x2times  13242  xrub  13255  elicc01  13410  1elunit  13414  divelunit  13438  lincmb01cmp  13439  unitssre  13443  0nelfz1  13488  fzpreddisj  13518  fznatpl1  13523  fztpval  13531  fraclt1  13752  fracle1  13753  flbi2  13767  fldiv4p1lem1div2  13785  fldiv4lem1div2  13787  fldiv  13810  modid  13846  1mod  13853  m1modnnsub1  13870  modm1p1mod0  13875  seqf1olem1  13994  reexpcl  14031  reexpclz  14035  expge0  14051  expge1  14052  expgt1  14053  bernneq  14182  bernneq2  14183  expnbnd  14185  expnlbnd  14186  expnlbnd2  14187  expmulnbnd  14188  discr1  14192  facwordi  14242  faclbnd3  14245  faclbnd4lem1  14246  faclbnd4lem4  14249  faclbnd6  14252  facavg  14254  hashv01gt1  14298  hashnn0n0nn  14344  hashunsnggt  14347  hash1snb  14372  hashgt12el  14375  hashgt12el2  14376  hashfun  14390  hashge2el2dif  14433  tpf1ofv2  14451  lsw0  14518  f1oun2prg  14870  cjexp  15103  re1  15107  im1  15108  rei  15109  imi  15110  01sqrexlem1  15195  01sqrexlem2  15196  01sqrexlem3  15197  01sqrexlem4  15198  01sqrexlem7  15201  resqrex  15203  sqrt1  15224  sqrt2gt1lt2  15227  sqrtm1  15228  abs1  15250  absrdbnd  15295  caubnd2  15311  mulcn2  15549  reccn2  15550  rlimno1  15607  o1fsum  15767  expcnv  15820  geolim  15826  geolim2  15827  georeclim  15828  geomulcvg  15832  geoisumr  15834  geoisum1c  15836  fprodge0  15949  fprodge1  15951  rerisefaccl  15973  refallfaccl  15974  ere  16045  ege2le3  16046  efgt1  16074  resin4p  16096  recos4p  16097  tanhbnd  16119  sinbnd  16138  cosbnd  16139  sinbnd2  16140  cosbnd2  16141  ef01bndlem  16142  sin01bnd  16143  cos01bnd  16144  cos1bnd  16145  cos2bnd  16146  sinltx  16147  sin01gt0  16148  cos01gt0  16149  sin02gt0  16150  sincos1sgn  16151  ene1  16168  rpnnen2lem2  16173  rpnnen2lem3  16174  rpnnen2lem4  16175  rpnnen2lem9  16180  rpnnen2lem12  16183  ruclem6  16193  ruclem11  16198  ruclem12  16199  3dvds  16291  flodddiv4  16375  sadcadd  16418  isprm3  16643  sqnprm  16663  coprm  16672  phibndlem  16731  pythagtriplem3  16780  pcmpt  16854  fldivp1  16859  pockthi  16869  infpn2  16875  basendxnmulrndx  17250  starvndxnbasendx  17258  scandxnbasendx  17270  vscandxnbasendx  17275  ipndxnbasendx  17286  basendxnocndx  17337  slotsbhcdif  17369  lt6abl  19861  srgbinomlem4  20201  0ringnnzr  20497  abvneg  20798  abvtrivd  20804  xrsmcmn  21370  xrsnsgrp  21383  gzrngunitlem  21407  gzrngunit  21408  rge0srg  21413  psgnodpmr  21565  remulg  21582  resubdrg  21583  psdmvr  22157  dscmet  24555  dscopn  24556  nrginvrcnlem  24674  idnghm  24726  tgioo  24779  blcvx  24781  iicmp  24871  iiconn  24872  iirev  24914  iihalf1  24916  iihalf2  24918  elii1  24920  elii2  24921  iimulcl  24922  icopnfcnv  24927  icopnfhmeo  24928  iccpnfhmeo  24930  xrhmeo  24931  xrhmph  24932  evth  24944  xlebnum  24950  htpycc  24965  reparphti  24982  pcoval1  24998  pco1  25000  pcoval2  25001  pcocn  25002  pcohtpylem  25004  pcopt  25007  pcopt2  25008  pcoass  25009  pcorevlem  25011  nmhmcn  25105  ncvs1  25142  ovolunlem1a  25481  vitalilem2  25594  vitalilem4  25596  vitalilem5  25597  vitali  25598  i1f1  25675  itg11  25676  itg2const  25725  dveflem  25964  dvlipcn  25979  dvcvx  26005  ply1remlem  26148  fta1blem  26154  vieta1lem2  26295  aalioulem3  26318  aalioulem5  26320  aaliou3lem2  26327  ulmbdd  26381  iblulm  26390  radcnvlem1  26396  dvradcnv  26404  abelthlem2  26415  abelthlem3  26416  abelthlem5  26418  abelthlem7  26421  abelth  26424  abelth2  26425  reeff1olem  26429  reeff1o  26430  sinhalfpilem  26445  tangtx  26487  sincos4thpi  26495  pige3ALT  26502  coskpi  26505  cos0pilt1  26514  recosf1o  26517  tanregt0  26521  efif1olem3  26526  efif1olem4  26527  loge  26568  logdivlti  26602  logcnlem4  26627  logf1o2  26632  logtayl  26642  logccv  26645  recxpcl  26657  cxplea  26678  cxpcn3lem  26729  cxpaddlelem  26733  loglesqrt  26743  ang180lem2  26792  angpined  26812  acosrecl  26885  atancj  26892  atanlogaddlem  26895  atantan  26905  atans2  26913  ressatans  26916  leibpi  26924  log2le1  26932  birthdaylem3  26935  cxp2lim  26958  cxploglim  26959  cxploglim2  26960  divsqrtsumlem  26961  cvxcl  26966  scvxcvx  26967  jensenlem2  26969  amgmlem  26971  emcllem2  26978  emcllem4  26980  emcllem6  26982  emcllem7  26983  emre  26987  emgt0  26988  harmonicbnd3  26989  harmonicubnd  26991  harmonicbnd4  26992  zetacvg  26996  ftalem1  27054  ftalem2  27055  ftalem5  27058  issqf  27117  cht1  27146  chp1  27148  ppiltx  27158  mumullem2  27161  ppiublem1  27183  ppiub  27185  chtublem  27192  chtub  27193  logfacbnd3  27204  logexprlim  27206  perfectlem2  27211  dchrinv  27242  dchr1re  27244  efexple  27262  bposlem1  27265  bposlem2  27266  bposlem5  27269  bposlem8  27272  lgsdir2lem1  27306  lgsdir2lem5  27310  lgsdir  27313  lgsne0  27316  lgsabs1  27317  lgsdinn0  27326  gausslemma2dlem0i  27345  lgseisen  27360  m1lgs  27369  2lgslem3  27385  addsq2nreurex  27425  2sqreultblem  27429  2sqreunnltblem  27432  chebbnd1lem3  27452  chebbnd1  27453  chtppilimlem1  27454  chtppilimlem2  27455  chtppilim  27456  chpchtlim  27460  vmadivsumb  27464  rplogsumlem2  27466  rpvmasumlem  27468  dchrmusumlema  27474  dchrmusum2  27475  dchrvmasumlem2  27479  dchrvmasumiflem1  27482  dchrisum0flblem1  27489  dchrisum0flblem2  27490  dchrisum0fno1  27492  rpvmasum2  27493  dchrisum0re  27494  dchrisum0lema  27495  dchrisum0lem1b  27496  dchrisum0lem1  27497  dchrisum0lem2a  27498  dchrisum0lem2  27499  logdivsum  27514  mulog2sumlem2  27516  2vmadivsumlem  27521  log2sumbnd  27525  selbergb  27530  selberg2b  27533  chpdifbndlem1  27534  selberg3lem1  27538  selberg3lem2  27539  selberg4lem1  27541  pntrmax  27545  pntrsumo1  27546  selbergsb  27556  pntrlog2bndlem3  27560  pntrlog2bndlem5  27562  pntpbnd1a  27566  pntpbnd2  27568  pntibndlem1  27570  pntibndlem3  27573  pntlemd  27575  pntlemc  27576  pntlemb  27578  pntlemr  27583  pntlemf  27586  pntlemk  27587  pntlemo  27588  pntlem3  27590  pntleml  27592  abvcxp  27596  ostth2lem1  27599  ostth1  27614  ostth2lem2  27615  ostth2lem3  27616  ostth2lem4  27617  ostth2  27618  ostth3  27619  ostth  27620  slotsinbpsd  28527  slotslnbpsd  28528  trgcgrg  28601  brbtwn2  28992  colinearalglem4  28996  ax5seglem2  29016  ax5seglem3  29018  axpaschlem  29027  axpasch  29028  axlowdimlem6  29034  axlowdimlem10  29038  axlowdimlem16  29044  axlowdim1  29046  axlowdim2  29047  axlowdim  29048  axcontlem2  29052  elntg2  29072  lfgrnloop  29212  lfuhgr1v0e  29341  usgrexmpldifpr  29345  usgrexmplef  29346  1loopgrvd2  29590  vdegp1bi  29624  lfgrwlkprop  29772  pthdlem1  29852  pthdlem2  29854  clwlkclwwlkf  30096  upgr4cycl4dv4e  30273  konigsberglem2  30341  konigsberglem3  30342  konigsberglem5  30344  frgrreg  30482  ex-dif  30511  ex-in  30513  ex-pss  30516  ex-res  30529  ex-fl  30535  nv1  30764  smcnlem  30786  ipidsq  30799  nmlno0lem  30882  norm-ii-i  31226  bcs2  31271  norm1  31338  nmopub2tALT  31998  nmfnleub2  32015  nmlnop0iALT  32084  unopbd  32104  nmopadjlem  32178  nmopcoadji  32190  pjnmopi  32237  pjbdlni  32238  hstle1  32315  hstle  32319  hstles  32320  stge1i  32327  stlesi  32330  staddi  32335  stadd3i  32337  strlem1  32339  strlem5  32344  jplem1  32357  cdj1i  32522  addltmulALT  32535  xlt2addrd  32851  sgnclre  32924  sgnnbi  32930  sgnpbi  32931  sgnmulsgp  32935  dp2lt10  32962  dp2ltsuc  32964  dp2ltc  32965  dplti  32983  dpmul4  32992  cshw1s2  33039  xrsmulgzz  33088  rearchi  33429  xrge0slmod  33431  prmidl0  33533  evl1deg3  33661  constrconj  33929  2sqr3minply  33964  submateqlem1  33991  xrge0iifcnv  34117  xrge0iifcv  34118  xrge0iifiso  34119  xrge0iifhom  34121  zrhre  34203  esumcst  34247  cntnevol  34412  omssubadd  34484  iwrdsplit  34571  dstfrvclim1  34662  coinfliprv  34667  ballotlem2  34673  ballotlem4  34683  ballotlemi1  34687  ballotlemic  34691  plymulx0  34731  plymulx  34732  signswch  34745  signstf  34750  signsvfn  34766  itgexpif  34790  hgt750lemd  34832  logdivsqrle  34834  hgt750lem  34835  hgt750lem2  34836  hgt750leme  34842  tgoldbachgnn  34843  subfacp1lem1  35407  subfacp1lem5  35412  resconn  35474  iisconn  35480  iillysconn  35481  problem2  35894  problem3  35895  sinccvglem  35900  fz0n  35959  dnibndlem12  36795  knoppcnlem4  36802  knoppndvlem13  36830  cnndvlem1  36843  irrdiff  37686  relowlpssretop  37726  sin2h  37977  cos2h  37978  tan2h  37979  poimirlem7  37994  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem22  38009  poimirlem23  38010  poimirlem29  38016  poimirlem31  38018  itg2addnclem3  38040  asindmre  38070  dvasin  38071  dvacos  38072  dvreasin  38073  dvreacos  38074  fdc  38112  geomcau  38126  cntotbnd  38163  heiborlem8  38185  bfplem2  38190  bfp  38191  aks4d1p1p7  42559  ine1  42791  re1m1e0m0  42874  sn-00idlem1  42875  sn-00idlem2  42876  remul02  42882  sn-0ne2  42883  reixi  42900  rei4  42901  remullid  42911  ipiiie0  42915  sn-0tie0  42941  sn-nnne0  42950  mulgt0b1d  42962  sn-0lt1  42965  sn-ltp1  42966  reneg1lt0  42970  sn-inelr  42977  rabren3dioph  43260  pellexlem5  43278  pellexlem6  43279  pell1qrgaplem  43318  pell14qrgap  43320  pellqrex  43324  pellfundre  43326  pellfundlb  43329  pellfund14gap  43332  jm2.17a  43405  acongeq  43428  jm2.23  43441  jm3.1lem2  43463  sqrtcval  44085  sqrtcval2  44086  resqrtval  44087  imsqrtval  44088  relexp01min  44157  cvgdvgrat  44757  lhe4.4ex1a  44773  binomcxplemnotnn0  44800  isosctrlem1ALT  45377  supxrgelem  45782  xrlexaddrp  45797  infxr  45811  infleinflem2  45815  sumnnodd  46075  limsup10exlem  46215  limsup10ex  46216  dvnprodlem3  46391  stoweidlem1  46444  stoweidlem18  46461  stoweidlem19  46462  stoweidlem26  46469  stoweidlem34  46477  stoweidlem40  46483  stoweidlem41  46484  stoweidlem59  46502  stoweid  46506  stirlinglem10  46526  stirlinglem11  46527  dirkercncflem1  46546  fourierdlem16  46566  fourierdlem21  46571  fourierdlem22  46572  fourierdlem42  46592  fourierdlem68  46617  fourierdlem83  46632  fourierdlem103  46652  sqwvfourb  46672  fouriersw  46674  etransclem23  46700  salgencntex  46786  ovn0lem  47008  smfmullem3  47236  smfmullem4  47237  nthrucw  47331  cjnpoly  47352  zm1nn  47765  ceilhalf1  47801  m1mod0mod1  47823  muldvdsfacgt  47849  fmtnosqrt  48017  nprmdvdsfacm1lem4  48101  perfectALTVlem2  48213  2exp340mod341  48224  8exp8mod9  48227  nfermltl8rev  48233  nnsum3primesprm  48281  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  tgblthelfgott  48306  tgoldbach  48308  usgrexmpl1lem  48512  usgrexmpl2lem  48517  usgrexmpl2nb1  48523  usgrexmpl2nb3  48525  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  usgrexmpl2trifr  48528  gpg3kgrtriexlem3  48576  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  rege1logbrege0  49049  rege1logbzge0  49050  blennnelnn  49067  dignnld  49094  nn0sumshdiglemA  49110  nn0sumshdiglem1  49112  rrx2xpref1o  49209  rrxlines  49224  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229  line2ylem  49242  line2x  49245  icccldii  49409  io1ii  49411  sepfsepc  49418