pellfund14

Description: Every positive Pell solution is a power of the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014)

		Ref	Expression
	Assertion	pellfund14	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to \exists x \in ℤ A = {PellFund (D)}^{x}$

Proof

Step	Hyp	Ref	Expression
1		pell14qrrp	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A \in ℝ^{+}$
2		pellfundrp	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to PellFund (D) \in ℝ^{+}$
3	2	adantr	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to PellFund (D) \in ℝ^{+}$
4		pellfundne1	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to PellFund (D) \neq 1$
5	4	adantr	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to PellFund (D) \neq 1$
6		reglogcl	$⊢ (A \in ℝ^{+} \land PellFund (D) \in ℝ^{+} \land PellFund (D) \neq 1) \to \frac{\log A}{\log PellFund (D)} \in ℝ$
7	1 3 5 6	syl3anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to \frac{\log A}{\log PellFund (D)} \in ℝ$
8	7	flcld	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to ⌊\frac{\log A}{\log PellFund (D)}⌋ \in ℤ$
9		pell14qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A \in ℝ$
10	9	recnd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A \in ℂ$
11	3 8	rpexpcld	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to {PellFund (D)}^{⌊\frac{\log A}{\log PellFund (D)}⌋} \in ℝ^{+}$
12	11	rpcnd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to {PellFund (D)}^{⌊\frac{\log A}{\log PellFund (D)}⌋} \in ℂ$
13	8	znegcld	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to - ⌊\frac{\log A}{\log PellFund (D)}⌋ \in ℤ$
14	3 13	rpexpcld	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \in ℝ^{+}$
15	14	rpcnd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \in ℂ$
16	14	rpne0d	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \neq 0$
17		simpl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to D \in (ℕ ∖ ◻_{ℕ})$
18		pell1qrss14	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to Pell1QR (D) \subseteq Pell14QR (D)$
19		pellfundex	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to PellFund (D) \in Pell1QR (D)$
20	18 19	sseldd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to PellFund (D) \in Pell14QR (D)$
21	20	adantr	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to PellFund (D) \in Pell14QR (D)$
22		pell14qrexpcl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land PellFund (D) \in Pell14QR (D) \land - ⌊\frac{\log A}{\log PellFund (D)}⌋ \in ℤ) \to {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \in Pell14QR (D)$
23	17 21 13 22	syl3anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \in Pell14QR (D)$
24		pell14qrmulcl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \in Pell14QR (D)) \to A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \in Pell14QR (D)$
25	23 24	mpd3an3	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \in Pell14QR (D)$
26		1rp	$⊢ 1 \in ℝ^{+}$
27	26	a1i	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to 1 \in ℝ^{+}$
28		modge0	$⊢ (\frac{\log A}{\log PellFund (D)} \in ℝ \land 1 \in ℝ^{+}) \to 0 \leq (\frac{\log A}{\log PellFund (D)}) \mod 1$
29	7 27 28	syl2anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to 0 \leq (\frac{\log A}{\log PellFund (D)}) \mod 1$
30	7	recnd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to \frac{\log A}{\log PellFund (D)} \in ℂ$
31	8	zcnd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to ⌊\frac{\log A}{\log PellFund (D)}⌋ \in ℂ$
32	30 31	negsubd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (\frac{\log A}{\log PellFund (D)}) + (- ⌊\frac{\log A}{\log PellFund (D)}⌋) = (\frac{\log A}{\log PellFund (D)}) - ⌊\frac{\log A}{\log PellFund (D)}⌋$
33		modfrac	$⊢ \frac{\log A}{\log PellFund (D)} \in ℝ \to (\frac{\log A}{\log PellFund (D)}) \mod 1 = (\frac{\log A}{\log PellFund (D)}) - ⌊\frac{\log A}{\log PellFund (D)}⌋$
34	7 33	syl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (\frac{\log A}{\log PellFund (D)}) \mod 1 = (\frac{\log A}{\log PellFund (D)}) - ⌊\frac{\log A}{\log PellFund (D)}⌋$
35	32 34	eqtr4d	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (\frac{\log A}{\log PellFund (D)}) + (- ⌊\frac{\log A}{\log PellFund (D)}⌋) = (\frac{\log A}{\log PellFund (D)}) \mod 1$
36	29 35	breqtrrd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to 0 \leq (\frac{\log A}{\log PellFund (D)}) + (- ⌊\frac{\log A}{\log PellFund (D)}⌋)$
37		reglog1	$⊢ (PellFund (D) \in ℝ^{+} \land PellFund (D) \neq 1) \to \frac{\log 1}{\log PellFund (D)} = 0$
38	3 5 37	syl2anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to \frac{\log 1}{\log PellFund (D)} = 0$
39		reglogmul	$⊢ (A \in ℝ^{+} \land {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \in ℝ^{+} \land (PellFund (D) \in ℝ^{+} \land PellFund (D) \neq 1)) \to \frac{\log A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}}{\log PellFund (D)} = (\frac{\log A}{\log PellFund (D)}) + (\frac{\log {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}}{\log PellFund (D)})$
40	1 14 3 5 39	syl112anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to \frac{\log A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}}{\log PellFund (D)} = (\frac{\log A}{\log PellFund (D)}) + (\frac{\log {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}}{\log PellFund (D)})$
41		reglogexpbas	$⊢ (- ⌊\frac{\log A}{\log PellFund (D)}⌋ \in ℤ \land (PellFund (D) \in ℝ^{+} \land PellFund (D) \neq 1)) \to \frac{\log {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}}{\log PellFund (D)} = - ⌊\frac{\log A}{\log PellFund (D)}⌋$
42	13 3 5 41	syl12anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to \frac{\log {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}}{\log PellFund (D)} = - ⌊\frac{\log A}{\log PellFund (D)}⌋$
43	42	oveq2d	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (\frac{\log A}{\log PellFund (D)}) + (\frac{\log {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}}{\log PellFund (D)}) = (\frac{\log A}{\log PellFund (D)}) + (- ⌊\frac{\log A}{\log PellFund (D)}⌋)$
44	40 43	eqtrd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to \frac{\log A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}}{\log PellFund (D)} = (\frac{\log A}{\log PellFund (D)}) + (- ⌊\frac{\log A}{\log PellFund (D)}⌋)$
45	36 38 44	3brtr4d	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to \frac{\log 1}{\log PellFund (D)} \leq \frac{\log A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}}{\log PellFund (D)}$
46	1 14	rpmulcld	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \in ℝ^{+}$
47		pellfundgt1	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to 1 < PellFund (D)$
48	47	adantr	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to 1 < PellFund (D)$
49		reglogleb	$⊢ ((1 \in ℝ^{+} \land A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \in ℝ^{+}) \land (PellFund (D) \in ℝ^{+} \land 1 < PellFund (D))) \to (1 \leq A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \leftrightarrow \frac{\log 1}{\log PellFund (D)} \leq \frac{\log A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}}{\log PellFund (D)})$
50	27 46 3 48 49	syl22anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (1 \leq A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \leftrightarrow \frac{\log 1}{\log PellFund (D)} \leq \frac{\log A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}}{\log PellFund (D)})$
51	45 50	mpbird	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to 1 \leq A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}$
52		modlt	$⊢ (\frac{\log A}{\log PellFund (D)} \in ℝ \land 1 \in ℝ^{+}) \to (\frac{\log A}{\log PellFund (D)}) \mod 1 < 1$
53	7 27 52	syl2anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (\frac{\log A}{\log PellFund (D)}) \mod 1 < 1$
54	35 53	eqbrtrd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (\frac{\log A}{\log PellFund (D)}) + (- ⌊\frac{\log A}{\log PellFund (D)}⌋) < 1$
55		reglogbas	$⊢ (PellFund (D) \in ℝ^{+} \land PellFund (D) \neq 1) \to \frac{\log PellFund (D)}{\log PellFund (D)} = 1$
56	3 5 55	syl2anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to \frac{\log PellFund (D)}{\log PellFund (D)} = 1$
57	54 44 56	3brtr4d	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to \frac{\log A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}}{\log PellFund (D)} < \frac{\log PellFund (D)}{\log PellFund (D)}$
58		reglogltb	$⊢ ((A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \in ℝ^{+} \land PellFund (D) \in ℝ^{+}) \land (PellFund (D) \in ℝ^{+} \land 1 < PellFund (D))) \to (A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} < PellFund (D) \leftrightarrow \frac{\log A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}}{\log PellFund (D)} < \frac{\log PellFund (D)}{\log PellFund (D)})$
59	46 3 3 48 58	syl22anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} < PellFund (D) \leftrightarrow \frac{\log A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}}{\log PellFund (D)} < \frac{\log PellFund (D)}{\log PellFund (D)})$
60	57 59	mpbird	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} < PellFund (D)$
61		pellfund14gap	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \in Pell14QR (D) \land (1 \leq A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} \land A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} < PellFund (D))) \to A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} = 1$
62	17 25 51 60 61	syl112anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} = 1$
63	31	negidd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to ⌊\frac{\log A}{\log PellFund (D)}⌋ + (- ⌊\frac{\log A}{\log PellFund (D)}⌋) = 0$
64	63	oveq2d	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to {PellFund (D)}^{⌊\frac{\log A}{\log PellFund (D)}⌋ + (- ⌊\frac{\log A}{\log PellFund (D)}⌋)} = {PellFund (D)}^{0}$
65	3	rpcnd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to PellFund (D) \in ℂ$
66	3	rpne0d	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to PellFund (D) \neq 0$
67		expaddz	$⊢ ((PellFund (D) \in ℂ \land PellFund (D) \neq 0) \land (⌊\frac{\log A}{\log PellFund (D)}⌋ \in ℤ \land - ⌊\frac{\log A}{\log PellFund (D)}⌋ \in ℤ)) \to {PellFund (D)}^{⌊\frac{\log A}{\log PellFund (D)}⌋ + (- ⌊\frac{\log A}{\log PellFund (D)}⌋)} = {PellFund (D)}^{⌊\frac{\log A}{\log PellFund (D)}⌋} {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}$
68	65 66 8 13 67	syl22anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to {PellFund (D)}^{⌊\frac{\log A}{\log PellFund (D)}⌋ + (- ⌊\frac{\log A}{\log PellFund (D)}⌋)} = {PellFund (D)}^{⌊\frac{\log A}{\log PellFund (D)}⌋} {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}$
69	65	exp0d	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to {PellFund (D)}^{0} = 1$
70	64 68 69	3eqtr3rd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to 1 = {PellFund (D)}^{⌊\frac{\log A}{\log PellFund (D)}⌋} {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}$
71	62 70	eqtrd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋} = {PellFund (D)}^{⌊\frac{\log A}{\log PellFund (D)}⌋} {PellFund (D)}^{- ⌊\frac{\log A}{\log PellFund (D)}⌋}$
72	10 12 15 16 71	mulcan2ad	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A = {PellFund (D)}^{⌊\frac{\log A}{\log PellFund (D)}⌋}$
73		oveq2	$⊢ x = ⌊\frac{\log A}{\log PellFund (D)}⌋ \to {PellFund (D)}^{x} = {PellFund (D)}^{⌊\frac{\log A}{\log PellFund (D)}⌋}$
74	73	rspceeqv	$⊢ (⌊\frac{\log A}{\log PellFund (D)}⌋ \in ℤ \land A = {PellFund (D)}^{⌊\frac{\log A}{\log PellFund (D)}⌋}) \to \exists x \in ℤ A = {PellFund (D)}^{x}$
75	8 72 74	syl2anc	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to \exists x \in ℤ A = {PellFund (D)}^{x}$

Metamath Proof Explorer

Theorem pellfund14

Proof